Setoid_rewrite failed, but succeeded when using '<-' or 'at'

Using Coq
1

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

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.
2

Your first morphism has eqfun as its conclusion:

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:

 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.

1 Like
3

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.

4

Isn’t that’s what at is for?