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