The Coq mailing list

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

Thank you Hugo,

I will keep it in my mind for when our code base upgrades to Coq-8.12+
It is more readily understandable (ie. it does not involve Ltac)
that M. Wuttke's hack although his is only for parsing and thus,
as soon as the expected result is good, understanding how it works
is not so critical.

Your proposed solution does not involve external parentheses
though. But would it work as well for length 3 chains
ie "x ⪯ y ⪯ z" ?

Best,

D.

----- Mail original -----
> De: "Hugo Herbelin" <Hugo.Herbelin AT inria.fr>
> À: "Dominique Larchey-Wendling" <dominique.larchey-wendling AT loria.fr>
> Cc: "coq-club" <coq-club AT inria.fr>
> Envoyé: Mercredi 29 Juillet 2020 14:20:25
> Objet: Re: [Coq-Club] Recursive Notation in Coq

> 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 *)
> > > ```