qed.
theorem le_fact_A:\forall n.S O < n \to
-fact ((S(S O))*n) \le exp (fact n) (S(S O)) * A ((S(S O))*n).
+fact (2*n) \le exp (fact n) 2 * A (2*n).
intros.
rewrite > eq_fact_B
[apply le_times_r.
qed.
theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
-B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
+B (2*n) \le exp 2 (pred (2*n)).
intros.
apply (le_times_to_le (exp (fact n) (S(S O))))
[apply lt_O_exp.
qed.
theorem le_B_exp: \forall n.
-B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
+B (2*n) \le exp 2 (pred (2*n)).
intro.cases n
[apply le_n
|cases n1
- [simplify.apply le_S.apply le_S.apply le_n
+ [simplify.apply le_n
|apply lt_SO_to_le_B_exp.
apply le_S_S.apply lt_O_S.
]
qed.
theorem le_A_exp: \forall n.
-A((S(S O))*n) \le (exp (S(S O)) ((S(S O)*n)))*A n.
+A(2*n) \le (exp 2 (pred (2*n)))*A n.
intro.
-apply (trans_le ? (B((S(S O))*n)*A n))
+apply (trans_le ? (B(2*n)*A n))
[apply le_A_BA
|apply le_times_l.
apply le_B_exp
]
qed.
+theorem times_SSO_pred: \forall n. 2*(pred n) \le pred (2*n).
+intro.cases n
+ [apply le_n
+ |simplify.apply le_plus_r.
+ apply le_n_Sn
+ ]
+qed.
+
+theorem le_S_times_SSO: \forall n. O < n \to S n \le 2*n.
+intros.
+elim H
+ [apply le_n
+ |rewrite > times_SSO.
+ apply le_S_S.
+ apply (trans_le ? (2*n1))
+ [assumption
+ |apply le_n_Sn
+ ]
+ ]
+qed.
+
theorem le_A_exp1: \forall n.
-A(exp (S(S O)) n) \le (exp (S(S O)) ((S(S O))*(exp (S(S O)) n))).
+A(exp 2 n) \le (exp 2 ((2*(exp 2 n)-(S(S n))))).
intro.elim n
- [simplify.apply le_S_S.apply le_O_n
- |change with (A ((S(S O))*((S(S O)))\sup n1)≤ ((S(S O)))\sup((S(S O))*((S(S O))\sup(S n1)))).
- apply (trans_le ? ((exp (S(S O)) ((S(S O)*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
+ [simplify.apply le_n
+ |change in ⊢ (? % ?) with (A(2*(exp 2 n1))).
+ apply (trans_le ? ((exp 2 (pred(2*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
[apply le_A_exp
- |apply (trans_le ? ((S(S O))\sup((S(S O))*((S(S O)))\sup(n1))*(S(S O))\sup((S(S O))*((S(S O)))\sup(n1))))
+ |apply (trans_le ? ((2)\sup(pred (2*(2)\sup(n1)))*(2)\sup(2*(2)\sup(n1)-S (S n1))))
[apply le_times_r.
assumption
|rewrite < exp_plus_times.
- simplify.rewrite < plus_n_O in ⊢ (? ? (? ? (? ? %))).
- apply le_n
+ apply le_exp
+ [apply lt_O_S
+ |cut (S(S n1) \le 2*(exp 2 n1))
+ [apply le_S_S_to_le.
+ change in ⊢ (? % ?) with (S(pred (2*(2)\sup(n1)))+(2*(2)\sup(n1)-S (S n1))).
+ rewrite < S_pred
+ [rewrite > eq_minus_S_pred in ⊢ (? ? %).
+ rewrite < S_pred
+ [rewrite < eq_minus_plus_plus_minus
+ [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?).
+ apply le_n
+ |assumption
+ ]
+ |apply lt_to_lt_O_minus.
+ apply (lt_to_le_to_lt ? (2*(S(S n1))))
+ [rewrite > times_n_SO in ⊢ (? % ?).
+ rewrite > sym_times.
+ apply lt_times_l1
+ [apply lt_O_S
+ |apply le_n
+ ]
+ |apply le_times_r.
+ assumption
+ ]
+ ]
+ |unfold.rewrite > times_n_SO in ⊢ (? % ?).
+ apply le_times
+ [apply le_n_Sn
+ |apply lt_O_exp.
+ apply lt_O_S
+ ]
+ ]
+ |elim n1
+ [apply le_n
+ |apply (trans_le ? (2*(S(S n2))))
+ [apply le_S_times_SSO.
+ apply lt_O_S
+ |apply le_times_r.
+ assumption
+ ]
+ ]
+ ]
+ ]
]
]
]
-qed.
+qed.
theorem monotonic_A: monotonic nat le A.
unfold.intros.
]
]
qed.
-
+
+(*
theorem le_A_exp2: \forall n. O < n \to
A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
intros.
]
]
qed.
+*)
(* example *)
theorem A_SO: A (S O) = S O.
]
qed.
+(*
(* a better result *)
theorem le_A_exp3: \forall n. S O < n \to
-A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n)).
+A(n) \le exp (pred n) (2*(exp 2 (2 * n)).
intro.
apply (nat_elim1 n).
intros.
apply False_ind.
apply (lt_to_not_le ? ? H1).
rewrite > H3.
- apply le_n
+ apply le_
]
]
qed.
+*)
theorem le_A_exp4: \forall n. S O < n \to
-A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * (pred n))).
+A(n) \le (pred n)*exp 2 ((2 * n) -3).
intro.
apply (nat_elim1 n).
intros.
elim H2
[elim (le_to_or_lt_eq (S O) a)
[rewrite > H3 in ⊢ (? % ?).
- apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
+ apply (trans_le ? (exp 2 (pred(2*a))*A a))
[apply le_A_exp
- |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
- ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*(pred a)))))
+ |apply (trans_le ? (2\sup(pred(2*a))*((pred a)*2\sup((2*a)-3))))
[apply le_times_r.
apply H
[rewrite > H3.
]
|assumption
]
- |rewrite > sym_times.
+ |rewrite < H3.
+ rewrite < assoc_times.
+ rewrite > sym_times in ⊢ (? (? % ?) ?).
rewrite > assoc_times.
- rewrite < exp_plus_times.
- apply (trans_le ?
- (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*(pred m))))
- [rewrite > assoc_times.
- apply le_times_r.
- rewrite < exp_plus_times.
+ apply le_times
+ [rewrite > H3.
+ elim a[apply le_n|simplify.apply le_plus_n_r]
+ |rewrite < exp_plus_times.
apply le_exp
[apply lt_O_S
- |rewrite < H3.
- simplify.
- rewrite < plus_n_O.
- apply le_S.apply le_S.
- rewrite < plus_n_O;
- apply le_S_S_to_le;
- rewrite > plus_n_Sm in \vdash (? ? %);
- rewrite < S_pred;
- [change in \vdash (? % ?) with ((S (pred a + pred a)) + m);
- apply le_plus_l;
- apply le_S_S_to_le;
- rewrite < S_pred;
- [rewrite > plus_n_Sm;rewrite > sym_plus;
- rewrite > plus_n_Sm;
- rewrite > H3;simplify in \vdash (? ? %);
- rewrite < plus_n_O;rewrite < S_pred;
- [apply le_n
- |apply lt_to_le;assumption]
- |apply lt_to_le;assumption]
- |apply lt_to_le;assumption]]
- |apply le_times_l.
- rewrite > times_exp.
- apply monotonic_exp1.
- rewrite > H3.
- rewrite > sym_times.
- cases a
- [apply le_n
- |simplify.
- rewrite < plus_n_Sm.
- apply le_S.
- apply le_n
+ |apply (trans_le ? (m+(m-3)))
+ [apply le_plus_l.
+ cases m[apply le_n|apply le_n_Sn]
+ |simplify.rewrite < plus_n_O.
+ rewrite > eq_minus_plus_plus_minus
+ [apply le_n
+ |rewrite > H3.
+ apply (trans_le ? (2*2))
+ [simplify.apply (le_n_Sn 3)
+ |apply le_times_r.assumption
+ ]
+ ]
+ ]
]
]
]
]
- |rewrite < H4 in H3.
- simplify in H3.
- rewrite > H3.
- simplify.
- apply le_S_S.apply le_S_S.apply le_O_n
+ |rewrite > H3.rewrite < H4.simplify.
+ apply le_S_S.apply lt_O_S
|apply not_lt_to_le.intro.
apply (lt_to_not_le ? ? H1).
rewrite > H3.
rewrite > H3.
rewrite > times_SSO.
apply le_n_Sn
- |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
+ |apply (trans_le ? ((exp 2 (pred(2*(S a))))*A (S a)))
[apply le_A_exp
- |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
- (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
+ |apply (trans_le ? ((2\sup(pred (2*S a)))*(a*(exp 2 ((2*(S a))-3)))))
[apply le_times_r.
- apply (trans_le ? ? ? (H (S a) ? ?));
+ apply H
[rewrite > H3.
apply le_S_S.
- simplify.
- rewrite > plus_n_SO.
- apply le_plus_r.
- rewrite < plus_n_O.
+ apply le_S_times_SSO.
assumption
|apply le_S_S.assumption
- |simplify in ⊢ (? (? (? % ?) ?) ?);
- apply le_times_r;apply le_exp;
- [apply le_S;apply le_n
- |apply le_times_r;simplify;apply le_n]
]
- |rewrite > sym_times.
- rewrite > assoc_times.
- rewrite < exp_plus_times.
- rewrite > H3;
- change in ⊢ (? ? (? (? % ?) ?)) with ((S (S O))*a);
- rewrite < times_exp;
- rewrite < sym_times in \vdash (? ? (? % ?));
- rewrite > assoc_times;
- apply le_times_r;
- rewrite < times_n_Sm in ⊢ (? (? ? (? ? %)) ?);
- rewrite > sym_plus in \vdash (? (? ? %) ?);
- rewrite > assoc_plus in \vdash (? (? ? %) ?);
- rewrite > exp_plus_times;apply le_times_r;
- rewrite < distr_times_plus in ⊢ (? (? ? %) ?);
- simplify in ⊢ (? ? (? ? (? ? %)));rewrite < plus_n_O;
- apply le_n
+ |rewrite > H3.
+ change in ⊢ (? ? (? % ?)) with (2*a).
+ rewrite > times_SSO.
+ change in ⊢ (? (? (? ? %) ?) ?) with (S(2*a)).
+ rewrite > minus_Sn_m
+ [change in ⊢ (? (? ? (? ? %)) ?) with (2*(exp 2 (S(2*a)-3))).
+ rewrite < assoc_times in ⊢ (? (? ? %) ?).
+ rewrite < assoc_times.
+ rewrite > sym_times in ⊢ (? (? % ?) ?).
+ rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
+ rewrite > assoc_times.
+ apply le_times_r.
+ rewrite < exp_plus_times.
+ apply le_exp
+ [apply lt_O_S
+ |rewrite < eq_minus_plus_plus_minus
+ [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?).
+ apply le_n
+ |apply le_S_S.
+ apply O_lt_const_to_le_times_const.
+ assumption
+ ]
+ ]
+ |apply le_S_S.
+ apply O_lt_const_to_le_times_const.
+ assumption
+ ]
]
]
]
qed.
theorem le_exp_primr: \forall n. S O < n \to
-exp n (prim n) \le exp (pred n) ((S(S O))*(S(S O)))*(exp (S(S O)) ((S(S O))*(S(S O)) * (pred n))).
+exp n (prim n) \le exp (pred n) 2*(exp 2 (2*(2*n-3))).
intros.
-apply (trans_le ? (exp (A n) (S(S O))))
+apply (trans_le ? (exp (A n) 2))
[change in ⊢ (? ? %) with ((A n)*((A n)*(S O))).
rewrite < times_n_SO.
apply leA_r2
- |apply (trans_le ? (exp (exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * (pred n)))) (S(S O))))
+ |apply (trans_le ? (exp ((pred n)*(exp 2 (2*n - 3))) 2))
[apply monotonic_exp1.
apply le_A_exp4.
assumption
|rewrite < times_exp.
rewrite > exp_exp_times.
- rewrite > exp_exp_times.
- rewrite > sym_times in ⊢ (? (? ? (? ? %)) ?).
- rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).
+ apply le_times_r.
+ rewrite > sym_times.
apply le_n
]
]
intros.reflexivity.
qed.
-lemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
+alias num (instance 0) = "natural number".
+lemma times_SSO: \forall n.2*(S n) = S(S(2*n)).
intro.simplify.rewrite < plus_n_Sm.reflexivity.
qed.
-theorem fact1: \forall n.
-fact ((S(S O))*n) \le (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n).
-intro.elim n
- [rewrite < times_n_O.apply le_n
+theorem lt_O_to_fact1: \forall n.O<n \to
+fact (2*n) \le (exp 2 (pred (2*n)))*(fact n)*(fact n).
+intros.elim H
+ [apply le_n
|rewrite > times_SSO.
rewrite > factS.
rewrite > factS.
rewrite < assoc_times.
rewrite > factS.
- apply (trans_le ? (((S(S O))*(S n1))*((S(S O))*(S n1))*(fact (((S(S O))*n1)))))
+ apply (trans_le ? ((2*(S n1))*(2*(S n1))*(fact (2*n1))))
[apply le_times_l.
rewrite > times_SSO.
apply le_times_r.
|rewrite > assoc_times.
rewrite > assoc_times.
rewrite > assoc_times in ⊢ (? ? %).
+ change in ⊢ (? ? (? (? ? %) ?)) with (S(2*n1)).
rewrite > exp_S.
rewrite > assoc_times in ⊢ (? ? %).
apply le_times_r.
rewrite < sym_times in ⊢ (? (? (? % ?) ?) ?).
rewrite > assoc_times.
rewrite > assoc_times.
- rewrite > exp_S.
- rewrite > assoc_times in ⊢ (? ? %).
- apply le_times_r.
- rewrite > sym_times in ⊢ (? ? %).
- rewrite > assoc_times in ⊢ (? ? %).
- rewrite > assoc_times in ⊢ (? ? %).
- apply le_times_r.
- rewrite < assoc_times in ⊢ (? ? %).
- rewrite < assoc_times in ⊢ (? ? %).
- rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
- rewrite > assoc_times in ⊢ (? ? %).
- rewrite > assoc_times in ⊢ (? ? %).
- apply le_times_r.
- rewrite > sym_times in ⊢ (? ? (? ? %)).
- rewrite > sym_times in ⊢ (? ? %).
- assumption
+ rewrite > S_pred in ⊢ (? ? (? (? ? %) ?))
+ [rewrite > exp_S.
+ rewrite > assoc_times in ⊢ (? ? %).
+ apply le_times_r.
+ rewrite > sym_times in ⊢ (? ? %).
+ rewrite > assoc_times in ⊢ (? ? %).
+ rewrite > assoc_times in ⊢ (? ? %).
+ apply le_times_r.
+ rewrite < assoc_times in ⊢ (? ? %).
+ rewrite < assoc_times in ⊢ (? ? %).
+ rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
+ rewrite > assoc_times in ⊢ (? ? %).
+ rewrite > assoc_times in ⊢ (? ? %).
+ apply le_times_r.
+ rewrite > sym_times in ⊢ (? ? (? ? %)).
+ rewrite > sym_times in ⊢ (? ? %).
+ assumption
+ |unfold.rewrite > times_n_SO in ⊢ (? % ?).
+ apply le_times
+ [apply le_n_Sn
+ |assumption
+ ]
+ ]
]
]
qed.
+theorem fact1: \forall n.
+fact (2*n) \le (exp 2 (pred (2*n)))*(fact n)*(fact n).
+intro.cases n
+ [apply le_n
+ |apply lt_O_to_fact1.
+ apply lt_O_S
+ ]
+qed.
+
theorem lt_O_fact: \forall n. O < fact n.
intro.elim n
[simplify.apply lt_O_S
projects / helm.git / commitdiff