From: Ferruccio Guidi Date: Wed, 17 Feb 2021 16:40:28 +0000 (+0100) Subject: propagating the arithmetics library, partial commit X-Git-Tag: make_still_working~161 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6604a232815858a6c75dd25ac45abd68438077ff;p=helm.git propagating the arithmetics library, partial commit + lib ported + minor corrections and renaming + old parked version of ynat removed --- diff --git a/matita/matita/contribs/lambdadelta/ground/arith/arith_2b.ma b/matita/matita/contribs/lambdadelta/ground/arith/arith_2b.ma index f284a3c6c..842fcc72a 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/arith_2b.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/arith_2b.ma @@ -22,7 +22,8 @@ lemma arith_l4 (m11) (m12) (m21) (m22): elim (nat_split_le_ge (m11+m12) m21) #Hm1121 [ lapply (nle_trans m11 ??? Hm1121) // #Hm121 lapply (nle_minus_dx_dx … Hm1121) #Hm12211 - yinj_nat_zero #H + /4 width=1 by nle_eq_zero_minus, yle_inj, eq_inv_yinj_nat_bi/ +| #n H12 #H +lapply (yle_inv_plus_bi_sn_inj … H) -H #Hmy2 +generalize in match H12; -H12 (**) (* rewrite in hyp *) +>(yplus_lminus_sn_refl_sn … Hmy2) in ⊢ (%→?); (yplus_lminus_dx_refl_sn … Hnx1) in ⊢ (%→?); -Hnx1 #H +lapply (eq_inv_yplus_bi_sn_inj … H) -H #H12 +/2 width=1 by conj/ +qed-. + +(*** yle_inv_plus_inj2 yle_inv_plus_inj_dx *) +lemma yle_inv_plus_sn_inj_dx (n) (x) (z): + x + yinj_nat n ≤ z → + ∧∧ x ≤ z - n & yinj_nat n ≤ z. +/3 width=3 by yle_plus_sn_dx_lminus_dx, yle_trans, conj/ +qed-. + +(*** yle_inv_plus_inj1 *) +lemma yle_inv_plus_sn_inj_sn (n) (x) (z): + yinj_nat n + x ≤ z → + ∧∧ x ≤ z - n & yinj_nat n ≤ z. +/2 width=1 by yle_inv_plus_sn_inj_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_lminus_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_lminus_succ.ma new file mode 100644 index 000000000..93e73cf84 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_lminus_succ.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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/arith/ynat_succ.ma". +include "ground/arith/ynat_le_lminus.ma". + +(* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************) + +(* Constructions with ylminus and ysucc *************************************) + +(*** yminus_succ1_inj *) +lemma ylminus_succ_sn (x) (n): + yinj_nat n ≤ x → ↑(x - n) = ↑x - n. +#x @(ynat_split_nat_inf … x) -x // +#m #n #Hnm +yinj_nat_zero #H - /4 width=1 by nle_eq_zero_minus, yle_inj, eq_inv_yinj_nat_bi/ -| #n H12 #H -lapply (yle_inv_plus_bi_sn_inj … H) -H #Hmy2 -generalize in match H12; -H12 (**) (* rewrite in hyp *) ->(yplus_minus1_sn_refl_sn … Hmy2) in ⊢ (%→?); (yplus_minus1_dx_refl_sn … Hnx1) in ⊢ (%→?); -Hnx1 #H -lapply (eq_inv_yplus_bi_sn_inj … H) -H #H12 -/2 width=1 by conj/ -qed-. - -(*** yle_inv_plus_inj2 yle_inv_plus_inj_dx *) -lemma yle_inv_plus_sn_inj_dx (n) (x) (z): - x + yinj_nat n ≤ z → - ∧∧ x ≤ z - n & yinj_nat n ≤ z. -/3 width=3 by yle_plus_sn_dx_minus1_dx, yle_trans, conj/ -qed-. - -(*** yle_inv_plus_inj1 *) -lemma yle_inv_plus_sn_inj_sn (n) (x) (z): - yinj_nat n + x ≤ z → - ∧∧ x ≤ z - n & yinj_nat n ≤ z. -/2 width=1 by yle_inv_plus_sn_inj_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_minus1_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_minus1_succ.ma deleted file mode 100644 index 76cfcaf73..000000000 --- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_minus1_succ.ma +++ /dev/null @@ -1,29 +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 "ground/arith/ynat_succ.ma". -include "ground/arith/ynat_le_minus1.ma". - -(* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************) - -(* Constructions with yminus1 and ysucc *************************************) - -(*** yminus_succ1_inj *) -lemma yminus1_succ_sn (x) (n): - yinj_nat n ≤ x → ↑(x - n) = ↑x - n. -#x @(ynat_split_nat_inf … x) -x // -#m #n #Hnm -yinj_nat_zero >(nminus_refl m) +/4 width=1 by ylt_inj, ylt_inv_inj_bi, nlt_minus_bi_dx/ +qed. + +(* Inversions with ylminus **************************************************) + +(*** yminus_to_lt *) +lemma ylt_inv_zero_lminus (m) (y): + (𝟎) < y - m → yinj_nat m < y. +#m #y @(ynat_split_nat_inf … y) -y // +#n yinj_nat_zero >(nminus_refl m) #Hmm +/4 width=2 by ylt_inv_inj_bi, ylt_inj, nlt_inv_minus_bi_dx/ +qed-. + +(* Destructions with ylminus ************************************************) + +(*** yminus_pred *) +lemma ylminus_pred_bi (x:ynat) (n): + (𝟎) < x → 𝟎 < n → x - n = ↓x - ↓n. +#x @(ynat_split_nat_inf … x) -x // +#m #n >yinj_nat_zero +#Hm #Hn ysucc_inj yinj_nat_zero >(nminus_refl m) -/4 width=1 by ylt_inj, ylt_inv_inj_bi, nlt_minus_bi_dx/ -qed. - -(* Inversions with yminus1 **************************************************) - -(*** yminus_to_lt *) -lemma ylt_inv_zero_minus1 (m) (y): - (𝟎) < y - m → yinj_nat m < y. -#m #y @(ynat_split_nat_inf … y) -y // -#n yinj_nat_zero >(nminus_refl m) #Hmm -/4 width=2 by ylt_inv_inj_bi, ylt_inj, nlt_inv_minus_bi_dx/ -qed-. - -(* Destructions with yminus1 ************************************************) - -(*** yminus_pred *) -lemma yminus1_pred_bi (x:ynat) (n): - (𝟎) < x → 𝟎 < n → x - n = ↓x - ↓n. -#x @(ynat_split_nat_inf … x) -x // -#m #n >yinj_nat_zero -#Hm #Hn ysucc_inj H -H // -qed-. - -lemma discr_YO_YS: ∀n. ynat_of_nat 0 = ⫯n → ⊥. (**) (* explicit coercion *) -/2 width=2 by discr_YS_YO/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/etc/ynat_old/ynat_le.etc b/matita/matita/contribs/lambdadelta/ground/etc/ynat_old/ynat_le.etc deleted file mode 100644 index bde84cf79..000000000 --- a/matita/matita/contribs/lambdadelta/ground/etc/ynat_old/ynat_le.etc +++ /dev/null @@ -1,84 +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 "ground_2/star.ma". -include "ground_2/ynat/ynat_iszero.ma". -include "ground_2/ynat/ynat_pred.ma". - -(* INFINITARY NATURAL NUMBERS ***********************************************) - -(* order relation *) -coinductive yle: relation ynat ≝ -| yle_O: ∀n. yle 0 n -| yle_S: ∀m,n. yle m n → yle (⫯m) (⫯n) -. - -interpretation "natural 'less or equal to'" 'leq x y = (yle x y). - -(* Inversion lemmas *********************************************************) - -fact yle_inv_O2_aux: ∀m,x. m ≤ x → x = 0 → m = 0. -#m #x * -m -x // -#m #x #_ #H elim (discr_YS_YO … H) (**) (* destructing lemma needed *) -qed-. - -lemma yle_inv_O2: ∀m. m ≤ 0 → m = 0. -/2 width =3 by yle_inv_O2_aux/ qed-. - -fact yle_inv_S1_aux: ∀x,y. x ≤ y → ∀m. x = ⫯m → ∃∃n. m ≤ n & y = ⫯n. -#x #y * -x -y -[ #y #m #H elim (discr_YO_YS … H) (**) (* destructing lemma needed *) -| #x #y #Hxy #m #H destruct /2 width=3 by ex2_intro/ -] -qed-. - -lemma yle_inv_S1: ∀m,y. ⫯m ≤ y → ∃∃n. m ≤ n & y = ⫯n. -/2 width=3 by yle_inv_S1_aux/ qed-. - -lemma yle_inv_S: ∀m,n. ⫯m ≤ ⫯n → m ≤ n. -#m #n #H elim (yle_inv_S1 … H) -H -#x #Hx #H destruct // -qed-. - -(* Properties ***************************************************************) - -let corec yle_refl: reflexive … yle ≝ ?. -* [ @yle_O | #x @yle_S // ] -qed. - -let corec yle_Y: ∀m. m ≤ ∞ ≝ ?. -* [ @yle_O | #m length_cons #H destruct +lemma list_length_inv_zero_dx (A:Type[0]) (l:list A): + |l| = 𝟎 → l = Ⓔ. +#A * // #a #l >list_length_cons #H +elim (eq_inv_nsucc_zero … H) qed-. -lemma length_inv_zero_sn (A:Type[0]) (l:list A): 0 = |l| → l = Ⓔ. -/2 width=1 by length_inv_zero_dx/ qed-. +lemma list_length_inv_zero_sn (A:Type[0]) (l:list A): + (𝟎) = |l| → l = Ⓔ. +/2 width=1 by list_length_inv_zero_dx/ qed-. -lemma length_inv_succ_dx (A:Type[0]) (l:list A) (x): |l| = ↑x → - ∃∃tl,a. x = |tl| & l = a ⨮ tl. +lemma list_length_inv_succ_dx (A:Type[0]) (l:list A) (x): + |l| = ↑x → + ∃∃tl,a. x = |tl| & l = a ⨮ tl. #A * -[ #x >length_nil #H destruct -| #a #l #x >length_cons #H destruct /2 width=4 by ex2_2_intro/ +[ #x >list_length_nil #H + elim (eq_inv_zero_nsucc … H) +| #a #l #x >list_length_cons #H + /3 width=4 by eq_inv_nsucc_bi, ex2_2_intro/ ] qed-. -lemma length_inv_succ_sn (A:Type[0]) (l:list A) (x): ↑x = |l| → - ∃∃tl,a. x = |tl| & l = a ⨮ tl. -/2 width=1 by length_inv_succ_dx/ qed. +lemma list_length_inv_succ_sn (A:Type[0]) (l:list A) (x): + ↑x = |l| → + ∃∃tl,a. x = |tl| & l = a ⨮ tl. +/2 width=1 by list_length_inv_succ_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/lib/logic.ma b/matita/matita/contribs/lambdadelta/ground/lib/logic.ma index dc7216480..fc2e2ea85 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/logic.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/logic.ma @@ -18,11 +18,17 @@ include "ground/notation/xoa/true_0.ma". include "ground/notation/xoa/or_2.ma". include "ground/notation/xoa/and_2.ma". -interpretation "logical false" 'false = False. +interpretation + "false (logic)" + 'false = False. -interpretation "logical true" 'true = True. +interpretation + "true (logic)" + 'true = True. -(* Logical properties missing in the basic library **************************) +(* LOGIC ********************************************************************) + +(* Constructions with And ***************************************************) lemma commutative_and: ∀A,B. A ∧ B → B ∧ A. #A #B * /2 width=1 by conj/ diff --git a/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma b/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma index ae707f2b9..ba513ae85 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma @@ -12,9 +12,16 @@ (* *) (**************************************************************************) -include "arithmetics/lstar.ma". +include "ground/lib/ltc.ma". +include "ground/arith/nat_plus.ma". -(* PROPERTIES OF NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE ***************) +(* NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE FOR FOR λδ-2A ***************) -definition llstar: ∀A:Type[0]. ∀B. (A→relation B) → nat → (A→relation B) ≝ - λA,B,R,l,a. lstar … (R a) l. +definition lstar_aux (B) (R:relation B) (l): relation B ≝ + λb1,b2. ∨∨ (∧∧ l = 𝟎 & b1 = b2) | (∧∧ l = 𝟏 & R b1 b2). + +definition lstar (B) (R:relation B): nat → relation B ≝ + ltc … nplus … (lstar_aux … R). + +definition llstar (A) (B) (R:relation3 A B B) (l:nat): relation3 A B B ≝ + λa. lstar … (R a) l. diff --git a/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma b/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma index 4f3962671..1d08fb15d 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground/insert_eq/insert_eq_0.ma". +include "ground/insert_eq/insert_eq_1.ma". include "ground/lib/functions.ma". (* LABELLED TRANSITIVE CLOSURE **********************************************) @@ -22,7 +22,7 @@ inductive ltc (A:Type[0]) (f) (B) (R:relation3 A B B): relation3 A B B ≝ | ltc_trans: ∀a1,a2,b1,b,b2. ltc … a1 b1 b → ltc … a2 b b2 → ltc … (f a1 a2) b1 b2 . -(* Basic properties *********************************************************) +(* Basic constructions ******************************************************) lemma ltc_sn (A) (f) (B) (R): ∀a1,b1,b. R a1 b1 b → ∀a2,b2. ltc A f B R a2 b b2 → ltc … f … R (f a1 a2) b1 b2. @@ -32,13 +32,13 @@ lemma ltc_dx (A) (f) (B) (R): ∀a1,b1,b. ltc A f B R a1 b1 b → ∀a2,b2. R a2 b b2 → ltc … f … R (f a1 a2) b1 b2. /3 width=3 by ltc_rc, ltc_trans/ qed. -(* Basic eliminators ********************************************************) +(* Basic eliminations *******************************************************) lemma ltc_ind_sn (A) (f) (B) (R) (Q:relation2 A B) (b2): associative … f → (∀a,b1. R a b1 b2 → Q a b1) → (∀a1,a2,b1,b. R a1 b1 b → ltc … f … R a2 b b2 → Q a2 b → Q (f a1 a2) b1) → ∀a,b1. ltc … f … R a b1 b2 → Q a b1. -#A #f #B #R #Q #b2 #Hf #IH1 #IH2 #a #b1 @(insert_eq_0 … b2) +#A #f #B #R #Q #b2 #Hf #IH1 #IH2 #a #b1 @(insert_eq_1 … b2) #b0 #H elim H -a -b1 -b0 /2 width=2 by/ #a1 #a2 #b1 #b #b0 #H #Hb2 #_ generalize in match Hb2; generalize in match a2; -Hb2 -a2 @@ -49,14 +49,14 @@ lemma ltc_ind_dx (A) (f) (B) (R) (Q:A→predicate B) (b1): associative … f → (∀a,b2. R a b1 b2 → Q a b2) → (∀a1,a2,b,b2. ltc … f … R a1 b1 b → Q a1 b → R a2 b b2 → Q (f a1 a2) b2) → ∀a,b2. ltc … f … R a b1 b2 → Q a b2. -#A #f #B #R #Q #b1 #Hf #IH1 #IH2 #a #b2 @(insert_eq_0 … b1) +#A #f #B #R #Q #b1 #Hf #IH1 #IH2 #a #b2 @(insert_eq_1 … b1) #b0 #H elim H -a -b0 -b2 /2 width=2 by/ #a1 #a2 #b0 #b #b2 #Hb0 #H #IHb0 #_ generalize in match IHb0; generalize in match Hb0; generalize in match a1; -IHb0 -Hb0 -a1 elim H -a2 -b -b2 /4 width=4 by ltc_trans/ qed-. -(* Advanced elimiators with reflexivity *************************************) +(* Advanced elimiations with reflexivity ************************************) lemma ltc_ind_sn_refl (A) (i) (f) (B) (R) (Q:relation2 A B) (b2): associative … f → right_identity … f i → reflexive B (R i) → @@ -78,7 +78,7 @@ lemma ltc_ind_dx_refl (A) (i) (f) (B) (R) (Q:A→predicate B) (b1): >(H2f a) -H2f /3 width=4 by ltc_rc/ qed-. -(* Properties with lsub *****************************************************) +(* Constructions with lsub **************************************************) lemma ltc_lsub_trans: ∀A,f. associative … f → ∀B,C,R,S. (∀n. lsub_trans B C (λL. R L n) S) → diff --git a/matita/matita/contribs/lambdadelta/ground/lib/ltc_ctc.ma b/matita/matita/contribs/lambdadelta/ground/lib/ltc_ctc.ma index 0f8ddd107..54b1117b6 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/ltc_ctc.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/ltc_ctc.ma @@ -17,9 +17,9 @@ include "ground/lib/ltc.ma". (* LABELLED TRANSITIVE CLOSURE **********************************************) -alias symbol "subseteq" = "relation inclusion". +alias symbol "subseteq" = "relation inclusion". (**) -(* Properties with contextual transitive closure ****************************) +(* Constructions with contextual transitive closure *************************) lemma ltc_CTC (C) (A) (i) (f) (B) (R:relation4 C A B B): left_identity … f i → @@ -28,13 +28,13 @@ lemma ltc_CTC (C) (A) (i) (f) (B) (R:relation4 C A B B): #b #b2 #_ #Hb2 #IH >(Hf i) -Hf /2 width=3 by ltc_dx/ qed. -(* Inversion lemmas with contextual transitive closure **********************) +(* Inversions with contextual transitive closure ****************************) lemma ltc_inv_CTC (C) (A) (i) (f) (B) (R:relation4 C A B B): associative … f → annulment_2 … f i → ∀c. ltc … f … (R c) i ⊆ CTC … (λc. R c i) c. #C #A #i #f #B #R #H1f #H2f #c #b1 #b2 -@(insert_eq_0 … i) #a #H +@(insert_eq_1 … i) #a #H @(ltc_ind_dx A f B … H) -a -b2 /2 width=1 by inj/ -H1f #a1 #a2 #b #b2 #_ #IH #Hb2 #H