# Setoid\_rewrite failed, but succeeded when using '\<-' or 'at'

**URL:** <https://discourse.rocq-prover.org/t/setoid-rewrite-failed-but-succeeded-when-using-or-at/1696>\
**Category:** Using Rocq\
**Created:** [June 13, 2022, 5:01am UTC](https://discourse.rocq-prover.org/t/setoid-rewrite-failed-but-succeeded-when-using-or-at/1696 "2022-06-13T05:01:51Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![angelbeats](https://avatars.discourse-cdn.com/v4/letter/a/b9e5f3/32.png) [@angelbeats](https://discourse.rocq-prover.org/u/angelbeats)\
**Post date:** [June 13, 2022, 5:01am UTC](https://discourse.rocq-prover.org/t/setoid-rewrite-failed-but-succeeded-when-using-or-at/1696/1 "2022-06-13T05:01:51Z")

</div>

Only l4 failed. What instance should I add to make this work?

```coq
Require Export Coq.Strings.String.

Definition eqb_string (x y : string) : bool :=
  if string_dec x y then true else false.
Definition total_map (A : Type) := string -> A.
Definition t_update {A : Type} (m : total_map A)
                    (x : string) (v : A) :=
  fun x' => if eqb_string x x' then v else m x'.

Inductive aexp : Type :=
  | ANum (n : nat)
  | APlus (a1 a2 : aexp).

Fixpoint aeval {A : Type} (st : total_map A) (a : aexp) : nat :=
  match a with
  | ANum n => n
  | APlus a1 a2 => (aeval st a1) + (aeval st a2)
  end.

Definition eqfun {A B : Type} (f g : B -> A) : Prop := forall x, f x = g x.

Require Import Setoid Relation_Definitions.
Lemma frefl {A B : Type} (f : B -> A) : eqfun f f. Proof. Admitted.
Lemma fsym {A B : Type} (f g : B -> A): eqfun f g -> eqfun g f. Proof. Admitted.
Lemma ftrans {A B : Type} (f g h : B -> A): eqfun f g -> eqfun g h -> eqfun f h. Proof. Admitted.

Add Parametric Relation {A B : Type} : (B -> A) (@eqfun A B)
  reflexivity proved by (@frefl A B)
  symmetry proved by (@fsym A B)
  transitivity proved by (@ftrans A B)
  as eqfun_rel.

Add Parametric Morphism {A : Type} : (@t_update A)
  with signature (@eqfun A string) ==> Logic.eq ==> Logic.eq ==> (@eqfun A string) as t_update_mor.
Proof. Admitted.

Add Parametric Morphism : aeval
  with signature (@eqfun nat string) ==> Logic.eq ==> Logic.eq as aeval_mor.
Proof. Admitted.

Lemma l1 {p q} {x} {a} : eqfun q p -> (t_update q x (aeval p a)) = (t_update q x (aeval q a)).
Proof.
  intros H. setoid_rewrite <- H. auto.
Qed.

Lemma l2 {p q} {x} {a} : eqfun q p -> (t_update q x (aeval p a)) = (t_update q x (aeval q a)).
Proof.
  intros H. setoid_rewrite H at 3. auto.
Qed.

Lemma l3 {p q r : total_map nat} {x} {a} : eqfun q p -> (t_update r x (aeval p a)) = (t_update r x (aeval q a)).
Proof.
  intros H. setoid_rewrite H. auto.
Qed.

Lemma l4 {p q} {x} {a} : eqfun q p -> (t_update q x (aeval p a)) = (t_update q x (aeval q a)).
Proof.
  intros H. Fail setoid_rewrite H. auto.
Admitted.

```

---

<div class="post-metadata">

**Author:** ![cpitclaudel](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/cpitclaudel/32/337_2.png) [@cpitclaudel](https://discourse.rocq-prover.org/u/cpitclaudel)\
**Post date:** [June 13, 2022, 5:39am UTC](https://discourse.rocq-prover.org/t/setoid-rewrite-failed-but-succeeded-when-using-or-at/1696/2 "2022-06-13T05:39:20Z")

</div>

Your first morphism has `eqfun` as its conclusion:

```coq
Add Parametric Morphism {A : Type} : (@t_update A)
  with signature (@eqfun A string) ==> Logic.eq ==> Logic.eq ==> (@eqfun A string) as t_update_mor.
Proof. Admitted.

```

… but your goal has `eq` as its conclusion:

```coq
 t_update q x (f p a) = t_update q x (f q a)

```

When you ask `setoid_rewrite` to rewrite `H : eqfun q p`, it tries to replace all three occurrences of `q` (including as an argument to `t_update` on both side). Hence the error.

You can confirm this by changing the goal to `eqfun (t_update q x (f p a)) (t_update q x (f q a))`; in that case, `setoid_rewrite H` works fine.

This is also white the right-to-left rewrite `setoid_rewrite <- H` works: the only occurence of `p` is as an argument to `f`, and the conclusion of `f_mor` is an equality.

---

<div class="post-metadata">

**Author:** ![angelbeats](https://avatars.discourse-cdn.com/v4/letter/a/b9e5f3/32.png) [@angelbeats](https://discourse.rocq-prover.org/u/angelbeats)\
**Post date:** [June 13, 2022, 8:39am UTC](https://discourse.rocq-prover.org/t/setoid-rewrite-failed-but-succeeded-when-using-or-at/1696/3 "2022-06-13T08:39:05Z")

</div>

I’ve updated `f` to `aeval` since `rewrite H` works on `f`.  
I don’t want to change the goal to `eqfun`. Which tactic should I use to rewrite only one occurence?  
I know `replace (eval q a) with (eval p a) by (rewrite H).`, I just don’t want that.

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [June 25, 2022, 9:29pm UTC](https://discourse.rocq-prover.org/t/setoid-rewrite-failed-but-succeeded-when-using-or-at/1696/4 "2022-06-25T21:29:50Z")

</div>

> [@angelbeats](#):
>
> rewrite only one occurence?

Isn’t that’s what `at` is for?