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: Hugo Herbelin <Hugo.Herbelin AT inria.fr>
  • To: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
  • Cc: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Recursive Notation in Coq
  • Date: Wed, 29 Jul 2020 14:20:25 +0200

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



Archive powered by MHonArc 2.6.19+.

Top of Page