The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

I think setoid_rewrite should be able to infer all those instances, and adding a subrelation is the right way to make it use extensionality. However, the way subtyping is implemented only Proper eq f for any f is inferred, independently of the arity of f. Here one must show the subrelation relation for eq <= (pointwise_relation A eq ==> ?) that was infered from the rewrite. For the [Proper (pointwise_relation A eq ==> eq) exist'] instances to be automatically inferred, you hence need to add also the following two instances:

(* Proper eq exists' is infered automatically, and we need to show eq <= (pointwise_relation A eq ==> eq) *)

Instance : forall A (R : relation A) (refl : Reflexive R) , subrelation eq R.

Proof.

  reduce. subst. apply refl.

Qed.

(** This show that (pointwise_relation A eq ==> eq) is Reflexive *)

Instance reflexive_pointwise: forall A B C (R : relation C), Reflexive R -> Reflexive (pointwise_relation A (@eq B) ==> R)%signature.

Proof.

  reduce. red in H0.

  apply functional_extensionality_dep in H0. subst.

  reflexivity.

Qed.

Cheers,

-- Matthieu

Le mar. 22 mars 2016 à 18:55, Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr> a écrit :

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,