Notation for inequality chain

Using Coq
1

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.

Many thanks in advance!
Yannick

2

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.

3

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.

4

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.

5

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].
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).