# Notation for inequality chain

Dear all,

I’d like to be able to write

``````Unset Printing Notations.
Compute (1 <= 2 <= 3 <= 4 <= 5)
``````

and have that result in

``````le 1 2 /\ le 2 3 /\ le 3 4 /\ le 4 5
``````

Coq ships with a built-in notation `a <= b <= c`, but I’d like that for arbitrary chain lengths. (I’m not actually interested in the case for `le`, but for another relation, which shouldn’t make a difference for the approach.)

Any hints or ideas how to implement such a notation?

If that doesn’t work, I’m also okay with something like `chain 1 <= 2 <= 3 <= 4 endchain`, i.e. explicit begin and end markers.

Yannick

Hi,

Something like this can be done with a bit of ltac trickery. The following notation doesn’t use a chain of `<=`s, but the recursive notation of lists:

``````From Coq Require Import List.
Import ListNotations.

Ltac chainToProp' xs :=
lazymatch xs with
| nil => constr:(True)
| cons ?x (cons ?y nil) => constr:(x <= y)
| cons ?x (cons ?y ?xs) =>
let z := chainToProp' (cons y xs) in
constr:(x <= y /\ z)
end.

Ltac chainToProp xs :=
let z := chainToProp' xs in
exact z.

Check ltac:(chainToProp [1;2;3;4]).

Notation "'chain' xs 'endchain'" := (ltac:(chainToProp xs)) (only parsing).

Check chain [1;2;3;4] endchain.
(* 1 <= 2 /\ 2 <= 3 <= 4 *)
(*      : Prop *)
``````

Note that this notation is `parseonly`.

Perhaps a better notation can be defined using custom entries (e.g. for allowing to use `<=` inside `chain ... chainend`), but I haven’t tried them out yet.

Depending on the kind of notations you want, you can use a recursive one:

``````Fixpoint le_list x l z :=
match l with
| nil => le x z
| cons y l => le x y /\ le_list y l z
end.

Notation "[ <= u , v , .. , y , z ]" := (le_list u (cons v .. (cons y nil) ..) z).

Eval compute in [<= 0, 1, 2, 3, 4].
(* = 0 <= 1 /\ 1 <= 2 /\ 2 <= 3 <= 4 : Prop *)
``````

I do not know if it is possible to achieve the same result with only a recursive notation (that is, without an auxiliary function). I have never succeeded in writing a recursive notation that duplicates some of its terms.

While the topic how how to obtain this kind of notations has been discussed at length on coq-club, I’m not sure nested conjunctions make for good (usable) theorem statements. When faced with a similar problem for graph parameters, I used the following (working with mathcomp):

``````Corollary Cockayne_Hedetniemi_chain:
sorted leq [:: ir; gamma; ii; alpha; Gamma; IR].

Lemma sorted_leq_nth s (srt_s : sorted leq s) :
forall i j, i < j -> i < size s -> j < size s -> nth 0 s i <= nth 0 s j.

Notation Cockayne_Hedetniemi i j :=
(@sorted_leq_nth _ Cockayne_Hedetniemi_chain i j erefl erefl erefl).
``````

This way, one can use: `apply: (Cockayne_Hedetniemi 1 4)` to solve `gamma <= Gamma`, using the fact that “_ < _” on natural numbers computes in mathcomp.

To compare, here is the same trick using `<?`, which is “the” computational variant of `<`, i.e. `Nat.lt`, in the standard library.

``````Parameter A : Type.
Parameter myle : A -> A -> Prop.
Parameter ir gamma ii alpha Gamma IR : A.
Parameter default : A.

Require Import List Arith Sorted.
Import ListNotations.

Corollary Cockayne_Hedetniemi_chain:
Sorted myle [ir; gamma; ii; alpha; Gamma; IR].