Stream: Coq users

Topic: Question on setoid rewrite inside `if` or `match`

YoungJu Song (Jul 15 2020 at 14:01):

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.

Li-yao (Jul 15 2020 at 16:25):

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.

Paolo Giarrusso (Jul 15 2020 at 19:06):

My workaround would be to use first case_match (from stdpp's tactics.v).

Paolo Giarrusso (Jul 15 2020 at 19:08):

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

YoungJu Song (Jul 20 2020 at 08:02):

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 13 2024 at 01:02 UTC