From 5c792a695677f2857e1984ababc9998d42fc8033 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 6 Jan 2013 16:17:47 +0000 Subject: [PATCH] refactoring ... --- matita/matita/contribs/lambda/Makefile | 2 +- .../lambda/{ => background}/notation.ma | 33 ++- .../lambda/{ => background}/preamble.ma | 4 +- .../contribs/lambda/{ => background}/xoa.ma | 0 .../lambda/{ => background}/xoa_notation.ma | 0 .../decomposed_trace.ma} | 22 +- .../contribs/lambda/paths/dst_computation.ma | 214 ++++++++++++++++++ .../paths/labeled_sequential_computation.ma | 112 +++++++++ .../paths/labeled_sequential_reduction.ma | 128 +++++++++++ .../{terms/pointer.ma => paths/path.ma} | 28 +-- .../contribs/lambda/paths/standard_order.ma | 162 +++++++++++++ .../standard_trace.ma} | 10 +- .../{terms/pointer_list.ma => paths/trace.ma} | 16 +- .../contribs/lambda/subterms/subterms.ma | 4 +- .../terms/labeled_sequential_computation.ma | 141 ++---------- .../terms/labeled_sequential_reduction.ma | 143 ------------ .../lambda/terms/parallel_computation.ma | 4 - .../lambda/terms/parallel_reduction.ma | 16 +- .../contribs/lambda/terms/pointer_order.ma | 148 ------------ .../lambda/terms/sequential_computation.ma | 105 +++++++++ .../lambda/terms/sequential_reduction.ma | 106 +++++++++ .../lambda/terms/{length.ma => size.ma} | 14 +- .../contribs/lambda/terms/st_computation.ma | 214 ------------------ matita/matita/contribs/lambda/terms/term.ma | 4 +- matita/matita/contribs/lambda/xoa.conf.xml | 2 +- 25 files changed, 938 insertions(+), 694 deletions(-) rename matita/matita/contribs/lambda/{ => background}/notation.ma (71%) rename matita/matita/contribs/lambda/{ => background}/preamble.ma (98%) rename matita/matita/contribs/lambda/{ => background}/xoa.ma (100%) rename matita/matita/contribs/lambda/{ => background}/xoa_notation.ma (100%) rename matita/matita/contribs/lambda/{terms/pointer_tree.ma => paths/decomposed_trace.ma} (68%) create mode 100644 matita/matita/contribs/lambda/paths/dst_computation.ma create mode 100644 matita/matita/contribs/lambda/paths/labeled_sequential_computation.ma create mode 100644 matita/matita/contribs/lambda/paths/labeled_sequential_reduction.ma rename matita/matita/contribs/lambda/{terms/pointer.ma => paths/path.ma} (75%) create mode 100644 matita/matita/contribs/lambda/paths/standard_order.ma rename matita/matita/contribs/lambda/{terms/pointer_list_standard.ma => paths/standard_trace.ma} (87%) rename matita/matita/contribs/lambda/{terms/pointer_list.ma => paths/trace.ma} (82%) delete mode 100644 matita/matita/contribs/lambda/terms/labeled_sequential_reduction.ma delete mode 100644 matita/matita/contribs/lambda/terms/pointer_order.ma create mode 100644 matita/matita/contribs/lambda/terms/sequential_computation.ma create mode 100644 matita/matita/contribs/lambda/terms/sequential_reduction.ma rename matita/matita/contribs/lambda/terms/{length.ma => size.ma} (80%) delete mode 100644 matita/matita/contribs/lambda/terms/st_computation.ma diff --git a/matita/matita/contribs/lambda/Makefile b/matita/matita/contribs/lambda/Makefile index cc3a3bf91..b8f68bb83 100644 --- a/matita/matita/contribs/lambda/Makefile +++ b/matita/matita/contribs/lambda/Makefile @@ -7,7 +7,7 @@ MAC_DIR = ../../../components/binaries/mac MAC = mac.native XOA_CONF = xoa.conf.xml -XOA_TARGETS = xoa_notation.ma xoa.ma +XOA_TARGETS = background/xoa_notation.ma background/xoa.ma all: xoa $(H)../../matitac.opt diff --git a/matita/matita/contribs/lambda/notation.ma b/matita/matita/contribs/lambda/background/notation.ma similarity index 71% rename from matita/matita/contribs/lambda/notation.ma rename to matita/matita/contribs/lambda/background/notation.ma index 4bfca6887..c698a5b12 100644 --- a/matita/matita/contribs/lambda/notation.ma +++ b/matita/matita/contribs/lambda/background/notation.ma @@ -14,6 +14,11 @@ (* GENERIC NOTATION *********************************************************) +(* Note: this should go to core_notation *) +notation "hvbox(a break ≺ b)" + non associative with precedence 45 + for @{ 'prec $a $b }. + notation "hvbox( # term 90 i )" non associative with precedence 46 for @{ 'VariableReferenceByIndex $i }. @@ -51,11 +56,35 @@ notation > "hvbox( ↑ term 46 M )" for @{ 'Lift 1 0 $M }. (* Note: the notation with "/" does not work *) -notation "hvbox( [ term 46 d ↙ break term 46 N ] break term 46 M )" +notation "hvbox( [ term 46 d break ↙ term 46 N ] break term 46 M )" non associative with precedence 46 for @{ 'DSubst $N $d $M }. notation > "hvbox( [ ↙ term 46 N ] break term 46 M )" non associative with precedence 46 for @{ 'DSubst $N 0 $M }. - \ No newline at end of file + +(* Note: we do not use → since it is reserved by CIC *) +notation "hvbox( M break ↦ term 46 N )" + non associative with precedence 45 + for @{ 'SeqRed $M $N }. + +notation "hvbox( M break ↦ [ term 46 p ] break term 46 N )" + non associative with precedence 45 + for @{ 'SeqRed $M $p $N }. + +notation "hvbox( M break ↦* term 46 N )" + non associative with precedence 45 + for @{ 'SeqRedStar $M $N }. + +notation "hvbox( M break ↦* [ term 46 s ] break term 46 N )" + non associative with precedence 45 + for @{ 'SeqRedStar $M $s $N }. + +notation "hvbox( M break ⤇ term 46 N )" + non associative with precedence 45 + for @{ 'ParRed $M $N }. + +notation "hvbox( M break ⤇* term 46 N )" + non associative with precedence 45 + for @{ 'ParRedStar $M $N }. diff --git a/matita/matita/contribs/lambda/preamble.ma b/matita/matita/contribs/lambda/background/preamble.ma similarity index 98% rename from matita/matita/contribs/lambda/preamble.ma rename to matita/matita/contribs/lambda/background/preamble.ma index c7c736f2c..dc5c14467 100644 --- a/matita/matita/contribs/lambda/preamble.ma +++ b/matita/matita/contribs/lambda/background/preamble.ma @@ -16,8 +16,8 @@ include "basics/star.ma". include "basics/lists/lstar.ma". include "arithmetics/exp.ma". -include "xoa_notation.ma". -include "xoa.ma". +include "background/xoa_notation.ma". +include "background/xoa.ma". (* logic *) diff --git a/matita/matita/contribs/lambda/xoa.ma b/matita/matita/contribs/lambda/background/xoa.ma similarity index 100% rename from matita/matita/contribs/lambda/xoa.ma rename to matita/matita/contribs/lambda/background/xoa.ma diff --git a/matita/matita/contribs/lambda/xoa_notation.ma b/matita/matita/contribs/lambda/background/xoa_notation.ma similarity index 100% rename from matita/matita/contribs/lambda/xoa_notation.ma rename to matita/matita/contribs/lambda/background/xoa_notation.ma diff --git a/matita/matita/contribs/lambda/terms/pointer_tree.ma b/matita/matita/contribs/lambda/paths/decomposed_trace.ma similarity index 68% rename from matita/matita/contribs/lambda/terms/pointer_tree.ma rename to matita/matita/contribs/lambda/paths/decomposed_trace.ma index fff98a856..2241fab10 100644 --- a/matita/matita/contribs/lambda/terms/pointer_tree.ma +++ b/matita/matita/contribs/lambda/paths/decomposed_trace.ma @@ -12,20 +12,20 @@ (* *) (**************************************************************************) -include "terms/pointer_list.ma". +include "paths/trace.ma". -(* POINTER TREE *************************************************************) +(* DECOMPOSED TRACE *********************************************************) -(* Policy: pointer tree metavariables: P, Q *) -(* Note: this is a binary tree on pointer sequences *) -inductive ptrt: Type[0] ≝ -| tnil : ptrt -| tcons: ptrl → ptrt → ptrt → ptrt +(* Policy: decomposed trace metavariables: P, Q *) +(* Note: this is a binary tree on traces *) +inductive dtrace: Type[0] ≝ +| tree_nil : dtrace +| tree_cons: trace → dtrace → dtrace → dtrace . -let rec length (P:ptrt) on P ≝ match P with -[ tnil ⇒ 0 -| tcons s Q1 Q2 ⇒ length Q2 + length Q1 + |s| +let rec size (P:dtrace) on P ≝ match P with +[ tree_nil ⇒ 0 +| tree_cons s Q1 Q2 ⇒ size Q2 + size Q1 + |s| ]. -interpretation "pointer tree length" 'card P = (length P). +interpretation "decomposed trace size" 'card P = (size P). diff --git a/matita/matita/contribs/lambda/paths/dst_computation.ma b/matita/matita/contribs/lambda/paths/dst_computation.ma new file mode 100644 index 000000000..2e5310a11 --- /dev/null +++ b/matita/matita/contribs/lambda/paths/dst_computation.ma @@ -0,0 +1,214 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "paths/standard_trace.ma". +include "paths/labeled_sequential_computation.ma". + +(* DECOMPOSED STANDARD COMPUTATION ***********************************************) + +(* Note: this is the "standard" computation of: + R. Kashima: "A proof of the Standization Theorem in λ-Calculus". (2000). +*) +inductive dst: relation term ≝ +| dst_vref: ∀s,M,i. is_whd s → M ↦*[s] #i → dst M (#i) +| dst_abst: ∀s,M,A1,A2. is_whd s → M ↦*[s] 𝛌.A1 → dst A1 A2 → dst M (𝛌.A2) +| dst_appl: ∀s,M,B1,B2,A1,A2. is_whd s → M ↦*[s] @B1.A1 → dst B1 B2 → dst A1 A2 → dst M (@B2.A2) +. + +interpretation "decomposed standard computation" + 'Std M N = (dst M N). + +notation "hvbox( M break ⓢ↦* term 46 N )" + non associative with precedence 45 + for @{ 'Std $M $N }. + +lemma dst_inv_lref: ∀M,N. M ⓢ↦* N → ∀j. #j = N → + ∃∃s. is_whd s & M ↦*[s] #j. +#M #N * -M -N +[ /2 width=3/ +| #s #M #A1 #A2 #_ #_ #_ #j #H destruct +| #s #M #B1 #B2 #A1 #A2 #_ #_ #_ #_ #j #H destruct +] +qed-. + +lemma dst_inv_abst: ∀M,N. M ⓢ↦* N → ∀C2. 𝛌.C2 = N → + ∃∃s,C1. is_whd s & M ↦*[s] 𝛌.C1 & C1 ⓢ↦* C2. +#M #N * -M -N +[ #s #M #i #_ #_ #C2 #H destruct +| #s #M #A1 #A2 #Hs #HM #A12 #C2 #H destruct /2 width=5/ +| #s #M #B1 #B2 #A1 #A2 #_ #_ #_ #_ #C2 #H destruct +] +qed-. + +lemma dst_inv_appl: ∀M,N. M ⓢ↦* N → ∀D2,C2. @D2.C2 = N → + ∃∃s,D1,C1. is_whd s & 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 +| #s #M #B1 #B2 #A1 #A2 #Hs #HM #HB12 #HA12 #D2 #C2 #H destruct /2 width=7/ +] +qed-. + +lemma dst_refl: reflexive … dst. +#M elim M -M /2 width=3/ /2 width=5/ /2 width=7/ +qed. + +lemma dst_step_sn: ∀N1,N2. N1 ⓢ↦* N2 → ∀s,M. is_whd s → M ↦*[s] N1 → M ⓢ↦* N2. +#N1 #N2 #H elim H -N1 -N2 +[ #r #N #i #Hr #HN #s #M #Hs #HMN + lapply (pl_sreds_trans … HMN … HN) -N /3 width=3/ +| #r #N #C1 #C2 #Hr #HN #_ #IHC12 #s #M #Hs #HMN + lapply (pl_sreds_trans … HMN … HN) -N /3 width=7/ +| #r #N #D1 #D2 #C1 #C2 #Hr #HN #_ #_ #IHD12 #IHC12 #s #M #Hs #HMN + lapply (pl_sreds_trans … HMN … HN) -N /3 width=9/ +] +qed-. + +lemma dst_step_rc: ∀s,M1,M2. is_whd s → M1 ↦*[s] M2 → M1 ⓢ↦* M2. +/3 width=5 by dst_step_sn/ +qed. + +lemma dst_lift: liftable dst. +#h #M1 #M2 #H elim H -M1 -M2 +[ /3 width=3/ +| #s #M #A1 #A2 #Hs #HM #_ #IHA12 #d + @(dst_abst … Hs) [2: @(pl_sreds_lift … HM) | skip ] -M // (**) (* auto fails here *) +| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ #IHB12 #IHA12 #d + @(dst_appl … Hs) [3: @(pl_sreds_lift … HM) |1,2: skip ] -M // (**) (* auto fails here *) +] +qed. + +lemma dst_inv_lift: deliftable_sn dst. +#h #N1 #N2 #H elim H -N1 -N2 +[ #s #N1 #i #Hs #HN1 #d #M1 #HMN1 + elim (pl_sreds_inv_lift … HN1 … HMN1) -N1 /3 width=3/ +| #s #N1 #C1 #C2 #Hs #HN1 #_ #IHC12 #d #M1 #HMN1 + elim (pl_sreds_inv_lift … HN1 … HMN1) -N1 #M2 #HM12 #HM2 + elim (lift_inv_abst … HM2) -HM2 #A1 #HAC1 #HM2 destruct + elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *) + @(ex2_intro … (𝛌.A2)) // /2 width=5/ +| #s #N1 #D1 #D2 #C1 #C2 #Hs #HN1 #_ #_ #IHD12 #IHC12 #d #M1 #HMN1 + elim (pl_sreds_inv_lift … HN1 … HMN1) -N1 #M2 #HM12 #HM2 + elim (lift_inv_appl … HM2) -HM2 #B1 #A1 #HBD1 #HAC1 #HM2 destruct + elim (IHD12 ???) -IHD12 [4: // |2,3: skip ] #B2 #HB12 #HBD2 destruct (**) (* simplify line *) + elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *) + @(ex2_intro … (@B2.A2)) // /2 width=7/ +] +qed-. + +lemma dst_dsubst: dsubstable dst. +#N1 #N2 #HN12 #M1 #M2 #H elim H -M1 -M2 +[ #s #M #i #Hs #HM #d elim (lt_or_eq_or_gt i d) #Hid + [ lapply (pl_sreds_dsubst … N1 … HM d) -HM + >(dsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) /2 width=3/ + | destruct >dsubst_vref_eq + @(dst_step_sn (↑[0,i]N1) … s) /2 width=1/ + | lapply (pl_sreds_dsubst … N1 … HM d) -HM + >(dsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) /2 width=3/ + ] +| #s #M #A1 #A2 #Hs #HM #_ #IHA12 #d + lapply (pl_sreds_dsubst … N1 … HM d) -HM /2 width=5/ (**) (* auto needs some help here *) +| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ #IHB12 #IHA12 #d + lapply (pl_sreds_dsubst … N1 … HM d) -HM /2 width=7/ (**) (* auto needs some help here *) +] +qed. + +lemma dst_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 (dst_inv_appl … H ???) -H [4: // |2,3: skip ] #s #B1 #M #Hs #HM1 #HB1 #H (**) (* simplify line *) + elim (dst_inv_abst … H ??) -H [3: // |2: skip ] #r #A1 #Hr #HM #HA1 (**) (* simplify line *) + lapply (pl_sreds_trans … HM1 … (dx:::r) (@B1.𝛌.A1) ?) /2 width=1/ -M #HM1 + lapply (pl_sreds_step_dx … HM1 (◊) ([↙B1]A1) ?) -HM1 // #HM1 + @(dst_step_sn … HM1) /2 width=1/ /4 width=1/ +| #p #A #A2 #_ #IHA2 #M1 #H + elim (dst_inv_abst … H ??) -H [3: // |2: skip ] /3 width=5/ (**) (* simplify line *) +| #p #B #B2 #A #_ #IHB2 #M1 #H + elim (dst_inv_appl … H ???) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *) +| #p #B #A #A2 #_ #IHA2 #M1 #H + elim (dst_inv_appl … H ???) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *) +] +qed-. + +lemma pl_sreds_dst: ∀s,M1,M2. M1 ↦*[s] M2 → M1 ⓢ↦* M2. +#s #M1 #M2 #H @(lstar_ind_r ????????? H) -s -M2 // /2 width=4 by dst_step_dx/ +qed. + +lemma dst_inv_pl_sreds_is_standard: ∀M,N. M ⓢ↦* N → + ∃∃r. M ↦*[r] N & is_standard r. +#M #N #H elim H -M -N +[ #s #M #i #Hs #HM + lapply (is_whd_is_standard … Hs) -Hs /2 width=3/ +| #s #M #A1 #A2 #Hs #HM #_ * #r #HA12 #Hr + lapply (pl_sreds_trans … HM (rc:::r) (𝛌.A2) ?) /2 width=1/ -A1 #HM + @(ex2_intro … HM) -M -A2 /3 width=1/ +| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ * #rb #HB12 #Hrb * #ra #HA12 #Hra + lapply (pl_sreds_trans … HM (dx:::ra) (@B1.A2) ?) /2 width=1/ -A1 #HM + lapply (pl_sreds_trans … HM (sn:::rb) (@B2.A2) ?) /2 width=1/ -B1 #HM + @(ex2_intro … HM) -M -B2 -A2 >associative_append /3 width=1/ +] +qed-. + +theorem dst_trans: transitive … dst. +#M1 #M #M2 #HM1 #HM2 +elim (dst_inv_pl_sreds_is_standard … HM1) -HM1 #s1 #HM1 #_ +elim (dst_inv_pl_sreds_is_standard … HM2) -HM2 #s2 #HM2 #_ +lapply (pl_sreds_trans … HM1 … HM2) -M /2 width=2/ +qed-. + +theorem pl_sreds_standard: ∀s,M,N. M ↦*[s] N → ∃∃r. M ↦*[r] N & is_standard r. +#s #M #N #H +@dst_inv_pl_sreds_is_standard /2 width=2/ +qed-. + +(* Note: we use "lapply (rewrite_r ?? is_whd … Hq)" (procedural) + in place of "cut (is_whd (q::r)) [ >Hq ]" (declarative) +*) +lemma dst_in_whd_swap: ∀p. in_whd p → ∀N1,N2. N1 ↦[p] N2 → ∀M1. M1 ⓢ↦* N1 → + ∃∃q,M2. in_whd q & M1 ↦[q] M2 & M2 ⓢ↦* N2. +#p #H @(in_whd_ind … H) -p +[ #N1 #N2 #H1 #M1 #H2 + elim (pl_sred_inv_nil … H1 ?) -H1 // #D #C #HN1 #HN2 + elim (dst_inv_appl … H2 … HN1) -N1 #s1 #D1 #N #Hs1 #HM1 #HD1 #H + elim (dst_inv_abst … H ??) -H [3: // |2: skip ] #s2 #C1 #Hs2 #HN #HC1 (**) (* simplify line *) + lapply (pl_sreds_trans … HM1 … (dx:::s2) (@D1.𝛌.C1) ?) /2 width=1/ -N #HM1 + lapply (pl_sreds_step_dx … HM1 (◊) ([↙D1]C1) ?) -HM1 // #HM1 + elim (pl_sreds_inv_pos … HM1 ?) -HM1 + [2: >length_append normalize in ⊢ (??(??%)); // ] + #q #r #M #Hq #HM1 #HM + lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -s1 -s2 * #Hq #Hr + @(ex3_2_intro … HM1) -M1 // -q + @(dst_step_sn … HM) /2 width=1/ +| #p #_ #IHp #N1 #N2 #H1 #M1 #H2 + elim (pl_sred_inv_dx … H1 ??) -H1 [3: // |2: skip ] #D #C1 #C2 #HC12 #HN1 #HN2 (**) (* simplify line *) + elim (dst_inv_appl … H2 … HN1) -N1 #s #B #A1 #Hs #HM1 #HBD #HAC1 + elim (IHp … HC12 … HAC1) -p -C1 #p #C1 #Hp #HAC1 #HC12 + lapply (pl_sreds_step_dx … HM1 (dx::p) (@B.C1) ?) -HM1 /2 width=1/ -A1 #HM1 + elim (pl_sreds_inv_pos … HM1 ?) -HM1 + [2: >length_append normalize in ⊢ (??(??%)); // ] + #q #r #M #Hq #HM1 #HM + lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -p -s * #Hq #Hr + @(ex3_2_intro … HM1) -M1 // -q /2 width=7/ +] +qed-. + +theorem pl_sreds_in_whd_swap: ∀s,M1,N1. M1 ↦*[s] N1 → + ∀p,N2. in_whd p → N1 ↦[p] N2 → + ∃∃q,r,M2. in_whd q & M1 ↦[q] M2 & M2 ↦*[r] N2 & + is_standard (q::r). +#s #M1 #N1 #HMN1 #p #N2 #Hp #HN12 +lapply (pl_sreds_dst … HMN1) -s #HMN1 +elim (dst_in_whd_swap … Hp … HN12 … HMN1) -p -N1 #q #M2 #Hq #HM12 #HMN2 +elim (dst_inv_pl_sreds_is_standard … HMN2) -HMN2 /3 width=8/ +qed-. diff --git a/matita/matita/contribs/lambda/paths/labeled_sequential_computation.ma b/matita/matita/contribs/lambda/paths/labeled_sequential_computation.ma new file mode 100644 index 000000000..57a88baa8 --- /dev/null +++ b/matita/matita/contribs/lambda/paths/labeled_sequential_computation.ma @@ -0,0 +1,112 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "terms/labeled_sequential_computation.ma". +include "paths/trace.ma". +include "paths/labeled_sequential_reduction.ma". + +(* PATH-LABELED SEQUENTIAL COMPUTATION (MULTISTEP) *******************************) + +(* Note: lstar shuld be replaced by l_sreds *) +definition pl_sreds: trace → relation term ≝ lstar … pl_sred. + +interpretation "path-labeled sequential computation" + 'SeqRedStar M s N = (pl_sreds s M N). + +lemma sreds_pl_sreds: ∀M,N. M ↦* N → ∃s. M ↦*[s] N. +/3 width=1 by sreds_l_sreds, sred_pl_sred/ +qed-. + +lemma pl_sreds_inv_sreds: ∀s,M,N. M ↦*[s] N → M ↦* N. +/3 width=5 by l_sreds_inv_sreds, pl_sred_inv_sred/ +qed-. + +lemma pl_sreds_refl: reflexive … (pl_sreds (◊)). +// +qed. + +lemma pl_sreds_step_sn: ∀p,M1,M. M1 ↦[p] M → ∀s,M2. M ↦*[s] M2 → M1 ↦*[p::s] M2. +/2 width=3/ +qed-. + +lemma pl_sreds_step_dx: ∀s,M1,M. M1 ↦*[s] M → ∀p,M2. M ↦[p] M2 → M1 ↦*[s@p::◊] M2. +/2 width=3/ +qed-. + +lemma pl_sreds_step_rc: ∀p,M1,M2. M1 ↦[p] M2 → M1 ↦*[p::◊] M2. +/2 width=1/ +qed. + +lemma pl_sreds_inv_nil: ∀s,M1,M2. M1 ↦*[s] M2 → ◊ = s → M1 = M2. +/2 width=5 by lstar_inv_nil/ +qed-. + +lemma pl_sreds_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 pl_sreds_inv_step_rc: ∀p,M1,M2. M1 ↦*[p::◊] M2 → M1 ↦[p] M2. +/2 width=1 by lstar_inv_step/ +qed-. + +lemma pl_sreds_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-. + +lemma lsred_compatible_rc: ho_compatible_rc pl_sreds. +/3 width=1/ +qed. + +lemma pl_sreds_compatible_sn: ho_compatible_sn pl_sreds. +/3 width=1/ +qed. + +lemma pl_sreds_compatible_dx: ho_compatible_dx pl_sreds. +/3 width=1/ +qed. + +lemma pl_sreds_lift: ∀s. liftable (pl_sreds s). +/2 width=1/ +qed. + +lemma pl_sreds_inv_lift: ∀s. deliftable_sn (pl_sreds s). +/3 width=3 by lstar_deliftable_sn, pl_sred_inv_lift/ +qed-. + +lemma pl_sreds_dsubst: ∀s. dsubstable_dx (pl_sreds s). +/2 width=1/ +qed. + +theorem pl_sreds_mono: ∀s. singlevalued … (pl_sreds s). +/3 width=7 by lstar_singlevalued, pl_sred_mono/ +qed-. + +theorem pl_sreds_trans: ltransitive … pl_sreds. +/2 width=3 by lstar_ltransitive/ +qed-. + +lemma pl_sreds_compatible_appl: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 → + @B1.A1 ↦*[(sn:::r)@dx:::s] @B2.A2. +#r #B1 #B2 #HB12 #s #A1 #A2 #HA12 +@(pl_sreds_trans … (@B2.A1)) /2 width=1/ +qed. + +lemma pl_sreds_compatible_beta: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 → + @B1.𝛌.A1 ↦*[(sn:::r)@(dx:::rc:::s)@◊::◊] [↙B2] A2. +#r #B1 #B2 #HB12 #s #A1 #A2 #HA12 +@(pl_sreds_trans … (@B2.𝛌.A1)) /2 width=1/ -r -B1 +@(pl_sreds_step_dx … (@B2.𝛌.A2)) // /3 width=1/ +qed. diff --git a/matita/matita/contribs/lambda/paths/labeled_sequential_reduction.ma b/matita/matita/contribs/lambda/paths/labeled_sequential_reduction.ma new file mode 100644 index 000000000..891af919e --- /dev/null +++ b/matita/matita/contribs/lambda/paths/labeled_sequential_reduction.ma @@ -0,0 +1,128 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "paths/path.ma". +include "terms/sequential_reduction.ma". + +(* PATH-LABELED SEQUENTIAL REDUCTION (SINGLE STEP) **************************) + +inductive pl_sred: path → relation term ≝ +| pl_sred_beta : ∀B,A. pl_sred (◊) (@B.𝛌.A) ([↙B]A) +| pl_sred_abst : ∀p,A1,A2. pl_sred p A1 A2 → pl_sred (rc::p) (𝛌.A1) (𝛌.A2) +| pl_sred_appl_sn: ∀p,B1,B2,A. pl_sred p B1 B2 → pl_sred (sn::p) (@B1.A) (@B2.A) +| pl_sred_appl_dx: ∀p,B,A1,A2. pl_sred p A1 A2 → pl_sred (dx::p) (@B.A1) (@B.A2) +. + +interpretation "path-labeled sequential reduction" + 'SeqRed M p N = (pl_sred p M N). + +lemma sred_pl_sred: ∀M,N. M ↦ N → ∃p. M ↦[p] N. +#M #N #H elim H -M -N +[ /2 width=2/ +| #A1 #A2 #_ * /3 width=2/ +| #B1 #B2 #A #_ * /3 width=2/ +| #B #A1 #A2 #_ * /3 width=2/ +] +qed-. + +lemma pl_sred_inv_sred: ∀p,M,N. M ↦[p] N → M ↦ N. +#p #M #N #H elim H -p -M -N // /2 width=1/ +qed-. + +lemma pl_sred_inv_vref: ∀p,M,N. M ↦[p] N → ∀i. #i = M → ⊥. +/3 width=5 by pl_sred_inv_sred, sred_inv_vref/ +qed-. + +lemma pl_sred_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 +| #p #B1 #B2 #A #_ #H destruct +| #p #B #A1 #A2 #_ #H destruct +] +qed-. + +lemma pl_sred_inv_rc: ∀p,M,N. M ↦[p] N → ∀q. rc::q = p → + ∃∃A1,A2. A1 ↦[q] A2 & 𝛌.A1 = M & 𝛌.A2 = N. +#p #M #N * -p -M -N +[ #B #A #q #H destruct +| #p #A1 #A2 #HA12 #q #H destruct /2 width=5/ +| #p #B1 #B2 #A #_ #q #H destruct +| #p #B #A1 #A2 #_ #q #H destruct +] +qed-. + +lemma pl_sred_inv_sn: ∀p,M,N. M ↦[p] N → ∀q. sn::q = p → + ∃∃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 #_ #q #H destruct +| #p #B1 #B2 #A #HB12 #q #H destruct /2 width=6/ +| #p #B #A1 #A2 #_ #q #H destruct +] +qed-. + +lemma pl_sred_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 +| #p #B1 #B2 #A #_ #q #H destruct +| #p #B #A1 #A2 #HA12 #q #H destruct /2 width=6/ +] +qed-. + +lemma pl_sred_lift: ∀p. liftable (pl_sred p). +#p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/ +#B #A #d dsubst_dsubst_ge // +qed. + +theorem pl_sred_mono: ∀p. singlevalued … (pl_sred p). +#p #M #N1 #H elim H -p -M -N1 +[ #B #A #N2 #H elim (pl_sred_inv_nil … H ?) -H // + #D #C #H #HN2 destruct // +| #p #A1 #A2 #_ #IHA12 #N2 #H elim (pl_sred_inv_rc … H ??) -H [3: // |2: skip ] (**) (* simplify line *) + #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ +| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (pl_sred_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *) + #D1 #D2 #C #HD12 #H #HN2 destruct /3 width=1/ +| #p #B #A1 #A2 #_ #IHA12 #N2 #H elim (pl_sred_inv_dx … H ??) -H [3: // |2: skip ] (**) (* simplify line *) + #D #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ +] +qed-. diff --git a/matita/matita/contribs/lambda/terms/pointer.ma b/matita/matita/contribs/lambda/paths/path.ma similarity index 75% rename from matita/matita/contribs/lambda/terms/pointer.ma rename to matita/matita/contribs/lambda/paths/path.ma index 79b269351..c9f4cc244 100644 --- a/matita/matita/contribs/lambda/terms/pointer.ma +++ b/matita/matita/contribs/lambda/paths/path.ma @@ -14,41 +14,41 @@ include "terms/term.ma". -(* POINTER ******************************************************************) +(* PATH *********************************************************************) -(* Policy: pointer step metavariables: c *) +(* Policy: path step metavariables: c *) (* Note: this is a step of a path in the tree representation of a term: rc (rectus) : proceed on the argument of an abstraction sn (sinister): proceed on the left argument of an application dx (dexter) : proceed on the right argument of an application *) -inductive ptr_step: Type[0] ≝ -| rc: ptr_step -| sn: ptr_step -| dx: ptr_step +inductive step: Type[0] ≝ +| rc: step +| sn: step +| dx: step . -definition is_dx: predicate ptr_step ≝ λc. dx = c. +definition is_dx: predicate step ≝ λc. dx = c. -(* Policy: pointer metavariables: p, q *) +(* Policy: path metavariables: p, q *) (* Note: this is a path in the tree representation of a term, heading to a redex *) -definition ptr: Type[0] ≝ list ptr_step. +definition path: Type[0] ≝ list step. (* Note: a redex is "in whd" when is not under an abstraction nor in the lefr argument of an application *) -definition in_whd: predicate ptr ≝ All … is_dx. +definition in_whd: predicate path ≝ All … is_dx. -lemma in_whd_ind: ∀R:predicate ptr. R (◊) → +lemma in_whd_ind: ∀R:predicate path. R (◊) → (∀p. in_whd p → R p → R (dx::p)) → ∀p. in_whd p → R p. #R #H #IH #p elim p -p // -H * #p #IHp * #H1 #H2 destruct /3 width=1/ qed-. -definition compatible_rc: predicate (ptr→relation term) ≝ λR. +definition compatible_rc: predicate (path→relation term) ≝ λR. ∀p,A1,A2. R p A1 A2 → R (rc::p) (𝛌.A1) (𝛌.A2). -definition compatible_sn: predicate (ptr→relation term) ≝ λR. +definition compatible_sn: predicate (path→relation term) ≝ λR. ∀p,B1,B2,A. R p B1 B2 → R (sn::p) (@B1.A) (@B2.A). -definition compatible_dx: predicate (ptr→relation term) ≝ λR. +definition compatible_dx: predicate (path→relation term) ≝ λR. ∀p,B,A1,A2. R p A1 A2 → R (dx::p) (@B.A1) (@B.A2). diff --git a/matita/matita/contribs/lambda/paths/standard_order.ma b/matita/matita/contribs/lambda/paths/standard_order.ma new file mode 100644 index 000000000..563cdce34 --- /dev/null +++ b/matita/matita/contribs/lambda/paths/standard_order.ma @@ -0,0 +1,162 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "paths/path.ma". + +(* STANDARD ORDER ************************************************************) + +(* Note: standard precedence relation on paths: p ≺ q + to serve as base for the order relations: p < q and p ≤ q *) +inductive sprec: relation path ≝ +| sprec_nil : ∀c,q. sprec (◊) (c::q) +| sprec_rc : ∀p,q. sprec (dx::p) (rc::q) +| sprec_sn : ∀p,q. sprec (rc::p) (sn::q) +| sprec_comp: ∀c,p,q. sprec p q → sprec (c::p) (c::q) +| sprec_skip: sprec (dx::◊) ◊ +. + +interpretation "standard 'precedes' on paths" + 'prec p q = (sprec p q). + +lemma sprec_inv_sn: ∀p,q. p ≺ q → ∀p0. sn::p0 = p → + ∃∃q0. p0 ≺ q0 & sn::q0 = q. +#p #q * -p -q +[ #c #q #p0 #H destruct +| #p #q #p0 #H destruct +| #p #q #p0 #H destruct +| #c #p #q #Hpq #p0 #H destruct /2 width=3/ +| #p0 #H destruct +] +qed-. + +lemma sprec_fwd_in_whd: ∀p,q. p ≺ q → in_whd q → in_whd p. +#p #q #H elim H -p -q // /2 width=1/ +[ #p #q * #H destruct +| #p #q * #H destruct +| #c #p #q #_ #IHpq * #H destruct /3 width=1/ +] +qed-. + +(* Note: this is p < q *) +definition slt: relation path ≝ TC … sprec. + +interpretation "standard 'less than' on paths" + 'lt p q = (slt p q). + +lemma slt_step_rc: ∀p,q. p ≺ q → p < q. +/2 width=1/ +qed. + +lemma slt_nil: ∀c,p. ◊ < c::p. +/2 width=1/ +qed. + +lemma slt_skip: dx::◊ < ◊. +/2 width=1/ +qed. + +lemma slt_comp: ∀c,p,q. p < q → c::p < c::q. +#c #p #q #H elim H -q /3 width=1/ /3 width=3/ +qed. + +theorem slt_trans: transitive … slt. +/2 width=3/ +qed-. + +lemma slt_refl: ∀p. p < p. +#p elim p -p /2 width=1/ +@(slt_trans … (dx::◊)) // +qed. + +(* Note: this is p ≤ q *) +definition sle: relation path ≝ star … sprec. + +interpretation "standard 'less or equal to' on paths" + 'leq p q = (sle p q). + +lemma sle_step_rc: ∀p,q. p ≺ q → p ≤ q. +/2 width=1/ +qed. + +lemma sle_step_sn: ∀p1,p,p2. p1 ≺ p → p ≤ p2 → p1 ≤ p2. +/2 width=3/ +qed-. + +lemma sle_rc: ∀p,q. dx::p ≤ rc::q. +/2 width=1/ +qed. + +lemma sle_sn: ∀p,q. rc::p ≤ sn::q. +/2 width=1/ +qed. + +lemma sle_skip: dx::◊ ≤ ◊. +/2 width=1/ +qed. + +lemma sle_nil: ∀p. ◊ ≤ p. +* // /2 width=1/ +qed. + +lemma sle_comp: ∀p1,p2. p1 ≤ p2 → ∀c. (c::p1) ≤ (c::p2). +#p1 #p2 #H elim H -p2 // /3 width=3/ +qed. + +lemma sle_skip_sle: ∀p. p ≤ ◊ → dx::p ≤ ◊. +#p #H @(star_ind_l ??????? H) -p // +#p #q #Hpq #_ #H @(sle_step_sn … H) -H /2 width=1/ +qed. + +theorem sle_trans: transitive … sle. +/2 width=3/ +qed-. + +lemma sle_cons: ∀p,q. dx::p ≤ sn::q. +#p #q +@(sle_trans … (rc::q)) /2 width=1/ +qed. + +lemma sle_dichotomy: ∀p1,p2:path. p1 ≤ p2 ∨ p2 ≤ p1. +#p1 elim p1 -p1 +[ * /2 width=1/ +| #c1 #p1 #IHp1 * /2 width=1/ + * #p2 cases c1 -c1 /2 width=1/ + elim (IHp1 p2) -IHp1 /3 width=1/ +] +qed-. + +lemma sle_inv_sn: ∀p,q. p ≤ q → ∀p0. sn::p0 = p → + ∃∃q0. p0 ≤ q0 & sn::q0 = q. +#p #q #H elim H -q /2 width=3/ +#q #q0 #_ #Hq0 #IHpq #p0 #H destruct +elim (IHpq p0 ?) -IHpq // #p1 #Hp01 #H +elim (sprec_inv_sn … Hq0 … H) -q /3 width=3/ +qed-. + +lemma in_whd_sle_nil: ∀p. in_whd p → p ≤ ◊. +#p #H @(in_whd_ind … H) -p // /2 width=1/ +qed. + +theorem in_whd_sle: ∀p. in_whd p → ∀q. p ≤ q. +#p #H @(in_whd_ind … H) -p // +#p #_ #IHp * /3 width=1/ * #q /2 width=1/ +qed. + +lemma sle_nil_inv_in_whd: ∀p. p ≤ ◊ → in_whd p. +#p #H @(star_ind_l ??????? H) -p // /2 width=3 by sprec_fwd_in_whd/ +qed-. + +lemma sle_inv_in_whd: ∀p. (∀q. p ≤ q) → in_whd p. +/2 width=1 by sle_nil_inv_in_whd/ +qed-. diff --git a/matita/matita/contribs/lambda/terms/pointer_list_standard.ma b/matita/matita/contribs/lambda/paths/standard_trace.ma similarity index 87% rename from matita/matita/contribs/lambda/terms/pointer_list_standard.ma rename to matita/matita/contribs/lambda/paths/standard_trace.ma index 0c3cc2364..5f3ec7085 100644 --- a/matita/matita/contribs/lambda/terms/pointer_list_standard.ma +++ b/matita/matita/contribs/lambda/paths/standard_trace.ma @@ -12,13 +12,13 @@ (* *) (**************************************************************************) -include "terms/pointer_list.ma". -include "terms/pointer_order.ma". +include "paths/trace.ma". +include "paths/standard_order.ma". -(* STANDARD POINTER LIST ****************************************************) +(* STANDARD TRACE ***********************************************************) -(* Note: to us, a "normal" computation contracts redexes in non-decreasing positions *) -definition is_standard: predicate ptrl ≝ Allr … ple. +(* Note: to us, a "standard" computation contracts redexes in non-decreasing positions *) +definition is_standard: predicate trace ≝ Allr … sle. lemma is_standard_compatible: ∀c,s. is_standard s → is_standard (c:::s). #c #s elim s -s // #p * // diff --git a/matita/matita/contribs/lambda/terms/pointer_list.ma b/matita/matita/contribs/lambda/paths/trace.ma similarity index 82% rename from matita/matita/contribs/lambda/terms/pointer_list.ma rename to matita/matita/contribs/lambda/paths/trace.ma index c1e710649..53b979809 100644 --- a/matita/matita/contribs/lambda/terms/pointer_list.ma +++ b/matita/matita/contribs/lambda/paths/trace.ma @@ -12,15 +12,15 @@ (* *) (**************************************************************************) -include "terms/pointer.ma". +include "paths/path.ma". -(* POINTER LIST *************************************************************) +(* TRACE ********************************************************************) -(* Policy: pointer list metavariables: r, s *) -definition ptrl: Type[0] ≝ list ptr. +(* Policy: trace metavariables: r, s *) +definition trace: Type[0] ≝ list path. (* Note: a "whd" computation contracts just redexes in the whd *) -definition is_whd: predicate ptrl ≝ All … in_whd. +definition is_whd: predicate trace ≝ All … in_whd. lemma is_whd_dx: ∀s. is_whd s → is_whd (dx:::s). #s elim s -s // @@ -32,13 +32,13 @@ lemma is_whd_append: ∀r. is_whd r → ∀s. is_whd s → is_whd (r@s). #q #r #IHr * /3 width=1/ qed. -definition ho_compatible_rc: predicate (ptrl→relation term) ≝ λR. +definition ho_compatible_rc: predicate (trace→relation term) ≝ λR. ∀s,A1,A2. R s A1 A2 → R (rc:::s) (𝛌.A1) (𝛌.A2). -definition ho_compatible_sn: predicate (ptrl→relation term) ≝ λR. +definition ho_compatible_sn: predicate (trace→relation term) ≝ λR. ∀s,B1,B2,A. R s B1 B2 → R (sn:::s) (@B1.A) (@B2.A). -definition ho_compatible_dx: predicate (ptrl→relation term) ≝ λR. +definition ho_compatible_dx: predicate (trace→relation term) ≝ λR. ∀s,B,A1,A2. R s A1 A2 → R (dx:::s) (@B.A1) (@B.A2). lemma lstar_compatible_rc: ∀R. compatible_rc R → ho_compatible_rc (lstar … R). diff --git a/matita/matita/contribs/lambda/subterms/subterms.ma b/matita/matita/contribs/lambda/subterms/subterms.ma index 1a2582a81..565ed833a 100644 --- a/matita/matita/contribs/lambda/subterms/subterms.ma +++ b/matita/matita/contribs/lambda/subterms/subterms.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "preamble.ma". -include "notation.ma". +include "background/preamble.ma". +include "background/notation.ma". (* SUBSETS OF SUBTERMS ******************************************************) diff --git a/matita/matita/contribs/lambda/terms/labeled_sequential_computation.ma b/matita/matita/contribs/lambda/terms/labeled_sequential_computation.ma index 0dc7c53b5..558968e25 100644 --- a/matita/matita/contribs/lambda/terms/labeled_sequential_computation.ma +++ b/matita/matita/contribs/lambda/terms/labeled_sequential_computation.ma @@ -12,134 +12,35 @@ (* *) (**************************************************************************) -include "terms/pointer_list.ma". -include "terms/parallel_computation.ma". +include "terms/sequential_computation.ma". -(* LABELED SEQUENTIAL COMPUTATION (MULTISTEP) *******************************) +(* ABSTRACT LABELED SEQUENTIAL COMPUTATION (MULTISTEP) **********************) -definition lsreds: ptrl → relation term ≝ lstar … lsred. +definition l_sreds: ∀S. (S→relation term) → list S → relation term ≝ + λS,R. lstar … R. -interpretation "labelled sequential computation" - 'SeqRedStar M s N = (lsreds s M N). - -notation "hvbox( M break ↦* [ term 46 s ] break term 46 N )" - non associative with precedence 45 - for @{ 'SeqRedStar $M $s $N }. - -lemma lsreds_refl: reflexive … (lsreds (◊)). -// -qed. - -lemma lsreds_step_sn: ∀p,M1,M. M1 ↦[p] M → ∀s,M2. M ↦*[s] M2 → M1 ↦*[p::s] M2. -/2 width=3/ -qed-. - -lemma lsreds_step_dx: ∀s,M1,M. M1 ↦*[s] M → ∀p,M2. M ↦[p] M2 → M1 ↦*[s@p::◊] M2. -/2 width=3/ -qed-. - -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. -/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. -/2 width=3 by lstar_inv_cons/ -qed-. - -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. -/2 width=1 by lstar_inv_pos/ -qed-. - -lemma lsred_compatible_rc: ho_compatible_rc lsreds. -/3 width=1/ -qed. - -lemma lsreds_compatible_sn: ho_compatible_sn lsreds. -/3 width=1/ -qed. - -lemma lsreds_compatible_dx: ho_compatible_dx lsreds. -/3 width=1/ -qed. - -lemma lsreds_lift: ∀s. liftable (lsreds s). -/2 width=1/ -qed. - -lemma lsreds_inv_lift: ∀s. deliftable_sn (lsreds s). -/3 width=3 by lstar_deliftable_sn, lsred_inv_lift/ +lemma sreds_l_sreds: ∀S,R. (∀M,N. M ↦ N → ∃a. R a M N) → + ∀M,N. M ↦* N → ∃l. l_sreds S R l M N. +#S #R #HR #M #N #H elim H -N +[ #N #N0 #_ #HN0 * #l #HMN + elim (HR … HN0) -HR -HN0 /3 width=5/ +| /2 width=2/ +] qed-. -lemma lsreds_dsubst: ∀s. dsubstable_dx (lsreds s). -/2 width=1/ -qed. - -theorem lsreds_mono: ∀s. singlevalued … (lsreds s). -/3 width=7 by lstar_singlevalued, lsred_mono/ -qed-. - -theorem lsreds_trans: ltransitive … lsreds. -/2 width=3 by lstar_ltransitive/ +lemma l_sreds_inv_sreds: ∀S,R. (∀a,M,N. R a M N → M ↦ N) → + ∀l,M,N. l_sreds S R l M N → M ↦* N. +#S #R #HR #l #M #N #H elim H -N // /3 by star_compl/ qed-. -lemma lsreds_compatible_appl: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 → - @B1.A1 ↦*[(sn:::r)@dx:::s] @B2.A2. -#r #B1 #B2 #HB12 #s #A1 #A2 #HA12 -@(lsreds_trans … (@B2.A1)) /2 width=1/ -qed. - -lemma lsreds_compatible_beta: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 → - @B1.𝛌.A1 ↦*[(sn:::r)@(dx:::rc:::s)@◊::◊] [↙B2] A2. -#r #B1 #B2 #HB12 #s #A1 #A2 #HA12 -@(lsreds_trans … (@B2.𝛌.A1)) /2 width=1/ -r -B1 -@(lsreds_step_dx … (@B2.𝛌.A2)) // /3 width=1/ -qed. - (* Note: "|s|" should be unparetesized *) -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 +lemma l_sreds_fwd_mult: ∀S,R. (∀a,M,N. R a M N → M ↦ N) → + ∀l,M1,M2. l_sreds S R l M1 M2 → + ♯{M2} ≤ ♯{M1} ^ (2 ^ (|l|)). +#S #R #HR #l #M1 #M2 #H @(lstar_ind_l ????????? H) -l -M1 normalize // +#a #l #M1 #M #HM1 #_ #IHM2 +lapply (HR … HM1) -HR -a #HM1 +lapply (sred_fwd_mult … HM1) #HM1 @(transitive_le … IHM2) -M2 /3 width=1 by le_exp1, lt_O_exp, lt_to_le/ (**) (* auto: slow without trace *) qed-. - -theorem lsreds_preds: ∀s,M1,M2. M1 ↦*[s] M2 → M1 ⤇* M2. -#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 // -#a #s #M1 #M #HM1 #_ #IHM2 -@(preds_step_sn … IHM2) -M2 /2 width=2/ -qed. - -lemma pred_lsreds: ∀M1,M2. M1 ⤇ M2 → ∃r. M1 ↦*[r] M2. -#M1 #M2 #H elim H -M1 -M2 /2 width=2/ -[ #A1 #A2 #_ * /3 width=2/ -| #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/ -| #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/ -qed-. - -theorem preds_lsreds: ∀M1,M2. M1 ⤇* M2 → ∃r. M1 ↦*[r] M2. -#M1 #M2 #H elim H -M2 /2 width=2/ -#M #M2 #_ #HM2 * #r #HM1 -elim (pred_lsreds … HM2) -HM2 #s #HM2 -lapply (lsreds_trans … HM1 … HM2) -M /2 width=2/ -qed-. - -theorem lsreds_conf: ∀s1,M0,M1. M0 ↦*[s1] M1 → ∀s2,M2. M0 ↦*[s2] M2 → - ∃∃r1,r2,M. M1 ↦*[r1] M & M2 ↦*[r2] M. -#s1 #M0 #M1 #HM01 #s2 #M2 #HM02 -lapply (lsreds_preds … HM01) -s1 #HM01 -lapply (lsreds_preds … HM02) -s2 #HM02 -elim (preds_conf … HM01 … HM02) -M0 #M #HM1 #HM2 -elim (preds_lsreds … HM1) -HM1 -elim (preds_lsreds … HM2) -HM2 /2 width=5/ -qed-. diff --git a/matita/matita/contribs/lambda/terms/labeled_sequential_reduction.ma b/matita/matita/contribs/lambda/terms/labeled_sequential_reduction.ma deleted file mode 100644 index 54daa9257..000000000 --- a/matita/matita/contribs/lambda/terms/labeled_sequential_reduction.ma +++ /dev/null @@ -1,143 +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 "terms/pointer.ma". -include "terms/multiplicity.ma". - -(* LABELED SEQUENTIAL REDUCTION (SINGLE STEP) *******************************) - -(* Note: the application "(A B)" is represented by "@B.A" following: - F. Kamareddine and R.P. Nederpelt: "A useful λ-notation". - 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_abst : ∀p,A1,A2. lsred p A1 A2 → lsred (rc::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) -. - -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 )" - non associative with precedence 45 - for @{ 'SeqRed $M $p $N }. - -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 -| #p #B1 #B2 #A #_ #i #H destruct -| #p #B #A1 #A2 #_ #i #H destruct -] -qed-. - -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 -| #p #B1 #B2 #A #_ #H destruct -| #p #B #A1 #A2 #_ #H destruct -] -qed-. - -lemma lsred_inv_rc: ∀p,M,N. M ↦[p] N → ∀q. rc::q = p → - ∃∃A1,A2. A1 ↦[q] A2 & 𝛌.A1 = M & 𝛌.A2 = N. -#p #M #N * -p -M -N -[ #B #A #q #H destruct -| #p #A1 #A2 #HA12 #q #H destruct /2 width=5/ -| #p #B1 #B2 #A #_ #q #H destruct -| #p #B #A1 #A2 #_ #q #H destruct -] -qed-. - -lemma lsred_inv_sn: ∀p,M,N. M ↦[p] N → ∀q. sn::q = p → - ∃∃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 #_ #q #H destruct -| #p #B1 #B2 #A #HB12 #q #H destruct /2 width=6/ -| #p #B #A1 #A2 #_ #q #H destruct -] -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. -#p #M #N * -p -M -N -[ #B #A #q #H destruct -| #p #A1 #A2 #_ #q #H destruct -| #p #B1 #B2 #A #_ #q #H destruct -| #p #B #A1 #A2 #HA12 #q #H destruct /2 width=6/ -] -qed-. - -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 *) -| // -| #p #B #D #A #_ #IHBD - @(lt_to_le_to_lt … (♯{B}*♯{B}+♯{A})) [ /2 width=1/ ] -D -p -| #p #B #A #C #_ #IHAC - @(lt_to_le_to_lt … (♯{B}+♯{A}*♯{A})) [ /2 width=1/ ] -C -p -] -@(transitive_le … (♯{B}*♯{B}+♯{A}*♯{A})) [ /2 width=1/ ] ->distributive_times_plus normalize /2 width=1/ -qed-. - -lemma lsred_lift: ∀p. liftable (lsred p). -#p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/ -#B #A #d dsubst_dsubst_ge // -qed. - -theorem lsred_mono: ∀p. singlevalued … (lsred p). -#p #M #N1 #H elim H -p -M -N1 -[ #B #A #N2 #H elim (lsred_inv_nil … H ?) -H // - #D #C #H #HN2 destruct // -| #p #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_rc … H ??) -H [3: // |2: skip ] (**) (* simplify line *) - #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ -| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (lsred_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *) - #D1 #D2 #C #HD12 #H #HN2 destruct /3 width=1/ -| #p #B #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_dx … H ??) -H [3: // |2: skip ] (**) (* simplify line *) - #D #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ -] -qed-. diff --git a/matita/matita/contribs/lambda/terms/parallel_computation.ma b/matita/matita/contribs/lambda/terms/parallel_computation.ma index 4f93f90a7..3b048d133 100644 --- a/matita/matita/contribs/lambda/terms/parallel_computation.ma +++ b/matita/matita/contribs/lambda/terms/parallel_computation.ma @@ -21,10 +21,6 @@ definition preds: relation term ≝ star … pred. interpretation "parallel computation" 'ParRedStar M N = (preds M N). -notation "hvbox( M ⤇* break term 46 N )" - non associative with precedence 45 - for @{ 'ParRedStar $M $N }. - lemma preds_refl: reflexive … preds. // qed. diff --git a/matita/matita/contribs/lambda/terms/parallel_reduction.ma b/matita/matita/contribs/lambda/terms/parallel_reduction.ma index a9190151b..2e082eaaa 100644 --- a/matita/matita/contribs/lambda/terms/parallel_reduction.ma +++ b/matita/matita/contribs/lambda/terms/parallel_reduction.ma @@ -12,13 +12,13 @@ (* *) (**************************************************************************) -include "terms/length.ma". -include "terms/labeled_sequential_reduction.ma". +include "terms/size.ma". +include "terms/sequential_reduction.ma". (* PARALLEL REDUCTION (SINGLE STEP) *****************************************) (* Note: the application "(A B)" is represented by "@B.A" - as for labelled sequential reduction + as for sequential reduction *) inductive pred: relation term ≝ | pred_vref: ∀i. pred (#i) (#i) @@ -30,10 +30,6 @@ inductive pred: relation term ≝ interpretation "parallel reduction" 'ParRed M N = (pred M N). -notation "hvbox( M ⤇ break term 46 N )" - non associative with precedence 45 - for @{ 'ParRed $M $N }. - lemma pred_refl: reflexive … pred. #M elim M -M // /2 width=1/ qed. @@ -131,7 +127,7 @@ elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/ qed-. theorem pred_conf: confluent … pred. -#M @(f_ind … length … M) -M #n #IH * normalize +#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 @@ -151,6 +147,6 @@ theorem pred_conf: confluent … pred. ] qed-. -lemma lsred_pred: ∀p,M,N. M ↦[p] N → M ⤇ N. -#p #M #N #H elim H -p -M -N /2 width=1/ +lemma sred_pred: ∀M,N. M ↦ N → M ⤇ N. +#M #N #H elim H -M -N /2 width=1/ qed. diff --git a/matita/matita/contribs/lambda/terms/pointer_order.ma b/matita/matita/contribs/lambda/terms/pointer_order.ma deleted file mode 100644 index 1ead95b99..000000000 --- a/matita/matita/contribs/lambda/terms/pointer_order.ma +++ /dev/null @@ -1,148 +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 "terms/pointer.ma". - -(* POINTER ORDER ************************************************************) - -(* Note: precedence relation on redex pointers: p ≺ q - to serve as base for the order relations: p < q and p ≤ q *) -inductive pprec: relation ptr ≝ -| pprec_nil : ∀c,q. pprec (◊) (c::q) -| ppprc_rc : ∀p,q. pprec (dx::p) (rc::q) -| ppprc_sn : ∀p,q. pprec (rc::p) (sn::q) -| pprec_comp: ∀c,p,q. pprec p q → pprec (c::p) (c::q) -| pprec_skip: pprec (dx::◊) ◊ -. - -interpretation "'precedes' on pointers" - 'prec p q = (pprec p q). - -(* Note: this should go to core_notation *) -notation "hvbox(a break ≺ b)" - non associative with precedence 45 - for @{ 'prec $a $b }. - -lemma pprec_fwd_in_whd: ∀p,q. p ≺ q → in_whd q → in_whd p. -#p #q #H elim H -p -q // /2 width=1/ -[ #p #q * #H destruct -| #p #q * #H destruct -| #c #p #q #_ #IHpq * #H destruct /3 width=1/ -] -qed-. - -(* Note: this is p < q *) -definition plt: relation ptr ≝ TC … pprec. - -interpretation "'less than' on redex pointers" - 'lt p q = (plt p q). - -lemma plt_step_rc: ∀p,q. p ≺ q → p < q. -/2 width=1/ -qed. - -lemma plt_nil: ∀c,p. ◊ < c::p. -/2 width=1/ -qed. - -lemma plt_skip: dx::◊ < ◊. -/2 width=1/ -qed. - -lemma plt_comp: ∀c,p,q. p < q → c::p < c::q. -#c #p #q #H elim H -q /3 width=1/ /3 width=3/ -qed. - -theorem plt_trans: transitive … plt. -/2 width=3/ -qed-. - -lemma plt_refl: ∀p. p < p. -#p elim p -p /2 width=1/ -@(plt_trans … (dx::◊)) // -qed. - -(* Note: this is p ≤ q *) -definition ple: relation ptr ≝ star … pprec. - -interpretation "'less or equal to' on redex pointers" - 'leq p q = (ple p q). - -lemma ple_step_rc: ∀p,q. p ≺ q → p ≤ q. -/2 width=1/ -qed. - -lemma ple_step_sn: ∀p1,p,p2. p1 ≺ p → p ≤ p2 → p1 ≤ p2. -/2 width=3/ -qed-. - -lemma ple_rc: ∀p,q. dx::p ≤ rc::q. -/2 width=1/ -qed. - -lemma ple_sn: ∀p,q. rc::p ≤ sn::q. -/2 width=1/ -qed. - -lemma ple_skip: dx::◊ ≤ ◊. -/2 width=1/ -qed. - -lemma ple_nil: ∀p. ◊ ≤ p. -* // /2 width=1/ -qed. - -lemma ple_comp: ∀p1,p2. p1 ≤ p2 → ∀c. (c::p1) ≤ (c::p2). -#p1 #p2 #H elim H -p2 // /3 width=3/ -qed. - -lemma ple_skip_ple: ∀p. p ≤ ◊ → dx::p ≤ ◊. -#p #H @(star_ind_l ??????? H) -p // -#p #q #Hpq #_ #H @(ple_step_sn … H) -H /2 width=1/ -qed. - -theorem ple_trans: transitive … ple. -/2 width=3/ -qed-. - -lemma ple_cons: ∀p,q. dx::p ≤ sn::q. -#p #q -@(ple_trans … (rc::q)) /2 width=1/ -qed. - -lemma ple_dichotomy: ∀p1,p2:ptr. p1 ≤ p2 ∨ p2 ≤ p1. -#p1 elim p1 -p1 -[ * /2 width=1/ -| #c1 #p1 #IHp1 * /2 width=1/ - * #p2 cases c1 -c1 /2 width=1/ - elim (IHp1 p2) -IHp1 /3 width=1/ -] -qed-. - -lemma in_whd_ple_nil: ∀p. in_whd p → p ≤ ◊. -#p #H @(in_whd_ind … H) -p // /2 width=1/ -qed. - -theorem in_whd_ple: ∀p. in_whd p → ∀q. p ≤ q. -#p #H @(in_whd_ind … H) -p // -#p #_ #IHp * /3 width=1/ * #q /2 width=1/ -qed. - -lemma ple_nil_inv_in_whd: ∀p. p ≤ ◊ → in_whd p. -#p #H @(star_ind_l ??????? H) -p // /2 width=3 by pprec_fwd_in_whd/ -qed-. - -lemma ple_inv_in_whd: ∀p. (∀q. p ≤ q) → in_whd p. -/2 width=1 by ple_nil_inv_in_whd/ -qed-. diff --git a/matita/matita/contribs/lambda/terms/sequential_computation.ma b/matita/matita/contribs/lambda/terms/sequential_computation.ma new file mode 100644 index 000000000..2fc5afd5a --- /dev/null +++ b/matita/matita/contribs/lambda/terms/sequential_computation.ma @@ -0,0 +1,105 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "terms/parallel_computation.ma". + +(* SEQUENTIAL COMPUTATION (MULTISTEP) ***************************************) + +definition sreds: relation term ≝ star … sred. + +interpretation "sequential computation" + 'SeqRedStar M N = (sreds M N). + +lemma sreds_refl: reflexive … sreds. +// +qed. + +lemma sreds_step_sn: ∀M1,M. M1 ↦ M → ∀M2. M ↦* M2 → M1 ↦* M2. +/2 width=3/ +qed-. + +lemma sreds_step_dx: ∀M1,M. M1 ↦* M → ∀M2. M ↦ M2 → M1 ↦* M2. +/2 width=3/ +qed-. + +lemma sreds_step_rc: ∀M1,M2. M1 ↦ M2 → M1 ↦* M2. +/2 width=1/ +qed. + +lemma lsred_compatible_abst: compatible_abst sreds. +/3 width=1/ +qed. + +lemma sreds_compatible_sn: compatible_sn sreds. +/3 width=1/ +qed. + +lemma sreds_compatible_dx: compatible_dx sreds. +/3 width=1/ +qed. + +lemma sreds_compatible_appl: compatible_appl sreds. +/3 width=3/ +qed. + +lemma sreds_lift: liftable sreds. +/2 width=1/ +qed. + +lemma sreds_inv_lift: deliftable_sn sreds. +/3 width=3 by star_deliftable_sn, sred_inv_lift/ +qed-. + +lemma sreds_dsubst: dsubstable_dx sreds. +/2 width=1/ +qed. + +theorem sreds_trans: transitive … sreds. +/2 width=3 by trans_star/ +qed-. + +(* Note: the substitution should be unparentesized *) +lemma sreds_compatible_beta: ∀B1,B2. B1 ↦* B2 → ∀A1,A2. A1 ↦* A2 → + @B1.𝛌.A1 ↦* ([↙B2] A2). +#B1 #B2 #HB12 #A1 #A2 #HA12 +@(sreds_trans … (@B2.𝛌.A1)) /2 width=1/ -B1 +@(sreds_step_dx … (@B2.𝛌.A2)) // /3 width=1/ +qed. + +theorem sreds_preds: ∀M1,M2. M1 ↦* M2 → M1 ⤇* M2. +#M1 #M2 #H @(star_ind_l ??????? H) -M1 // +#M1 #M #HM1 #_ #IHM2 +@(preds_step_sn … IHM2) -M2 /2 width=2/ +qed. + +lemma pred_sreds: ∀M1,M2. M1 ⤇ M2 → M1 ↦* M2. +#M1 #M2 #H elim H -M1 -M2 // /2 width=1/ +qed-. + +theorem preds_sreds: ∀M1,M2. M1 ⤇* M2 → M1 ↦* M2. +#M1 #M2 #H elim H -M2 // +#M #M2 #_ #HM2 #HM1 +lapply (pred_sreds … HM2) -HM2 #HM2 +@(sreds_trans … HM1 … HM2) +qed-. + +theorem sreds_conf: ∀M0,M1. M0 ↦* M1 → ∀M2. M0 ↦* M2 → + ∃∃M. M1 ↦* M & M2 ↦* M. +#M0 #M1 #HM01 #M2 #HM02 +lapply (sreds_preds … HM01) #HM01 +lapply (sreds_preds … HM02) #HM02 +elim (preds_conf … HM01 … HM02) -M0 #M #HM1 #HM2 +lapply (preds_sreds … HM1) -HM1 +lapply (preds_sreds … HM2) -HM2 /2 width=3/ +qed-. diff --git a/matita/matita/contribs/lambda/terms/sequential_reduction.ma b/matita/matita/contribs/lambda/terms/sequential_reduction.ma new file mode 100644 index 000000000..cfd1fbe7f --- /dev/null +++ b/matita/matita/contribs/lambda/terms/sequential_reduction.ma @@ -0,0 +1,106 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "terms/multiplicity.ma". + +(* SEQUENTIAL REDUCTION (SINGLE STEP) ***************************************) + +(* Note: the application "(A B)" is represented by "@B.A" following: + F. Kamareddine and R.P. Nederpelt: "A useful λ-notation". + Theoretical Computer Science 155(1), Elsevier (1996), pp. 85-109. +*) +inductive sred: relation term ≝ +| sred_beta : ∀B,A. sred (@B.𝛌.A) ([↙B]A) +| sred_abst : ∀A1,A2. sred A1 A2 → sred (𝛌.A1) (𝛌.A2) +| sred_appl_sn: ∀B1,B2,A. sred B1 B2 → sred (@B1.A) (@B2.A) +| sred_appl_dx: ∀B,A1,A2. sred A1 A2 → sred (@B.A1) (@B.A2) +. + +interpretation "sequential reduction" + 'SeqRed M N = (sred M N). + +lemma sred_inv_vref: ∀M,N. M ↦ N → ∀i. #i = M → ⊥. +#M #N * -M -N +[ #B #A #i #H destruct +| #A1 #A2 #_ #i #H destruct +| #B1 #B2 #A #_ #i #H destruct +| #B #A1 #A2 #_ #i #H destruct +] +qed-. + +lemma sred_inv_abst: ∀M,N. M ↦ N → ∀C1. 𝛌.C1 = M → + ∃∃C2. C1 ↦ C2 & 𝛌.C2 = N. +#M #N * -M -N +[ #B #A #C #H destruct +| #A1 #A2 #HA12 #C1 #H destruct /2 width=3/ +| #B1 #B2 #A #_ #C1 #H destruct +| #B #A1 #A2 #_ #C1 #H destruct +] +qed-. + +lemma sred_inv_appl: ∀M,N. M ↦ N → ∀D,C. @D.C = M → + ∨∨ (∃∃C0. 𝛌.C0 = C & [↙D] C0 = N) + | (∃∃D0. D ↦ D0 & @D0.C = N) + | (∃∃C0. C ↦ C0 & @D.C0 = N). +#M #N * -M -N +[ #B #A #D #C #H destruct /3 width=3/ +| #A1 #A2 #_ #D #C #H destruct +| #B1 #B2 #A #HB12 #D #C #H destruct /3 width=3/ +| #B #A1 #A2 #HA12 #D #C #H destruct /3 width=3/ +] +qed-. + +lemma sred_fwd_mult: ∀M,N. M ↦ N → ♯{N} < ♯{M} * ♯{M}. +#M #N #H elim H -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 *) +| // +| #B #D #A #_ #IHBD + @(lt_to_le_to_lt … (♯{B}*♯{B}+♯{A})) [ /2 width=1/ ] -D +| #B #A #C #_ #IHAC + @(lt_to_le_to_lt … (♯{B}+♯{A}*♯{A})) [ /2 width=1/ ] -C +] +@(transitive_le … (♯{B}*♯{B}+♯{A}*♯{A})) [ /2 width=1/ ] +>distributive_times_plus normalize /2 width=1/ +qed-. + +lemma sred_lift: liftable sred. +#h #M1 #M2 #H elim H -M1 -M2 normalize /2 width=1/ +#B #A #d dsubst_dsubst_ge // +qed. diff --git a/matita/matita/contribs/lambda/terms/length.ma b/matita/matita/contribs/lambda/terms/size.ma similarity index 80% rename from matita/matita/contribs/lambda/terms/length.ma rename to matita/matita/contribs/lambda/terms/size.ma index 81ce2e379..8ba84e7cc 100644 --- a/matita/matita/contribs/lambda/terms/length.ma +++ b/matita/matita/contribs/lambda/terms/size.ma @@ -14,18 +14,18 @@ include "terms/lift.ma". -(* LENGTH *******************************************************************) +(* SIZE *********************************************************************) (* Note: this gives the number of abstractions and applications in M *) -let rec length M on M ≝ match M with +let rec size M on M ≝ match M with [ VRef i ⇒ 0 -| Abst A ⇒ length A + 1 -| Appl B A ⇒ (length B) + (length A) + 1 +| Abst A ⇒ size A + 1 +| Appl B A ⇒ (size B) + (size A) + 1 ]. -interpretation "term length" - 'card M = (length M). +interpretation "term size" + 'card M = (size M). -lemma length_lift: ∀h,M,d. |↑[d, h] M| = |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/terms/st_computation.ma b/matita/matita/contribs/lambda/terms/st_computation.ma deleted file mode 100644 index 1cd7a9f97..000000000 --- a/matita/matita/contribs/lambda/terms/st_computation.ma +++ /dev/null @@ -1,214 +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 "terms/labeled_sequential_computation.ma". -include "terms/pointer_list_standard.ma". - -(* KASHIMA'S "ST" COMPUTATION ***********************************************) - -(* Note: this is the "standard" computation of: - R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000). -*) -inductive st: relation term ≝ -| st_vref: ∀s,M,i. is_whd s → M ↦*[s] #i → st M (#i) -| st_abst: ∀s,M,A1,A2. is_whd s → M ↦*[s] 𝛌.A1 → st A1 A2 → st M (𝛌.A2) -| st_appl: ∀s,M,B1,B2,A1,A2. is_whd s → 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 )" - non associative with precedence 45 - for @{ 'Std $M $N }. - -lemma st_inv_lref: ∀M,N. M ⓢ⤇* N → ∀j. #j = N → - ∃∃s. is_whd s & M ↦*[s] #j. -#M #N * -M -N -[ /2 width=3/ -| #s #M #A1 #A2 #_ #_ #_ #j #H destruct -| #s #M #B1 #B2 #A1 #A2 #_ #_ #_ #_ #j #H destruct -] -qed-. - -lemma st_inv_abst: ∀M,N. M ⓢ⤇* N → ∀C2. 𝛌.C2 = N → - ∃∃s,C1. is_whd s & M ↦*[s] 𝛌.C1 & C1 ⓢ⤇* C2. -#M #N * -M -N -[ #s #M #i #_ #_ #C2 #H destruct -| #s #M #A1 #A2 #Hs #HM #A12 #C2 #H destruct /2 width=5/ -| #s #M #B1 #B2 #A1 #A2 #_ #_ #_ #_ #C2 #H destruct -] -qed-. - -lemma st_inv_appl: ∀M,N. M ⓢ⤇* N → ∀D2,C2. @D2.C2 = N → - ∃∃s,D1,C1. is_whd s & 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 -| #s #M #B1 #B2 #A1 #A2 #Hs #HM #HB12 #HA12 #D2 #C2 #H destruct /2 width=7/ -] -qed-. - -lemma st_refl: reflexive … st. -#M elim M -M /2 width=3/ /2 width=5/ /2 width=7/ -qed. - -lemma st_step_sn: ∀N1,N2. N1 ⓢ⤇* N2 → ∀s,M. is_whd s → M ↦*[s] N1 → M ⓢ⤇* N2. -#N1 #N2 #H elim H -N1 -N2 -[ #r #N #i #Hr #HN #s #M #Hs #HMN - lapply (lsreds_trans … HMN … HN) -N /3 width=3/ -| #r #N #C1 #C2 #Hr #HN #_ #IHC12 #s #M #Hs #HMN - lapply (lsreds_trans … HMN … HN) -N /3 width=7/ -| #r #N #D1 #D2 #C1 #C2 #Hr #HN #_ #_ #IHD12 #IHC12 #s #M #Hs #HMN - lapply (lsreds_trans … HMN … HN) -N /3 width=9/ -] -qed-. - -lemma st_step_rc: ∀s,M1,M2. is_whd s → M1 ↦*[s] M2 → M1 ⓢ⤇* M2. -/3 width=5 by st_step_sn/ -qed. - -lemma st_lift: liftable st. -#h #M1 #M2 #H elim H -M1 -M2 -[ /3 width=3/ -| #s #M #A1 #A2 #Hs #HM #_ #IHA12 #d - @(st_abst … Hs) [2: @(lsreds_lift … HM) | skip ] -M // (**) (* auto fails here *) -| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ #IHB12 #IHA12 #d - @(st_appl … Hs) [3: @(lsreds_lift … HM) |1,2: skip ] -M // (**) (* auto fails here *) -] -qed. - -lemma st_inv_lift: deliftable_sn st. -#h #N1 #N2 #H elim H -N1 -N2 -[ #s #N1 #i #Hs #HN1 #d #M1 #HMN1 - elim (lsreds_inv_lift … HN1 … HMN1) -N1 /3 width=3/ -| #s #N1 #C1 #C2 #Hs #HN1 #_ #IHC12 #d #M1 #HMN1 - elim (lsreds_inv_lift … HN1 … HMN1) -N1 #M2 #HM12 #HM2 - elim (lift_inv_abst … HM2) -HM2 #A1 #HAC1 #HM2 destruct - elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *) - @(ex2_intro … (𝛌.A2)) // /2 width=5/ -| #s #N1 #D1 #D2 #C1 #C2 #Hs #HN1 #_ #_ #IHD12 #IHC12 #d #M1 #HMN1 - elim (lsreds_inv_lift … HN1 … HMN1) -N1 #M2 #HM12 #HM2 - elim (lift_inv_appl … HM2) -HM2 #B1 #A1 #HBD1 #HAC1 #HM2 destruct - elim (IHD12 ???) -IHD12 [4: // |2,3: skip ] #B2 #HB12 #HBD2 destruct (**) (* simplify line *) - elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *) - @(ex2_intro … (@B2.A2)) // /2 width=7/ -] -qed-. - -lemma st_dsubst: dsubstable st. -#N1 #N2 #HN12 #M1 #M2 #H elim H -M1 -M2 -[ #s #M #i #Hs #HM #d elim (lt_or_eq_or_gt i d) #Hid - [ lapply (lsreds_dsubst … N1 … HM d) -HM - >(dsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) /2 width=3/ - | destruct >dsubst_vref_eq - @(st_step_sn (↑[0,i]N1) … s) /2 width=1/ - | lapply (lsreds_dsubst … N1 … HM d) -HM - >(dsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) /2 width=3/ - ] -| #s #M #A1 #A2 #Hs #HM #_ #IHA12 #d - lapply (lsreds_dsubst … N1 … HM d) -HM /2 width=5/ (**) (* auto needs some help here *) -| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ #IHB12 #IHA12 #d - lapply (lsreds_dsubst … N1 … HM d) -HM /2 width=7/ (**) (* auto needs some help here *) -] -qed. - -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 #Hs #HM1 #HB1 #H (**) (* simplify line *) - elim (st_inv_abst … H ??) -H [3: // |2: skip ] #r #A1 #Hr #HM #HA1 (**) (* simplify line *) - lapply (lsreds_trans … HM1 … (dx:::r) (@B1.𝛌.A1) ?) /2 width=1/ -M #HM1 - lapply (lsreds_step_dx … HM1 (◊) ([↙B1]A1) ?) -HM1 // #HM1 - @(st_step_sn … HM1) /2 width=1/ /4 width=1/ -| #p #A #A2 #_ #IHA2 #M1 #H - elim (st_inv_abst … H ??) -H [3: // |2: skip ] /3 width=5/ (**) (* simplify line *) -| #p #B #B2 #A #_ #IHB2 #M1 #H - elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *) -| #p #B #A #A2 #_ #IHA2 #M1 #H - elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *) -] -qed-. - -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. - -lemma st_inv_lsreds_is_standard: ∀M,N. M ⓢ⤇* N → - ∃∃r. M ↦*[r] N & is_standard r. -#M #N #H elim H -M -N -[ #s #M #i #Hs #HM - lapply (is_whd_is_standard … Hs) -Hs /2 width=3/ -| #s #M #A1 #A2 #Hs #HM #_ * #r #HA12 #Hr - lapply (lsreds_trans … HM (rc:::r) (𝛌.A2) ?) /2 width=1/ -A1 #HM - @(ex2_intro … HM) -M -A2 /3 width=1/ -| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ * #rb #HB12 #Hrb * #ra #HA12 #Hra - lapply (lsreds_trans … HM (dx:::ra) (@B1.A2) ?) /2 width=1/ -A1 #HM - lapply (lsreds_trans … HM (sn:::rb) (@B2.A2) ?) /2 width=1/ -B1 #HM - @(ex2_intro … HM) -M -B2 -A2 >associative_append /3 width=1/ -] -qed-. - -theorem st_trans: transitive … st. -#M1 #M #M2 #HM1 #HM2 -elim (st_inv_lsreds_is_standard … HM1) -HM1 #s1 #HM1 #_ -elim (st_inv_lsreds_is_standard … 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_standard r. -#s #M #N #H -@st_inv_lsreds_is_standard /2 width=2/ -qed-. - -(* Note: we use "lapply (rewrite_r ?? is_whd … Hq)" (procedural) - in place of "cut (is_whd (q::r)) [ >Hq ]" (declarative) -*) -lemma st_lsred_swap: ∀p. in_whd p → ∀N1,N2. N1 ↦[p] N2 → ∀M1. M1 ⓢ⤇* N1 → - ∃∃q,M2. in_whd q & M1 ↦[q] M2 & M2 ⓢ⤇* N2. -#p #H @(in_whd_ind … H) -p -[ #N1 #N2 #H1 #M1 #H2 - elim (lsred_inv_nil … H1 ?) -H1 // #D #C #HN1 #HN2 - elim (st_inv_appl … H2 … HN1) -N1 #s1 #D1 #N #Hs1 #HM1 #HD1 #H - elim (st_inv_abst … H ??) -H [3: // |2: skip ] #s2 #C1 #Hs2 #HN #HC1 (**) (* simplify line *) - lapply (lsreds_trans … HM1 … (dx:::s2) (@D1.𝛌.C1) ?) /2 width=1/ -N #HM1 - lapply (lsreds_step_dx … HM1 (◊) ([↙D1]C1) ?) -HM1 // #HM1 - elim (lsreds_inv_pos … HM1 ?) -HM1 - [2: >length_append normalize in ⊢ (??(??%)); // ] - #q #r #M #Hq #HM1 #HM - lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -s1 -s2 * #Hq #Hr - @(ex3_2_intro … HM1) -M1 // -q - @(st_step_sn … HM) /2 width=1/ -| #p #_ #IHp #N1 #N2 #H1 #M1 #H2 - elim (lsred_inv_dx … H1 ??) -H1 [3: // |2: skip ] #D #C1 #C2 #HC12 #HN1 #HN2 (**) (* simplify line *) - elim (st_inv_appl … H2 … HN1) -N1 #s #B #A1 #Hs #HM1 #HBD #HAC1 - elim (IHp … HC12 … HAC1) -p -C1 #p #C1 #Hp #HAC1 #HC12 - lapply (lsreds_step_dx … HM1 (dx::p) (@B.C1) ?) -HM1 /2 width=1/ -A1 #HM1 - elim (lsreds_inv_pos … HM1 ?) -HM1 - [2: >length_append normalize in ⊢ (??(??%)); // ] - #q #r #M #Hq #HM1 #HM - lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -p -s * #Hq #Hr - @(ex3_2_intro … HM1) -M1 // -q /2 width=7/ -] -qed-. - -theorem lsreds_lsred_swap: ∀s,M1,N1. M1 ↦*[s] N1 → - ∀p,N2. in_whd p → N1 ↦[p] N2 → - ∃∃q,r,M2. in_whd q & M1 ↦[q] M2 & M2 ↦*[r] N2 & - is_standard (q::r). -#s #M1 #N1 #HMN1 #p #N2 #Hp #HN12 -lapply (st_lsreds … HMN1) -s #HMN1 -elim (st_lsred_swap … Hp … HN12 … HMN1) -p -N1 #q #M2 #Hq #HM12 #HMN2 -elim (st_inv_lsreds_is_standard … HMN2) -HMN2 /3 width=8/ -qed-. diff --git a/matita/matita/contribs/lambda/terms/term.ma b/matita/matita/contribs/lambda/terms/term.ma index 6910bdda6..cf688d606 100644 --- a/matita/matita/contribs/lambda/terms/term.ma +++ b/matita/matita/contribs/lambda/terms/term.ma @@ -14,8 +14,8 @@ (* Initial invocation: - Patience on us to gain peace and perfection! - *) -include "preamble.ma". -include "notation.ma". +include "background/preamble.ma". +include "background/notation.ma". (* TERM STRUCTURE ***********************************************************) diff --git a/matita/matita/contribs/lambda/xoa.conf.xml b/matita/matita/contribs/lambda/xoa.conf.xml index 9f923b7ae..74b24697f 100644 --- a/matita/matita/contribs/lambda/xoa.conf.xml +++ b/matita/matita/contribs/lambda/xoa.conf.xml @@ -4,7 +4,7 @@ $(MATITA_RT_BASE_DIR)
- contribs/lambda/ + contribs/lambda/background/ xoa xoa_notation basics/pts.ma -- 2.39.2