# Library UsefulTypes

Require Export Coq.Init.Notations.
Require Export tactics.
Require Export Peano.
Require Export Basics.
Require Export Bool.
Require Export Arith.
Require Export Arith.EqNat.
Require Omega.

Notation "{ a , b : T \$ P }" :=
{a : T \$ {b : T \$ P}}
(at level 0, a at level 99, b at level 99).
Notation "{ a , b , c : T \$ P }" :=
{a : T \$ {b : T \$ {c : T \$ P}}}
(at level 0, a at level 99, b at level 99, c at level 99).
Notation "{ a , b , c , d : T \$ P }" :=
{a : T \$ {b : T \$ {c : T \$ {d : T \$ P}}}}
(at level 0, a at level 99, b at level 99, c at level 99, d at level 99).
Notation "{ a , b , c , d , e : T \$ P }" :=
{a : T \$ {b : T \$ {c : T \$ {d : T \$ {e : T \$ P}}}}}
(at level 0, a at level 99, b at level 99, c at level 99, d at level 99, e at level 99).
Notation "{ a , b , c , d , e , f : T \$ P }" :=
{a : T \$ {b : T \$ {c : T \$ {d : T \$ {e : T \$ {f : T \$ P}}}}}}
(at level 0, a at level 99, b at level 99, c at level 99, d at level 99, e at level 99, f at level 99).

Notation "[ x , .. , y ]" := (cons x .. (cons y []) ..).

Theorem beq_nat_sym :
(n m : nat),
beq_nat n m = beq_nat m n.
Proof.
induction n; sp.
unfold beq_nat; destruct m; sp.
simpl; destruct m; simpl; sp.
Qed.

Definition Deq (T : Type) := (x y : T), {x = y} + {x y}.

Lemma deq_prod :
(A B : Type), Deq ADeq BDeq (A × B).
Proof.
unfold Deq; introv da db; introv; sp.
generalize (da x0 y0) (db x y); introv ea eb; sp; subst; sp;
right; intro k; inversion k; sp.
Defined.

Hint Resolve deq_prod : Deq.

Definition assert (b : bool) : Prop := b = true.

Lemma fold_assert :
b,
(b = true) = assert b.
Proof.
unfold assert; auto.
Qed.

Lemma assert_orb :
a b,
assert (a || b) → assert a + assert b.
Proof.
destruct a; destruct b; sp.
Qed.

Lemma assert_andb :
a b,
assert (a && b) assert a assert b.
Proof.
destruct a; destruct b; sp; split; sp.
Qed.

Lemma assert_of_andb :
a b,
assert (a && b) <=> assert a # assert b.
Proof.
destruct a; destruct b; sp; split; sp.
Qed.

Lemma not_assert :
b, b = false ¬ assert b.
Proof.
destruct b; unfold assert; simpl; split; sp.
Qed.

Lemma not_of_assert :
b, b = false <=> ! assert b.
Proof.
destruct b; unfold assert; simpl; split; sp.
Qed.

Lemma andb_true :
a b,
a && b = true a = true b = true.
Proof.
destruct a; destruct b; simpl; sp; split; sp.
Qed.

Lemma andb_eq_true :
a b,
a && b = true <=> a = true # b = true.
Proof.
destruct a; destruct b; simpl; sp; split; sp.
Qed.

Lemma max_prop1 :
a b, a max a b.
Proof.
induction a; simpl; sp; try omega.
destruct b; auto.
assert (a max a b); auto; omega.
Qed.

Lemma max_prop2 :
a b, b max a b.
Proof.
induction a; simpl; sp; try omega.
destruct b; auto; try omega.
assert (b max a b); auto; omega.
Qed.

Lemma max_or :
a b,
(max a b = a) (max a b = b).
Proof.
induction a; simpl; sp; try omega.
destruct b; auto.
assert (max a b = a max a b = b) by apply IHa; sp.
Qed.

Theorem comp_ind:
P: natProp,
( n: nat, ( m: nat, m < nP m) → P n)
→ n:nat, P n.
Proof.
intros P H n.
assert ( n:nat , m:nat, m < nP m).
intro n0. induction n0 as [| n']; intros.
inversion H0.
apply le_S_n in H0.
apply le_lt_or_eq in H0.
sp; subst; sp.
apply H0 with (n := S n).
auto.
Qed.

Theorem comp_ind_type :
P: natType,
( n: nat, ( m: nat, m < nP m) → P n)
→ n:nat, P n.
Proof.
intros P H n.
assert ( n:nat , m:nat, m < nP m).
intro n0. induction n0 as [| n']; intros.
omega.
destruct (eq_nat_dec m n'); subst; auto.
apply IHn'; omega.
apply H; apply X.
Defined.

Lemma trivial_if :
T,
b : bool,
t : T,
(if b then t else t) = t.
Proof.
intros; destruct b; auto.
Qed.

Hint Rewrite trivial_if.

Lemma minus0 :
n, n - 0 = n.
Proof.
destruct n; auto.
Qed.

Lemma pair_inj :
A B,
a c : A,
b d : B,
(a, b) = (c, d)a = c b = d.
Proof.
sp; inversion H; sp.
Qed.

Lemma S_inj :
a b, S a = S ba = b.
Proof.
auto.
Qed.

Lemma S_le_inj :
a b, S a S ba b.
Proof.
sp; omega.
Qed.

Lemma S_lt_inj :
a b, S a < S ba < b.
Proof.
sp; omega.
Qed.

Lemma not_or :
a b,
¬ (a b)¬ a ¬ b.
Proof.
sp; apply H; sp.
Qed.

Lemma not_over_or :
a b,
!(a [+] b) <=> !a # !b.
Proof.
sp; split; sp.
Qed.

Theorem apply_eq :
{A B} (f: AB) {a1 a2:A},
a1 = a2f a1 = f a2.
Proof. intros. rewrite H. reflexivity.
Qed.

Theorem iff_push_down_forall : A (P Q: AProp) ,
( a, P a <=> Q a) → (( a, P a) <=> ( a, Q a)).
Proof. introv Hiff. repeat split; intros; apply Hiff; auto.
Qed.

Theorem iff_push_down_forallT : A (P Q: A[univ]) ,
( a, P a <=> Q a) → (( a, P a) <=> ( a, Q a)).
Proof. introv Hiff. repeat split; intros; apply Hiff; auto.
Qed.

Theorem iff_push_down_impliesT : P Q R,
(R → (P <=> Q)) → ((RP) <=> (RQ)).
Proof. introv Hiff. repeat split; intros; apply Hiff; auto.
Qed.

Lemma sum_assoc :
a b c,
(a [+] (b [+] c)) <=> ((a [+] b) [+] c).
Proof.
sp; split; sp.
Qed.

Definition isInl {A B : Type}
(d : A + B) : bool :=
match d with
| inl _true
| inr _false
end.

Definition isInr {A B : Type}
(d : A + B) : bool :=
match d with
| inl _false
| inr _true
end.

Definition isInlInl {A B C D: Type}
(d : (A + B) + (C + D)) : bool :=
match d with
| inl (inl _) ⇒ true
| _false
end.

Definition liftNth {A: Type}
(f : Abool) (l : list A ) (n:nat) : bool :=
match (nth_error l n) with
| Some xf x
| Nonefalse
end.

Definition liftInl {A B : Type}
(f : Abool) (d : A + B) : bool :=
match d with
| inl af a
| inr _false
end.

Notation deq_nat := NPeano.Nat.eq_dec.
Hint Resolve NPeano.Nat.eq_dec : Deq.

Definition eq_existsT (A : Type)
(B : AType)
(a a' : A)
(b : B a)
(b' : B a')
(ea : a = a')
(eb : match ea in _ = a' return B a' with eq_reflb end = b')
: existT B a b = existT B a' b'
:= match ea as ea
in _ = a'
return b' : B a',
match ea in _ = a' return B a' with eq_reflb end = b'
→ existT B a b = existT B a' b'
with
| eq_reflfun b' ebmatch eb with eq_refleq_refl (existT B a b) end
end b' eb.

Lemma dep_pair_eq :
{T : Type} {a b : T} (eq : a = b) (P : TProp) (pa : P a) (pb : P b),
@eq_rect T a P pa b eq = pb
→ exist P a pa = exist P b pb.
Proof.
intros.
rewrite <- H.
rewrite <- eq.
reflexivity.
Qed.

Ltac apply_tiff_f H1 H2 :=
let H3 := fresh in (
(pose proof (fst (H1) H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
(pose proof (fst(H1 _) H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
(pose proof (fst(H1 _ _) H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
(pose proof (fst(H1 _ _ _) H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
(pose proof (fst(H1 _ _ _ _) H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
(pose proof (fst(H1 _ _ _ _ _) H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
(pose proof (fst(H1 _ _ _ _ _ _) H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
(pose proof (fst(H1 _ _ _ _ _ _ _) H2) as H3; clear H2; pose proof H3 as H2; clear H3)).

Ltac apply_tiff_b H1 H2 :=
let H3 := fresh in (
(pose proof (snd (H1) H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
(pose proof (snd(H1 _) H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
(pose proof (snd(H1 _ _) H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
(pose proof (snd(H1 _ _ _) H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
(pose proof (snd(H1 _ _ _ _) H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
(pose proof (snd(H1 _ _ _ _ _) H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
(pose proof (snd(H1 _ _ _ _ _ _) H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
(pose proof (snd(H1 _ _ _ _ _ _ _) H2) as H3; clear H2; pose proof H3 as H2; clear H3)).

Tactic Notation "apply_tiff" constr(H1) constr(H2) :=
(apply_tiff_f H1 H2 || apply_tiff_b H1 H2) .

Tactic Notation "refl" := reflexivity.

Theorem and_tiff_compat_l:
A B C : [univ], (B <=> C) → (A # B <=> A # C).
Proof.
introv Hiff. rw Hiff. apply t_iff_refl.
Qed.

Definition transport {T:Type} {a b:T} {P:TType} (eq:a=b) (pa: P a) : (P b):=
@eq_rect T a P pa b eq.

Definition typeCast {A B:Type} (eq:A=B) (pa: A) : (B):=
@eq_rect Type A (fun XX) pa B eq.

Definition injective_fun {A B: Type} (f: AB) :=
(a1 a2: A), (f a1= f a2) → a1=a2.

Lemma min_eq : n1 n2,
n1=n2min n1 n2 = n2.
Proof.
introv H. rewrite H.
apply Min.min_idempotent.
Qed.

Lemma negb_eq_true :
b, negb b = true <=> ! (assert b).
Proof.
intro.
unfold assert; destruct b; simpl; split; sp.
Qed.

Definition left_identity {S T : Type} (f: ST) (g: TS): Type :=
s: S , (g (f s)) = s.

Definition bijection {S T : Type} (f: ST) (g: TS) : Type
:= prod (left_identity f g) (left_identity g f).

Definition injection {S T : Type} (f: ST) :=
(s1 s2 : S), (f s1 = f s2) → s1=s2.

Lemma left_id_injection: {S T : Type} (f: ST) (g: TS),
left_identity f ginjection f.
Proof.
introv lid feq.
apply_eq g feq ffeq.
rw lid in ffeq.
rw lid in ffeq.
trivial.
Qed.

Definition equipollent (A B : Type)
:= {f : AB \$ { g : BA \$ bijection f g }}.

constructive defn. of surjection -- it gives the right inverse for free. classical one may be obtained by changing sig to ex
Definition Csurjection {S T : Type} (f: ST) :=
(t : T), {s : S \$ f s =t}.

Lemma injection_surjection_equipollent
: {S T : Type} (f: ST) ,
injection f
→ Csurjection f
→ equipollent S T.
Proof.
Abort.
http://cstheory.stackexchange.com/questions/18962/formalizing-the-theory-of-finite-sets-in-type-theory
Definition Fin (n:nat)
:= {m:nat & if lt_dec m n then unit else void}.

Lemma Fin_eq:
(n: nat) (fa fb : Fin n),
(projT1 fa) = (projT1 fb)
→ fa = fb.
Proof.
introv Heq.
destruct fa as [a ap].
destruct fb as [b bp].
allsimpl.
subst.
apply eq_existsT with (ea := eq_refl).
remember (lt_dec b n); destruct s; destruct ap, bp; auto.
Qed.

Lemma Fin_decidable : (n:nat), Deq (Fin n).
Proof.
unfold Deq.
intros.
destruct (NPeano.Nat.eq_dec (projT1 x) (projT1 y)) as [T|F];[left|right].
- apply Fin_eq; auto.
- intro Heq. destruct F. destruct x. destruct y.
inverts Heq. allsimpl. reflexivity.
Defined.

Hint Resolve Fin_decidable : Deq.

Lemma equipollent_Deq : (A B:Type),
Deq A
→ equipollent A B
→ Deq B.
Proof.
unfold Deq, equipollent, bijection.
introv Ha Heq. intros. exrepnd.
pose proof (Ha (g x) (g y)) as Hd.
dorn Hd; [left| right].
- apply left_id_injection in Heq1.
repnud Heq1. auto.
- introv Heq. apply Hd. f_equal; auto.
Qed.

Hint Resolve equipollent_Deq : Deq.

Lemma bool2_Equi :
equipollent bool (Fin 2).
Abort.

This is a strong constructive version of finiteness of a type. It says that there should be a bijection between some finite initial segment of numbers and that type
Definition Finite (T : Type) :=
{n:nat \$ equipollent ( Fin n) T}.

Lemma Finite_Deq : (A:Type),
Finite A
→ Deq A.
Proof.
introv Hf.
repnud Hf. exrepnd.
eapply equipollent_Deq.
apply Fin_decidable.
exact Hf0.
Qed.

Hint Resolve Finite_Deq : Deq.

Lemma prod_assoc :
a b c,
(a # b) # c <=> a # (b # c).
Proof.
sp; split; sp.
Qed.

Lemma prod_comm :
a b,
a # b <=> b # a.
Proof.
sp; split; sp.
Qed.

Lemma or_true_l :
t, True [+] t <=> True.
Proof. sp. Qed.

Lemma or_true_r :
t, t [+] True <=> True.
Proof. sp. Qed.

Lemma or_false_r : t, t [+] False <=> t.
Proof. sp; split; sp. Qed.

Lemma or_false_l : t, False [+] t <=> t.
Proof. sp; split; sp. Qed.

Lemma and_true_l :
t, True # t <=> t.
Proof. sp; split; sp. Qed.

Lemma not_false_is_true : !False <=> True.
Proof. sp; split; sp. Qed.

Lemma forall_num_lt_d : m P,
( n, n < S mP n)
→ P 0 # ( n, n < mP (S n) ).
Proof.
introv Hlt.
dimp (Hlt 0); auto; [omega|].
dands; auto.
introv Hgt.
apply lt_n_S in Hgt.
eauto.
Qed.
Ltac dforall_lt_hyp name :=
repeat match goal with
[ H : n : nat , n< S ?m → ?C |- _ ] ⇒
apply forall_num_lt_d in H;
let Hyp := fresh name in
destruct H as [Hyp H]
| [ H : x : ?T , _ < 0 → _ |- _ ] ⇒ clear H
end.

Definition decidable (P: [univ]):= (P + (!P))%type.

Lemma decidable_prod :
(P Q: [univ]),
decidable P
→ decidable Q
→ decidable (P × Q).
Proof.
introv Hpd Hqd.
unfold decidable;
destruct Hpd; destruct Hqd;
try (left; dands; auto; fail);
(right; introv Hc; repnd; auto).
Defined.

Require Import Coq.Logic.Eqdep_dec.

Lemma UIPReflDeq: { A : Type} (deq : Deq A)
(a: A) (p: a=a), p= eq_refl.
Proof.
intros.
remember (@eq_refl A a) as eqr.
apply UIP_dec.
auto.
Qed.

Definition DeqP (A : Type):=
x0 y0 : A, x0 = y0 x0 y0.

Lemma DeqDeqp : {A : Type},
Proof.
introv deq.
intros x y.
destruct (deq x y);[left|right]; auto.
Qed.

copied from Coq.Logic.EqDep_dec.v and converted things from Prop to Type (and ex to sigT)

Let projT {A : Type} {x: A} (dec: Deq A)
{P:AType} (exP: sigT P) (def:P x) : P x :=
match exP with
| existT x' prf
match dec x' x with
| left eqprfeq_rect x' P prf x eqprf
| _def
end
end.
Theorem injRightsigT:
{A : Type} {x: A} (dec: Deq A) (P:AType) (y y':P x),
existT P x y = existT P x y'y = y'.
Proof.
intros.
cut (projT dec
(existT _ x y) y = projT dec (existT _ x y') y).
simpl.
case (dec x x).
intro e.
elim e using K_dec; trivial.

apply DeqDeqp. trivial.

intros.
case n; trivial.

case H.
reflexivity.
Qed.

Ltac EqDecSndEq :=
let dec:= fresh "dec" in
repeat match goal with
[H : @existT ?A _ _ _ = _ |- _ ] ⇒
assert (Deq A) as dec by eauto with Deq;
apply (injRightsigT dec) in H; clear dec
end.

Lemma DeqTrue: {A} (deq : Deq A) (a : A),
(deq a a) = (left (@eq_refl A a)).
Proof.
intros; auto.
destruct (deq a a) as [HH| HH].
- f_equal.
apply UIPReflDeq; auto.
- destruct HH. auto.
Defined.

Lemma DeqSym: {A} T (deq : Deq A) (a b: A)
(f : (a=b) → T) (c:T),
match deq a b with
| left pf p
| _c
end
=
match deq b a with
| left pf (eq_sym p)
| _c
end.
Proof.
intros.
destruct (deq a b) as [HH| HH].
- destruct (deq a b) as [H| H]; subst;sp.
destruct (deq b b); sp;[].
pose proof (UIPReflDeq deq _ e) as XX.
rw XX.
auto.
- destruct (deq b a) as [H| H]; subst; sp.
Defined.

Definition constantFn {A B : Type} (f: AB): [univ] :=
a1 a2, f a1 = f a2.

Lemma constantMapEq :
{A B : Type} (f: AB),
constantFn f
→ l1 l2,
length l1 = length l2
→ map f l1 = map f l2.
Proof.
introv Hc. repnud Hc.
induction l1 as [| h1 t1 Hind]; introv Hleq;
destruct l2; inverts Hleq;[|]; simpl. auto.
f_equal; auto; congruence.
Defined.

Definition DeqBool : Deq bool := bool_dec.

Hint Resolve deq_prod DeqBool: Deq.

Definition sigTDeq
{A : Type} (deq : Deq A)
(P : AType)
(deqf : (a:A), Deq (P a)) :
Deq (sigT P).
introv.
destruct (deq (projT1 x) (projT1 y)) as [Heq | Hneq];
[| right].
- destruct x as [xa xb]. allsimpl.
revert xb. rewrite Heq.
intros. allsimpl.
destruct y as [ya yb].
allsimpl.
destruct ((deqf ya) xb yb) as [beq | bneq];[left|right].
+ f_equal; auto.
+ introv Hc. EqDecSndEq.
apply bneq. exact Hc.
- introv Heq. apply (f_equal (@projT1 _ _)) in Heq.
apply Hneq. exact Heq.
Defined.

Definition Deq2Bool {A : Type} (deq : Deq A) (a b : A)
: bool.
destruct (deq a b);[exact true | exact false].
Defined.

Hint Resolve sigTDeq : Deq.

Lemma and_true_r :
t, t # True <=> t.
Proof. sp; split; sp. Qed.