Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Recursive Notation in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Recursive Notation in Coq


Chronological Thread 
  • 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 Coq

      
Hi 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

        






Archive powered by MHonArc 2.6.19+.

Top of Page