Library enhancements

Misc stuff

This module does the importing of the Coq library and collects many results that don't really fit anywhere else. Some parts should probably put into separate files, such as the counted_list. There are also a lot of lemmas where I try to prove something just for better understanding of the intuitionistic logic of Coq.

Require Export Coq.Bool.Bool.
Require Export Arith.
Require Omega.
Require Export Coq.Lists.List.
Export ListNotations.

Definition non_empty_type(A : Type) : Prop := ∃(a : A ), True.

Definition injective{X Y : Type}(f : X → Y) : Prop :=
  ∀(x y : X), f x = f y → x = y.

Definition enumerator(X : Type) : Type := {f : nat → X | injective f}.

Definition enum_elem{X : Type}(f : enumerator X) : X := proj1_sig f 0.

Definition countably_infinite(X : Type) : Prop :=
  ∃(f : enumerator X ), True.

Definition enum_infinite{X : Type}(f : enumerator X) : countably_infinite X :=
  ex_intro _ f I.

Lemma countably_infinite_non_empty :
  ∀(X : Type)(P : Prop),
    (∀(non_empty : X), P) →
    countably_infinite X →
      P.

Recognizers for the library

Definition is_some{A : Type}(opt : option A) : Prop :=
  match opt with
    | Some _ ⇒ True
    | None ⇒ False
  end.

Definition is_none{A : Type}(opt : option A) : Prop :=
  match opt with
    | Some _ ⇒ False
    | None ⇒ True
  end.

Lemma neg_is_none : ∀(A : Type)(o : option A),
  ¬ (is_some o ) → is_none o.

Lemma option_contradiction : ∀(A : Type)(o : option A),
  is_some o → is_none o → False.

Definition is_inl{A B : Type}(ab : A + B) : Prop :=
  match ab with
    | inl _ ⇒ True
    | inr _ ⇒ False
  end.

Definition is_inr{A B : Type}(ab : A + B) : Prop :=
  match ab with
    | inl _ ⇒ False
    | inr _ ⇒ True
  end.

Definition swap_pair{A B : Type}(ab : A × B) : B × A := (snd ab , fst ab ).

Lemma split_nat_case_lt : ∀(n m : nat)(P : Prop),
  (n < m → P) → (n ≥ m → P) → P.

Lemma split_nat_case_le : ∀(n m : nat)(P : Prop),
  (n ≤ m → P) → (n > m → P) → P.

Inductive dep_and (A : Type) (B : A → Type) : Type :=
  dep_conj : ∀(a : A), B a → dep_and A B.

Notation " p # P /#\ Q " := (dep_and P (fun(p : P) ⇒ Q))
    (at level 80, right associativity) : type_scope.

Lemma iff_right : ∀{P Q : Prop}, (P ↔ Q) → P → Q.

Lemma iff_left : ∀{P Q : Prop}, (P ↔ Q) → Q → P.

Definition eq_type(A : Type) : Type := ∀(x y : A), {x = y }+{x ≠ y }.

Lemma eq_equal : ∀(A B : Type)(f : eq_type A)(a : A)(b1 b2 : B),
  (if f a a then b1 else b2 ) = b1.

Lemma eq_unequal : ∀(A B : Type)(f : eq_type A)(a1 a2 : A)(b1 b2 : B),
  a1 ≠ a2 →
    (if f a1 a2 then b1 else b2 ) = b2.

function update

Definition function_update{A B : Type}(a_eq : eq_type A)
                          (f : A → B)(a0 : A)(b0 : B) : A → B :=
   fun(a : A) ⇒
     if a_eq a a0 then b0
     else f a.

Lemma function_update_eq :
  ∀{A B : Type}(a_eq : eq_type A)(f : A → B)(a : A)(b : B),
    function_update a_eq f a b a = b.

Lemma function_update_unequal :
  ∀{A B : Type}(a_eq : eq_type A)(f : A → B)(a1 a2 : A)(b : B),
    a1 ≠ a2 →
      function_update a_eq f a1 b a2 = f a2.

Lemma function_update_twice :
  ∀{A B : Type}(a_eq : eq_type A)(f : A → B)(a0 : A)(b0 : B),
    function_update a_eq (function_update a_eq f a0 b0) a0 b0 a0 =
    function_update a_eq f a0 b0 a0.

Lemma function_update_split :
  ∀{A B : Type}(P : B → Prop)
        (a_eq : eq_type A)(f : A → B)(a a' : A)(b : B),
    (a = a' → P b) →
    (a ≠ a' → P (f a')) →
      P (function_update a_eq f a b a').

Lemma function_update_split_result :
  ∀{A B : Type}(a_eq : eq_type A)(f : A → B)(a1 a2 : A)(b1 b2 : B),
    b1 = b2 →
    f a2 = b2 →
      function_update a_eq f a1 b1 a2 = b2.

Definition fcompose{X Y Z : Type}(f : Y → Z)(g : X → Y)(x : X) : Z :=
  f(g(x)).

Lemma ge_refl : ∀(n : nat), n ≥ n.

Lemma add_minus_diag : ∀(a b : nat), a + b - b = a.

Lemma plus_minus_assoc : ∀(a b c : nat),
  b ≥ c → a + b - c = a + (b - c ).

Intuitionistic exercises

Lemma bcontrapositive : ∀{P Q : bool},
  (P = true → Q = true) →
    (negb Q = true → negb P = true).

Lemma contrapositive : ∀{P Q : Prop}, (P → Q) → (¬Q → ¬P).

Lemma neg_implies : ∀(P Q : Prop), ~(P → Q ) → (¬P → ¬Q).

Lemma neg_neg_implies : ∀(P Q : Prop), ~~(P → Q ) → (~~P → ~~Q).

Lemma iff_neg : ∀(P Q : Prop), (P ↔ Q) → (¬P ↔ ¬Q).

Lemma iff_and : ∀(P1 P2 Q1 Q2 : Prop),
  (P1 ↔ Q1) → (P2 ↔ Q2) → ((P1 ∧ P2 ) ↔ (Q1 ∧ Q2 )).

Lemma neg_double_neg : ∀{P : Prop}, P → ¬ ¬ P.

Lemma exists_not_not_implies : ∀{A : Type}{P : A → Prop},
  (∃ a : A , ¬ P a) → (¬ ∀(a : A), P a).

Lemma forall_not_iff_not_exists : ∀{A : Type}{P : A → Prop},
  (∀(a : A), ¬ P a ) ↔ (¬ ∃ a : A , P a ).

Lemma or_neg_neg_and : ∀(P Q : Prop),
  ((¬ P ) ∨ (¬ Q )) → ¬ (P ∧ Q ).

Lemma double_neg_impl_neg_or :
  ∀(P Q : Prop), (~~(P → Q )) ↔ (~~(~P ∨ Q )).

Definition dneg_or(P Q : Prop) : Prop := ¬ (~ P ∧ ¬ Q ).

Lemma dneg_or_intro : ∀(P Q : Prop), P → dneg_or P Q.

Lemma dneg_or_elim : ∀(G P Q : Prop),
  (P → G) → (Q → G) → dneg_or P Q → ¬ ¬ G.

Lemma single_prop_ax_correct : ∀(P : Prop),
  dneg_or P (¬ P).

Lemma prop_ax_down_correct : ∀(G P : Prop),
  dneg_or P (dneg_or (¬ P) G).

Lemma prop_ax_up_correct : ∀(G P : Prop),
  dneg_or P (dneg_or (¬ P) G) → True.

Lemma prop_and_down_correct : ∀(G P Q : Prop),
  dneg_or P G → dneg_or Q G → dneg_or (P ∧ Q) G.

Lemma prop_and_up_correct : ∀(G P Q : Prop),
  dneg_or (P ∧ Q) G → (dneg_or P G ) ∧ dneg_or Q G.

Lemma prop_or_down_correct : ∀(G P Q : Prop),
  dneg_or (¬ P) (dneg_or (¬ Q) G) → dneg_or (¬ (P ∧ Q )) G.

Lemma prop_or_up_correct_context : ∀(G P Q : Prop),
   dneg_or (¬ (P ∧ Q )) G → dneg_or (¬ P) (dneg_or (¬ Q) G).

Lemma prop_or_up_correct : ∀(P Q : Prop),
   (¬ (P ∧ Q )) → dneg_or (¬ P) (¬ Q).

Lemma prop_neg_down_correct : ∀(G P : Prop),
  dneg_or P G → dneg_or (¬ ¬ P) G.

Lemma prop_neg_up_correct : ∀(G P : Prop),
  dneg_or (¬ ¬ P) G → dneg_or P G.

max

Lemma max_mono_both : ∀(n1 n2 n3 n4 : nat),
n1 ≤ n3 → n2 ≤ n4 → max n1 n2 ≤ max n3 n4.

counted lists

Inductive counted_list(A : Type) : nat → Type :=
  | counted_nil : counted_list A 0
  | counted_cons : ∀(n : nat),
      A → counted_list A n → counted_list A (S n).

Implicit Arguments counted_nil [[A]].
Implicit Arguments counted_cons [A n].

Definition counted_head{A : Type}{n : nat}(l : counted_list A (S n)) : A :=
  match l in (counted_list _ n')
          return (match n' return Type with
                    | 0 ⇒ nat
                    | S _ ⇒ A
                  end)
  with
    | counted_nil ⇒ 0
    | counted_cons _ a _ ⇒ a
  end.

Fixpoint counted_map{A B : Type}{n : nat}(f : A → B)(al : counted_list A n) :
                                                           counted_list B n :=
  match al with
    | counted_nil ⇒ counted_nil
    | counted_cons n a al ⇒ counted_cons (f a) (counted_map f al)
  end.

Fixpoint list_of_counted_list{A : Type}{n : nat}(l : counted_list A n) :
                                                                      list A :=
  match l with
    | counted_nil ⇒ []
    | counted_cons n a l ⇒ a :: (list_of_counted_list l )
  end.

Lemma list_of_counted_list_map :
  ∀(A B : Type)(n : nat)(f : A → B)(al : counted_list A n),
    list_of_counted_list (counted_map f al) = map f (list_of_counted_list al).

Lemma length_list_of_counted_list :
  ∀(A : Type)(n : nat)(l : counted_list A n),
    length (list_of_counted_list l) = n.

Lemma less_length_counted_list :
  ∀{A : Type}(i n : nat)(l : counted_list A n),
    i < n → i < length (list_of_counted_list l).

Lemma counted_list_eta : ∀{A : Type}{n : nat}(l : counted_list A n),
  match n return counted_list A n → Prop with
    | 0 ⇒ fun(l : counted_list A 0) ⇒ l = counted_nil
    | S n ⇒ fun(l : counted_list A (S n)) ⇒
      ∃(a : A)(tl : counted_list A n ), l = counted_cons a tl
  end l.

Lemma counted_list_eta_1 : ∀{A : Type}(l : counted_list A 1),
  ∃(a : A ), l = counted_cons a counted_nil.

Lemma counted_0_destruction :
  ∀(A : Type)(P : counted_list A 0 → Prop)(v : counted_list A 0),
    P counted_nil →
      P v.

Lemma counted_list_equal :
  ∀{A : Type}{n : nat}(l1 l2 : counted_list A n),
    list_of_counted_list l1 = list_of_counted_list l2 →
      l1 = l2.