The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Thanks for that suggestion; I'm still learning to remember the 
possibilities of tactics in terms!

It is worth pointing out that this is inherently a parsing-only 
notation, as there is no magic inversion of Ltac code to detect when a 
Gallina term could have been produced by a notation rule as fancy as 
this one.  If you are willing to have your desugared goals contain 
literal calls to functions like [chainToProp], it is quite possible to 
get printing using your notation, too, if you skip the Ltac.

On 7/28/20 9:08 AM, Maximilian Wuttke wrote:
> Hi Club,
>
>
> In addition to the solution I posted on Discourse [1], here's an
> implementation of Adam's idea:
>
> ```
> Fixpoint chainToProp {X : Type} (R : X->X->Prop) (xs : list X) : Prop :=
>    match xs with
>    | nil => True
>    | x :: xs =>
>      match xs with
>      | nil => True
>      | y :: nil => R x y
>      | y ::   _ => R x y /\ chainToProp R xs
>      end
>    end.
>
> Notation "'chain' xs 'endchain'" := (ltac:(let x := eval cbv
> [chainToProp] in (chainToProp le xs) in exact x)) (only parsing).
>
> Check chain [1;2;3;4] endchain.
> (* 1 <= 2 /\ 2 <= 3 /\ 3 <= 4 *)
> (*      : Prop *)
> ```
>
> [1]: <https://coq.discourse.group/t/notation-for-inequality-chain/979/2>
>
>
> On 28/07/2020 14:44, Adam Chlipala wrote:
> > My guess is that (1) you may need to add some kind of brackets around
> > the notation, and (2) you may need to build a Gallina list of the
> > different elements and then apply a Gallina function that checks
> > relatedness of adjacent elements.  There is indeed a built-in notation
> > facility for variable-length forms, but I don't think it allows
> > constructing subterms out of adjacent parts of the original argument
> > list, and it doesn't allow referencing the same notation recursively in
> > the expansion.
> >
> > On 7/28/20 8:39 AM, Dominique Larchey-Wendling wrote:
> > > Dear all,
> > >
> > > If a notations wizard could help me at defining
> > > the following recursive notation in Coq, I would
> > > be very grateful.
> > >
> > > x ⪯ y ⪯ .. ⪯ z := red x y /\ y ⪯ .. ⪯ z
> > >
> > > where red : _ -> _ -> Prop
> > >
> > > ie
> > >
> > > a ⪯ b ⪯ c ⪯ d would be (red a b) /\ (red b c /\ red c d).
> > >
> > > Sequences must have length >=2 (otherwise they would be meaningless)
> > >
> > > Thank you very much for some insights,
> > >
> > > Dominique