# Notation for inequality chain

**URL:** <https://discourse.rocq-prover.org/t/notation-for-inequality-chain/979>\
**Category:** Using Rocq\
**Created:** [July 28, 2020, 11:59am UTC](https://discourse.rocq-prover.org/t/notation-for-inequality-chain/979 "2020-07-28T11:59:55Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![yforster](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/yforster/32/30_2.png) [@yforster](https://discourse.rocq-prover.org/u/yforster)\
**Post date:** [July 28, 2020, 11:59am UTC](https://discourse.rocq-prover.org/t/notation-for-inequality-chain/979/1 "2020-07-28T11:59:56Z")

</div>

Dear all,

I’d like to be able to write

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

```

and have that result in

```auto
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.

Many thanks in advance!  
Yannick

---

<div class="post-metadata">

**Author:** ![mwuttke97](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mwuttke97/32/104_2.png) [@mwuttke97](https://discourse.rocq-prover.org/u/mwuttke97)\
**Post date:** [July 28, 2020, 12:38pm UTC](https://discourse.rocq-prover.org/t/notation-for-inequality-chain/979/2 "2020-07-28T12:38:21Z")

</div>

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:

```auto
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.

---

<div class="post-metadata">

**Author:** ![silene](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/silene/32/485_2.png) [@silene](https://discourse.rocq-prover.org/u/silene)\
**Post date:** [July 29, 2020, 9:16am UTC](https://discourse.rocq-prover.org/t/notation-for-inequality-chain/979/3 "2020-07-29T09:16:34Z")

</div>

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

```coq
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.

---

<div class="post-metadata">

**Author:** ![chdoc](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/chdoc/32/552_2.png) [@chdoc](https://discourse.rocq-prover.org/u/chdoc)\
**Post date:** [August 1, 2020, 12:53pm UTC](https://discourse.rocq-prover.org/t/notation-for-inequality-chain/979/4 "2020-08-01T12:53:34Z")

</div>

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

```auto
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.

---

<div class="post-metadata">

**Author:** ![herbelin](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/herbelin/32/111_2.png) [@herbelin](https://discourse.rocq-prover.org/u/herbelin)\
**Post date:** [August 24, 2020, 4:07pm UTC](https://discourse.rocq-prover.org/t/notation-for-inequality-chain/979/5 "2020-08-24T16:07:35Z")

</div>

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

```auto
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].
Admitted.

Coercion eq_true : bool >-> Sortclass.

Lemma sorted_leq_nth s (srt_s : Sorted myle s) : 
  forall i j, i <? j -> i <? length s -> j <? length s -> myle (nth i s default) (nth j s default).
Admitted.

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

Goal myle gamma Gamma.
apply (Cockayne_Hedetniemi 1 4).

```