# Misc.v: Preliminaries

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 <> yfalse = 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.

## Definition of iterator compn

compn f u n x is defined as (f (u (n-1)).. (f (u 0) x))

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

Lemma comp0 : (A:Type) (f:AAA) (x:A) (u:natA), compn f x u 0 = x.

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

## Reducing if constructs

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.

## Classical reasoning

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

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 → (AC) → (BC) → C.

Lemma orc_left : A B:Prop, Aorc A B.

Lemma orc_right : A B:Prop, Borc 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¬ BFalse) → orc A B.

Lemma class_and : A B, class Aclass Bclass (A B).

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

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

Lemma exc_intro : (A :Type)(P:AProp) (x:A), P xexc P.

Lemma class_exc : (A :Type)(P:AProp), class (exc P).

Lemma exc_intro_class : (A:Type) (P:AProp), (( 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 → (PQ) → ¬ ¬ PQ.

## Extensional equality

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

Lemma feq_refl : A B (f:AB), feq f f.

Lemma feq_sym : A B (f g : AB), feq f gfeq g f.

Lemma feq_trans : A B (f g h: AB), feq f gfeq g hfeq f h.

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

Add Parametric Relation (A B : Type) : (AB) (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.

Computational version of elimination on CompSpec

Lemma CompSpec_rect : (A : Type) (eq lt : AAProp) (x y : A)
(P : comparisonType),
(eq x yP Eq) →
(lt x yP Lt) →
(lt y xP Gt)
→ c : comparison, CompSpec eq lt x y cP c.

Decidability
Require Omega.

Lemma dec_sig_lt : P : natProp, ( x, {P x}+{ ¬ P x})
→ n, {i | i < n P i}+{ i, i < n¬ P i}.

Lemma dec_exists_lt : P : natProp, ( 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).