The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

To reformulate Jacques-Pascal question:

How to tell setoid_rewrite to use functional extensionality to rewrite under lambdas ?

We are able to define the following instance (which is basically functional extensionality) :

Program Instance :
  forall A B, subrelation (@pointwise_relation A B eq) eq.

So that rewriting happens when the context of the lambda is simple. We can then use setoid_rewrite to prove the following lemma:

forall A B (f g:A->B), (forall x, f x = g x) -> (fun x => f x) = (fun x => g x).

But if now we define :

Definition exists' {A:Type} P := exists (x:A), P x.

And we try to prove :

Lemma L :
  forall A (P1 P2:A -> Prop),
    (forall x, P1 x = P2 x) ->
    exists' (fun x => P1 x) = exists' (fun x => P2 x).

This does not work, because the lambda is applied to something. We need to define the instance :

Program Instance :
   forall A B (f : A -> B), Proper (eq ==> eq) f.

But this does not work if the lambda is not the last parameter of exist'. then we need all the others instances...

So the question becomes : is there any way to tell setoid_rewrite that any context is respectful of Liebniz equality ?

--
JH




Le 22/03/2016 18:22, Benoît Viguier a écrit :

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,

Attachment: signature.asc
Description: OpenPGP digital signature