# Library rt.util.notation

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

(* Here we define a more verbose notation for projections of pairs... *)
Section Pair.

Context {A B: Type}.
Variable p: A × B.
Definition pair_1st := fst p.
Definition pair_2nd := snd p.

End Pair.

(* ...and triples. *)
Section Triple.

Context {A B C: Type}.
Variable p: A × B × C.
Definition triple_1st (p: A × B × C) := fst (fst p).
Definition triple_2nd := snd (fst p).
Definition triple_3rd := snd p.

End Triple.

(* Define a wrapper from an element to a singleton list. *)
Definition make_sequence {T: Type} (opt: option T) :=
match opt with
| Some j[:: j]
| None[::]
end.

(* Next we define a notation for the big concatenation operator.*)

Reserved Notation "\cat_ ( m <= i < n ) F"
(at level 41, F at level 41, i, m, n at level 50,
format "'[' \cat_ ( m <= i < n ) '/ ' F ']'").

Notation "\cat_ ( m <= i < n ) F" :=
(\big[cat/[::]]_(m i < n) F%N) : nat_scope.

Reserved Notation "\cat_ ( m <= i < n | P ) F"
(at level 41, F at level 41, P at level 41, i, m, n at level 50,
format "'[' \cat_ ( m <= i < n | P ) '/ ' F ']'").

Notation "\cat_ ( m <= i < n | P ) F" :=
(\big[cat/[::]]_(m i < n | P) F%N) : nat_scope.

Reserved Notation "\cat_ ( i < n ) F"
(at level 41, F at level 41, i, n at level 50,
format "'[' \cat_ ( i < n ) '/ ' F ']'").

Notation "\cat_ ( i < n ) F" :=
(\big[cat/[::]]_(i < n) F%N) : nat_scope.

Reserved Notation "\cat_ ( i < n | P ) F"
(at level 41, F at level 41, i, n at level 50,
format "'[' \cat_ ( i < n | P ) '/ ' F ']'").

Notation "\cat_ ( i < n | P ) F" :=
(\big[cat/[::]]_(i < n | P) F%N) : nat_scope.

(* Let's define big operators for lists of pairs. *)

Reserved Notation "\sum_ ( ( m , n ) <- r ) F"
(at level 41, F at level 41, m, n at level 50,
format "'[' \sum_ ( ( m , n ) <- r ) '/ ' F ']'").

Notation "\sum_ ( ( m , n ) <- r ) F" :=
(\sum_(i <- r) (let '(m,n) := i in F)) : nat_scope.

Reserved Notation "\sum_ ( ( m , n ) <- r | P ) F"
(at level 41, F at level 30, P at level 41, m, n at level 50,
format "'[' \sum_ ( ( m , n ) <- r | P ) '/ ' F ']'").

Notation "\sum_ ( ( m , n ) <- r | P ) F" :=
(\sum_(i <- r | (let '(m,n) := i in P))
(let '(m,n) := i in F)) : nat_scope.

Reserved Notation "\max_ ( ( m , n ) <- r ) F"
(at level 41, F at level 41, m, n at level 50,
format "'[' \max_ ( ( m , n ) <- r ) '/ ' F ']'").

Notation "\max_ ( ( m , n ) <- r ) F" :=
(\max_(i <- r) (let '(m,n) := i in F)) : nat_scope.

Reserved Notation "\max_ ( ( m , n ) <- r | P ) F"
(at level 41, F at level 30, P at level 41, m, n at level 50,
format "'[' \max_ ( ( m , n ) <- r | P ) '/ ' F ']'").

Notation "\max_ ( ( m , n ) <- r | P ) F" :=
(\max_(i <- r | (let '(m,n) := i in P))
(let '(m,n) := i in F)) : nat_scope.

Notation "[ 'seq' ( x , y ) <- s | C ]" :=
(filter (fun ilet '(x,y) := i in C%B) s)
(at level 0, x at level 99,
format "[ '[hv' 'seq' ( x , y ) <- s '/ ' | C ] ']'") : seq_scope.

(* In case we use an (option list T), we can define membership
without having to match the option type. *)

Reserved Notation "x \In A"
(at level 70, format "'[hv' x '/ ' \In A ']'", no associativity).
Notation "x \In A" :=
(if A is Some B then in_mem x (mem B) else false) : bool_scope.