Set Implicit Arguments.
Require Export Arith.
Require Import Coq.Classes.SetoidTactics.
Require Import Coq.Classes.SetoidClass.
Require Import Coq.Classes.Morphisms.

Open Local Scope signature_scope.

Lemma beq_nat_neq: ∀ x y : nat, x <> y → false = beq_nat x y.

Lemma if_beq_nat_nat_eq_dec : ∀ A (x y:nat) (a b:A),
  (if beq_nat x y then a else b) = if eq_nat_dec x y then a else b.

Definition ifte A (test:bool) (thn els:A) := if test then thn else els.

Add Parametric Morphism (A:Type) : (@ifte A)
  with signature (eq ⇒eq ⇒ eq ⇒ eq) as ifte_morphism1.

Add Parametric Morphism (A:Type) x : (@ifte A x)
  with signature (eq ⇒ eq ⇒ eq) as ifte_morphism2.

Add Parametric Morphism (A:Type) x y : (@ifte A x y)
  with signature (eq ⇒ eq) as ifte_morphism3.

Fixpoint compn (A:Type)(f:A → A → A) (x:A) (u:nat → A) (n:nat) {struct n}: A :=
   match n with O ⇒ x | (S p) ⇒ f (u p) (compn f x u p) end.

Lemma comp0 : ∀ (A:Type) (f:A → A → A) (x:A) (u:nat → A), compn f x u 0 = x.

Lemma compS : ∀ (A:Type) (f:A → A → A) (x:A) (u:nat → A) (n:nat),
              compn f x u (S n) = f (u n) (compn f x u n).

Lemma if_then : ∀ (P:Prop) (b:{ P }+{ ¬ P })(A:Type)(p q:A),
      P → (if b then p else q) = p.

Lemma if_else : ∀ (P :Prop) (b:{ P }+{ ¬ P })(A:Type)(p q:A),
      ¬P → (if b then p else q) = q.

Lemma if_then_not : ∀ (P Q:Prop) (b:{ P }+{ Q })(A:Type)(p q:A),
      ¬ Q → (if b then p else q) = p.

Lemma if_else_not : ∀ (P Q:Prop) (b:{ P }+{ Q })(A:Type)(p q:A),
      ¬P → (if b then p else q) = q.

Definition class (A:Prop) := ¬ ¬ A → A.

Lemma class_neg : ∀ A:Prop, class ( ¬ A).

Lemma class_false : class False.
Hint Resolve class_neg class_false.

Definition orc (A B:Prop) := ∀ C:Prop, class C → (A → C) → (B → C) → C.

Lemma orc_left : ∀ A B:Prop, A → orc A B.

Lemma orc_right : ∀ A B:Prop, B → orc A B.

Hint Resolve orc_left orc_right.

Lemma class_orc : ∀ A B, class (orc A B).

Implicit Arguments class_orc [].

Lemma orc_intro : ∀ A B, ( ¬ A → ¬ B → False) → orc A B.

Lemma class_and : ∀ A B, class A → class B → class (A ∧ B).

Lemma excluded_middle : ∀ A, orc A ( ¬ A).

Definition exc (A :Type)(P:A → Prop) :=
   ∀ C:Prop, class C → (∀ x:A, P x → C) → C.

Lemma exc_intro : ∀ (A :Type)(P:A → Prop) (x:A), P x → exc P.

Lemma class_exc : ∀ (A :Type)(P:A → Prop), class (exc P).

Lemma exc_intro_class : ∀ (A:Type) (P:A → Prop), ((∀ x, ¬ P x) → False) → exc P.

Lemma not_and_elim_left : ∀ A B, ¬ (A ∧ B) → A → ¬B.

Lemma not_and_elim_right : ∀ A B, ¬ (A ∧ B) → B → ¬A.

Hint Resolve class_orc class_and class_exc excluded_middle.

Lemma class_double_neg : ∀ P Q: Prop, class Q → (P → Q) → ¬ ¬ P → Q.

Definition feq A B (f g : A → B) := ∀ x, f x = g x.

Lemma feq_refl : ∀ A B (f:A→B), feq f f.

Lemma feq_sym : ∀ A B (f g : A → B), feq f g → feq g f.

Lemma feq_trans : ∀ A B (f g h: A → B), feq f g → feq g h → feq f h.

Hint Resolve feq_refl.
Hint Immediate feq_sym.
Hint Unfold feq.

Add Parametric Relation (A B : Type) : (A → B) (feq (A:=A) (B:=B))
  reflexivity proved by (feq_refl (A:=A) (B:=B))
  symmetry proved by (feq_sym (A:=A) (B:=B))
  transitivity proved by (feq_trans (A:=A) (B:=B))
as feq_rel.

Lemma CompSpec_rect : ∀ (A : Type) (eq lt : A → A → Prop) (x y : A)
       (P : comparison → Type),
       (eq x y → P Eq) →
       (lt x y → P Lt) →
       (lt y x → P Gt)
    → ∀ c : comparison, CompSpec eq lt x y c → P c.

Require Omega.

Lemma dec_sig_lt : ∀ P : nat → Prop, (∀ x, {P x}+{ ¬ P x})
  → ∀ n, {i | i < n ∧ P i}+{∀ i, i < n → ¬ P i}.

Lemma dec_exists_lt : ∀ P : nat → Prop, (∀ x, {P x}+{ ¬ P x})
  → ∀ n, {exists i, i < n ∧ P i}+{¬ exists i, i < n ∧ P i}.

Definition eq_nat2_dec : ∀ p q : nat*nat, { p=q }+{¬ p=q }.
Defined.

Lemma nat_compare_specT
   : ∀ x y : nat, CompareSpecT (x = y) (x < y)%nat (y < x)%nat (nat_compare x y).