From: Ferruccio Guidi Date: Mon, 17 Dec 2012 22:24:07 +0000 (+0000) Subject: - lambda: some parts commented out, some refactoring X-Git-Tag: make_still_working~1388 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5ca47b58902b9f2583ad1354b860c04ea62df46c;p=helm.git - lambda: some parts commented out, some refactoring and some notational changes - lib: some additions from the preamble of "lambda" - predefined_virtuals: some additions --- diff --git a/matita/matita/contribs/lambda/delifting_substitution.ma b/matita/matita/contribs/lambda/delifting_substitution.ma index 6ad8d252c..aa9d9586c 100644 --- a/matita/matita/contribs/lambda/delifting_substitution.ma +++ b/matita/matita/contribs/lambda/delifting_substitution.ma @@ -27,28 +27,28 @@ interpretation "delifting substitution" 'DSubst D d M = (dsubst D d M). (* Note: the notation with "/" does not work *) -notation "hvbox( [ term 46 d ⬐ break term 46 D ] break term 46 M )" +notation "hvbox( [ term 46 d ↙ break term 46 D ] break term 46 M )" non associative with precedence 46 for @{ 'DSubst $D $d $M }. -notation > "hvbox( [ ⬐ term 46 D ] break term 46 M )" +notation > "hvbox( [ ↙ term 46 D ] break term 46 M )" non associative with precedence 46 for @{ 'DSubst $D 0 $M }. -lemma dsubst_vref_lt: ∀i,d,D. i < d → [d ⬐ D] #i = #i. +lemma dsubst_vref_lt: ∀i,d,D. i < d → [d ↙ D] #i = #i. normalize /2 width=1/ qed. -lemma dsubst_vref_eq: ∀d,D. [d ⬐ D] #d = ↑[d]D. +lemma dsubst_vref_eq: ∀i,D. [i ↙ D] #i = ↑[i]D. normalize // qed. -lemma dsubst_vref_gt: ∀i,d,D. d < i → [d ⬐ D] #i = #(i-1). +lemma dsubst_vref_gt: ∀i,d,D. d < i → [d ↙ D] #i = #(i-1). normalize /2 width=1/ qed. theorem dsubst_lift_le: ∀h,D,M,d1,d2. d2 ≤ d1 → - [d2 ⬐ ↑[d1 - d2, h] D] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ⬐ D] M. + [d2 ↙ ↑[d1 - d2, h] D] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ↙ D] M. #h #D #M elim M -M [ #i #d1 #d2 #Hd21 elim (lt_or_eq_or_gt i d2) #Hid2 [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1 @@ -68,7 +68,7 @@ theorem dsubst_lift_le: ∀h,D,M,d1,d2. d2 ≤ d1 → qed. theorem dsubst_lift_be: ∀h,D,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h → - [d2 ⬐ D] ↑[d1, h + 1] M = ↑[d1, h] M. + [d2 ↙ D] ↑[d1, h + 1] M = ↑[d1, h] M. #h #D #M elim M -M [ #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1 [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2 @@ -85,7 +85,7 @@ theorem dsubst_lift_be: ∀h,D,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h → qed. theorem dsubst_lift_ge: ∀h,D,M,d1,d2. d1 + h ≤ d2 → - [d2 ⬐ D] ↑[d1, h] M = ↑[d1, h] [d2 - h ⬐ D] M. + [d2 ↙ D] ↑[d1, h] M = ↑[d1, h] [d2 - h ↙ D] M. #h #D #M elim M -M [ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i (d2-h)) #Hid2h [ >(dsubst_vref_lt … Hid2h) elim (lt_or_ge i d1) #Hid1 @@ -112,7 +112,7 @@ theorem dsubst_lift_ge: ∀h,D,M,d1,d2. d1 + h ≤ d2 → qed. theorem dsubst_dsubst_ge: ∀D1,D2,M,d1,d2. d1 ≤ d2 → - [d2 ⬐ D2] [d1 ⬐ D1] M = [d1 ⬐ [d2 - d1 ⬐ D2] D1] [d2 + 1 ⬐ D2] M. + [d2 ↙ D2] [d1 ↙ D1] M = [d1 ↙ [d2 - d1 ↙ D2] D1] [d2 + 1 ↙ D2] M. #D1 #D2 #M elim M -M [ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i d1) #Hid1 [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 @@ -135,29 +135,29 @@ theorem dsubst_dsubst_ge: ∀D1,D2,M,d1,d2. d1 ≤ d2 → qed. theorem dsubst_dsubst_lt: ∀D1,D2,M,d1,d2. d2 < d1 → - [d2 ⬐ [d1 - d2 -1 ⬐ D1] D2] [d1 ⬐ D1] M = [d1 - 1 ⬐ D1] [d2 ⬐ D2] M. + [d2 ↙ [d1 - d2 -1 ↙ D1] D2] [d1 ↙ D1] M = [d1 - 1 ↙ D1] [d2 ↙ D2] M. #D1 #D2 #M #d1 #d2 #Hd21 lapply (ltn_to_ltO … Hd21) #Hd1 >dsubst_dsubst_ge in ⊢ (???%); /2 width=1/ dsubst_dsubst_ge // qed. -lemma head_lsred_lhap1: ∀p. in_head p → ∀M,N. M ⇀[p] N → M ⓗ⇀[p] N. +lemma head_lsred_lhap1: ∀p. in_head p → ∀M,N. M ↦[p] N → M ⓗ↦[p] N. #p #H @(in_head_ind … H) -p [ #M #N #H elim (lsred_inv_nil … H ?) -H // | #p #_ #IHp #M #N #H @@ -77,11 +77,11 @@ lemma head_lsred_lhap1: ∀p. in_head p → ∀M,N. M ⇀[p] N → M ⓗ⇀[p] N ] qed. -lemma lhap1_inv_head: ∀p,M,N. M ⓗ⇀[p] N → in_head p. +lemma lhap1_inv_head: ∀p,M,N. M ⓗ↦[p] N → in_head p. #p #M #N #H elim H -p -M -N // /2 width=1/ qed-. -lemma lhap1_inv_lsred: ∀p,M,N. M ⓗ⇀[p] N → M ⇀[p] N. +lemma lhap1_inv_lsred: ∀p,M,N. M ⓗ↦[p] N → M ↦[p] N. #p #M #N #H elim H -p -M -N // /2 width=1/ qed-. diff --git a/matita/matita/contribs/lambda/labelled_sequential_computation.ma b/matita/matita/contribs/lambda/labelled_sequential_computation.ma index a609078fe..f305f90cb 100644 --- a/matita/matita/contribs/lambda/labelled_sequential_computation.ma +++ b/matita/matita/contribs/lambda/labelled_sequential_computation.ma @@ -22,29 +22,29 @@ definition lsreds: pseq → relation term ≝ lstar … lsred. interpretation "labelled sequential computation" 'SeqRedStar M s N = (lsreds s M N). -notation "hvbox( M break ⇀* [ term 46 s ] break term 46 N )" +notation "hvbox( M break ↦* [ term 46 s ] break term 46 N )" non associative with precedence 45 for @{ 'SeqRedStar $M $s $N }. -lemma lsreds_step_rc: ∀p,M1,M2. M1 ⇀[p] M2 → M1 ⇀*[p::◊] M2. +lemma lsreds_step_rc: ∀p,M1,M2. M1 ↦[p] M2 → M1 ↦*[p::◊] M2. /2 width=1/ qed. -lemma lsreds_inv_nil: ∀s,M1,M2. M1 ⇀*[s] M2 → ◊ = s → M1 = M2. +lemma lsreds_inv_nil: ∀s,M1,M2. M1 ↦*[s] M2 → ◊ = s → M1 = M2. /2 width=5 by lstar_inv_nil/ qed-. -lemma lsreds_inv_cons: ∀s,M1,M2. M1 ⇀*[s] M2 → ∀q,r. q::r = s → - ∃∃M. M1 ⇀[q] M & M ⇀*[r] M2. +lemma lsreds_inv_cons: ∀s,M1,M2. M1 ↦*[s] M2 → ∀q,r. q::r = s → + ∃∃M. M1 ↦[q] M & M ↦*[r] M2. /2 width=3 by lstar_inv_cons/ qed-. -lemma lsreds_inv_step_rc: ∀p,M1,M2. M1 ⇀*[p::◊] M2 → M1 ⇀[p] M2. +lemma lsreds_inv_step_rc: ∀p,M1,M2. M1 ↦*[p::◊] M2 → M1 ↦[p] M2. /2 width=1 by lstar_inv_step/ qed-. -lemma lsreds_inv_pos: ∀s,M1,M2. M1 ⇀*[s] M2 → 0 < |s| → - ∃∃p,r,M. p::r = s & M1 ⇀[p] M & M ⇀*[r] M2. +lemma lsreds_inv_pos: ∀s,M1,M2. M1 ↦*[s] M2 → 0 < |s| → + ∃∃p,r,M. p::r = s & M1 ↦[p] M & M ↦*[r] M2. /2 width=1 by lstar_inv_pos/ qed-. @@ -81,7 +81,7 @@ theorem lsreds_trans: ltransitive … lsreds. qed-. (* Note: "|s|" should be unparetesized *) -lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ⇀*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)). +lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ↦*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)). #s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 normalize // #p #s #M1 #M #HM1 #_ #IHM2 lapply (lsred_fwd_mult … HM1) -p #HM1 diff --git a/matita/matita/contribs/lambda/labelled_sequential_reduction.ma b/matita/matita/contribs/lambda/labelled_sequential_reduction.ma index 0c75f86e2..40d518846 100644 --- a/matita/matita/contribs/lambda/labelled_sequential_reduction.ma +++ b/matita/matita/contribs/lambda/labelled_sequential_reduction.ma @@ -22,7 +22,7 @@ include "multiplicity.ma". Theoretical Computer Science 155(1), Elsevier (1996), pp. 85-109. *) inductive lsred: ptr → relation term ≝ -| lsred_beta : ∀B,A. lsred (◊) (@B.𝛌.A) ([⬐B]A) +| lsred_beta : ∀B,A. lsred (◊) (@B.𝛌.A) ([↙B]A) | lsred_abst : ∀p,A1,A2. lsred p A1 A2 → lsred (sn::p) (𝛌.A1) (𝛌.A2) | lsred_appl_sn: ∀p,B1,B2,A. lsred p B1 B2 → lsred (sn::p) (@B1.A) (@B2.A) | lsred_appl_dx: ∀p,B,A1,A2. lsred p A1 A2 → lsred (dx::p) (@B.A1) (@B.A2) @@ -32,11 +32,11 @@ interpretation "labelled sequential reduction" 'SeqRed M p N = (lsred p M N). (* Note: we do not use → since it is reserved by CIC *) -notation "hvbox( M break ⇀ [ term 46 p ] break term 46 N )" +notation "hvbox( M break ↦ [ term 46 p ] break term 46 N )" non associative with precedence 45 for @{ 'SeqRed $M $p $N }. -lemma lsred_inv_vref: ∀p,M,N. M ⇀[p] N → ∀i. #i = M → ⊥. +lemma lsred_inv_vref: ∀p,M,N. M ↦[p] N → ∀i. #i = M → ⊥. #p #M #N * -p -M -N [ #B #A #i #H destruct | #p #A1 #A2 #_ #i #H destruct @@ -45,8 +45,8 @@ lemma lsred_inv_vref: ∀p,M,N. M ⇀[p] N → ∀i. #i = M → ⊥. ] qed-. -lemma lsred_inv_nil: ∀p,M,N. M ⇀[p] N → ◊ = p → - ∃∃B,A. @B. 𝛌.A = M & [⬐B] A = N. +lemma lsred_inv_nil: ∀p,M,N. M ↦[p] N → ◊ = p → + ∃∃B,A. @B. 𝛌.A = M & [↙B] A = N. #p #M #N * -p -M -N [ #B #A #_ destruct /2 width=4/ | #p #A1 #A2 #_ #H destruct @@ -55,9 +55,9 @@ lemma lsred_inv_nil: ∀p,M,N. M ⇀[p] N → ◊ = p → ] qed-. -lemma lsred_inv_sn: ∀p,M,N. M ⇀[p] N → ∀q. sn::q = p → - (∃∃A1,A2. A1 ⇀[q] A2 & 𝛌.A1 = M & 𝛌.A2 = N) ∨ - ∃∃B1,B2,A. B1 ⇀[q] B2 & @B1.A = M & @B2.A = N. +lemma lsred_inv_sn: ∀p,M,N. M ↦[p] N → ∀q. sn::q = p → + (∃∃A1,A2. A1 ↦[q] A2 & 𝛌.A1 = M & 𝛌.A2 = N) ∨ + ∃∃B1,B2,A. B1 ↦[q] B2 & @B1.A = M & @B2.A = N. #p #M #N * -p -M -N [ #B #A #q #H destruct | #p #A1 #A2 #HA12 #q #H destruct /3 width=5/ @@ -66,8 +66,8 @@ lemma lsred_inv_sn: ∀p,M,N. M ⇀[p] N → ∀q. sn::q = p → ] qed-. -lemma lsred_inv_dx: ∀p,M,N. M ⇀[p] N → ∀q. dx::q = p → - ∃∃B,A1,A2. A1 ⇀[q] A2 & @B.A1 = M & @B.A2 = N. +lemma lsred_inv_dx: ∀p,M,N. M ↦[p] N → ∀q. dx::q = p → + ∃∃B,A1,A2. A1 ↦[q] A2 & @B.A1 = M & @B.A2 = N. #p #M #N * -p -M -N [ #B #A #q #H destruct | #p #A1 #A2 #_ #q #H destruct @@ -76,7 +76,7 @@ lemma lsred_inv_dx: ∀p,M,N. M ⇀[p] N → ∀q. dx::q = p → ] qed-. -lemma lsred_fwd_mult: ∀p,M,N. M ⇀[p] N → #{N} < #{M} * #{M}. +lemma lsred_fwd_mult: ∀p,M,N. M ↦[p] N → #{N} < #{M} * #{M}. #p #M #N #H elim H -p -M -N [ #B #A @(le_to_lt_to_lt … (#{A}*#{B})) // normalize /3 width=1 by lt_minus_to_plus_r, lt_times/ (**) (* auto: too slow without trace *) diff --git a/matita/matita/contribs/lambda/length.ma b/matita/matita/contribs/lambda/length.ma new file mode 100644 index 000000000..abb629433 --- /dev/null +++ b/matita/matita/contribs/lambda/length.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". + +(* LENGTH *******************************************************************) + +(* Note: this gives the number of abstractions and applications in M *) +let rec length M on M ≝ match M with +[ VRef i ⇒ 0 +| Abst A ⇒ length A + 1 +| Appl B A ⇒ (length B) + (length A) + 1 +]. + +interpretation "term length" + 'card M = (length M). + +lemma length_lift: ∀h,M,d. |↑[d, h] M| = |M|. +#h #M elim M -M normalize // +qed. diff --git a/matita/matita/contribs/lambda/lift.ma b/matita/matita/contribs/lambda/lift.ma index 43443e5b4..17ea9692b 100644 --- a/matita/matita/contribs/lambda/lift.ma +++ b/matita/matita/contribs/lambda/lift.ma @@ -16,8 +16,8 @@ include "term.ma". (* RELOCATION ***************************************************************) -(* Policy: depth (level) metavariables: d, e - height metavariables : h, k +(* Policy: level metavariables : d, e + height metavariables: h, k *) (* Note: indexes start at zero *) let rec lift h d M on M ≝ match M with @@ -48,12 +48,12 @@ lemma lift_vref_ge: ∀d,h,i. d ≤ i → ↑[d, h] #i = #(i+h). #d #h #i #H elim (le_to_or_lt_eq … H) -H normalize // /3 width=1/ qed. - +(* lemma lift_vref_pred: ∀d,i. d < i → ↑[d, 1] #(i-1) = #i. #d #i #Hdi >lift_vref_ge /2 width=1/ (dsubst_vref_lt … Hid) normalize // diff --git a/matita/matita/contribs/lambda/parallel_reduction.ma b/matita/matita/contribs/lambda/parallel_reduction.ma index 6b352da4d..eaa8b7ce1 100644 --- a/matita/matita/contribs/lambda/parallel_reduction.ma +++ b/matita/matita/contribs/lambda/parallel_reduction.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "size.ma". +include "length.ma". include "labelled_sequential_reduction.ma". (* PARALLEL REDUCTION (SINGLE STEP) *****************************************) @@ -24,13 +24,13 @@ inductive pred: relation term ≝ | pred_vref: ∀i. pred (#i) (#i) | pred_abst: ∀A1,A2. pred A1 A2 → pred (𝛌.A1) (𝛌.A2) | pred_appl: ∀B1,B2,A1,A2. pred B1 B2 → pred A1 A2 → pred (@B1.A1) (@B2.A2) -| pred_beta: ∀B1,B2,A1,A2. pred B1 B2 → pred A1 A2 → pred (@B1.𝛌.A1) ([⬐B2]A2) +| pred_beta: ∀B1,B2,A1,A2. pred B1 B2 → pred A1 A2 → pred (@B1.𝛌.A1) ([↙B2]A2) . interpretation "parallel reduction" 'ParRed M N = (pred M N). -notation "hvbox( M ⥤ break term 46 N )" +notation "hvbox( M ⤇ break term 46 N )" non associative with precedence 45 for @{ 'ParRed $M $N }. @@ -38,7 +38,7 @@ lemma pred_refl: reflexive … pred. #M elim M -M // /2 width=1/ qed. -lemma pred_inv_vref: ∀M,N. M ⥤ N → ∀i. #i = M → #i = N. +lemma pred_inv_vref: ∀M,N. M ⤇ N → ∀i. #i = M → #i = N. #M #N * -M -N // [ #A1 #A2 #_ #i #H destruct | #B1 #B2 #A1 #A2 #_ #_ #i #H destruct @@ -46,8 +46,8 @@ lemma pred_inv_vref: ∀M,N. M ⥤ N → ∀i. #i = M → #i = N. ] qed-. -lemma pred_inv_abst: ∀M,N. M ⥤ N → ∀A. 𝛌.A = M → - ∃∃C. A ⥤ C & 𝛌.C = N. +lemma pred_inv_abst: ∀M,N. M ⤇ N → ∀A. 𝛌.A = M → + ∃∃C. A ⤇ C & 𝛌.C = N. #M #N * -M -N [ #i #A0 #H destruct | #A1 #A2 #HA12 #A0 #H destruct /2 width=3/ @@ -56,9 +56,9 @@ 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. +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 | #A1 #A2 #_ #B0 #A0 #H destruct @@ -88,7 +88,7 @@ lemma pred_inv_lift: deliftable_sn pred. elim (lift_inv_abst … HM) -HM #A1 #HAC1 #H elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2 elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct - @(ex2_intro … ([⬐B2]A2)) /2 width=1/ + @(ex2_intro … ([↙B2]A2)) /2 width=1/ ] qed-. @@ -122,8 +122,8 @@ 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 → 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 // @@ -131,7 +131,7 @@ 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 +#M @(f_ind … length … 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 @@ -151,6 +151,6 @@ theorem pred_conf: confluent … pred. ] qed-. -lemma lsred_pred: ∀p,M,N. M ⇀[p] N → M ⥤ N. +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/policy.txt b/matita/matita/contribs/lambda/policy.txt index 987d9f8b1..7743f9bbd 100644 --- a/matita/matita/contribs/lambda/policy.txt +++ b/matita/matita/contribs/lambda/policy.txt @@ -9,9 +9,9 @@ R : arbitrary relation T, U : arbitrary small type c : pointer step -d, e : variable reference depth +d, e : variable reference level h : relocation height -i, j : de Bruijn index +i, j : variable reference depth (de Bruijn index) k : relocation height l : arbitrary list m, n : measures on terms diff --git a/matita/matita/contribs/lambda/preamble.ma b/matita/matita/contribs/lambda/preamble.ma index 958f1059a..c7c736f2c 100644 --- a/matita/matita/contribs/lambda/preamble.ma +++ b/matita/matita/contribs/lambda/preamble.ma @@ -28,16 +28,6 @@ notation "⊥" non associative with precedence 90 for @{'false}. -(* 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 → ⊥. diff --git a/matita/matita/contribs/lambda/replace.sh b/matita/matita/contribs/lambda/replace.sh new file mode 100644 index 000000000..5e281b251 --- /dev/null +++ b/matita/matita/contribs/lambda/replace.sh @@ -0,0 +1,10 @@ +#!/bin/sh +for MA in `find -name "*.ma"`; do + echo ${MA}; sed "s!$1!$2!g" ${MA} > ${MA}.new + if diff ${MA} ${MA}.new > /dev/null; + then rm -f ${MA}.new; + else mv -f ${MA} ${MA}.old; mv -f ${MA}.new ${MA}; + fi +done + +unset MA diff --git a/matita/matita/contribs/lambda/size.ma b/matita/matita/contribs/lambda/size.ma deleted file mode 100644 index 2ae1c539a..000000000 --- a/matita/matita/contribs/lambda/size.ma +++ /dev/null @@ -1,31 +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 "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/st_computation.ma b/matita/matita/contribs/lambda/st_computation.ma index 75d72ed0c..cce418715 100644 --- a/matita/matita/contribs/lambda/st_computation.ma +++ b/matita/matita/contribs/lambda/st_computation.ma @@ -20,20 +20,20 @@ include "labelled_hap_computation.ma". R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000). *) inductive st: relation term ≝ -| st_vref: ∀s,M,i. M ⓗ⇀*[s] #i → st M (#i) -| st_abst: ∀s,M,A1,A2. M ⓗ⇀*[s] 𝛌.A1 → st A1 A2 → st M (𝛌.A2) -| st_appl: ∀s,M,B1,B2,A1,A2. M ⓗ⇀*[s] @B1.A1 → st B1 B2 → st A1 A2 → st M (@B2.A2) +| st_vref: ∀s,M,i. M ⓗ↦*[s] #i → st M (#i) +| st_abst: ∀s,M,A1,A2. M ⓗ↦*[s] 𝛌.A1 → st A1 A2 → st M (𝛌.A2) +| st_appl: ∀s,M,B1,B2,A1,A2. M ⓗ↦*[s] @B1.A1 → st B1 B2 → st A1 A2 → st M (@B2.A2) . interpretation "'st' computation" 'Std M N = (st M N). -notation "hvbox( M ⓢ⥤* break term 46 N )" +notation "hvbox( M ⓢ⤇* break term 46 N )" non associative with precedence 45 for @{ 'Std $M $N }. -lemma st_inv_lref: ∀M,N. M ⓢ⥤* N → ∀j. #j = N → - ∃s. M ⓗ⇀*[s] #j. +lemma st_inv_lref: ∀M,N. M ⓢ⤇* N → ∀j. #j = N → + ∃s. M ⓗ↦*[s] #j. #M #N * -M -N [ /2 width=2/ | #s #M #A1 #A2 #_ #_ #j #H destruct @@ -41,8 +41,8 @@ lemma st_inv_lref: ∀M,N. M ⓢ⥤* N → ∀j. #j = N → ] qed-. -lemma st_inv_abst: ∀M,N. M ⓢ⥤* N → ∀C2. 𝛌.C2 = N → - ∃∃s,C1. M ⓗ⇀*[s] 𝛌.C1 & C1 ⓢ⥤* C2. +lemma st_inv_abst: ∀M,N. M ⓢ⤇* N → ∀C2. 𝛌.C2 = N → + ∃∃s,C1. M ⓗ↦*[s] 𝛌.C1 & C1 ⓢ⤇* C2. #M #N * -M -N [ #s #M #i #_ #C2 #H destruct | #s #M #A1 #A2 #HM #A12 #C2 #H destruct /2 width=4/ @@ -50,8 +50,8 @@ lemma st_inv_abst: ∀M,N. M ⓢ⥤* N → ∀C2. 𝛌.C2 = N → ] qed-. -lemma st_inv_appl: ∀M,N. M ⓢ⥤* N → ∀D2,C2. @D2.C2 = N → - ∃∃s,D1,C1. M ⓗ⇀*[s] @D1.C1 & D1 ⓢ⥤* D2 & C1 ⓢ⥤* C2. +lemma st_inv_appl: ∀M,N. M ⓢ⤇* N → ∀D2,C2. @D2.C2 = N → + ∃∃s,D1,C1. M ⓗ↦*[s] @D1.C1 & D1 ⓢ⤇* D2 & C1 ⓢ⤇* C2. #M #N * -M -N [ #s #M #i #_ #D2 #C2 #H destruct | #s #M #A1 #A2 #_ #_ #D2 #C2 #H destruct @@ -63,7 +63,7 @@ lemma st_refl: reflexive … st. #M elim M -M /2 width=2/ /2 width=4/ /2 width=6/ qed. -lemma st_step_sn: ∀N1,N2. N1 ⓢ⥤* N2 → ∀s,M. M ⓗ⇀*[s] N1 → M ⓢ⥤* N2. +lemma st_step_sn: ∀N1,N2. N1 ⓢ⤇* N2 → ∀s,M. M ⓗ↦*[s] N1 → M ⓢ⤇* N2. #N1 #N2 #H elim H -N1 -N2 [ #r #N #i #HN #s #M #HMN lapply (lhap_trans … HMN … HN) -N /2 width=2/ @@ -74,7 +74,7 @@ lemma st_step_sn: ∀N1,N2. N1 ⓢ⥤* N2 → ∀s,M. M ⓗ⇀*[s] N1 → M ⓢ ] qed-. -lemma st_step_rc: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → M1 ⓢ⥤* M2. +lemma st_step_rc: ∀s,M1,M2. M1 ⓗ↦*[s] M2 → M1 ⓢ⤇* M2. /3 width=4 by st_step_sn/ qed. @@ -123,8 +123,8 @@ lemma st_dsubst: dsubstable st. ] qed. -lemma st_inv_lsreds_is_le: ∀M,N. M ⓢ⥤* N → - ∃∃r. M ⇀*[r] N & is_le r. +lemma st_inv_lsreds_is_le: ∀M,N. M ⓢ⤇* N → + ∃∃r. M ↦*[r] N & is_le r. #M #N #H elim H -M -N [ #s #M #i #H lapply (lhap_inv_lsreds … H) @@ -144,13 +144,13 @@ lemma st_inv_lsreds_is_le: ∀M,N. M ⓢ⥤* N → ] qed-. -lemma st_step_dx: ∀p,M,M2. M ⇀[p] M2 → ∀M1. M1 ⓢ⥤* M → M1 ⓢ⥤* M2. +lemma st_step_dx: ∀p,M,M2. M ↦[p] M2 → ∀M1. M1 ⓢ⤇* M → M1 ⓢ⤇* M2. #p #M #M2 #H elim H -p -M -M2 [ #B #A #M1 #H elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] #s #B1 #M #HM1 #HB1 #H (**) (* simplify line *) elim (st_inv_abst … H ??) -H [3: // |2: skip ] #r #A1 #HM #HA1 (**) (* simplify line *) lapply (lhap_trans … HM1 … (dx:::r) (@B1.𝛌.A1) ?) /2 width=1/ -M #HM1 - lapply (lhap_step_dx … HM1 (◊) ([⬐B1]A1) ?) -HM1 // #HM1 + lapply (lhap_step_dx … HM1 (◊) ([↙B1]A1) ?) -HM1 // #HM1 @(st_step_sn … HM1) /2 width=1/ | #p #A #A2 #_ #IHA2 #M1 #H elim (st_inv_abst … H ??) -H [3: // |2: skip ] /3 width=4/ (**) (* simplify line *) @@ -161,14 +161,14 @@ lemma st_step_dx: ∀p,M,M2. M ⇀[p] M2 → ∀M1. M1 ⓢ⥤* M → M1 ⓢ⥤* ] qed-. -lemma st_lhap1_swap: ∀p,N1,N2. N1 ⓗ⇀[p] N2 → ∀M1. M1 ⓢ⥤* N1 → - ∃∃q,M2. M1 ⓗ⇀[q] M2 & M2 ⓢ⥤* N2. +lemma st_lhap1_swap: ∀p,N1,N2. N1 ⓗ↦[p] N2 → ∀M1. M1 ⓢ⤇* N1 → + ∃∃q,M2. M1 ⓗ↦[q] M2 & M2 ⓢ⤇* N2. #p #N1 #N2 #H elim H -p -N1 -N2 [ #D #C #M1 #H elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] #s #D1 #N #HM1 #HD1 #H (**) (* simplify line *) elim (st_inv_abst … H ??) -H [3: // |2: skip ] #r #C1 #HN #HC1 (**) (* simplify line *) lapply (lhap_trans … HM1 … (dx:::r) (@D1.𝛌.C1) ?) /2 width=1/ -N #HM1 - lapply (lhap_step_dx … HM1 (◊) ([⬐D1]C1) ?) -HM1 // #HM1 + lapply (lhap_step_dx … HM1 (◊) ([↙D1]C1) ?) -HM1 // #HM1 elim (lhap_inv_pos … HM1 ?) -HM1 [2: >length_append normalize in ⊢ (??(??%)); // ] #q #r #M #_ #HM1 #HM -s @@ -185,7 +185,7 @@ lemma st_lhap1_swap: ∀p,N1,N2. N1 ⓗ⇀[p] N2 → ∀M1. M1 ⓢ⥤* N1 → ] qed-. -lemma st_lsreds: ∀s,M1,M2. M1 ⇀*[s] M2 → M1 ⓢ⥤* M2. +lemma st_lsreds: ∀s,M1,M2. M1 ↦*[s] M2 → M1 ⓢ⤇* M2. #s #M1 #M2 #H @(lstar_ind_r ????????? H) -s -M2 // /2 width=4 by st_step_dx/ qed. @@ -196,14 +196,14 @@ elim (st_inv_lsreds_is_le … HM2) -HM2 #s2 #HM2 #_ lapply (lsreds_trans … HM1 … HM2) -M /2 width=2/ qed-. -theorem lsreds_standard: ∀s,M,N. M ⇀*[s] N → - ∃∃r. M ⇀*[r] N & is_le r. +theorem lsreds_standard: ∀s,M,N. M ↦*[s] N → + ∃∃r. M ↦*[r] N & is_le r. #s #M #N #H @st_inv_lsreds_is_le /2 width=2/ qed-. -theorem lsreds_lhap1_swap: ∀s,M1,N1. M1 ⇀*[s] N1 → ∀p,N2. N1 ⓗ⇀[p] N2 → - ∃∃q,r,M2. M1 ⓗ⇀[q] M2 & M2 ⇀*[r] N2 & is_le (q::r). +theorem lsreds_lhap1_swap: ∀s,M1,N1. M1 ↦*[s] N1 → ∀p,N2. N1 ⓗ↦[p] N2 → + ∃∃q,r,M2. M1 ⓗ↦[q] M2 & M2 ↦*[r] N2 & is_le (q::r). #s #M1 #N1 #HMN1 #p #N2 #HN12 lapply (st_lsreds … HMN1) -s #HMN1 elim (st_lhap1_swap … HN12 … HMN1) -p -N1 #q #M2 #HM12 #HMN2 diff --git a/matita/matita/contribs/lambda/term.ma b/matita/matita/contribs/lambda/term.ma index 660830d27..92a838fb4 100644 --- a/matita/matita/contribs/lambda/term.ma +++ b/matita/matita/contribs/lambda/term.ma @@ -18,11 +18,11 @@ include "preamble.ma". (* TERM STRUCTURE ***********************************************************) -(* Policy: term metavariables: A, B, C, D, M, N - de Bruijn indexes : i, j +(* Policy: term metavariables : A, B, C, D, M, N + depth metavariables: i, j *) inductive term: Type[0] ≝ -| VRef: nat → term (* variable reference by index *) +| VRef: nat → term (* variable reference by depth *) | Abst: term → term (* function formation *) | Appl: term → term → term (* function application *) . @@ -47,7 +47,7 @@ notation "hvbox( 𝛌 . term 46 A )" notation "hvbox( @ term 46 C . break term 46 A )" non associative with precedence 46 for @{ 'Application $C $A }. - +(* definition appl_compatible_dx: predicate (relation term) ≝ λR. ∀B,A1,A2. R A1 A2 → R (@B.A1) (@B.A2). @@ -55,3 +55,4 @@ lemma star_appl_compatible_dx: ∀R. appl_compatible_dx R → appl_compatible_dx (star … R). #R #HR #B #A1 #A2 #H elim H -A2 // /3 width=3/ qed. +*) diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma index 76b4239d4..4b90f7518 100644 --- a/matita/matita/lib/basics/logic.ma +++ b/matita/matita/lib/basics/logic.ma @@ -153,7 +153,7 @@ interpretation "exists on two predicates" 'exists2 x1 x2 = (ex2 ? x1 x2). lemma ex2_commute: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0. #A0 #P0 #P1 * /2 width=3/ -qed. +qed-. (* iff *) definition iff := diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma index 8b746ef68..84dd7c362 100644 --- a/matita/matita/lib/basics/relations.ma +++ b/matita/matita/lib/basics/relations.ma @@ -51,6 +51,13 @@ definition antisymmetric: ∀A.∀R:relation A.Prop definition singlevalued: ∀A,B. predicate (relation2 A B) ≝ λA,B,R. ∀a,b1. R a b1 → ∀b2. R a b2 → b1 = b2. +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. + +definition confluent: ∀A. predicate (relation A) ≝ λA,R. + ∀a0. confluent1 … R a0. + (* Reflexive closure ************) definition RC: ∀A:Type[0]. relation A → relation A ≝ diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 2972d58e9..51f3f0781 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1508,14 +1508,14 @@ let predefined_classes = [ ["#"; "⌘"; ]; ["-"; "÷"; "⊢"; "⊩"; ]; ["="; "≃"; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; ]; - ["→"; "⇀"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; - ["⇒"; "⥤"; "➾"; "⇨"; "➡"; "➸"; "⇉"; "⥰"; ] ; + ["→"; "↦"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; + ["⇒"; "⤇"; "➾"; "⇨"; "➡"; "➸"; "⇉"; "⥰"; ] ; ["^"; "↑"; ] ; ["⇑"; "⇧"; "⬆"; ] ; ["⇓"; "⇩"; "⬇"; "⬊"; "➷"; ] ; ["↔"; "⇔"; "⬄"; "⬌"; ] ; ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; ]; - ["_"; "⬐"; "⎽"; "⎼"; "⎻"; "⎺"; ]; + ["_"; "↓"; "↙"; "⎽"; "⎼"; "⎻"; "⎺"; ]; ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ; ["("; "❨"; "❪"; "❲"; "（"; ]; [")"; "❩"; "❫"; "❳"; "）"; ];