Library Range

Require Import Arith.
Require Import types.
Require Import Omega.
Require Import Eqdep_dec.
Require Import Peano_dec.

Definition lowrange (u:nat):={k|k<=u}.
Definition range (b u:nat):={k|b<=k /\ k<=u}.
Definition lowrangt (u:nat):={k|k<u}.
Definition rangt (b u:nat):={k|b<=k /\ k<u}.


Theorem K_nat : forall (x:nat) (P:x = x -> Prop),
P (refl_equal x) -> forall p:x = x, P p.

Theorem eq_rect_eq_nat : forall (p:nat) (Q:nat->Type)
(x:Q p) (h:p=p), x = eq_rect p Q x p h.



Scheme le_ind' := Induction for le Sort Prop.
Check le_ind'.

Lemma le_uniqueness_proof: forall (n m:nat)
(p q:n<=m), p=q.


Definition lowrange_identity (u:nat) (N:lowrange u):nat:=
match N with
|exist n _=>n
end.
Implicit Arguments lowrange_identity [u].

Definition natfunc_lowrange (A:Type) (f:nat->A) (u:nat) (N:lowrange u):=
f (lowrange_identity N).
Implicit Arguments natfunc_lowrange [A].

Definition natfunc_lowrange_Prop:=@natfunc_lowrange Prop.

Definition le_lowrange (u:nat):=natfunc_lowrange_Prop
(fun k=>k<=u) u.

Lemma le_lowrange_in: forall (u:nat) (N:lowrange u),
le_lowrange u N.

Theorem lowrange_eq: forall (u:nat) (N M:lowrange u),
N=M->lowrange_identity N=lowrange_identity M.

Theorem lowrange_identity_le: forall (u:nat) (N:lowrange u),
lowrange_identity N<=u.

Theorem lowrange_identity_injective: forall (u:nat),
injective (@lowrange_identity u).

Definition lowrange_injective_le_fun (n m:nat) (Hnm:n<=m)
(I:lowrange n):=
match I return lowrange m with
|exist i pin=>exist _ i (le_trans i n m pin Hnm)
end.

Lemma lowrange_injective_le: forall (n m:nat) (Hnm:n<=m),
injective (lowrange_injective_le_fun n m Hnm).

Lemma lowrange_injective_S_func_aux: forall (n m:nat),
n<=S m -> n<>S m -> n<=m.
Definition lowrange_injective_S_func (n m:nat)
(f:lowrange n->lowrange m) (If:injective f)
(I:lowrange (S n)):=
match I with
|exist i pin =>
 match eq_nat_dec i (S n) return lowrange (S m) with
 | left pin2 => exist _ (S m) (le_refl (S m))
 | right pin2 =>
   let Im:=f (exist _ i
    (lowrange_injective_S_func_aux i n pin pin2)) in
   let Im_nat:=lowrange_identity Im in
   exist _ Im_nat (le_S Im_nat m (lowrange_identity_le m Im))
 end
end.

Lemma lowrange_injective_S: forall (n m:nat)
(f:lowrange n->lowrange m) (If:injective f),
injective (lowrange_injective_S_func n m f If).

Definition lowrange_prevfunc (A:Type) (u:nat) (f:lowrange (S u)->A)
(I:lowrange u):A:=
match I with
|exist i pin =>f (exist _ i (le_S i u pin))
end.
Implicit Arguments lowrange_prevfunc [A u].

Lemma lowrange_prevfunc_injective: forall (A:Type) (u:nat)
(f:lowrange (S u)->A), injective f->
injective (lowrange_prevfunc f).

Lemma lowrange_injective_P_func_aux: forall (n m:nat)
(f:lowrange (S n)->lowrange (S m)) (If:injective f)
(I:lowrange n),
let F:=lowrange_prevfunc f in
let fSn_nat:=lowrange_identity (f (exist _ (S n) (le_n _))) in
lowrange_identity (F I)=S m->fSn_nat<=m.
Lemma lowrange_injective_P_func_aux2: forall (n m:nat)
(F:lowrange n->lowrange (S m)) (I:lowrange n),
lowrange_identity(F I)<>S m->
lowrange_identity (F I)<=m.
Definition lowrange_injective_P_func (n m:nat)
(f:lowrange (S n)->lowrange (S m)) (If:injective f)
(I:lowrange n):lowrange m:=
let F:=lowrange_prevfunc f in
match I with
|exist i pin =>
 match eq_nat_dec
  (lowrange_identity (F I)) (S m)
  return lowrange m with
 | left pin2 =>
  let fSn:=f (exist _ (S n) (le_n _)) in
  let fSn_nat:=lowrange_identity fSn in
  exist (fun k=>k<=m) fSn_nat
   (lowrange_injective_P_func_aux n m f If I pin2)
 | right pin2 =>
  let FI_nat:=lowrange_identity (F I) in
  exist (fun k=>k<=m) FI_nat
   (lowrange_injective_P_func_aux2 n m F I pin2)
 end
end.

Definition lowrange_injective_P: forall (n m:nat)
(f:lowrange (S n)->lowrange (S m)) (If:injective f),
injective (lowrange_injective_P_func n m f If).

Lemma lowrange_0_unique: exists! Z:lowrange 0, True.

Lemma lowrange_S_pair: forall (u:nat),
{Z:lowrange (S u)&{F:lowrange (S u)|Z<>F}}.

Lemma lowrange_injective_n0: forall (u:nat),
~exists f:lowrange (S u)->lowrange 0, injective f.

Lemma lowrange_injective_n: forall (m n:nat), m<n->
~exists f:lowrange n->lowrange m, injective f.

Theorem lowrange_discr : forall m n:nat,
(lowrange m) = (lowrange n) -> m = n.
Print Assumptions lowrange_discr.
Theorem lowrange_exist_eq: forall (u m n:nat) (mH:m<=u) (nH:n<=u),
m=n-> exist (fun k=>k<=u) m mH=exist (fun k=>k<=u) n nH.



Lemma lt_uniqueness_proof: forall (n m:nat)
(p q:n<m), p=q.

Definition lowrangt_identity (u:nat) (N:lowrangt u):nat:=
match N with
|exist n _=>n
end.
Implicit Arguments lowrangt_identity [u].

Definition natfunc_lowrangt (A:Type) (f:nat->A) (u:nat) (N:lowrangt u):=
f (lowrangt_identity N).
Implicit Arguments natfunc_lowrangt [A].

Definition lowrangt_lowrange_identity (u:nat) (I:lowrangt u)
:lowrange u:=
match I with
|exist i pim=>exist _ i (le_Sn_le i u pim)
end.
Lemma lowrangt_lowrange_identity_injective: forall (u:nat),
injective(lowrangt_lowrange_identity u).

Definition lowrangtS_lowrange_identity (u:nat) (I:lowrangt (S u))
:lowrange u:=
match I with
|exist i pim=>exist _ i (le_S_n i u pim)
end.
Lemma lowrangtS_lowrange_identity_injective: forall (u:nat),
injective(lowrangtS_lowrange_identity u).

Definition lowrange_lowrangtS_identity (u:nat) (I:lowrange u)
:lowrangt (S u):=
match I with
|exist i pim=>exist _ i (le_n_S i u pim)
end.
Lemma lowrange_lowrangtS_identity_injective: forall (u:nat),
injective(lowrange_lowrangtS_identity u).

Lemma lowrangt_injective_Sn: forall (m n:nat), m<n->
~exists f:lowrangt (S n)->lowrangt (S m), injective f.

Lemma lowrangt_0_nonihabited: ~inhabited (lowrangt 0).

Lemma lowrangt_S_ihabited: forall (u:nat),
inhabited (lowrangt (S u)).

Lemma lowrangt_injective_0: forall (u:nat),
~exists f:lowrangt (S u)->lowrangt 0, injective f.

Lemma lowrangt_injective_n: forall (m n:nat), m<n->
~exists f:lowrangt n->lowrangt m, injective f.

Theorem lowrangt_discr : forall m n:nat,
(lowrangt m) = (lowrangt n) -> m = n.

Theorem lowrangt_exist_eq: forall (u m n:nat) (mH:m<u) (nH:n<u),
m=n-> exist (fun k=>k<u) m mH=exist (fun k=>k<u) n nH.

Definition lowrangt_prevfunc (A:Type) (u:nat) (f:lowrangt (S u)->A)
(I:lowrangt u):A:=
match I with
|exist i pin =>f (exist _ i (lt_S i u pin))
end.
Implicit Arguments lowrangt_prevfunc [A u].