From 9f7f534a11f08bb66815eddf957959eb0eaeb71f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 24 Aug 2012 14:45:02 +0000 Subject: [PATCH] some renaming ... --- matita/matita/contribs/BTM/arith.ma | 76 +++++++++++++++++++ .../classes => BTM/character}/class.ma | 4 +- .../classes => BTM/character}/class_pt.ma | 2 +- .../classes => BTM/character}/triple.ma | 2 +- matita/matita/contribs/BTM/root | 1 + matita/matita/contribs/character/preamble.ma | 57 -------------- matita/matita/contribs/character/root | 1 - 7 files changed, 81 insertions(+), 62 deletions(-) create mode 100644 matita/matita/contribs/BTM/arith.ma rename matita/matita/contribs/{character/classes => BTM/character}/class.ma (98%) rename matita/matita/contribs/{character/classes => BTM/character}/class_pt.ma (98%) rename matita/matita/contribs/{character/classes => BTM/character}/triple.ma (98%) create mode 100644 matita/matita/contribs/BTM/root delete mode 100644 matita/matita/contribs/character/preamble.ma delete mode 100644 matita/matita/contribs/character/root diff --git a/matita/matita/contribs/BTM/arith.ma b/matita/matita/contribs/BTM/arith.ma new file mode 100644 index 000000000..e2656f6c2 --- /dev/null +++ b/matita/matita/contribs/BTM/arith.ma @@ -0,0 +1,76 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/matita/matita/contribs/character/classes/class.ma b/matita/matita/contribs/BTM/character/class.ma similarity index 98% rename from matita/matita/contribs/character/classes/class.ma rename to matita/matita/contribs/BTM/character/class.ma index 3cc8d08a7..4ed0330fb 100644 --- a/matita/matita/contribs/character/classes/class.ma +++ b/matita/matita/contribs/BTM/character/class.ma @@ -12,14 +12,14 @@ (* *) (**************************************************************************) -(* ?: MATITA SOURCE FILES +(* 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 "preamble.ma". +include "arith.ma". (* CHARACTER CLASSES ********************************************************) diff --git a/matita/matita/contribs/character/classes/class_pt.ma b/matita/matita/contribs/BTM/character/class_pt.ma similarity index 98% rename from matita/matita/contribs/character/classes/class_pt.ma rename to matita/matita/contribs/BTM/character/class_pt.ma index 2533674df..24ad9a24e 100644 --- a/matita/matita/contribs/character/classes/class_pt.ma +++ b/matita/matita/contribs/BTM/character/class_pt.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "classes/class.ma". +include "character/class.ma". (* CHARACTER CLASSES ********************************************************) diff --git a/matita/matita/contribs/character/classes/triple.ma b/matita/matita/contribs/BTM/character/triple.ma similarity index 98% rename from matita/matita/contribs/character/classes/triple.ma rename to matita/matita/contribs/BTM/character/triple.ma index 6b85df2a0..272b7ffe2 100644 --- a/matita/matita/contribs/character/classes/triple.ma +++ b/matita/matita/contribs/BTM/character/triple.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "classes/class_pt.ma". +include "character/class_pt.ma". (* TRIPLES OF CHARACTER CLASSES *********************************************) diff --git a/matita/matita/contribs/BTM/root b/matita/matita/contribs/BTM/root new file mode 100644 index 000000000..d385301e7 --- /dev/null +++ b/matita/matita/contribs/BTM/root @@ -0,0 +1 @@ +baseuri=cic:/matita/BTM diff --git a/matita/matita/contribs/character/preamble.ma b/matita/matita/contribs/character/preamble.ma deleted file mode 100644 index 8d674d3e9..000000000 --- a/matita/matita/contribs/character/preamble.ma +++ /dev/null @@ -1,57 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 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-. diff --git a/matita/matita/contribs/character/root b/matita/matita/contribs/character/root deleted file mode 100644 index 059686b38..000000000 --- a/matita/matita/contribs/character/root +++ /dev/null @@ -1 +0,0 @@ -baseuri=cic:/matita/character -- 2.39.2