The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

On Wed, Mar 23, 2016 at 3:56 PM Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr> wrote:

Hi Matthieu,

Thank you for the answer.

Perhaps you could help us understand by explaining us what is the process followed by setoid_rewrite (i.e., what instances is searched for, and how two instances you give here are used).

Hi,

  

  the unsatisfiable constraints message is giving you the instances that we are looking for:

 ?X30==[A P1 P2 H |- relation Prop] (internal placeholder) {?r}

 ?X31==[A P1 P2 H (do_subrelation:=do_subrelation)

         |- Proper

              (pointwise_relation A eq ==>

               ?X30@{__:=A; __:=P1; __:=P2; __:=H}) exists']

         (internal placeholder) {?p}

 ?X41==[A P1 P2 H |- relation Prop] (internal placeholder) {?r0}

 ?X42==[A P1 P2 H (do_subrelation:=do_subrelation)

         |- Proper

              (?X30@{__:=A; __:=P1; __:=P2; __:=H} ==>

               ?X41@{__:=A; __:=P1; __:=P2; __:=H} ==> flip impl) eq]

         (internal placeholder) {?p0}

 ?X43==[A P1 P2 H

         |- ProperProxy ?X41@{__:=A; __:=P1; __:=P2; __:=H}

              (exists' (fun x : A => P2 x))] (internal placeholder) {?p1}

You can ignore the relation existentials. The constraints are processed in order of the existentials (increasing). So we first look for an instance of Proper (pointwise eq ==> ?) exists'. There are no such declared instances, so we try to find an instance of Proper ?R exists' such that subrelation ?R (pointwise eq ==> ?) (the flag do_subrelation implies that we can try this, this form of "subtyping" is restricted to toplevel constraints). The instance found for Proper ?R exists' is Proper eq exists' and we're left with the subrelation subgoal, now subrelation eq (pointwise eq ==> ?), which can be derived with the instances I gave.

Apart from subrelation there is another "generic" instance which normalizes signatures w.r.t. flip, to allow deriving Proper (flip R ==> flip R') f from Proper (R ==> R') f for example.

Most of the proof search is defined in Coq.Classes.Morphisms, and you can see what is searched for using Set Typeclasses Debug.

Also Typeclasses eauto := n will limit the search to depth n which can be useful for debugging. The search strategy is depth-first search, which makes it very sensitive to looping instances. I don't know why this makes your search loop, but a common cause is that instances are applied too eagerly. For example the one I gave you:

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

This might be dangerous as it can apply to any goal subrelation ?R ?R', one should rather guard it to ensure this is called only when the first argument is eq, like this:

Lemma subreleqr : ...

Hint Extern 4 (subrelation eq _) => class_apply @subreleqr : typeclass_instances.

(* class_apply avoids typeclass resolution so that the Reflexive subgoal is produced here *)

Improving the performance of setoid_rewrite by controlling this proof search is actually one thing we're working on right now.

Hope this helps,

-- Matthieu 

Le 23/03/2016 15:10, Matthieu Sozeau a écrit :

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,