From 35e633b9f0e0ae36641e0f6d29aaed7ceb4e3c75 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 23 Aug 2012 17:15:24 +0000 Subject: [PATCH] we updated the contribution porting it to the new matita ... --- matita/matita/contribs/character/Makefile | 18 --- .../contribs/character/classes/class.ma | 95 ++++++++++++++++ .../contribs/character/classes/class_pt.ma | 74 ++++++++++++ .../contribs/character/classes/props_pt.ma | 107 ------------------ .../character/classes/{defs.ma => triple.ma} | 41 ++++--- matita/matita/contribs/character/depends | 5 - matita/matita/contribs/character/preamble.ma | 93 ++++++--------- 7 files changed, 231 insertions(+), 202 deletions(-) delete mode 100644 matita/matita/contribs/character/Makefile create mode 100644 matita/matita/contribs/character/classes/class.ma create mode 100644 matita/matita/contribs/character/classes/class_pt.ma delete mode 100644 matita/matita/contribs/character/classes/props_pt.ma rename matita/matita/contribs/character/classes/{defs.ma => triple.ma} (53%) delete mode 100644 matita/matita/contribs/character/depends diff --git a/matita/matita/contribs/character/Makefile b/matita/matita/contribs/character/Makefile deleted file mode 100644 index 8262cd704..000000000 --- a/matita/matita/contribs/character/Makefile +++ /dev/null @@ -1,18 +0,0 @@ -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 diff --git a/matita/matita/contribs/character/classes/class.ma b/matita/matita/contribs/character/classes/class.ma new file mode 100644 index 000000000..3cc8d08a7 --- /dev/null +++ b/matita/matita/contribs/character/classes/class.ma @@ -0,0 +1,95 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/matita/matita/contribs/character/classes/class_pt.ma b/matita/matita/contribs/character/classes/class_pt.ma new file mode 100644 index 000000000..2533674df --- /dev/null +++ b/matita/matita/contribs/character/classes/class_pt.ma @@ -0,0 +1,74 @@ +(**************************************************************************) +(* ___ *) +(* ||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 + 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 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 exp_n_m_plus_1 in Ht; 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. diff --git a/matita/matita/contribs/character/classes/defs.ma b/matita/matita/contribs/character/classes/triple.ma similarity index 53% rename from matita/matita/contribs/character/classes/defs.ma rename to matita/matita/contribs/character/classes/triple.ma index 8283373db..6b85df2a0 100644 --- a/matita/matita/contribs/character/classes/defs.ma +++ b/matita/matita/contribs/character/classes/triple.ma @@ -12,22 +12,31 @@ (* *) (**************************************************************************) -include "preamble.ma". +include "classes/class_pt.ma". -(* NOTE: OEIS sequence identifiers - P(n): A016777 "3n+1" - T(n): A155504 "(3h+1)*3^(k+1)" -*) +(* TRIPLES OF CHARACTER CLASSES *********************************************) -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) -. +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-. -inductive S: nat → Prop ≝ - | s1: ∀i. P i → S (i * 2) - | s2: ∀i. T i → S (i * 2) -. +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_plus #H +elim (not_b_divides_nbr … H) -H // +qed-. diff --git a/matita/matita/contribs/character/depends b/matita/matita/contribs/character/depends deleted file mode 100644 index 7079205b1..000000000 --- a/matita/matita/contribs/character/depends +++ /dev/null @@ -1,5 +0,0 @@ -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 diff --git a/matita/matita/contribs/character/preamble.ma b/matita/matita/contribs/character/preamble.ma index e2656f6c2..8d674d3e9 100644 --- a/matita/matita/contribs/character/preamble.ma +++ b/matita/matita/contribs/character/preamble.ma @@ -12,65 +12,46 @@ (* *) (**************************************************************************) -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 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-. -- 2.39.2