The Coq mailing list

[Benoît Viguier <beviguier AT gmail.com>]

Hi Jacques-Pascal,

I don't know if this is what you are looking for but you have :

rewrite [<-] ?H [in ...]

which is equivalent to :

rewrite [<-] H [in ...].
rewrite [<-] H [in ...].
rewrite [<-] H [in ...].
rewrite [<-] H [in ...].
...

this will replace every occurrences until it fails (care for infinite recursion !). If rewrite can not be applied to the goal it does nothing.

You also have

rewrite [<-] !H [in ...]

which is the same as "?" but will fail if it can not be applied at least once.

Kind regards.

2016-03-22 17:36 GMT+01:00 Jacques-Pascal Deplaix <jp.deplaix AT gmail.com>:

Hi,

I'm doing proofs in coq which requires a rewrite as soon as possible in
the proof and we've been struggling in finding a way to rewrite every
single occurrences of the current goal (which has « fun x =>
ThingsToRewrite … » and other nightmares).
We've come to the following solution:

```
Program Instance :
forall A B, subrelation (@pointwise_relation A B eq) eq.
Next Obligation.
apply func_ext_dep. intros. rewrite H. reflexivity.
Qed.

Program Instance :
forall A B C D E F G H I J K (f : A -> B -> C -> D -> E -> F -> G -> H
-> I -> J -> K), Proper (eq ==> eq ==> eq ==> eq ==> eq ==> eq ==> eq
==> eq ==> eq ==> eq ==> eq) f.
Next Obligation.
compute. intros. f_equal; auto.
Qed.

Program Instance :
forall A B C D E F G H I J (f : A -> B -> C -> D -> E -> F -> G -> H
-> I -> J), Proper (eq ==> eq ==> eq ==> eq ==> eq ==> eq ==> eq ==> eq
==> eq ==> eq) f.
Next Obligation.
compute. intros. f_equal; auto.
Qed.

Program Instance :
forall A B C D E F G H I (f : A -> B -> C -> D -> E -> F -> G -> H ->
I), Proper (eq ==> eq ==> eq ==> eq ==> eq ==> eq ==> eq ==> eq ==> eq) f.
Next Obligation.
compute. intros. f_equal; auto.
Qed.

Program Instance :
forall A B C D E F G H (f : A -> B -> C -> D -> E -> F -> G -> H),
Proper (eq ==> eq ==> eq ==> eq ==> eq ==> eq ==> eq ==> eq) f.
Next Obligation.
compute. intros. f_equal; auto.
Qed.

Program Instance :
forall A B C D E F G (f : A -> B -> C -> D -> E -> F -> G), Proper (eq
==> eq ==> eq ==> eq ==> eq ==> eq ==> eq) f.
Next Obligation.
compute. intros. f_equal; auto.
Qed.

Program Instance :
forall A B C D E F (f : A -> B -> C -> D -> E -> F), Proper (eq ==> eq
==> eq ==> eq ==> eq ==> eq) f.
Next Obligation.
compute. intros. f_equal; auto.
Qed.

Program Instance :
forall A B C D E (f : A -> B -> C -> D -> E), Proper (eq ==> eq ==> eq
==> eq ==> eq) f.
Next Obligation.
compute. intros. f_equal; auto.
Qed.

Program Instance :
forall A B C D (f : A -> B -> C -> D), Proper (eq ==> eq ==> eq ==> eq) f.
Next Obligation.
compute. intros. f_equal; auto.
Qed.

Program Instance :
forall A B C (f : A -> B -> C), Proper (eq ==> eq ==> eq) f.
Next Obligation.
compute. intros. f_equal; auto.
Qed.

Program Instance :
forall A B (f : A -> B), Proper (eq ==> eq) f.
Next Obligation.
compute. intros. f_equal; auto.
Qed.
```
```
and then use setoid_rewrite instead of rewrite.


NOTE: the order of the Proper instances are relevant. The other way
around, it will loop infinity.


We were wondering if there was a nicer way to do that ? Maybe already in
the coq standard library ?
In other words, is there a standard way to rewrite everywhere in the
current goal ?


Cheers,