The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Below is the variant I needed but thx a lot !!!

Dominique

-------

Axiom phi : Type -> Type.
Axiom red : forall {X Y : Type}, phi X -> phi Y -> Prop.

Ltac chainToProp' xs :=
  lazymatch xs with
  | pair ?x (pair ?y ?xs) =>
    let z := chainToProp' (pair y xs) in
    constr:(red x y /\ z)
  | pair ?x ?y => constr:(red x y)
  end.

Ltac chainToProp xs :=
  let z := chainToProp' xs in
  exact z.

Axiom X0 X1 X2 X3 : Type.
Axiom x0 : phi X0.
Axiom x1 : phi X1.
Axiom x2 : phi X2.
Axiom x3 : phi X3.

Declare Scope chain.
Delimit Scope chain with chain_scope.
Notation "x ⪯ y" := (pair x y) (at level 80, right associativity, only
parsing) : chain.
Notation "'chain' xs 'endchain'" := (ltac:(chainToProp (xs %
chain_scope))) (only parsing).
Check chain x0 ⪯ x1 ⪯ x2 ⪯ x3 endchain.


----- Mail original -----
> De: "Maximilian Wuttke" <mwuttke97 AT posteo.de>
> À: "coq-club" <coq-club AT inria.fr>
> Envoyé: Mardi 28 Juillet 2020 15:51:33
> Objet: Re: [Coq-Club] Recursive Notation in Coq

> On 28/07/2020 15:32, Adam Chlipala wrote:
>> 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
>> <http://adam.chlipala.net/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.
> 
> Using pairs + ltac for this is a good idea! I implemented it below.
> 
> I also solved the 'problem' that list notation had to be used inside
> `chain ... endchain`. Now we can write `chain 1 <=, 2 <=, 3` (note the
> comma). This solution uses a scope in which `<=,` is an infix for pairs.
> 
>> red {X Y : Type} : phi X -> phi Y -> Prop  where phi : Type -> Type
> 
> In the code below, I used a slightly different type of `red`, but you
> should be able to adapt the code to your type.
> 
> 
> ```
> (* This is a bit different than asked *)
> Axiom phi : Type -> Type.
> Axiom red : forall {X : Type}, X -> phi X -> Prop.
> 
> Ltac chainToProp' xs :=
>  lazymatch xs with
>  | pair ?x (pair ?y ?xs) =>
>    let z := chainToProp' (pair y xs) in
>    constr:(red x y /\ z)
>  | pair ?x ?y => constr:(red x y)
>  end.
> 
> Ltac chainToProp xs :=
>  let z := chainToProp' xs in
>  exact z.
> 
> Axiom X0 : Type.
> Axiom a : X0.
> Axiom b : phi X0.
> Axiom c : phi (phi X0).
> Axiom d : phi (phi (phi X0)).
> 
> Declare Scope chain.
> Delimit Scope chain with chain_scope.
> Notation "x <=, y" := (pair x y) (at level 80, right associativity, only
> parsing) : chain.
> Notation "'chain' xs 'endchain'" := (ltac:(chainToProp (xs %
> chain_scope))) (only parsing).
> Check chain a <=, b <=, c <=, d endchain.
> (* red a b /\ red b c /\ red c d *)
> (*      : Prop *)
> ```