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 _ _ : T ⇒ True).

Empty relation.

Notation FFalse := (fun _ _ : T ⇒ False).

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 f ⇒ ax1 e f ∨ ax2 e f).

Relational intersection.

Definition and_rel (p P : relation T) :=
(fun e f : T ⇒ p 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 ↔.

Global Instance and_pred_eq_pred_eq_pred_eq_pred :
Proper (eq_pred ==> eq_pred ==> eq_pred) and_pred.

∧ is a morphism for ⇔.

Global Instance and_rel_eq_rel_eq_rel_eq_rel :
Proper (eq_rel ==> eq_rel ==> eq_rel) and_rel.

∨ 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 ⇒.

Global Instance and_rel_stronger_stronger_stronger :
Proper (stronger ==> stronger ==> stronger) and_rel.

∨ is a morphism for ⇒.

Global Instance or_rel_stronger_stronger_stronger :
Proper (stronger ==> stronger ==> stronger) or_rel.

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