The Coq mailing list

[Maximilian Wuttke <mwuttke97 AT posteo.de>]

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