--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "nat/exp.ma".
+include "nat/relevant_equations.ma".
+
+alias num (instance 0) = "natural number".
+
+theorem plus_inv_O3: ∀m,n. 0 = n + m → 0 = n ∧ 0 = m.
+ intros 2; elim n names 0; clear n; simplify; intros;
+ [ autobatch | destruct ].
+qed.
+
+theorem times_inv_O3_S: ∀x,y. 0 = x * (S y) → x = 0.
+ intros; rewrite < times_n_Sm in H;
+ lapply linear plus_inv_O3 to H; decompose;autobatch.
+qed.
+
+theorem not_3_divides_1: ∀n. 1 = n * 3 → False.
+ intros 1; rewrite > sym_times; simplify;
+ elim n names 0; simplify; intros; destruct;
+ rewrite > sym_plus in Hcut; simplify in Hcut; destruct Hcut.
+qed.
+
+variant le_inv_S_S: ∀m,n. S m ≤ S n → m ≤ n
+≝ le_S_S_to_le.
+
+theorem plus_inv_S_S_S: ∀x,y,z. S x = S y + S z → S y ≤ x ∧ S z ≤ x.
+ simplify; intros; destruct;autobatch.
+qed.
+
+theorem times_inv_S_m_SS: ∀k,n,m. S n = m * (S (S k)) → m ≤ n.
+ intros 3; elim m names 0; clear m; simplify; intros; destruct;
+ clear H; autobatch by le_S_S, transitive_le, le_plus_n, le_plus_n_r.
+qed.
+
+theorem plus_3_S3n: ∀n. S (S n * 3) = 3 + S (n * 3).
+ intros; autobatch depth = 1.
+qed.
+
+theorem times_exp_x_y_Sz: ∀x,y,z. x * y \sup (S z) = (x * y \sup z) * y.
+ intros; autobatch depth = 1.
+qed.
+
+definition acc_nat: (nat → Prop) → nat →Prop ≝
+ λP:nat→Prop. λn. ∀m. m ≤ n → P m.
+
+theorem wf_le: ∀P. P 0 → (∀n. acc_nat P n → P (S n)) → ∀n. acc_nat P n.
+ unfold acc_nat; intros 4; elim n names 0; clear n;
+ [ intros; autobatch by (eq_ind ? ? P), H, H2, le_n_O_to_eq.
+ (* lapply linear le_n_O_to_eq to H2; destruct; autobatch *)
+ | intros 3; elim m; clear m; intros; clear H3;
+ [ clear H H1; autobatch depth = 2
+ | clear H; lapply linear le_inv_S_S to H4;
+ apply H1; clear H1; intros;
+ apply H2; clear H2; autobatch depth = 2
+ ]
+ ].
+qed.
+
+theorem wf_nat_ind:
+ ∀P:nat→Prop. P O → (∀n. (∀m. m ≤ n → P m) → P (S n)) → ∀n. P n.
+ intros; lapply linear depth=2 wf_le to H, H1 as H0;
+ autobatch.
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* BTM: MATITA SOURCE FILES
+ * Suggested invocation to start formal specifications with:
+ * - Patience on me to gain peace and perfection! -
+ * 2008 September 22:
+ * specification starts.
+ *)
+
+include "arith.ma".
+
+(* CHARACTER CLASSES ********************************************************)
+
+(* Note: OEIS sequence identifiers
+ P(n): A016777 "3n+1"
+ T(n): A155504 "(3h+1)*3^(k+1)"
+*)
+
+inductive P: predicate nat ≝
+ | p1: P 1
+ | p2: ∀i,j. T i → P j → P (i + j)
+with T: predicate nat ≝
+ | t1: ∀i. P i → T (i * 3)
+ | t2: ∀i. T i → T (i * 3)
+.
+
+inductive S: predicate nat ≝
+ | s1: ∀i. P i → S (i * 2)
+ | s2: ∀i. T i → S (i * 2)
+.
+
+inductive Q: predicate nat ≝
+ | q1: ∀i. P i → Q (i * 2 + 3)
+ | q2: ∀i. Q i → Q (i * 3)
+.
+
+(* Basic eliminators ********************************************************)
+
+axiom p_ind: ∀R:predicate nat. R 1 →
+ (∀i,j. T i → R j → R (i + j)) →
+ ∀j. P j → R j.
+
+axiom t_ind: ∀R:predicate nat.
+ (∀i. P i → R (i * 3)) →
+ (∀i. R i → R (i * 3)) →
+ ∀i. T i → R i.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact p_inv_O_aux: ∀i. P i → i = 0 → False.
+#i #H @(p_ind … H) -i
+[ #H destruct
+| #i #j #_ #IH #H
+ elim (plus_inv_O3 … H) -H /2 width=1/
+]
+qed-.
+
+lemma p_inv_O: P 0 → False.
+/2 width=3 by p_inv_O_aux/ qed-.
+
+fact t_inv_O_aux: ∀i. T i → i = 0 → False.
+#i #H @(t_ind … H) -i #i #IH #H
+lapply (times_inv_S2_O3 … H) -H /2 width=1/
+/2 width=3 by p_inv_O_aux/
+qed-.
+
+lemma t_inv_O: T 0 → False.
+/2 width=3 by t_inv_O_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma t_3: T 3.
+/2 width=1/ qed.
+
+lemma p_pos: ∀i. P i → ∃k. i = k + 1.
+* /2 width=2/
+#H elim (p_inv_O … H)
+qed.
+
+lemma t_pos: ∀i. T i → ∃k. i = k + 1.
+* /2 width=2/
+#H elim (t_inv_O … H)
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "character/class.ma".
+
+(* CHARACTER CLASSES ********************************************************)
+
+(* Arithmetics of classes P and T *******************************************)
+
+lemma pt_inv_gen: ∀i.
+ (P i → ∃h. i = h * 3 + 1) ∧
+ (T i → ∃∃h,k. i = (h * 3 + 1) * 3 ^ (k + 1)).
+#i @(nat_elim1 … i) -i #i #IH
+@conj #H
+[ inversion H -H
+ [ #H destruct /2 width=2/
+ | #i0 #j0 #Hi0 #Hj0 #H destruct
+ elim (t_pos … Hi0) #i #H destruct
+ elim (p_pos … Hj0) #j #H destruct
+ elim (IH (i+1) ?) // #_ #H
+ elim (H Hi0) -H -Hi0 #hi #ki #H >H -H
+ elim (IH (j+1) ?) -IH // #H #_ -i
+ elim (H Hj0) -H -Hj0 #hj #H >H -j
+ <associative_plus >exp_n_m_plus_1 /2 width=2/
+ ]
+| @(T_inv_ind … H) -H #i0 #Hi0 #H destruct
+ [ elim (p_pos … Hi0) #i #H destruct
+ elim (IH (i+1) ?) -IH /2 width=1 by monotonic_le_plus_r/ #H #_
+ elim (H Hi0) -H -Hi0 #hi #H >H -i
+ @(ex1_2_intro … hi 0) //
+ | elim (t_pos … Hi0) #i #H destruct
+ elim (IH (i+1) ?) -IH /2 width=1 by monotonic_le_plus_r/ #_ #H
+ elim (H Hi0) -H -Hi0 #hi #ki #H >H -i
+ >associative_times <exp_n_m_plus_1 /2 width=3/
+ ]
+]
+qed-.
+
+theorem p_inv_gen: ∀i. P i → ∃h. i = h * 3 + 1.
+#i #Hi elim (pt_inv_gen i) /2 width=1/
+qed-.
+
+theorem t_inv_gen: ∀i. T i → ∃∃h,k. i = (h * 3 + 1) * 3 ^ (k + 1).
+#i #Hi elim (pt_inv_gen i) /2 width=1/
+qed-.
+
+theorem p_gen: ∀i. P (i * 3 + 1).
+#i @(nat_ind_plus … i) -i //
+#i #IHi >times_n_plus_1_m >associative_plus /2 width=1/
+qed.
+
+theorem t_gen: ∀i,j. T ((i * 3 + 1) * 3 ^ (j + 1)).
+#i #j @(nat_ind_plus … j) -j /2 width=1/
+#j #IH >exp_n_m_plus_1 <associative_times /2 width=1/
+qed.
+
+lemma pt_discr: ∀i. P i → T i → False.
+#i #Hp #Ht
+elim (p_inv_gen … Hp) -Hp #hp #Hp
+elim (t_inv_gen … Ht) -Ht #ht #kt #Ht destruct
+>exp_n_m_plus_1 in Ht; <associative_times #H
+elim (not_b_divides_nbr … H) -H //
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "character/class_pt.ma".
+
+(* TRIPLES OF CHARACTER CLASSES *********************************************)
+
+lemma not_p_pS: ∀i. P i → P (i + 1) → False.
+#i #Hi #HSi
+elim (p_inv_gen … Hi) -Hi #hi #Hi
+elim (p_inv_gen … HSi) -HSi #hSi #HSi destruct
+lapply (injective_plus_l … HSi) -HSi #H
+elim (not_b_divides_nbr … H) -H //
+qed-.
+
+lemma not_p_pSS: ∀i. P i → P (i + 2) → False.
+#i #Hi #HSi
+elim (p_inv_gen … Hi) -Hi #hi #Hi
+elim (p_inv_gen … HSi) -HSi #hSi #HSi destruct
+>plus_plus_comm_23 in HSi; #H
+lapply (injective_plus_l … H) -H #H
+elim (not_b_divides_nbr … H) -H //
+qed-.
+
+lemma not_p_tS: ∀i. P i → T (i + 1) → False.
+#i #Hp #Ht
+elim (p_inv_gen … Hp) -Hp #hp #Hp
+elim (t_inv_gen … Ht) -Ht #ht #kt #Ht destruct
+>exp_n_m_plus_1 in Ht; <associative_times >associative_plus #H
+elim (not_b_divides_nbr … H) -H //
+qed-.
--- /dev/null
+baseuri=cic:/matita/BTM
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* ?: MATITA SOURCE FILES
- * Suggested invocation to start formal specifications with:
- * - Patience on me to gain peace and perfection! -
- * 2008 September 22:
- * specification starts.
- *)
-
-include "preamble.ma".
-
-(* CHARACTER CLASSES ********************************************************)
-
-(* Note: OEIS sequence identifiers
- P(n): A016777 "3n+1"
- T(n): A155504 "(3h+1)*3^(k+1)"
-*)
-
-inductive P: predicate nat ≝
- | p1: P 1
- | p2: ∀i,j. T i → P j → P (i + j)
-with T: predicate nat ≝
- | t1: ∀i. P i → T (i * 3)
- | t2: ∀i. T i → T (i * 3)
-.
-
-inductive S: predicate nat ≝
- | s1: ∀i. P i → S (i * 2)
- | s2: ∀i. T i → S (i * 2)
-.
-
-inductive Q: predicate nat ≝
- | q1: ∀i. P i → Q (i * 2 + 3)
- | q2: ∀i. Q i → Q (i * 3)
-.
-
-(* Basic eliminators ********************************************************)
-
-axiom p_ind: ∀R:predicate nat. R 1 →
- (∀i,j. T i → R j → R (i + j)) →
- ∀j. P j → R j.
-
-axiom t_ind: ∀R:predicate nat.
- (∀i. P i → R (i * 3)) →
- (∀i. R i → R (i * 3)) →
- ∀i. T i → R i.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact p_inv_O_aux: ∀i. P i → i = 0 → False.
-#i #H @(p_ind … H) -i
-[ #H destruct
-| #i #j #_ #IH #H
- elim (plus_inv_O3 … H) -H /2 width=1/
-]
-qed-.
-
-lemma p_inv_O: P 0 → False.
-/2 width=3 by p_inv_O_aux/ qed-.
-
-fact t_inv_O_aux: ∀i. T i → i = 0 → False.
-#i #H @(t_ind … H) -i #i #IH #H
-lapply (times_inv_S2_O3 … H) -H /2 width=1/
-/2 width=3 by p_inv_O_aux/
-qed-.
-
-lemma t_inv_O: T 0 → False.
-/2 width=3 by t_inv_O_aux/ qed-.
-
-(* Basic properties *********************************************************)
-
-lemma t_3: T 3.
-/2 width=1/ qed.
-
-lemma p_pos: ∀i. P i → ∃k. i = k + 1.
-* /2 width=2/
-#H elim (p_inv_O … H)
-qed.
-
-lemma t_pos: ∀i. T i → ∃k. i = k + 1.
-* /2 width=2/
-#H elim (t_inv_O … H)
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "classes/class.ma".
-
-(* CHARACTER CLASSES ********************************************************)
-
-(* Arithmetics of classes P and T *******************************************)
-
-lemma pt_inv_gen: ∀i.
- (P i → ∃h. i = h * 3 + 1) ∧
- (T i → ∃∃h,k. i = (h * 3 + 1) * 3 ^ (k + 1)).
-#i @(nat_elim1 … i) -i #i #IH
-@conj #H
-[ inversion H -H
- [ #H destruct /2 width=2/
- | #i0 #j0 #Hi0 #Hj0 #H destruct
- elim (t_pos … Hi0) #i #H destruct
- elim (p_pos … Hj0) #j #H destruct
- elim (IH (i+1) ?) // #_ #H
- elim (H Hi0) -H -Hi0 #hi #ki #H >H -H
- elim (IH (j+1) ?) -IH // #H #_ -i
- elim (H Hj0) -H -Hj0 #hj #H >H -j
- <associative_plus >exp_n_m_plus_1 /2 width=2/
- ]
-| @(T_inv_ind … H) -H #i0 #Hi0 #H destruct
- [ elim (p_pos … Hi0) #i #H destruct
- elim (IH (i+1) ?) -IH /2 width=1 by monotonic_le_plus_r/ #H #_
- elim (H Hi0) -H -Hi0 #hi #H >H -i
- @(ex1_2_intro … hi 0) //
- | elim (t_pos … Hi0) #i #H destruct
- elim (IH (i+1) ?) -IH /2 width=1 by monotonic_le_plus_r/ #_ #H
- elim (H Hi0) -H -Hi0 #hi #ki #H >H -i
- >associative_times <exp_n_m_plus_1 /2 width=3/
- ]
-]
-qed-.
-
-theorem p_inv_gen: ∀i. P i → ∃h. i = h * 3 + 1.
-#i #Hi elim (pt_inv_gen i) /2 width=1/
-qed-.
-
-theorem t_inv_gen: ∀i. T i → ∃∃h,k. i = (h * 3 + 1) * 3 ^ (k + 1).
-#i #Hi elim (pt_inv_gen i) /2 width=1/
-qed-.
-
-theorem p_gen: ∀i. P (i * 3 + 1).
-#i @(nat_ind_plus … i) -i //
-#i #IHi >times_n_plus_1_m >associative_plus /2 width=1/
-qed.
-
-theorem t_gen: ∀i,j. T ((i * 3 + 1) * 3 ^ (j + 1)).
-#i #j @(nat_ind_plus … j) -j /2 width=1/
-#j #IH >exp_n_m_plus_1 <associative_times /2 width=1/
-qed.
-
-lemma pt_discr: ∀i. P i → T i → False.
-#i #Hp #Ht
-elim (p_inv_gen … Hp) -Hp #hp #Hp
-elim (t_inv_gen … Ht) -Ht #ht #kt #Ht destruct
->exp_n_m_plus_1 in Ht; <associative_times #H
-elim (not_b_divides_nbr … H) -H //
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "classes/class_pt.ma".
-
-(* TRIPLES OF CHARACTER CLASSES *********************************************)
-
-lemma not_p_pS: ∀i. P i → P (i + 1) → False.
-#i #Hi #HSi
-elim (p_inv_gen … Hi) -Hi #hi #Hi
-elim (p_inv_gen … HSi) -HSi #hSi #HSi destruct
-lapply (injective_plus_l … HSi) -HSi #H
-elim (not_b_divides_nbr … H) -H //
-qed-.
-
-lemma not_p_pSS: ∀i. P i → P (i + 2) → False.
-#i #Hi #HSi
-elim (p_inv_gen … Hi) -Hi #hi #Hi
-elim (p_inv_gen … HSi) -HSi #hSi #HSi destruct
->plus_plus_comm_23 in HSi; #H
-lapply (injective_plus_l … H) -H #H
-elim (not_b_divides_nbr … H) -H //
-qed-.
-
-lemma not_p_tS: ∀i. P i → T (i + 1) → False.
-#i #Hp #Ht
-elim (p_inv_gen … Hp) -Hp #hp #Hp
-elim (t_inv_gen … Ht) -Ht #ht #kt #Ht destruct
->exp_n_m_plus_1 in Ht; <associative_times >associative_plus #H
-elim (not_b_divides_nbr … H) -H //
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "arithmetics/exp.ma".
-include "../lambda_delta/ground_2/arith.ma".
-
-lemma plus_inv_O3: ∀m,n. n + m = 0 → n = 0 ∧ m = 0.
-#m * /2 width=1/ normalize
-#n #H destruct
-qed-.
-
-lemma times_inv_S2_O3: ∀m,n. n * (S m) = 0 → n = 0.
-#m #n <times_n_Sm #H
-elim (plus_inv_O3 … H) -H //
-qed-.
-
-lemma exp_n_m_plus_1: ∀n,m. n ^ (m + 1) = (n ^ m) * n.
-// qed.
-
-lemma times_n_plus_1_m: ∀n,m. (n + 1) * m = m + n * m.
-#n #m >distributive_times_plus_r //
-qed.
-
-lemma lt_plus_nmn_false: ∀m,n. n + m < n → False.
-#m #n elim n -n
-[ #H elim (lt_zero_false … H)
-| /3 width=1/
-]
-qed-.
-
-lemma not_b_divides_nbr: ∀b,r. 0 < r → r < b →
- ∀n,m. n * b + r = m * b → False.
-#b #r #Hr #Hrb #n elim n -n
-[ * normalize
- [ -Hrb #H destruct elim (lt_refl_false … Hr)
- | -Hr #m #H destruct
- elim (lt_plus_nmn_false … Hrb)
- ]
-| #n #IHn * normalize
- [ -IHn -Hrb #H destruct
- elim (plus_inv_O3 … H) -H #_ #H destruct
- elim (lt_refl_false … Hr)
- | -Hr -Hrb /3 width=3/
- ]
-]
-qed-.
+++ /dev/null
-baseuri=cic:/matita/character
projects / helm.git / commitdiff