The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

This is an interesting challenge and I can't resist proposing a
solution with recursive notations, even if it is a bit hackish (it
beta-expands the expected expression via a combinator to deal with the
duplication of inner variables). Also, it happens to require a small
extension which is not available in 8.12 (see Coq PR #12765 which I
just submitted [1]). Nevertheless, with this extension, the following
works for parsing, as well as for printing (as long as the
beta-expansions are preserved):

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

Notation iter := (fun b A a => red a b /\ A b).
Notation termin b := (fun a => red a b).
Notation "x  ⪯ y  ⪯ ..  ⪯ z  ⪯ t" := (iter y .. (iter z (termin t)) .. x)
  (at level 70, y at next level, z at next level, t at next level).

Axiom X0 X1 X2 X3 : Type.
Axiom x0 : phi X0.
Axiom x1 : phi X1.
Axiom x2 : phi X2.
Axiom x3 : phi X3.
Check x0 ⪯ x1 ⪯ x2 ⪯ x3.
(* x0 ⪯ x1 ⪯ x2 ⪯ x3 *)

Best,

Hugo

[1] https://github.com/coq/coq/pull/12765

On Tue, Jul 28, 2020 at 04:01:35PM +0200, Dominique Larchey-Wendling wrote:
> 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 *)
> > ```