# Library tools

This module contains simple notations, definitions, tactics and lemmas, independant of the rest of the developpement.

Notation " [ x , y ] " := (cons (@pair _ _ x y) nil) : list_scope.
Infix "∘" := Basics.compose (at level 20).

Simple arithmetic facts.
Global Instance proper_plus_le : Proper (le ==> le ==> le) plus.
Global Instance proper_S_le : Proper (le ==> le) S.

Variation of the Bool.reflect function, for type bool+A instead of bool.
Inductive reflect3 {A : Set} (P :Prop) (Q : A Prop) (R : Prop) : bool + A Set :=
| r3_false : P reflect3 P Q R (inl false)
| r3_Some a : Q a reflect3 P Q R (inr a)
| r3_true : R reflect3 P Q R (inl true).

Section s.

# Predicates and relations.

Hypothesis T : Set.

## Relational operators.

Top relation.
Notation TTrue := (fun _ _ : TTrue).
Empty relation.
Notation FFalse := (fun _ _ : TFalse).
Relational entailment.
Definition stronger : relation (relation T) :=
fun ax1 ax2 ⇒ ( e f : T, ax1 e f ax2 e f).
Relational union.
Definition or_rel (ax1 ax2 : relation T) :=
(fun e fax1 e f ax2 e f).
Relational intersection.
Definition and_rel (p P : relation T) :=
(fun e f : Tp e f P e f).
Relational equivalence.
Definition eq_rel (P Q :relation T) := e f, P e f Q e f.

Notations.
Infix "⇒" := stronger (at level 70).
Infix "∨" := or_rel (at level 60).
Infix "∧" := and_rel (at level 40).
Infix "⇔" := eq_rel (at level 60).

## Predicates operators.

A predicate over T maps every element of T to a proposition.
Definition predicate T := T Prop.
Predicate conjunction.
Definition and_pred (A B : predicate T) (e : T) : Prop := A e B e.
Coercion from predicates to relations.
Definition rel : predicate T relation T :=
fun (A : predicate T) (e f : T) ⇒ A e A f.
Predicate equivalence.
Definition eq_pred (P Q : predicate T) := e, P e Q e.

Notations.
Infix "⊗" := and_pred (at level 60, right associativity).
Notation " A ^2 " := (rel A) (at level 65).
Infix "↔" := eq_pred (at level 60).

## General properties of the operators.

Relational entailment is a preorder.
Global Instance stronger_Preorder : PreOrder stronger.
Relational equivalence is an equivalence relation.
Global Instance eq_rel_Equivalence : Equivalence eq_rel.
Predicate equivalence is an equivalence relation.
Global Instance eq_pred_Equivalence : Equivalence eq_pred.
The relations obtained from equivalent predicates are equivalent.
Global Instance rel_eq_pred_eq_rel :
Proper (eq_pred ==> eq_rel) rel.
is a morphism for .
is a morphism for .
is a morphism for .
Global Instance or_rel_eq_rel_eq_rel_eq_rel :
Proper (eq_rel ==> eq_rel ==> eq_rel) or_rel.
is a morphism for .
is a morphism for .

## Simple tautologies.

Lemma FFalse_spec : A, FFalse A.
Lemma TTrue_spec : A, A TTrue.
Lemma or_rel_stronger_l A B : A A B.
Lemma or_rel_stronger_r A B : B A B.
Lemma assoc_or_rel1 A B C : A (B C) (A B) C.
Lemma or_and_distr {A B C} : (A B) (A C) A (B C).
Lemma and_or_distr {A B C} : A (B C) (A B) (A C).
Lemma and_stronger_l {A B} : A B B.
Lemma rel_and_pred {A B} : ((A^2) (B^2)) ((A B)^2).
End s.
Notation TTrue := (fun _ _True).
Notation FFalse := (fun _ _False).
Infix "⇒" := stronger (at level 70).
Infix "∨" := or_rel (at level 60).
Infix "∧" := and_rel (at level 40).
Infix "⇔" := eq_rel (at level 60).
Infix "⊗" := and_pred (at level 60, right associativity).
Notation " A ^2 " := (rel A) (at level 65).
Infix "↔" := eq_pred (at level 60).

## Lemmas aimed at proving that some function φ is a morphism.

Lemma proper_stronger_l {S:Set} {T} (A B:relation S) (C:relation T) φ :
B A Proper (A ==> C) φ Proper (B ==> C) φ.

Lemma proper_stronger_r {S} {T:Set} (A:relation S) (B C:relation T) φ :
B C Proper (A ==> B) φ Proper (A ==> C) φ.

Lemma proper_or_split {S:Set} {T} (A B:relation S) (C:relation T) φ :
Proper ((A B) ==> C) φ Proper (A ==> C) φ Proper (B ==> C) φ.

Lemma proper_and_split {S} {T:Set} (A:relation S) (B C:relation T) φ :
Proper (A ==> (B C)) φ Proper (A ==> B) φ Proper (A ==> C) φ.