From 5102e7f780e83c7fef1d3826f81dfd37ee4028bc Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 11 Oct 2015 14:39:30 +0000 Subject: [PATCH] ground_2 milestone: multiple relocation with lists of booleans basic_2: simplified formalization starts: partial commit of the grammar component --- .../{multiple => etc_new/frees}/frees.ma | 0 .../frees}/frees_append.ma | 0 .../{multiple => etc_new/frees}/frees_lift.ma | 0 .../{multiple => etc_new/frees}/frees_lreq.ma | 0 .../{grammar => etc_new/lenv}/lenv_append.ma | 58 +++-- .../{grammar => etc_new/lenv}/lenv_length.ma | 41 ++-- .../lambdadelta/basic_2/grammar/item.ma | 4 +- .../lambdadelta/basic_2/grammar/lreq.ma | 19 +- .../basic_2/notation/relations/freestar_3.ma | 19 ++ .../lambdadelta/ground_2/lib/arith.ma | 9 + .../contribs/lambdadelta/ground_2/lib/list.ma | 8 + .../ground_2/notation/relations/rafter_3.ma | 19 ++ .../notation/relations/rat_3.ma | 2 +- .../notation/relations/rminus_3.ma | 2 +- .../ground_2/notation/relations/runion_3.ma | 19 ++ .../mr2.ma => ground_2/relocation/mr2_at.ma} | 27 ++- .../relocation}/mr2_minus.ma | 15 +- .../relocation}/mr2_plus.ma | 11 +- .../relocation/trace.ma} | 17 +- .../ground_2/relocation/trace_after.ma | 205 ++++++++++++++++++ .../ground_2/relocation/trace_at.ma | 193 +++++++++++++++++ .../ground_2/relocation/trace_sor.ma | 33 +++ .../lambdadelta/ground_2/web/ground_2.ldw.xml | 3 + .../lambdadelta/ground_2/web/ground_2_src.tbl | 11 +- .../lambdadelta/ground_2/ynat/ynat_le.ma | 4 +- .../lambdadelta/ground_2/ynat/ynat_lt.ma | 18 +- .../lambdadelta/ground_2/ynat/ynat_plus.ma | 4 +- .../lambdadelta/ground_2/ynat/ynat_pred.ma | 8 +- .../lambdadelta/ground_2/ynat/ynat_succ.ma | 8 +- matita/matita/predefined_virtuals.ml | 2 +- 30 files changed, 652 insertions(+), 107 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{multiple => etc_new/frees}/frees.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{multiple => etc_new/frees}/frees_append.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{multiple => etc_new/frees}/frees_lift.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{multiple => etc_new/frees}/frees_lreq.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{grammar => etc_new/lenv}/lenv_append.ma (74%) rename matita/matita/contribs/lambdadelta/basic_2/{grammar => etc_new/lenv}/lenv_length.ma (66%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/freestar_3.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/relations/rafter_3.ma rename matita/matita/contribs/lambdadelta/{basic_2 => ground_2}/notation/relations/rat_3.ma (94%) rename matita/matita/contribs/lambdadelta/{basic_2 => ground_2}/notation/relations/rminus_3.ma (94%) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/relations/runion_3.ma rename matita/matita/contribs/lambdadelta/{basic_2/multiple/mr2.ma => ground_2/relocation/mr2_at.ma} (79%) rename matita/matita/contribs/lambdadelta/{basic_2/multiple => ground_2/relocation}/mr2_minus.ma (88%) rename matita/matita/contribs/lambdadelta/{basic_2/multiple => ground_2/relocation}/mr2_plus.ma (89%) rename matita/matita/contribs/lambdadelta/{basic_2/multiple/mr2_mr2.ma => ground_2/relocation/trace.ma} (65%) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/trace_after.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sor.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/multiple/frees.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_append.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_append.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/multiple/frees_append.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_append.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lift.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lift.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lreq.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lreq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lreq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_append.ma similarity index 74% rename from matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_append.ma index 0afb82db5..4f5f26fc9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_append.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "ground_2/notation/functions/append_2.ma". +include "ground_2/ynat/ynat_plus.ma". include "basic_2/notation/functions/snbind2_3.ma". include "basic_2/notation/functions/snabbr_2.ma". include "basic_2/notation/functions/snabst_2.ma". @@ -41,19 +42,27 @@ definition d_appendable_sn: predicate (lenv→relation term) ≝ λR. (* Basic properties *********************************************************) +lemma append_atom: ∀L. L @@ ⋆ = L. +// qed. + +lemma append_pair: ∀I,L,K,V. L @@ (K.ⓑ{I}V) = (L @@ K).ⓑ{I}V. +// qed. + lemma append_atom_sn: ∀L. ⋆ @@ L = L. -#L elim L -L normalize // +#L elim L -L // +#L #I #V >append_pair // qed. lemma append_assoc: associative … append. -#L1 #L2 #L3 elim L3 -L3 normalize // +#L1 #L2 #L3 elim L3 -L3 // qed. lemma append_length: ∀L1,L2. |L1 @@ L2| = |L1| + |L2|. -#L1 #L2 elim L2 -L2 normalize // +#L1 #L2 elim L2 -L2 // +#L2 #I #V2 >append_pair >length_pair >length_pair // qed. -lemma ltail_length: ∀I,L,V. |ⓑ{I}V.L| = |L| + 1. +lemma ltail_length: ∀I,L,V. |ⓑ{I}V.L| = ⫯|L|. #I #L #V >append_length // qed. @@ -70,13 +79,15 @@ qed-. lemma append_inj_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| → L1 = L2 ∧ K1 = K2. #K1 elim K1 -K1 -[ * normalize /2 width=1 by conj/ - #K2 #I2 #V2 #L1 #L2 #_ length_atom >length_pair + #H elim (ysucc_inv_O_sn … H) +| #K1 #I1 #V1 #IH * + [ #L1 #L2 #_ >length_atom >length_pair + #H elim (ysucc_inv_O_dx … H) | #K2 #I2 #V2 #L1 #L2 #H1 #H2 elim (destruct_lpair_lpair_aux … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *) - elim (IH … H1) -IH -H1 /2 width=1 by conj/ + elim (IH … H1) -IH -H1 /3 width=1 by ysucc_inv_inj, conj/ ] ] qed-. @@ -85,15 +96,17 @@ qed-. lemma append_inj_dx: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |L1| = |L2| → L1 = L2 ∧ K1 = K2. #K1 elim K1 -K1 -[ * normalize /2 width=1 by conj/ - #K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct - normalize in H2; >append_length in H2; #H - elim (plus_xySz_x_false … H) -| #K1 #I1 #V1 #IH * normalize - [ #L1 #L2 #H1 #H2 destruct - normalize in H2; >append_length in H2; #H - elim (plus_xySz_x_false … (sym_eq … H)) - | #K2 #I2 #V2 #L1 #L2 #H1 #H2 +[ * /2 width=1 by conj/ + #K2 #I2 #V2 #L1 #L2 >append_atom >append_pair #H destruct + >length_pair >append_length append_pair >append_atom #H destruct + >length_pair >append_length append_pair >append_pair #H1 #H2 elim (destruct_lpair_lpair_aux … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *) elim (IH … H1) -IH -H1 /2 width=1 by conj/ ] @@ -108,13 +121,13 @@ lemma append_inv_pair_dx: ∀I,L,K,V. L @@ K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V. #I #L #K #V #H elim (append_inj_dx … (⋆.ⓑ{I}V) … H) // qed-. -lemma length_inv_pos_dx_ltail: ∀L,l. |L| = l + 1 → +lemma length_inv_pos_dx_ltail: ∀L,l. |L| = ⫯l → ∃∃I,K,V. |K| = l & L = ⓑ{I}V.K. #Y #l #H elim (length_inv_pos_dx … H) -H #I #L #V #Hl #HLK destruct elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/ qed-. -lemma length_inv_pos_sn_ltail: ∀L,l. l + 1 = |L| → +lemma length_inv_pos_sn_ltail: ∀L,l. ⫯l = |L| → ∃∃I,K,V. l = |K| & L = ⓑ{I}V.K. #Y #l #H elim (length_inv_pos_sn … H) -H #I #L #V #Hl #HLK destruct elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/ @@ -126,6 +139,7 @@ qed-. lemma lenv_ind_alt: ∀R:predicate lenv. R (⋆) → (∀I,L,T. R L → R (ⓑ{I}T.L)) → ∀L. R L. -#R #IH1 #IH2 #L @(f_ind … length … L) -L #x #IHx * // -IH1 -#L #I #V normalize #H destruct elim (lpair_ltail L I V) /3 width=1 by/ +#R #IH1 #IH2 #L @(ynat_f_ind … length … L) -L #x #IHx * // -IH1 +#L #I #V #H destruct elim (lpair_ltail L I V) +/4 width=1 by monotonic_ylt_plus_sn/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_length.ma similarity index 66% rename from matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_length.ma index 7c31b59e7..7a0cdfc92 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_length.ma @@ -12,41 +12,48 @@ (* *) (**************************************************************************) +include "ground_2/ynat/ynat_lt.ma". include "basic_2/grammar/lenv.ma". (* LENGTH OF A LOCAL ENVIRONMENT ********************************************) let rec length L ≝ match L with [ LAtom ⇒ 0 -| LPair L _ _ ⇒ length L + 1 +| LPair L _ _ ⇒ ⫯(length L) ]. interpretation "length (local environment)" 'card L = (length L). +(* Basic properties *********************************************************) + +lemma length_atom: |⋆| = 0. +// qed. + +lemma length_pair: ∀I,L,V. |L.ⓑ{I}V| = ⫯|L|. +// qed. + +lemma length_inj: ∀L. |L| < ∞. +#L elim L -L /2 width=1 by ylt_succ_Y/ +qed. + (* Basic inversion lemmas ***************************************************) lemma length_inv_zero_dx: ∀L. |L| = 0 → L = ⋆. -* // #L #I #V normalize length_pair +#H elim (ysucc_inv_O_dx … H) qed-. -lemma length_inv_zero_sn: ∀L. 0 = |L| → L = ⋆. -* // #L #I #V normalize length_atom #H elim (ysucc_inv_O_sn … H) qed-. -lemma length_inv_pos_sn: ∀l,L. l + 1 = |L| → +lemma length_inv_pos_sn: ∀l,L. ⫯l = |L| → ∃∃I,K,V. l = |K| & L = K. ⓑ{I}V. -#l * -[ normalize length_pair >length_pair #H + lapply (ysucc_inv_inj … H) -H #HL12 + elim (ynat_cases l) /3 width=1 by lreq_zero/ + * /3 width=1 by lreq_succ/ +| #H elim (ysucc_inv_O_dx … H) +] qed. lemma lreq_sym: ∀l,m. symmetric … (lreq l m). @@ -168,14 +171,14 @@ qed-. lemma lreq_inv_succ2: ∀I2,K2,L1,V2,l,m. L1 ⩬[l, m] K2.ⓑ{I2}V2 → 0 < l → ∃∃I1,K1,V1. K1 ⩬[⫰l, m] K2 & L1 = K1.ⓑ{I1}V1. -#I2 #K2 #L1 #V2 #l #m #H #Hl elim (lreq_inv_succ1 … (lreq_sym … H)) -H +#I2 #K2 #L1 #V2 #l #m #H #Hl elim (lreq_inv_succ1 … (lreq_sym … H)) -H /3 width=5 by lreq_sym, ex2_3_intro/ qed-. (* Basic forward lemmas *****************************************************) lemma lreq_fwd_length: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → |L1| = |L2|. -#L1 #L2 #l #m #H elim H -L1 -L2 -l -m normalize // +#L1 #L2 #l #m #H elim H -L1 -L2 -l -m // qed-. (* Advanced inversion lemmas ************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/freestar_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/freestar_3.ma new file mode 100644 index 000000000..d9cfb81bd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/freestar_3.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( L ⊢ break 𝐅 * ⦃ term 46 T ⦄ ≡ break term 46 f )" + non associative with precedence 45 + for @{ 'FreeStar $L $T $f }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index b23fb9de8..5f8451a27 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -12,11 +12,17 @@ (* *) (**************************************************************************) +include "ground_2/notation/functions/successor_1.ma". +include "ground_2/notation/functions/predecessor_1.ma". include "arithmetics/nat.ma". include "ground_2/lib/star.ma". (* ARITHMETICAL PROPERTIES **************************************************) +interpretation "nat successor" 'Successor m = (S m). + +interpretation "nat predecessor" 'Predecessor m = (pred m). + (* Iota equations ***********************************************************) lemma pred_O: pred 0 = 0. @@ -133,6 +139,9 @@ lemma lt_zero_false: ∀n. n < 0 → ⊥. #n #H elim (lt_to_not_le … H) -H /2 width=1 by/ qed-. +lemma lt_le_false: ∀x,y. x < y → y ≤ x → ⊥. +/3 width=4 by lt_refl_false, lt_to_le_to_lt/ qed-. + lemma pred_inv_refl: ∀m. pred m = m → m = 0. * // normalize #m #H elim (lt_refl_false m) // qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma index 9355f9c56..e72b54531 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma @@ -28,6 +28,14 @@ interpretation "nil (list)" 'Nil = (nil ?). interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl). +let rec length (A:Type[0]) (l:list A) on l ≝ match l with +[ nil ⇒ 0 +| cons _ l ⇒ length A l + 1 +]. + +interpretation "length (list)" + 'card l = (length ? l). + let rec all A (R:predicate A) (l:list A) on l ≝ match l with [ nil ⇒ ⊤ diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rafter_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rafter_3.ma new file mode 100644 index 000000000..d36582711 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rafter_3.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( f1 ⊚ break term 46 f2 ≡ break term 46 f )" + non associative with precedence 45 + for @{ 'RAfter $f1 $f2 $f }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rat_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rat_3.ma similarity index 94% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/rat_3.ma rename to matita/matita/contribs/lambdadelta/ground_2/notation/relations/rat_3.ma index a63dc95f2..8b99f61cd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rat_3.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rat_3.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) notation "hvbox( @ ⦃ term 46 T1 , break term 46 f ⦄ ≡ break term 46 T2 )" non associative with precedence 45 diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rminus_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rminus_3.ma similarity index 94% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/rminus_3.ma rename to matita/matita/contribs/lambdadelta/ground_2/notation/relations/rminus_3.ma index c896a982f..1d397e536 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rminus_3.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rminus_3.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) notation "hvbox( T1 ▭ break term 46 T2 ≡ break term 46 T )" non associative with precedence 45 diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/runion_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/runion_3.ma new file mode 100644 index 000000000..16120c08d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/runion_3.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( L1 ⋓ break term 46 L2 ≡ break term 46 L )" + non associative with precedence 45 + for @{ 'RUnion $L1 $L2 $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_at.ma similarity index 79% rename from matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma rename to matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_at.ma index 71869b02b..b3517a77b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_at.ma @@ -12,17 +12,16 @@ (* *) (**************************************************************************) -include "ground_2/ynat/ynat_lt.ma". -include "basic_2/notation/relations/rat_3.ma". -include "basic_2/grammar/term_vector.ma". +include "ground_2/notation/relations/rat_3.ma". +include "ground_2/relocation/mr2.ma". (* MULTIPLE RELOCATION WITH PAIRS *******************************************) -inductive at: list2 ynat nat → relation nat ≝ +inductive at: mr2 → relation nat ≝ | at_nil: ∀i. at (◊) i i -| at_lt : ∀cs,l,m,i1,i2. yinj i1 < l → +| at_lt : ∀cs,l,m,i1,i2. i1 < l → at cs i1 i2 → at ({l, m} @ cs) i1 i2 -| at_ge : ∀cs,l,m,i1,i2. l ≤ yinj i1 → +| at_ge : ∀cs,l,m,i1,i2. l ≤ i1 → at cs (i1 + m) i2 → at ({l, m} @ cs) i1 i2 . @@ -62,12 +61,24 @@ lemma at_inv_cons_lt: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 → i1 < l → @⦃i1, cs⦄ ≡ i2. #cs #l #m #i1 #m2 #H elim (at_inv_cons … H) -H * // #Hli1 #_ #Hi1l -elim (ylt_yle_false … Hi1l Hli1) +elim (lt_le_false … Hi1l Hli1) qed-. lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 → l ≤ i1 → @⦃i1 + m, cs⦄ ≡ i2. #cs #l #m #i1 #m2 #H elim (at_inv_cons … H) -H * // #Hi1l #_ #Hli1 -elim (ylt_yle_false … Hi1l Hli1) +elim (lt_le_false … Hi1l Hli1) +qed-. + +(* Main properties **********************************************************) + +theorem at_mono: ∀cs,i,i1. @⦃i, cs⦄ ≡ i1 → ∀i2. @⦃i, cs⦄ ≡ i2 → i1 = i2. +#cs #i #i1 #H elim H -cs -i -i1 +[ #i #x #H <(at_inv_nil … H) -x // +| #cs #l #m #i #i1 #Hil #_ #IHi1 #x #H + lapply (at_inv_cons_lt … H Hil) -H -Hil /2 width=1 by/ +| #cs #l #m #i #i1 #Hli #_ #IHi1 #x #H + lapply (at_inv_cons_ge … H Hli) -H -Hli /2 width=1 by/ +] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_minus.ma similarity index 88% rename from matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma rename to matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_minus.ma index 3c5f8da5c..9fd40ad6b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_minus.ma @@ -12,17 +12,16 @@ (* *) (**************************************************************************) -include "ground_2/ynat/ynat_minus.ma". -include "basic_2/notation/relations/rminus_3.ma". -include "basic_2/multiple/mr2.ma". +include "ground_2/notation/relations/rminus_3.ma". +include "ground_2/relocation/mr2.ma". (* MULTIPLE RELOCATION WITH PAIRS *******************************************) -inductive minuss: nat → relation (list2 ynat nat) ≝ +inductive minuss: nat → relation mr2 ≝ | minuss_nil: ∀i. minuss i (◊) (◊) -| minuss_lt : ∀cs1,cs2,l,m,i. yinj i < l → minuss i cs1 cs2 → +| minuss_lt : ∀cs1,cs2,l,m,i. i < l → minuss i cs1 cs2 → minuss i ({l, m} @ cs1) ({l - i, m} @ cs2) -| minuss_ge : ∀cs1,cs2,l,m,i. l ≤ yinj i → minuss (m + i) cs1 cs2 → +| minuss_ge : ∀cs1,cs2,l,m,i. l ≤ i → minuss (m + i) cs1 cs2 → minuss i ({l, m} @ cs1) cs2 . @@ -64,12 +63,12 @@ lemma minuss_inv_cons1_ge: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 → l ≤ i → cs1 ▭ m + i ≡ cs2. #cs1 #cs2 #l #m #i #H elim (minuss_inv_cons1 … H) -H * // #cs #Hil #_ #_ #Hli -elim (ylt_yle_false … Hil Hli) +elim (lt_le_false … Hil Hli) qed-. lemma minuss_inv_cons1_lt: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 → i < l → ∃∃cs. cs1 ▭ i ≡ cs & cs2 = {l - i, m} @ cs. #cs1 #cs2 #l #m #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/ -#Hli #_ #Hil elim (ylt_yle_false … Hil Hli) +#Hli #_ #Hil elim (lt_le_false … Hil Hli) qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma similarity index 89% rename from matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma rename to matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma index 455b669be..11ffaa407 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma @@ -12,13 +12,12 @@ (* *) (**************************************************************************) -include "ground_2/ynat/ynat_plus.ma". -include "basic_2/multiple/mr2.ma". +include "ground_2/relocation/mr2.ma". (* MULTIPLE RELOCATION WITH PAIRS *******************************************) -let rec pluss (cs:list2 ynat nat) (i:nat) on cs ≝ match cs with -[ nil2 ⇒ ◊ +let rec pluss (cs:mr2) (i:nat) on cs ≝ match cs with +[ nil2 ⇒ ◊ | cons2 l m cs ⇒ {l + i, m} @ pluss cs i ]. @@ -28,7 +27,7 @@ interpretation "plus (multiple relocation with pairs)" (* Basic properties *********************************************************) lemma pluss_SO2: ∀l,m,cs. ({l, m} @ cs) + 1 = {⫯l, m} @ cs + 1. -// qed. +normalize // qed. (* Basic inversion lemmas ***************************************************) @@ -42,6 +41,6 @@ lemma pluss_inv_cons2: ∀i,l,m,cs2,cs. cs + i = {l, m} @ cs2 → #i #l #m #cs2 * [ normalize #H destruct | #l1 #m1 #cs1 whd in ⊢ (??%?→?); #H destruct - >yplus_minus_inj /2 width=3 by ex2_intro/ + (IH … Htl) -tl -cs1 -x // +| #cs1 #cs2 #x #_ #IH #y #H elim (after_inv_false1 … H) -H + #tly #H #Htl destruct >(IH … Htl) -cs1 -cs2 -x // +] +qed-. + +theorem after_inj: ∀cs1,x,cs. cs1 ⊚ x ≡ cs → ∀y. cs1 ⊚ y ≡ cs → x = y. +#cs1 #x #cs #H elim H -cs1 -x -cs +[ #y #H elim (after_inv_empty1 … H) -H // +| #cs1 #x #cs #_ #b #IH #y #H elim (after_inv_true1 … H) -H + #tly #tl #b0 #H1 #H2 #Htl destruct >(IH … Htl) -tl -cs1 -x // +| #cs1 #x #cs #_ #IH #y #H elim (after_inv_false1 … H) -H + #tl #H #Htl destruct >(IH … Htl) -tl -cs1 -x // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma new file mode 100644 index 000000000..f4b6f8d3a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma @@ -0,0 +1,193 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/notation/relations/rat_3.ma". +include "ground_2/relocation/trace.ma". + +(* RELOCATION TRACE *********************************************************) + +inductive at: trace → relation nat ≝ + | at_zero : ∀cs. at (Ⓣ @ cs) 0 0 + | at_succ : ∀cs,i,j. at cs i j → at (Ⓣ @ cs) (⫯i) (⫯j) + | at_false: ∀cs,i,j. at cs i j → at (Ⓕ @ cs) i (⫯j). + +interpretation "relocation (trace)" + 'RAt i1 cs i2 = (at cs i1 i2). + +(* Basic inversion lemmas ***************************************************) + +fact at_inv_empty_aux: ∀cs,i,j. @⦃i, cs⦄ ≡ j → cs = ◊ → ⊥. +#cs #i #j * -cs -i -j +#cs [2,3: #i #j #_ ] #H destruct +qed-. + +lemma at_inv_empty: ∀i,j. @⦃i, ◊⦄ ≡ j → ⊥. +/2 width=5 by at_inv_empty_aux/ qed-. + +fact at_inv_true_aux: ∀cs,i,j. @⦃i, cs⦄ ≡ j → ∀tl. cs = Ⓣ @ tl → + (i = 0 ∧ j = 0) ∨ + ∃∃i0,j0. i = ⫯i0 & j = ⫯j0 & @⦃i0, tl⦄ ≡ j0. +#cs #i #j * -cs -i -j +#cs [2,3: #i #j #Hij ] #tl #H destruct +/3 width=5 by ex3_2_intro, or_introl, or_intror, conj/ +qed-. + +lemma at_inv_true: ∀cs,i,j. @⦃i, Ⓣ @ cs⦄ ≡ j → + (i = 0 ∧ j = 0) ∨ + ∃∃i0,j0. i = ⫯i0 & j = ⫯j0 & @⦃i0, cs⦄ ≡ j0. +/2 width=3 by at_inv_true_aux/ qed-. + +lemma at_inv_true_zero_sn: ∀cs,j. @⦃0, Ⓣ @ cs⦄ ≡ j → j = 0. +#cs #j #H elim (at_inv_true … H) -H * // +#i0 #j0 #H destruct +qed-. + +lemma at_inv_true_zero_dx: ∀cs,i. @⦃i, Ⓣ @ cs⦄ ≡ 0 → i = 0. +#cs #i #H elim (at_inv_true … H) -H * // +#i0 #j0 #_ #H destruct +qed-. + +lemma at_inv_true_succ_sn: ∀cs,i,j. @⦃⫯i, Ⓣ @ cs⦄ ≡ j → + ∃∃j0. j = ⫯j0 & @⦃i, cs⦄ ≡ j0. +#cs #i #j #H elim (at_inv_true … H) -H * +[ #H destruct +| #i0 #j0 #H1 #H2 destruct /2 width=3 by ex2_intro/ +] +qed-. + +lemma at_inv_true_succ_dx: ∀cs,i,j. @⦃i, Ⓣ @ cs⦄ ≡ ⫯j → + ∃∃i0. i = ⫯i0 & @⦃i0, cs⦄ ≡ j. +#cs #i #j #H elim (at_inv_true … H) -H * +[ #_ #H destruct +| #i0 #j0 #H1 #H2 destruct /2 width=3 by ex2_intro/ +] +qed-. + +lemma at_inv_true_succ: ∀cs,i,j. @⦃⫯i, Ⓣ @ cs⦄ ≡ ⫯j → + @⦃i, cs⦄ ≡ j. +#cs #i #j #H elim (at_inv_true … H) -H * +[ #H destruct +| #i0 #j0 #H1 #H2 destruct // +] +qed-. + +lemma at_inv_true_O_S: ∀cs,j. @⦃0, Ⓣ @ cs⦄ ≡ ⫯j → ⊥. +#cs #j #H elim (at_inv_true … H) -H * +[ #_ #H destruct +| #i0 #j0 #H1 destruct +] +qed-. + +lemma at_inv_true_S_O: ∀cs,i. @⦃⫯i, Ⓣ @ cs⦄ ≡ 0 → ⊥. +#cs #i #H elim (at_inv_true … H) -H * +[ #H destruct +| #i0 #j0 #_ #H1 destruct +] +qed-. + +fact at_inv_false_aux: ∀cs,i,j. @⦃i, cs⦄ ≡ j → ∀tl. cs = Ⓕ @ tl → + ∃∃j0. j = ⫯j0 & @⦃i, tl⦄ ≡ j0. +#cs #i #j * -cs -i -j +#cs [2,3: #i #j #Hij ] #tl #H destruct +/2 width=3 by ex2_intro/ +qed-. + +lemma at_inv_false: ∀cs,i,j. @⦃i, Ⓕ @ cs⦄ ≡ j → + ∃∃j0. j = ⫯j0 & @⦃i, cs⦄ ≡ j0. +/2 width=3 by at_inv_false_aux/ qed-. + +lemma at_inv_false_S: ∀cs,i,j. @⦃i, Ⓕ @ cs⦄ ≡ ⫯j → @⦃i, cs⦄ ≡ j. +#cs #i #j #H elim (at_inv_false … H) -H +#j0 #H destruct // +qed-. + +lemma at_inv_false_O: ∀cs,i. @⦃i, Ⓕ @ cs⦄ ≡ 0 → ⊥. +#cs #i #H elim (at_inv_false … H) -H +#j0 #H destruct +qed-. + +(* Basic properties *********************************************************) + +lemma at_monotonic: ∀cs,i2,j2. @⦃i2, cs⦄ ≡ j2 → ∀i1. i1 < i2 → + ∃∃j1. @⦃i1, cs⦄ ≡ j1 & j1 < j2. +#cs #i2 #j2 #H elim H -cs -i2 -j2 +[ #cs #i1 #H elim (lt_zero_false … H) +| #cs #i #j #Hij #IH * /2 width=3 by ex2_intro, at_zero/ + #i1 #H lapply (lt_S_S_to_lt … H) -H + #H elim (IH … H) -i + #j1 #Hij1 #H /3 width=3 by le_S_S, ex2_intro, at_succ/ +| #cs #i #j #_ #IH #i1 #H elim (IH … H) -i + /3 width=3 by le_S_S, ex2_intro, at_false/ +] +qed-. + +lemma at_at_dec: ∀cs,i,j. Decidable (@⦃i, cs⦄ ≡ j). +#cs elim cs -cs [ | * #cs #IH ] +[ /3 width=3 by at_inv_empty, or_intror/ +| * [2: #i ] * [2,4: #j ] + [ elim (IH i j) -IH + /4 width=1 by at_inv_true_succ, at_succ, or_introl, or_intror/ + | -IH /3 width=3 by at_inv_true_O_S, or_intror/ + | -IH /3 width=3 by at_inv_true_S_O, or_intror/ + | -IH /2 width=1 by or_introl, at_zero/ + ] +| #i * [2: #j ] + [ elim (IH i j) -IH + /4 width=1 by at_inv_false_S, at_false, or_introl, or_intror/ + | -IH /3 width=3 by at_inv_false_O, or_intror/ + ] +] +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma at_increasing: ∀cs,i,j. @⦃i, cs⦄ ≡ j → i ≤ j. +#cs #i elim i -i // +#i0 #IHi #j #H elim (at_monotonic … H i0) -H +/3 width=3 by le_to_lt_to_lt/ +qed-. + +lemma at_length_lt: ∀cs,i,j. @⦃i, cs⦄ ≡ j → j < |cs|. +#cs elim cs -cs [ | * #cs #IH ] #i #j #H normalize +[ elim (at_inv_empty … H) +| elim (at_inv_true … H) * -H // + #i0 #j0 #H1 #H2 #Hij0 destruct /3 width=2 by le_S_S/ +| elim (at_inv_false … H) -H + #j0 #H #H0 destruct /3 width=2 by le_S_S/ +] +qed-. + +(* Main properties **********************************************************) + +theorem at_mono: ∀cs,i,j1. @⦃i, cs⦄ ≡ j1 → ∀j2. @⦃i, cs⦄ ≡ j2 → j1 = j2. +#cs #i #j1 #H elim H -cs -i -j1 +#cs [ |2,3: #i #j1 #_ #IH ] #j2 #H +[ lapply (at_inv_true_zero_sn … H) -H // +| elim (at_inv_true_succ_sn … H) -H + #j0 #H destruct #H >(IH … H) -cs -i -j1 // +| elim (at_inv_false … H) -H + #j0 #H destruct #H >(IH … H) -cs -i -j1 // +] +qed-. + +theorem at_inj: ∀cs,i1,j. @⦃i1, cs⦄ ≡ j → ∀i2. @⦃i2, cs⦄ ≡ j → i1 = i2. +#cs #i1 #j #H elim H -cs -i1 -j +#cs [ |2,3: #i1 #j #_ #IH ] #i2 #H +[ lapply (at_inv_true_zero_dx … H) -H // +| elim (at_inv_true_succ_dx … H) -H + #i0 #H destruct #H >(IH … H) -cs -i1 -j // +| elim (at_inv_false … H) -H + #j0 #H destruct #H >(IH … H) -cs -i1 -j0 // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sor.ma new file mode 100644 index 000000000..f4e79a6ce --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sor.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/notation/relations/runion_3.ma". +include "ground_2/relocation/trace.ma". + +(* RELOCATION TRACE *********************************************************) + +inductive sor: relation3 trace trace trace ≝ + | sor_empty: sor (◊) (◊) (◊) + | sor_inh : ∀cs1,cs2,cs. sor cs1 cs2 cs → + ∀b1,b2. sor (b1 @ cs1) (b2 @ cs2) ((b1 ∨ b2) @ cs). + +interpretation + "union (trace)" + 'RUnion L1 L2 L = (sor L2 L1 L). + +(* Basic properties *********************************************************) + +lemma sor_sym: ∀cs1,cs2,cs. cs1 ⋓ cs2 ≡ cs → cs2 ⋓ cs1 ≡ cs. +#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs /2 width=1 by sor_inh/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml index af06ffa1d..19c11b207 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml @@ -12,6 +12,9 @@ and its timeline. + + Multiple relocation with lists of booleans. + Natural numbers with infinity. diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl index 0ba823065..2c23eacc1 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl @@ -9,6 +9,15 @@ table { ] } ] + class "green" + [ { "multiple relocation" * } { + [ { "" * } { + [ "trace" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" * ] + [ "mr2" "mr2_at ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" * ] + } + ] + } + ] class "grass" [ { "natural numbers with infinity" * } { [ { "" * } { @@ -23,7 +32,7 @@ table { class "yellow" [ { "extensions to the library" * } { [ { "" * } { - [ "star" "lstar" "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? )" + [ "star" "lstar" "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ⫯? ) ( ⫰? )" "list ( ◊ ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )" * ] } diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma index 613a9793c..1a986f03c 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma @@ -83,7 +83,7 @@ qed-. (* Inversion lemmas on successor ********************************************) -fact yle_inv_succ1_aux: ∀x,y. x ≤ y → ∀m. x = ⫯m → m ≤ ⫰y ∧ ⫯⫰y = y. +fact yle_inv_succ1_aux: ∀x,y:ynat. x ≤ y → ∀m. x = ⫯m → m ≤ ⫰y ∧ ⫯⫰y = y. #x #y * -x -y [ #x #y #Hxy #m #H elim (ysucc_inv_inj_sn … H) -H #n #H1 #H2 destruct elim (le_inv_S1 … Hxy) -Hxy @@ -92,7 +92,7 @@ fact yle_inv_succ1_aux: ∀x,y. x ≤ y → ∀m. x = ⫯m → m ≤ ⫰y ∧ ] qed-. -lemma yle_inv_succ1: ∀m,y. ⫯m ≤ y → m ≤ ⫰y ∧ ⫯⫰y = y. +lemma yle_inv_succ1: ∀m,y:ynat. ⫯m ≤ y → m ≤ ⫰y ∧ ⫯⫰y = y. /2 width=3 by yle_inv_succ1_aux/ qed-. lemma yle_inv_succ: ∀m,n. ⫯m ≤ ⫯n → m ≤ n. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma index 2a9fbb515..664510dda 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma @@ -64,14 +64,14 @@ lemma ylt_inv_Y2: ∀x:ynat. x < ∞ → ∃n. x = yinj n. #H elim (ylt_inv_Y1 … H) qed-. -lemma ylt_inv_O1: ∀n. 0 < n → ⫯⫰n = n. +lemma ylt_inv_O1: ∀n:ynat. 0 < n → ⫯⫰n = n. * // #n #H lapply (ylt_inv_inj … H) -H normalize /3 width=1 by S_pred, eq_f/ qed-. (* Inversion lemmas on successor ********************************************) -fact ylt_inv_succ1_aux: ∀x,y. x < y → ∀m. x = ⫯m → m < ⫰y ∧ ⫯⫰y = y. +fact ylt_inv_succ1_aux: ∀x,y:ynat. x < y → ∀m. x = ⫯m → m < ⫰y ∧ ⫯⫰y = y. #x #y * -x -y [ #x #y #Hxy #m #H elim (ysucc_inv_inj_sn … H) -H #n #H1 #H2 destruct elim (le_inv_S1 … Hxy) -Hxy @@ -81,7 +81,7 @@ fact ylt_inv_succ1_aux: ∀x,y. x < y → ∀m. x = ⫯m → m < ⫰y ∧ ⫯⫰ ] qed-. -lemma ylt_inv_succ1: ∀m,y. ⫯m < y → m < ⫰y ∧ ⫯⫰y = y. +lemma ylt_inv_succ1: ∀m,y:ynat. ⫯m < y → m < ⫰y ∧ ⫯⫰y = y. /2 width=3 by ylt_inv_succ1_aux/ qed-. lemma ylt_inv_succ: ∀m,n. ⫯m < ⫯n → m < n. @@ -130,14 +130,14 @@ qed-. (* Basic properties *********************************************************) -lemma ylt_O1: ∀x. ⫯⫰x = x → 0 < x. +lemma ylt_O1: ∀x:ynat. ⫯⫰x = x → 0 < x. * // * /2 width=1 by ylt_inj/ normalize #H destruct qed. (* Properties on predecessor ************************************************) -lemma ylt_pred: ∀m,n. m < n → 0 < m → ⫰m < ⫰n. +lemma ylt_pred: ∀m,n:ynat. m < n → 0 < m → ⫰m < ⫰n. #m #n * -m -n /4 width=1 by ylt_inv_inj, ylt_inj, monotonic_lt_pred/ qed. @@ -155,10 +155,14 @@ qed. lemma ylt_succ_Y: ∀x. x < ∞ → ⫯x < ∞. * /2 width=1 by/ qed. -lemma yle_succ1_inj: ∀x,y. ⫯yinj x ≤ y → x < y. +lemma yle_succ1_inj: ∀x. ∀y:ynat. ⫯yinj x ≤ y → x < y. #x * /3 width=1 by yle_inv_inj, ylt_inj/ qed. +lemma ylt_succ2_refl: ∀x,y:ynat. x < y → x < ⫯x. +#x #y #H elim (ylt_fwd_gen … H) -y /2 width=1 by ylt_inj/ +qed. + (* Properties on order ******************************************************) lemma yle_split_eq: ∀m,n:ynat. m ≤ n → m < n ∨ m = n. @@ -195,7 +199,7 @@ lemma yle_ylt_trans: ∀x:ynat. ∀y:ynat. ∀z:ynat. y < z → x ≤ y → x < ] qed-. -lemma yle_inv_succ1_lt: ∀x,y. ⫯x ≤ y → 0 < y ∧ x ≤ ⫰y. +lemma yle_inv_succ1_lt: ∀x,y:ynat. ⫯x ≤ y → 0 < y ∧ x ≤ ⫰y. #x #y #H elim (yle_inv_succ1 … H) -H /3 width=1 by ylt_O1, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma index e710032b0..16a933acf 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma @@ -93,12 +93,12 @@ qed. (* Inversion lemmas on successor *********************************************) -lemma yplus_inv_succ_lt_dx: ∀x,y,z. 0 < y → x + y = ⫯z → x + ⫰y = z. +lemma yplus_inv_succ_lt_dx: ∀x,y,z:ynat. 0 < y → x + y = ⫯z → x + ⫰y = z. #x #y #z #H <(ylt_inv_O1 y) // >yplus_succ2 /2 width=1 by ysucc_inv_inj/ qed-. -lemma yplus_inv_succ_lt_sn: ∀x,y,z. 0 < x → x + y = ⫯z → ⫰x + y = z. +lemma yplus_inv_succ_lt_sn: ∀x,y,z:ynat. 0 < x → x + y = ⫯z → ⫰x + y = z. #x #y #z #H <(ylt_inv_O1 x) // >yplus_succ1 /2 width=1 by ysucc_inv_inj/ diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma index 1f14ea6c0..8d17df7ff 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma @@ -20,16 +20,16 @@ include "ground_2/ynat/ynat.ma". (* the predecessor function *) definition ypred: ynat → ynat ≝ λm. match m with -[ yinj m ⇒ pred m +[ yinj m ⇒ ⫰m | Y ⇒ Y ]. interpretation "ynat predecessor" 'Predecessor m = (ypred m). -lemma ypred_O: ⫰0 = 0. +lemma ypred_O: ⫰(yinj 0) = yinj 0. // qed. -lemma ypred_S: ∀m:nat. ⫰(S m) = m. +lemma ypred_S: ∀m:nat. ⫰(⫯m) = yinj m. // qed. lemma ypred_Y: (⫰∞) = ∞. @@ -37,7 +37,7 @@ lemma ypred_Y: (⫰∞) = ∞. (* Inversion lemmas *********************************************************) -lemma ypred_inv_refl: ∀m. ⫰m = m → m = 0 ∨ m = ∞. +lemma ypred_inv_refl: ∀m:ynat. ⫰m = m → m = 0 ∨ m = ∞. * // #m #H lapply (yinj_inj … H) -H (**) (* destruct lemma needed *) /4 width=1 by pred_inv_refl, or_introl, eq_f/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma index c4c989f77..be5bef707 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma @@ -19,13 +19,13 @@ include "ground_2/ynat/ynat_pred.ma". (* the successor function *) definition ysucc: ynat → ynat ≝ λm. match m with -[ yinj m ⇒ S m +[ yinj m ⇒ ⫯m | Y ⇒ Y ]. interpretation "ynat successor" 'Successor m = (ysucc m). -lemma ysucc_inj: ∀m:nat. ⫯m = S m. +lemma ysucc_inj: ∀m:nat. ⫯(yinj m) = yinj (⫯m). // qed. lemma ysucc_Y: ⫯(∞) = ∞. @@ -36,7 +36,7 @@ lemma ysucc_Y: ⫯(∞) = ∞. lemma ypred_succ: ∀m. ⫰⫯m = m. * // qed. -lemma ynat_cases: ∀n:ynat. n = 0 ∨ ∃m. n = ⫯m. +lemma ynat_cases: ∀n:ynat. n = 0 ∨ ∃m:ynat. n = ⫯m. * [ * /2 width=1 by or_introl/ #n @or_intror @(ex_intro … n) // (**) (* explicit constructor *) @@ -86,7 +86,7 @@ lemma ysucc_inv_O_sn: ∀m. yinj 0 = ⫯m → ⊥. (**) (* explicit coercion *) #n #_ #H destruct qed-. -lemma ysucc_inv_O_dx: ∀m. ⫯m = 0 → ⊥. +lemma ysucc_inv_O_dx: ∀m:ynat. ⫯m = 0 → ⊥. /2 width=2 by ysucc_inv_O_sn/ qed-. (* Eliminators **************************************************************) diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 3b04c75b3..7d0ab3a8e 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1561,7 +1561,7 @@ let predefined_classes = [ ["M"; "ℳ"; "𝕄"; "𝐌"; "Ⓜ"; ] ; ["n"; "𝕟"; "𝐧"; "𝛈"; "ⓝ"; ] ; ["N"; "ℕ"; "№"; "𝐍"; "Ⓝ"; ] ; - ["o"; "θ"; "ϑ"; "𝕠"; "∘"; "ø"; "○"; "𝐨"; "𝛉"; "ⓞ"; ] ; + ["o"; "θ"; "ϑ"; "𝕠"; "∘"; "⊚"; "ø"; "○"; "𝐨"; "𝛉"; "ⓞ"; ] ; ["O"; "Θ"; "𝕆"; "𝐎"; "𝚯"; "𝚹"; "Ⓞ"; ] ; ["p"; "π"; "𝕡"; "𝐩"; "𝛑"; "ⓟ"; ] ; ["P"; "Π"; "℘"; "ℙ"; "𝐏"; "𝚷"; "Ⓟ"; ] ; -- 2.39.2