From: Ferruccio Guidi Date: Mon, 3 Dec 2012 19:41:24 +0000 (+0000) Subject: - nat.ma: we added a general induction principle X-Git-Tag: make_still_working~1417 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6b87a3e9d6dd7c3abb922750587444ac3fd08e16;p=helm.git - nat.ma: we added a general induction principle - lambda: we have the diamond property of parallel reduction notation bugfixes in term and muktiplicity --- diff --git a/matita/matita/contribs/lambda/delifting_substitution.ma b/matita/matita/contribs/lambda/delifting_substitution.ma index 11ce88761..38087f4fe 100644 --- a/matita/matita/contribs/lambda/delifting_substitution.ma +++ b/matita/matita/contribs/lambda/delifting_substitution.ma @@ -143,3 +143,9 @@ qed. definition dsubstable_dx: predicate (relation term) ≝ λR. ∀D,M1,M2. R M1 M2 → ∀d. R ([d ⬐ D] M1) ([d ⬐ D] M2). + +definition dsubstable_sn: predicate (relation term) ≝ λR. + ∀D1,D2. R D1 D2 → ∀M,d. R ([d ⬐ D1] M) ([d ⬐ D2] M). + +definition dsubstable: predicate (relation term) ≝ λR. + ∀D1,D2. R D1 D2 → ∀M1,M2. R M1 M2 → ∀d. R ([d ⬐ D1] M1) ([d ⬐ D2] M2). diff --git a/matita/matita/contribs/lambda/multiplicity.ma b/matita/matita/contribs/lambda/multiplicity.ma index e8b72762b..040f1c67b 100644 --- a/matita/matita/contribs/lambda/multiplicity.ma +++ b/matita/matita/contribs/lambda/multiplicity.ma @@ -23,7 +23,7 @@ let rec mult M on M ≝ match M with | Appl B A ⇒ (mult B) + (mult A) ]. -interpretation "multiplicity" +interpretation "term multiplicity" 'Multiplicity M = (mult M). notation "hvbox( #{ term 46 M } )" @@ -35,11 +35,11 @@ lemma mult_positive: ∀M. 0 < #{M}. qed. lemma mult_lift: ∀h,M,d. #{↑[d, h] M} = #{M}. -#H #M elim M -M normalize // +#h #M elim M -M normalize // qed. -theorem mult_dsubst: ∀C,M,d. #{[d ⬐ C] M} ≤ #{M} * #{C}. -#C #M elim M -M +theorem mult_dsubst: ∀D,M,d. #{[d ⬐ D] M} ≤ #{M} * #{D}. +#D #M elim M -M [ #i #d elim (lt_or_eq_or_gt i d) #Hid [ >(dsubst_vref_lt … Hid) normalize // | destruct >dsubst_vref_eq normalize // diff --git a/matita/matita/contribs/lambda/parallel_reduction.ma b/matita/matita/contribs/lambda/parallel_reduction.ma index 4cb204bb9..7aa47be7f 100644 --- a/matita/matita/contribs/lambda/parallel_reduction.ma +++ b/matita/matita/contribs/lambda/parallel_reduction.ma @@ -12,7 +12,8 @@ (* *) (**************************************************************************) -include "multiplicity.ma". +include "size.ma". +include "labelled_sequential_reduction.ma". (* PARALLEL REDUCTION (SINGLE STEP) *****************************************) @@ -55,6 +56,17 @@ lemma pred_inv_abst: ∀M,N. M ⥤ N → ∀A. 𝛌.A = M → ] qed-. +lemma pred_inv_appl: ∀M,N. M ⥤ N → ∀B,A. @B.A = M → + (∃∃D,C. B ⥤ D & A ⥤ C & @D.C = N) ∨ + ∃∃A0,D,C0. B ⥤ D & A0 ⥤ C0 & 𝛌.A0 = A & [⬐D]C0 = N. +#M #N * -M -N +[ #i #B0 #A0 #H destruct +| #A #C #_ #B0 #A0 #H destruct +| #B #D #A #C #HBD #HAC #B0 #A0 #H destruct /3 width=5/ +| #B #D #A #C #HBD #HAC #B0 #A0 #H destruct /3 width=7/ +] +qed-. + lemma pred_lift: liftable pred. #h #M1 #M2 #H elim H -M1 -M2 normalize // /2 width=1/ #D #D #A #C #_ #_ #IHBD #IHAC #d (dsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) // + | destruct >dsubst_vref_eq >dsubst_vref_eq /2 width=1/ + | >(dsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) // + ] +| normalize /2 width=1/ +| normalize /2 width=1/ +| normalize #B #D #A #C #_ #_ #IHBD #IHAC #d + >dsubst_dsubst_ge // /2 width=1/ +] +qed. + +lemma pred_conf1_vref: ∀i. confluent1 … pred (#i). +#i #M1 #H1 #M2 #H2 +<(pred_inv_vref … H1) -H1 [3: // |2: skip ] (**) (* simplify line *) +<(pred_inv_vref … H2) -H2 [3: // |2: skip ] (**) (* simplify line *) +/2 width=3/ +qed-. + +lemma pred_conf1_abst: ∀A. confluent1 … pred A → confluent1 … pred (𝛌.A). +#A #IH #M1 #H1 #M2 #H2 +elim (pred_inv_abst … H1 ??) -H1 [3: // |2: skip ] #A1 #HA1 #H destruct (**) (* simplify line *) +elim (pred_inv_abst … H2 ??) -H2 [3: // |2: skip ] #A2 #HA2 #H destruct (**) (* simplify line *) +elim (IH … HA1 … HA2) -A /3 width=3/ +qed-. + +lemma pred_conf1_appl_beta: ∀B,B1,B2,C,C2,M1. + (∀M0. |M0| < |B|+|𝛌.C|+1 → confluent1 ? pred M0) → (**) (* ? needed in place of … *) + B ⥤ B1 → B ⥤ B2 → 𝛌.C ⥤ M1 → C ⥤ C2 → + ∃∃M. @B1.M1 ⥤ M & [⬐B2]C2 ⥤ M. +#B #B1 #B2 #C #C2 #M1 #IH #HB1 #HB2 #H1 #HC2 +elim (pred_inv_abst … H1 ??) -H1 [3: // |2: skip ] #C1 #HC1 #H destruct (**) (* simplify line *) +elim (IH B … HB1 … HB2) -HB1 -HB2 // +elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/ +qed-. + +theorem pred_conf: confluent … pred. +#M @(f_ind … size … M) -M #n #IH * normalize +[ /2 width=3 by pred_conf1_vref/ +| /3 width=4 by pred_conf1_abst/ +| #B #A #H #M1 #H1 #M2 #H2 destruct + elim (pred_inv_appl … H1 ???) -H1 [5: // |2,3: skip ] * (**) (* simplify line *) + elim (pred_inv_appl … H2 ???) -H2 [5,10: // |2,3,7,8: skip ] * (**) (* simplify line *) + [ #B2 #A2 #HB2 #HA2 #H2 #B1 #A1 #HB1 #HA1 #H1 destruct + elim (IH A … HA1 … HA2) -HA1 -HA2 // + elim (IH B … HB1 … HB2) // -A -B /3 width=5/ + | #C #B2 #C2 #HB2 #HC2 #H2 #HM2 #B1 #N #HB1 #H #HM1 destruct + @(pred_conf1_appl_beta … IH) // (**) (* /2 width=7 by pred_conf1_appl_beta/ does not work *) + | #B2 #N #B2 #H #HM2 #C #B1 #C1 #HB1 #HC1 #H1 #HM1 destruct + @ex2_1_commute @(pred_conf1_appl_beta … IH) // + | #C #B2 #C2 #HB2 #HC2 #H2 #HM2 #C0 #B1 #C1 #HB1 #HC1 #H1 #HM1 destruct + elim (IH B … HB1 … HB2) -HB1 -HB2 // + elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/ + ] +] +qed-. + +lemma lsred_pred: ∀p,M,N. M ⇀[p] N → M ⥤ N. +#p #M #N #H elim H -p -M -N /2 width=1/ +qed. diff --git a/matita/matita/contribs/lambda/preamble.ma b/matita/matita/contribs/lambda/preamble.ma index f3884b229..8e4b8fc96 100644 --- a/matita/matita/contribs/lambda/preamble.ma +++ b/matita/matita/contribs/lambda/preamble.ma @@ -19,10 +19,7 @@ include "arithmetics/exp.ma". include "xoa_notation.ma". include "xoa.ma". -(* Note: notation for nil not involving brackets *) -notation > "◊" - non associative with precedence 90 - for @{'nil}. +(* logic *) (* Note: For some reason this cannot be in the standard library *) interpretation "logical false" 'false = False. @@ -31,6 +28,22 @@ notation "⊥" non associative with precedence 90 for @{'false}. +lemma ex2_1_commute: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0. +#A0 #P0 #P1 * /2 width=3/ +qed. + +(* relations *) + +definition confluent1: ∀A. relation A → predicate A ≝ λA,R,a0. + ∀a1. R a0 a1 → ∀a2. R a0 a2 → + ∃∃a. R a1 a & R a2 a. + +(* Note: confluent1 would be redundant if \Pi-reduction where enabled *) +definition confluent: ∀A. predicate (relation A) ≝ λA,R. + ∀a0. confluent1 … R a0. + +(* arithmetics *) + lemma lt_refl_false: ∀n. n < n → ⊥. #n #H elim (lt_to_not_eq … H) -H /2 width=1/ qed-. @@ -75,3 +88,10 @@ lemma tri_gt: ∀A,a1,a2,a3,n1,n2. n2 < n1 → tri A n1 n2 a1 a2 a3 = a3. | #n1 #IH #n2 elim n2 -n2 // /3 width=1/ ] qed. + +(* lists *) + +(* Note: notation for nil not involving brackets *) +notation > "◊" + non associative with precedence 90 + for @{'nil}. diff --git a/matita/matita/contribs/lambda/size.ma b/matita/matita/contribs/lambda/size.ma new file mode 100644 index 000000000..2ae1c539a --- /dev/null +++ b/matita/matita/contribs/lambda/size.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "lift.ma". + +(* SIZE *********************************************************************) + +(* Note: this gives the number of abstractions and applications in M *) +let rec size M on M ≝ match M with +[ VRef i ⇒ 0 +| Abst A ⇒ size A + 1 +| Appl B A ⇒ (size B) + (size A) + 1 +]. + +interpretation "term size" + 'card M = (size M). + +lemma size_lift: ∀h,M,d. |↑[d, h] M| = |M|. +#h #M elim M -M normalize // +qed. diff --git a/matita/matita/contribs/lambda/term.ma b/matita/matita/contribs/lambda/term.ma index 2e6a6e0ec..8c688dc8e 100644 --- a/matita/matita/contribs/lambda/term.ma +++ b/matita/matita/contribs/lambda/term.ma @@ -44,10 +44,6 @@ notation "hvbox( 𝛌 . term 46 A )" non associative with precedence 46 for @{ 'Abstraction $A }. -notation > "hvbox( 𝛌 term 46 A )" - non associative with precedence 46 - for @{ 'Abstraction $A }. - notation "hvbox( @ term 46 C . break term 46 A )" non associative with precedence 46 for @{ 'Application $C $A }. diff --git a/matita/matita/contribs/lambda/xoa.conf.xml b/matita/matita/contribs/lambda/xoa.conf.xml index 620113e79..1343a2c1e 100644 --- a/matita/matita/contribs/lambda/xoa.conf.xml +++ b/matita/matita/contribs/lambda/xoa.conf.xml @@ -10,6 +10,7 @@ basics/pts.ma 2 1 3 2 + 4 3 3 diff --git a/matita/matita/contribs/lambda/xoa.ma b/matita/matita/contribs/lambda/xoa.ma index 1a92dbad0..2d9ee54a3 100644 --- a/matita/matita/contribs/lambda/xoa.ma +++ b/matita/matita/contribs/lambda/xoa.ma @@ -32,6 +32,14 @@ inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝ interpretation "multiple existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2). +(* multiple existental quantifier (4, 3) *) + +inductive ex4_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3:A0→A1→A2→Prop) : Prop ≝ + | ex4_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → ex4_3 ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (4, 3)" 'Ex P0 P1 P2 P3 = (ex4_3 ? ? ? P0 P1 P2 P3). + (* multiple disjunction connective (3) *) inductive or3 (P0,P1,P2:Prop) : Prop ≝ diff --git a/matita/matita/contribs/lambda/xoa_notation.ma b/matita/matita/contribs/lambda/xoa_notation.ma index a2a26eb6e..de716c381 100644 --- a/matita/matita/contribs/lambda/xoa_notation.ma +++ b/matita/matita/contribs/lambda/xoa_notation.ma @@ -34,6 +34,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) }. +(* multiple existental quantifier (4, 3) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) }. + (* multiple disjunction connective (3) *) notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2)" diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma index 56935028f..67b7de50b 100644 --- a/matita/matita/lib/arithmetics/nat.ma +++ b/matita/matita/lib/arithmetics/nat.ma @@ -495,6 +495,13 @@ cut (∀q:nat. q ≤ n → P q) /2/ ] qed. +lemma f_ind: ∀A. ∀f:A→ℕ. ∀P:predicate A. + (∀n. (∀a. f a < n → P a) → ∀a. f a = n → P a) → ∀a. P a. +#A #f #P #H #a +cut (∀n,a. f a = n → P a) /2 width=3/ -a +#n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto very slow (274s) without #n *) +qed-. + (* More negated equalities **************************************************) theorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m.