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.


Operators and Unfolding

Tactic to prove fold unfold lemmas
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).

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.

Lemma to prove the symmetric property of the =n= operator
Lemma beq_nat_symm:
  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.

Defining an operator for equality of boolean values
Notation "A =b= B" :=
  (eqb A B) (at level 70, right associativity).



Lemmas For Peano Natural Numbers

Lemma to show that the equality the successors of two natural numbers implies the equality of the two natural number
Lemma succ_eq:
  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.

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.

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.

Lemma to show that subtracting 0 from a natural number gives the same number
Lemma minus_n_0:
  forall (n : nat),
    n - 0 = n.



Defining Ordered Types

A relation R defines a total order on a set A iff for some x, y, z in A:
(1) (x R y) /\ (<y R x) => x = y (Anti-symmtery)
(2) (x R y) /\ (y R z) => (x R z) (Transitivity)
(3) (x R y) \/ (y R x) (Connexity)
In this project, such a relation is captured through comparison functions of type A -> A -> element_comparison. This section defines a specification for comparison functions to define a total ordering on the type whose elements it compares
Type alias for the predefined inductive type comparison
Inductive 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.

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.

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.

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.

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

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.

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.

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

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.

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.



Pairwise and Option Type Equalities

Lemma to show that the equality of a pair of values is equivalent to the equality of the corresponding elements of each pair
Lemma pairwise_equality:
  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.



Lemmas for max

Lemma to show that for two values of type nat, one or the other must be the maximum values
Lemma max_cases:
  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).

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.



Reflections

Lemma to relate = and =n= for the same nat values
Lemma prop_to_bool_helper:
  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).

Lemma to relate || and \/
Lemma disjunction_to_prop:
  forall (b1 b2 : bool),
    (b1 || b2 = true) -> (b1 = true) \/ (b2 = true).