coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Recursive Notation in Coq
- Date: Tue, 28 Jul 2020 15:54:25 +0200 (CEST)
Yes I could form the type
list { X & phi X } (*which might generate universe inconsistencies at some point*)
or work with heterogenous lists, but I hoped maybe a notation
would give a nicer solution. Thx anyway.
De: "Adam Chlipala" <adamc AT csail.mit.edu>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Mardi 28 Juillet 2020 15:32:57
Objet: Re: [Coq-Club] Recursive Notation in Coq
That's harder to do with the solution where you build a list and call a Gallina function, but it only requires standard use of heterogeneous list types (e.g., see Chapter 9 of CPDT). Type inference is quite smart enough to reconstruct a list of types from a (heterogeneous) list of values of those types. And, if working with heterogeneous lists doesn't seem worth the trouble, you can use a notation that constructs a tuple and passes it off to Ltac, which can do recursive traversal of tuples as easily as of various list types.
On 7/28/20 9:14 AM, Dominique Larchey-Wendling wrote:
Thanks for the suggestion but can you do it when the type X is not uniform? I mean the type of red is actually red {X Y : Type} : phi X -> phi Y -> Prop where phi : Type -> Type D. ----- Mail original -----De: "Maximilian Wuttke" <mwuttke97 AT posteo.de> À: "coq-club" <coq-club AT inria.fr> Envoyé: Mardi 28 Juillet 2020 15:08:43 Objet: Re: [Coq-Club] Recursive Notation in CoqHi Club, In addition to the solution I posted on Discourse [1], here's an implementation of Adam's idea: ``` Fixpoint chainToProp {X : Type} (R : X->X->Prop) (xs : list X) : Prop := match xs with | nil => True | x :: xs => match xs with | nil => True | y :: nil => R x y | y :: _ => R x y /\ chainToProp R xs end end. Notation "'chain' xs 'endchain'" := (ltac:(let x := eval cbv [chainToProp] in (chainToProp le xs) in exact x)) (only parsing). Check chain [1;2;3;4] endchain. (* 1 <= 2 /\ 2 <= 3 /\ 3 <= 4 *) (* : Prop *) ``` [1]: <https://coq.discourse.group/t/notation-for-inequality-chain/979/2> On 28/07/2020 14:44, Adam Chlipala wrote:My guess is that (1) you may need to add some kind of brackets around the notation, and (2) you may need to build a Gallina list of the different elements and then apply a Gallina function that checks relatedness of adjacent elements. There is indeed a built-in notation facility for variable-length forms, but I don't think it allows constructing subterms out of adjacent parts of the original argument list, and it doesn't allow referencing the same notation recursively in the expansion. On 7/28/20 8:39 AM, Dominique Larchey-Wendling wrote:Dear all, If a notations wizard could help me at defining the following recursive notation in Coq, I would be very grateful. x ⪯ y ⪯ .. ⪯ z := red x y /\ y ⪯ .. ⪯ z where red : _ -> _ -> Prop ie a ⪯ b ⪯ c ⪯ d would be (red a b) /\ (red b c /\ red c d). Sequences must have length >=2 (otherwise they would be meaningless) Thank you very much for some insights, Dominique
- Re: [Coq-Club] Recursive Notation in Coq, (continued)
- Re: [Coq-Club] Recursive Notation in Coq, Adam Chlipala, 07/28/2020
- Re: [Coq-Club] Recursive Notation in Coq, Maximilian Wuttke, 07/28/2020
- Re: [Coq-Club] Recursive Notation in Coq, Adam Chlipala, 07/28/2020
- Re: [Coq-Club] Recursive Notation in Coq, Dominique Larchey-Wendling, 07/28/2020
- Re: [Coq-Club] Recursive Notation in Coq, Adam Chlipala, 07/28/2020
- Re: [Coq-Club] Recursive Notation in Coq, Maximilian Wuttke, 07/28/2020
- Re: [Coq-Club] Recursive Notation in Coq, Dominique Larchey-Wendling, 07/28/2020
- Re: [Coq-Club] Recursive Notation in Coq, Hugo Herbelin, 07/29/2020
- Re: [Coq-Club] Recursive Notation in Coq, Dominique Larchey-Wendling, 07/29/2020
- Re: [Coq-Club] Recursive Notation in Coq, Hugo Herbelin, 07/29/2020
- Re: [Coq-Club] Recursive Notation in Coq, Dominique Larchey-Wendling, 07/28/2020
- Re: [Coq-Club] Recursive Notation in Coq, Maximilian Wuttke, 07/28/2020
- Re: [Coq-Club] Recursive Notation in Coq, Adam Chlipala, 07/28/2020
- Re: [Coq-Club] Recursive Notation in Coq, Dominique Larchey-Wendling, 07/28/2020
- Re: [Coq-Club] Recursive Notation in Coq, Maximilian Wuttke, 07/28/2020
- Re: [Coq-Club] Recursive Notation in Coq, Adam Chlipala, 07/28/2020
Archive powered by MHonArc 2.6.19+.