coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Rewrite everywhere
- Date: Tue, 22 Mar 2016 18:55:33 +0100
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.
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
- [Coq-Club] Rewrite everywhere, Jacques-Pascal Deplaix, 03/22/2016
- Re: [Coq-Club] Rewrite everywhere, Benoît Viguier, 03/22/2016
- Re: [Coq-Club] Rewrite everywhere, Jacques-Henri Jourdan, 03/22/2016
- Re: [Coq-Club] Rewrite everywhere, Matthieu Sozeau, 03/23/2016
- Re: [Coq-Club] Rewrite everywhere, Jacques-Pascal Deplaix, 03/23/2016
- Re: [Coq-Club] Rewrite everywhere, Jacques-Henri Jourdan, 03/23/2016
- Re: [Coq-Club] Rewrite everywhere, Matthieu Sozeau, 03/24/2016
- Re: [Coq-Club] Rewrite everywhere, Matthieu Sozeau, 03/23/2016
- Re: [Coq-Club] Rewrite everywhere, Jacques-Henri Jourdan, 03/22/2016
- Re: [Coq-Club] Rewrite everywhere, Benoît Viguier, 03/22/2016
Archive powered by MHonArc 2.6.18.