+++ /dev/null
-BIN=../../
-
-DIR=$(shell basename $$PWD)
-
-H=@
-
-$(DIR) all:
- $(H)$(BIN)matitac
-$(DIR).opt opt all.opt:
- $(H)$(BIN)matitac.opt
-clean:
- $(H)$(BIN)matitaclean
-clean.opt:
- $(H)$(BIN)matitaclean.opt
-depend:
- $(H)$(BIN)matitadep
-depend.opt:
- $(H)$(BIN)matitadep.opt
--- /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 "preamble.ma".
-
-(* NOTE: OEIS sequence identifiers
- P(n): A016777 "3n+1"
- T(n): A155504 "(3h+1)*3^(k+1)"
-*)
-
-inductive P: nat → Prop ≝
- | p1: P 1
- | p2: ∀i,j. T i → P j → P (i + j)
-with T: nat → Prop ≝
- | t1: ∀i. P i → T (i * 3)
- | t2: ∀i. T i → T (i * 3)
-.
-
-inductive S: nat → Prop ≝
- | s1: ∀i. P i → S (i * 2)
- | s2: ∀i. T i → S (i * 2)
-.
+++ /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/defs.ma".
-
-theorem p_inv_O: P 0 → False.
- intros; inversion H;intros;
- [apply (not_eq_O_S ? H1)
- |autobatch.
- ]
-qed.
-
-theorem t_inv_O: T 0 → False.
- intros; inversion H; clear H; intros;
- [ lapply linear times_inv_O3_S to H1; destruct; autobatch depth = 2
- | lapply linear times_inv_O3_S to H2; destruct; autobatch depth = 2
- ].
-qed.
-
-theorem p_pos: ∀i. P i → ∃k. i = S k.
- intros 1; elim i 0; clear i; intros;
- [ lapply linear p_inv_O to H; decompose
- | autobatch depth = 2
- ].
-qed.
-
-theorem t_pos: ∀i. T i → ∃k. i = S k.
- intros 1; elim i names 0; clear i; intros;
- [ lapply linear t_inv_O to H; decompose
- | autobatch depth = 2
- ].
-qed.
-
-theorem t_1: T 1 → False.
- intros; inversion H; clear H; intros;
- [ lapply not_3_divides_1 to H1; decompose
- | lapply not_3_divides_1 to H2; decompose
- ].
-qed.
-
-theorem t_3: T 3.
- change in ⊢ (? %) with (1 * 3);
- autobatch depth = 2.
-qed.
-
-theorem pt_inv_gen: ∀i.
- (P i → ∃h. i = S (h * 3)) ∧
- (T i → ∃h,k. i = S (h * 3) * 3 \sup (S k)).
- intros 1; elim i using wf_nat_ind names 0; clear i; intros; split; intros;
- [ lapply linear p_inv_O to H; decompose
- | lapply linear t_inv_O to H; decompose
- | inversion H1; clear H1; intros;
- [ destruct; autobatch paramodulation
- | clear H3; lapply t_pos to H1; lapply p_pos to H2; decompose; destruct;
- lapply linear plus_inv_S_S_S to H4; decompose;
- lapply H to H4; lapply H to H3; clear H H4 H3; decompose; clear H3 H4;
- lapply linear H to H2; lapply linear H5 to H1; decompose;
- rewrite > H; rewrite > H2; clear H H2;
- rewrite < plus_n_Sm; rewrite > times_exp_x_y_Sz; autobatch depth = 2
- ]
- | inversion H1; clear H1; intros;
- [ lapply linear times_inv_S_m_SS to H2 as H0;
- lapply linear H to H0; decompose; clear H2;
- lapply linear H to H1; decompose; destruct;
- autobatch depth = 4
- | clear H2; lapply linear times_inv_S_m_SS to H3 as H0;
- lapply linear H to H0; decompose; clear H;
- lapply linear H2 to H1; decompose; destruct;
- autobatch depth = 4
- ]
- ].
-qed.
-
-theorem p_inv_gen: ∀i. P i → ∃h. i = S (h * 3).
- intros; lapply depth = 1 pt_inv_gen; decompose;
- lapply linear H1 to H as H0; autobatch depth = 1.
-qed.
-
-theorem t_inv_gen: ∀i. T i → ∃h,k. i = (S (h * 3)) * 3 \sup (S k).
- intros; lapply depth = 1 pt_inv_gen; decompose;
- lapply linear H2 to H as H0; autobatch depth = 2.
-qed.
-
-theorem p_gen: ∀i. P (S (i * 3)).
- intros; elim i names 0; clear i; intros;
- [ simplify; autobatch depth = 2
- | rewrite > plus_3_S3n ; autobatch depth = 2
- ].
-qed.
-
-theorem t_gen: ∀i,j. T (S (i * 3) * 3 \sup (S j)).
- intros; elim j names 0; clear j; intros;
- [ simplify in ⊢ (? (? ? %)); autobatch depth = 2
- | rewrite > times_exp_x_y_Sz; autobatch depth = 2
- ].
-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
-preamble.ma nat/exp.ma nat/relevant_equations.ma
-classes/defs.ma preamble.ma
-classes/props_pt.ma classes/defs.ma
-nat/exp.ma
-nat/relevant_equations.ma
(* *)
(**************************************************************************)
-include "nat/exp.ma".
-include "nat/relevant_equations.ma".
+include "arithmetics/exp.ma".
+include "../lambda_delta/ground_2/arith.ma".
-alias num (instance 0) = "natural number".
+lemma plus_inv_O3: ∀m,n. n + m = 0 → n = 0 ∧ m = 0.
+#m * /2 width=1/ normalize
+#n #H destruct
+qed-.
-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.
+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-.
-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.
+lemma exp_n_m_plus_1: ∀n,m. n ^ (m + 1) = (n ^ m) * n.
+// 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.
+lemma times_n_plus_1_m: ∀n,m. (n + 1) * m = m + n * m.
+#n #m >distributive_times_plus_r //
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.
+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-.
projects / helm.git / commitdiff