Lemma lt_le_dec : forall n m : N, {n < m} + {m <= n}.
Lemma lt_z_two : 0 < 2.
Lemma le_pred : forall n m : N, n <= m -> pred n <= pred m.
Lemma lt_mult_right : forall x y z : N, x < y -> 0 < z -> x * z < y * z.
Lemma le_mult_right : forall x y z : N, x <= y -> x * z <= y * z.
Lemma le_irrelevent : forall n m (H1 H2:le n m), H1=H2.
Lemma minus3:forall (a b c:nat),(c<=b<=a)-> a+(b-c)=b+(a-c).
Lemma minus4:forall (a b c d:nat), (d<=c<=b)->
(a+b)+(c-d)=(a+c)+(b-d).
The power function does not exist in the standard library
Fixpoint power (m : N) : N -> N :=
match m with
| O => fun _ : N => 1
| S n => fun x : N => power n x * x
end.
Factorial function. Does not exist in Arith.
Needed for special operations on polynomials.
Fixpoint fac (n : N) : N :=
match n with
| O => 1
| S m => S m * fac m
end.
Lemma nat_fac_gtzero : forall n : N, 0 < fac n.
Lemma not_r_sumbool_rec : forall (A B : Prop) (S : Set) (l r : S), ~ B -> forall H : {A} + {B},
sumbool_rec (fun _ : {A} + {B} => S) (fun x : A => l) (fun x : B => r) H = l.
Lemma not_l_sumbool_rec : forall (A B : Prop) (S : Set) (l r : S), ~ A -> forall H : {A} + {B},
sumbool_rec (fun _ : {A} + {B} => S) (fun x : A => l) (fun x : B => r) H = r.
Lemma POS_anti_convert : forall n : N, S n = Zpos (P_of_succ_nat n) :>Z.
Lemma NEG_anti_convert : forall n : N, (- S n)%Z = Zneg (P_of_succ_nat n).
Lemma lt_O_positive_to_nat : forall (p : positive) (m : N), 0 < m -> 0 < Pmult_nat p m.
Lemma anti_convert_pred_convert : forall p : positive,
p = P_of_succ_nat (pred (nat_of_P p)).
Lemma p_is_some_anti_convert : forall p : positive, exists n : N, p = P_of_succ_nat n.
Lemma convert_is_POS : forall p : positive, nat_of_P p = Zpos p :>Z.
Lemma min_convert_is_NEG : forall p : positive, (- nat_of_P p)%Z = Zneg p.
Lemma surj_eq:forall (n m:nat),
((Z_of_nat n)=(Z_of_nat m))%Z -> n=m.
Lemma surj_le:forall (n m:nat),
((Z_of_nat n)<=(Z_of_nat m))%Z -> n<=m.
Lemma surj_lt:forall (n m:nat),
((Z_of_nat n)<(Z_of_nat m))%Z -> n<m.
Lemma surj_not:forall (n m:nat),
((Z_of_nat n)<>(Z_of_nat m))%Z -> n<>m.
Lemma lt_lt_minus:forall(q p l:nat),
q<l -> p<q -> p+(l-q)<l.
Lemma inject_nat_convert :
forall p : positive, Z_of_nat (nat_of_P p) = BinInt.Zpos p.
Definition Z_to_nat: forall (z:Z),(0<=z)%Z->nat.
Defined.
Lemma Z_to_nat_correct:forall (z:Z)(H:(0<=z)%Z),
z=(Z_of_nat (Z_to_nat H)).
Lemma Z_exh : forall z : Z, (exists n : N, z = n) \/ (exists n : N, z = (- n)%Z).
Lemma nats_Z_ind : forall P : Z -> Prop,
(forall n : N, P n) -> (forall n : N, P (- n)%Z) -> forall z : Z, P z.
Lemma pred_succ_Z_ind : forall P : Z -> Prop, P 0%Z ->
(forall n : Z, P n -> P (n + 1)%Z) -> (forall n : Z, P n -> P (n - 1)%Z) -> forall z : Z, P z.
Lemma Zmult_minus_distr_r : forall n m p : Z, (p * (n - m))%Z = (p * n - p * m)%Z.
Lemma Zodd_Zeven_min1 : forall x : Z, Zeven.Zodd x -> Zeven.Zeven (x - 1).
Definition caseZ_diff (A : Type) (z : Z) (f : N -> N -> A) :=
match z with
| Z0 => f 0 0
| Zpos m => f (nat_of_P m) 0
| Zneg m => f 0 (nat_of_P m)
end.
Lemma caseZ_diff_O : forall (A : Type) (f : N -> N -> A), caseZ_diff 0 f = f 0 0.
Lemma caseZ_diff_Pos : forall (A : Type) (f : N -> N -> A) (n : N),
caseZ_diff n f = f n 0.
Lemma caseZ_diff_Neg : forall (A : Type) (f : N -> N -> A) (n : N),
caseZ_diff (- n) f = f 0 n.
Lemma proper_caseZ_diff : forall (A : Type) (f : N -> N -> A),
(forall m n p q : N, m + q = n + p -> f m n = f p q) ->
forall m n : N, caseZ_diff (m - n) f = f m n.
Lemma diff_Z_ind : forall P : Z -> Prop, (forall m n : N, P (m - n)%Z) -> forall z : Z, P z.
Lemma Zlt_reg_mult_l : forall x y z : Z,
(x > 0)%Z -> (y < z)%Z -> (x * y < x * z)%Z.
Lemma Zlt_opp : forall x y : Z, (x < y)%Z -> (- x > - y)%Z.
Lemma Zlt_conv_mult_l : forall x y z : Z,
(x < 0)%Z -> (y < z)%Z -> (x * y > x * z)%Z.
Lemma Zgt_not_eq : forall x y : Z, (x > y)%Z -> x <> y.
Lemma Zmult_absorb : forall x y z : Z,
x <> 0%Z -> (x * y)%Z = (x * z)%Z -> y = z.
Section Well_foundedT.
Variable A : Type.
Variable R : A -> A -> Prop.
The accessibility predicate is defined to be non-informative
Inductive Acc : A -> Prop :=
Acc_intro : forall x : A, (forall y : A, R y x -> Acc y) -> Acc x.
End Well_foundedT.
Section AccT.
Variable A : Type.
Definition well_founded (P : A -> A -> Prop) := forall a : A, Acc _ P a.
End AccT.
Section IndT.
Variable A : Type.
Variable R : A -> A -> Prop.
Section AccIter.
Variable P : A -> Type.
Variable F : forall x : A, (forall y : A, R y x -> P y) -> P x.
Lemma Acc_inv : forall x : A, Acc R x -> forall y : A, R y x -> Acc R y.
Fixpoint Acc_iter (x : A) (a : Acc R x) {struct a} :
P x := F x (fun (y : A) (h : R y x) => Acc_iter y (Acc_inv x a y h)).
End AccIter.
Hypothesis Rwf : well_founded A R.
Theorem well_founded_induction_type :
forall P : A -> Type,
(forall x : A, (forall y : A, R y x -> P y) -> P x) -> forall a : A, P a.
End IndT.
Section InductionT.
Variable A : Type.
Variable f : A -> N.
Definition ltof (a b : A) := f a < f b.
Theorem well_founded_ltof : well_founded A ltof.
Theorem induction_ltof2T : forall P : A -> Type,
(forall x : A, (forall y : A, ltof y x -> P y) -> P x) -> forall a : A, P a.
End InductionT.
Section InductionTT.
Lemma lt_wf_rect : forall (p : N) (P : N -> Type),
(forall n : N, (forall m : N, m < n -> P m) -> P n) -> P p.
End InductionTT.
This new version of postive recursion gives access to
both n and n+1 for the 2n+1 case, while still maintaining efficency.
Fixpoint positive_rect2_helper
(P : positive -> Type)
(c1 : forall p : positive, P (Psucc p) -> P p -> P (xI p))
(c2 : forall p : positive, P p -> P (xO p))
(c3 : P 1%positive)
(b : bool) (p : positive) {struct p} : P (if b then Psucc p else p) :=
match p return (P (if b then Psucc p else p)) with
| xH => if b return P (if b then (Psucc xH) else xH) then (c2 _ c3) else c3
| xO p' => if b return P (if b then (Psucc (xO p')) else xO p')
then (c1 _ (positive_rect2_helper P c1 c2 c3 true _) (positive_rect2_helper P c1 c2 c3 false _))
else (c2 _ (positive_rect2_helper P c1 c2 c3 false _))
| xI p' => if b return P (if b then (Psucc (xI p')) else xI p')
then (c2 _ (positive_rect2_helper P c1 c2 c3 true _))
else (c1 _ (positive_rect2_helper P c1 c2 c3 true _) (positive_rect2_helper P c1 c2 c3 false _))
end.
Definition positive_rect2
(P : positive -> Type)
(c1 : forall p : positive, P (Psucc p) -> P p -> P (xI p))
(c2 : forall p : positive, P p -> P (xO p))
(c3 : P 1%positive) (p : positive) : P p :=
positive_rect2_helper P c1 c2 c3 false p.
Lemma positive_rect2_helper_bool : forall P c1 c2 c3 p,
positive_rect2_helper P c1 c2 c3 true p =
positive_rect2_helper P c1 c2 c3 false (Psucc p).
Lemma positive_rect2_red1 : forall P c1 c2 c3 p,
positive_rect2 P c1 c2 c3 (xI p) =
c1 p (positive_rect2 P c1 c2 c3 (Psucc p)) (positive_rect2 P c1 c2 c3 p).
Lemma positive_rect2_red2 : forall P c1 c2 c3 p,
positive_rect2 P c1 c2 c3 (xO p) =
c2 p (positive_rect2 P c1 c2 c3 p).
Lemma positive_rect2_red3 : forall P c1 c2 c3,
positive_rect2 P c1 c2 c3 (xH) = c3.
(P : positive -> Type)
(c1 : forall p : positive, P (Psucc p) -> P p -> P (xI p))
(c2 : forall p : positive, P p -> P (xO p))
(c3 : P 1%positive)
(b : bool) (p : positive) {struct p} : P (if b then Psucc p else p) :=
match p return (P (if b then Psucc p else p)) with
| xH => if b return P (if b then (Psucc xH) else xH) then (c2 _ c3) else c3
| xO p' => if b return P (if b then (Psucc (xO p')) else xO p')
then (c1 _ (positive_rect2_helper P c1 c2 c3 true _) (positive_rect2_helper P c1 c2 c3 false _))
else (c2 _ (positive_rect2_helper P c1 c2 c3 false _))
| xI p' => if b return P (if b then (Psucc (xI p')) else xI p')
then (c2 _ (positive_rect2_helper P c1 c2 c3 true _))
else (c1 _ (positive_rect2_helper P c1 c2 c3 true _) (positive_rect2_helper P c1 c2 c3 false _))
end.
Definition positive_rect2
(P : positive -> Type)
(c1 : forall p : positive, P (Psucc p) -> P p -> P (xI p))
(c2 : forall p : positive, P p -> P (xO p))
(c3 : P 1%positive) (p : positive) : P p :=
positive_rect2_helper P c1 c2 c3 false p.
Lemma positive_rect2_helper_bool : forall P c1 c2 c3 p,
positive_rect2_helper P c1 c2 c3 true p =
positive_rect2_helper P c1 c2 c3 false (Psucc p).
Lemma positive_rect2_red1 : forall P c1 c2 c3 p,
positive_rect2 P c1 c2 c3 (xI p) =
c1 p (positive_rect2 P c1 c2 c3 (Psucc p)) (positive_rect2 P c1 c2 c3 p).
Lemma positive_rect2_red2 : forall P c1 c2 c3 p,
positive_rect2 P c1 c2 c3 (xO p) =
c2 p (positive_rect2 P c1 c2 c3 p).
Lemma positive_rect2_red3 : forall P c1 c2 c3,
positive_rect2 P c1 c2 c3 (xH) = c3.
Iteration for natural numbers.