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].