The Coq mailing list

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

My solution does not involve parentheses and it works for length 3
(but not for length 2: this requires an extra rule).

If you are ready to have parentheses, the following actually also
works in previous versions of Coq (with the same drawback that there
is a bit of "noise" in the encoding).

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

Notation split := (fun x => x).
Notation iter := (fun b A a => red a b /\ A b).
Notation termin b := (fun a => red a b).
Notation "'chain' x ⪯ y ⪯ .. ⪯ z ⪯ t 'endchain'" := (split (iter y .. (iter z 
(termin t)) ..) x).

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

Check chain x0 ⪯ x1 ⪯ x2 ⪯ x3 endchain.
---

The following also works with previous versions of Coq:

Notation "x ⪯ y ⪯ .. ⪯ z <= t" := (split (iter y .. (iter z (termin t)) ..) x)
  (at level 70, y at next level, z at next level, t at next level).

To go into details, this is because #12765 improves two things. Adding
"split" compensates the first improvement (support for applied
recursive pattern) by breaking the applied pattern into two distinct
applications. Adding a closing parenthesis (here "endchain"), or a
different symbol for the last "<=", compensates a slight weakness with
the needed factorization between a recursive pattern and what comes
after it in grammar rule.

Best,

Hugo

On Wed, Jul 29, 2020 at 03:06:36PM +0200, Dominique Larchey-Wendling wrote:
> 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 *)
> > > > ```