The Coq mailing list

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

Thanks for the suggestion but can you do it
when the type X is not uniform? I mean the 
type of red is actually

red {X Y : Type} : phi X -> phi Y -> Prop  where phi : Type -> Type

D.

----- Mail original -----
> De: "Maximilian Wuttke" <mwuttke97 AT posteo.de>
> À: "coq-club" <coq-club AT inria.fr>
> Envoyé: Mardi 28 Juillet 2020 15:08:43
> Objet: Re: [Coq-Club] Recursive Notation in Coq

> 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
>>