The Coq mailing list

[Jacques-Pascal Deplaix <jp.deplaix AT gmail.com>]

Hi,

Thanks for your answer but it doesn't work. Well it sort of works for
some cases (it's horribly slow tho: 15s for one setoid_rewrite) and it
doesn't terminate otherwise.
Do you have an other solution/fix ?

Cheers,

On 03/23/2016 03:10 PM, Matthieu Sozeau wrote:
> 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
>  
> <mailto: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
>>     
>> <<mailto:jp.deplaix AT gmail.com>jp.deplaix AT gmail.com
>>     
>> <mailto: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,
>>
>>
>