Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Rewrite everywhere

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Rewrite everywhere


Chronological Thread 
  • From: Jacques-Pascal Deplaix <jp.deplaix AT gmail.com>
  • To: coq-club AT inria.fr
  • Cc: arthur AT chargueraud.org, François Pottier <Francois.Pottier AT inria.fr>, mattam AT mattam.org, jacques-henri.jourdan AT inria.fr
  • Subject: [Coq-Club] Rewrite everywhere
  • Date: Tue, 22 Mar 2016 17:36:35 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jp.deplaix AT gmail.com; spf=Pass smtp.mailfrom=jp.deplaix AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f43.google.com
  • Ironport-phdr: 9a23:PQXWLx/AHPnvrf9uRHKM819IXTAuvvDOBiVQ1KB91eIcTK2v8tzYMVDF4r011RmSDdWdsq4P2rKempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lSsiL04/mj6ibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwuwwZgf8q9tZBXKPmZOx4COUAVHV1e1wyscbsrFzISRaFznoaSGQf1BRSUCbf6xSvfJ76qzb3ra9F0TKRNMm+Yb0sXT2j/+8/SgeuhCofMzc44EnYj8VxiORQpxf39E83+JLdfIzAbKk2RajaZ95PADMZBss=
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: 0xCC355C4A.asc
Description: application/pgp-keys


Archive powered by MHonArc 2.6.18.

Top of Page