Library paraphernalia
The Paraphernalia library contains general definitions and lemmas which are
important across the entire project
Require Import Arith Bool List.
Require Export Arith Bool List.
Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.
Operator for equality predicate beq_nat, defined for peano natural numbers
Notation "A =n= B" :=
(beq_nat A B) (at level 70, right associativity).
(beq_nat A B) (at level 70, right associativity).
Lemma to unfold beq_nat
Lemma fold_unfold_beq_nat_Sn_Sm:
forall (n m : nat),
beq_nat (S n) (S m) = beq_nat n m.
forall (n m : nat),
beq_nat (S n) (S m) = beq_nat n m.
Lemma to prove the symmetric property of the =n= operator
Lemma beq_nat_symm:
forall (x y : nat),
(x =n= y) = (y =n= x).
forall (x y : nat),
(x =n= y) = (y =n= x).
Lemma to assert trivial equalities
Lemma trivial_equality:
forall (A : Type)
(v : A),
v = v.
forall (A : Type)
(v : A),
v = v.
Defining an operator for equality of boolean values
Notation "A =b= B" :=
(eqb A B) (at level 70, right associativity).
(eqb A B) (at level 70, right associativity).
Lemmas For Peano Natural Numbers
Lemma succ_eq:
forall (a b : nat),
S a = S b -> a = b.
forall (a b : nat),
S a = S b -> a = b.
Lemma to show that adding some value to equal natural numbers results in
equal natural number
Lemma add_to_both_sides:
forall (x y z : nat),
x = y -> x + z = y + z.
forall (x y z : nat),
x = y -> x + z = y + z.
Lemma to unfold minus for the successor of some natural number and 0
Lemma minus_Sn_0:
forall (n : nat),
S n - 0 = S n.
forall (n : nat),
S n - 0 = S n.
Lemma to unfold minus for the successors of two natural numbers
Lemma minus_Sn_Sm:
forall (n m : nat),
S n - S m = n - m.
forall (n m : nat),
S n - S m = n - m.
Lemma to show that subtracting 0 from a natural number gives the same number
Lemma minus_n_0:
forall (n : nat),
n - 0 = n.
forall (n : nat),
n - 0 = n.
Defining Ordered Types
Inductive element_comparison :=
| Lt : element_comparison
| Eq : element_comparison
| Gt : element_comparison.
| Lt : element_comparison
| Eq : element_comparison
| Gt : element_comparison.
Predicate to check if a value of type element_comparison is an Lt or an Eq;
we use this to define a total order
Definition leq (ce : element_comparison) : bool :=
match ce with
| Lt =>
true
| Eq =>
true
| Gt =>
false
end.
match ce with
| Lt =>
true
| Eq =>
true
| Gt =>
false
end.
Axiom requiring comparison functions defined for some type A to map to
Eq if and only if the values being compared are equal
Axiom relating_Eq_eq:
forall (A : Type)
(a b : A)
(compare : A -> A -> element_comparison),
compare a b = Eq <-> a = b.
forall (A : Type)
(a b : A)
(compare : A -> A -> element_comparison),
compare a b = Eq <-> a = b.
Definition of anti-symmetric property for comparison functions
Definition anti_symmetry
(A : Type)
(compare : A -> A -> element_comparison) :=
forall (a b : A),
leq (compare a b) = true ->
leq (compare b a) = true ->
compare a b = Eq.
(A : Type)
(compare : A -> A -> element_comparison) :=
forall (a b : A),
leq (compare a b) = true ->
leq (compare b a) = true ->
compare a b = Eq.
Defintion of transitive property for comparison functions
Definition transitivity
(A : Type)
(compare : A -> A -> element_comparison) :=
forall (a b c : A),
leq (compare a b) = true ->
leq (compare b c) = true ->
leq (compare a c) = true.
(A : Type)
(compare : A -> A -> element_comparison) :=
forall (a b c : A),
leq (compare a b) = true ->
leq (compare b c) = true ->
leq (compare a c) = true.
Defintion of connexity property for comparison functions
Definition connexity
(A : Type)
(compare : A -> A -> element_comparison) :=
forall (a b : A),
(leq (compare a b) = true)
\/
(leq (compare b a) = true).
(A : Type)
(compare : A -> A -> element_comparison) :=
forall (a b : A),
(leq (compare a b) = true)
\/
(leq (compare b a) = true).
Specifiction of a comparison function to define a total order on the set whose
elements the function compares
Definition specification_of_compare_defining_total_order
(A : Type)
(compare : A -> A -> element_comparison) :=
anti_symmetry A compare
/\
transitivity A compare
/\
connexity A compare.
(A : Type)
(compare : A -> A -> element_comparison) :=
anti_symmetry A compare
/\
transitivity A compare
/\
connexity A compare.
For some relation R defined on some set A, the reflexive property states
that for all x in A, it must be the case that (x R x). This lemma shows
that if a comparison function defines a total order on some type A, then it
also has the property of reflexivity
Lemma reflexivity_total_order:
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A),
specification_of_compare_defining_total_order A compare ->
leq (compare x x) = true.
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A),
specification_of_compare_defining_total_order A compare ->
leq (compare x x) = true.
Lemma relating the Lt and Gt constructors for a comparison function which
defines a total order
Lemma relating_Lt_Gt_total_order:
forall (A : Type)
(compare : A -> A -> element_comparison)
(a b : A),
specification_of_compare_defining_total_order A compare ->
(compare a b = Lt <-> compare b a = Gt).
forall (A : Type)
(compare : A -> A -> element_comparison)
(a b : A),
specification_of_compare_defining_total_order A compare ->
(compare a b = Lt <-> compare b a = Gt).
Definition of comparison function over Coq's Peano natural numbers
Definition compare_int (i j : nat) : element_comparison :=
if i <? j then Lt else if i =n= j then Eq else Gt.
if i <? j then Lt else if i =n= j then Eq else Gt.
Theorem to show that compare_int defines a total order over nat
Theorem compare_int_defines_a_total_order:
specification_of_compare_defining_total_order nat compare_int.
specification_of_compare_defining_total_order nat compare_int.
Pairwise and Option Type Equalities
Lemma pairwise_equality:
forall (A : Type)
(x1 x2 y1 y2 : A),
(x1, x2) = (y1, y2) <-> x1 = y1 /\ x2 = y2.
forall (A : Type)
(x1 x2 y1 y2 : A),
(x1, x2) = (y1, y2) <-> x1 = y1 /\ x2 = y2.
Lemma to show that the equality of two values of the option type is equivalent
to the equality of the values contained by the option type values
Lemma some_x_equal_some_y:
forall (A : Type)
(x y : A),
Some x = Some y <-> x = y.
forall (A : Type)
(x y : A),
Some x = Some y <-> x = y.
Lemmas for max
Lemma max_cases:
forall (a b : nat),
max a b = a \/ max a b = b.
forall (a b : nat),
max a b = a \/ max a b = b.
Lemma to unfold max the successors of two natural numbers
Lemma fold_unfold_max_Sn_Sm:
forall (n m : nat),
max (S n) (S m) = S (max n m).
forall (n m : nat),
max (S n) (S m) = S (max n m).
Lemma to show that given a value of type nat and its successor, the latter is
always the maximum value
Lemma H_max_S:
forall (a : nat),
max (a + 1) a = a + 1.
forall (a : nat),
max (a + 1) a = a + 1.
Lemma prop_to_bool_helper:
forall (a : nat),
a = a -> ((a =n= a) = true).
forall (a : nat),
a = a -> ((a =n= a) = true).
Lemma to relate = and =n= for different nat values
Lemma prop_to_bool:
forall (a b : nat),
a = b -> ((a =n= b) = true).
forall (a b : nat),
a = b -> ((a =n= b) = true).
Lemma to relate || and \/
Lemma disjunction_to_prop:
forall (b1 b2 : bool),
(b1 || b2 = true) -> (b1 = true) \/ (b2 = true).
forall (b1 b2 : bool),
(b1 || b2 = true) -> (b1 = true) \/ (b2 = true).