I want to use setoid rewrite inside
if (or in general,
match), but I am not sure how to do this.
What would be the most idiomatic way to do this?
Below is a minimal (self-contained) example.
From Coq Require Import Morphisms Setoid RelationClasses. Set Implicit Arguments. Variable A: Type. Variable rel: relation A. Variable ctx: A -> A. Global Instance rel_PreOrder: PreOrder rel. Proof. Admitted. Global Instance ctx_good: Proper (rel ==> rel) ctx. Proof. Admitted. Variable a0 a1 weird: A. Hypothesis REL: rel a0 a1. Goal rel (ctx a0) (ctx a1). Proof. rewrite REL. reflexivity. Qed. Goal rel (if true then ctx a0 else weird) (ctx a1). Proof. Fail rewrite REL. Fail setoid_rewrite REL. Abort. Definition myif X (c: bool) (l r: X): X := if c then l else r. Lemma if_myif: forall X (c: bool) (l r: X), (if c then l else r) = myif c l r. Proof. reflexivity. Qed. Global Instance myif_rel: Proper (eq ==> rel ==> rel ==> rel) (@myif A). Proof. repeat intro. unfold myif. subst. destruct y; auto. Qed. Goal rel (if true then ctx a0 else weird) (ctx a1). Proof. rewrite if_myif. rewrite REL. cbn. reflexivity. Qed.
I'd also like to know whether that's possible. Wrapping it into a
myif function like you did is the only way I know.
My workaround would be to use first
case_match (from stdpp's tactics.v).
Side comment on that code: instead of
Global Instance myif_rel: Proper (eq ==> rel ==> rel ==> rel) (@myif A). you'd want
Global Instance myif_rel cond: Proper (rel ==> rel ==> rel) (@myif A cond). — you don't need setoid rewriting for "normal" rewrites
Thanks for your repiles!
@Li-yao That definitely makes me less guilty. Thanks for sharing your experience.
@Paolo Giarrusso Unfortunately, in my case, the
if true then ctx a0 else weird can be wrapped by a context that contains more
if, which I don't want to destruct.
Last updated: Oct 01 2023 at 18:01 UTC