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: Jun 18 2024 at 08:01 UTC