From: Ferruccio Guidi Date: Tue, 4 Dec 2012 17:59:17 +0000 (+0000) Subject: we started Kashima's proof of standardization X-Git-Tag: make_still_working~1414 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=984f552a6b54e8b870d6e32df8325345d0f1ea5b;p=helm.git we started Kashima's proof of standardization --- diff --git a/matita/matita/contribs/lambda/hap_computation.ma b/matita/matita/contribs/lambda/hap_computation.ma new file mode 100644 index 000000000..869fa94d4 --- /dev/null +++ b/matita/matita/contribs/lambda/hap_computation.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "hap_reduction.ma". + +(* KASHIMA'S "HAP" COMPUTATION **********************************************) + +(* Note: this is the "head in application" computation of: + R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000). +*) +definition hap: relation term ≝ star … hap1. + diff --git a/matita/matita/contribs/lambda/hap_reduction.ma b/matita/matita/contribs/lambda/hap_reduction.ma new file mode 100644 index 000000000..7b07524fc --- /dev/null +++ b/matita/matita/contribs/lambda/hap_reduction.ma @@ -0,0 +1,53 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "labelled_sequential_reduction.ma". + +(* KASHIMA'S "HAP" COMPUTATION (SINGLE STEP) ********************************) + +(* Note: this is one step of the "head in application" computation of: + R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000). +*) +inductive hap1: relation term ≝ +| hap1_beta: ∀B,A. hap1 (@B.𝛌.A) ([⬐B]A) +| hap1_appl: ∀B,A1,A2. hap1 A1 A2 → hap1 (@B.A1) (@B.A2) +. + +lemma hap1_lift: liftable hap1. +#h #M1 #M2 #H elim H -M1 -M2 normalize /2 width=1/ +#B #A #d dsubst_dsubst_ge // +qed. + +lemma hap1_lsred: ∀M,N. hap1 M N → + ∃∃p. in_spine p & M ⇀[p] N. +#M #N #H elim H -M -N /2 width=3/ +#B #A1 #A2 #_ * /3 width=3/ +qed-. diff --git a/matita/matita/contribs/lambda/labelled_sequential_reduction.ma b/matita/matita/contribs/lambda/labelled_sequential_reduction.ma index be86cb234..6957484e6 100644 --- a/matita/matita/contribs/lambda/labelled_sequential_reduction.ma +++ b/matita/matita/contribs/lambda/labelled_sequential_reduction.ma @@ -21,8 +21,8 @@ include "multiplicity.ma". F. Kamareddine and R.P. Nederpelt: "A useful λ-notation". Theoretical Computer Science 155(1), Elsevier (1996), pp. 85-109. *) -inductive lsred: rpointer → relation term ≝ -| lsred_beta : ∀A,D. lsred (◊) (@D.𝛌.A) ([⬐D]A) +inductive lsred: rptr → relation term ≝ +| lsred_beta : ∀B,A. lsred (◊) (@B.𝛌.A) ([⬐B]A) | lsred_abst : ∀p,A,C. lsred p A C → lsred p (𝛌.A) (𝛌.C) | lsred_appl_sn: ∀p,B,D,A. lsred p B D → lsred (true::p) (@B.A) (@D.A) | lsred_appl_dx: ∀p,B,A,C. lsred p A C → lsred (false::p) (@B.A) (@B.C) @@ -38,7 +38,7 @@ notation "hvbox( M break ⇀ [ term 46 p ] break term 46 N )" lemma lsred_inv_vref: ∀p,M,N. M ⇀[p] N → ∀i. #i = M → ⊥. #p #M #N * -p -M -N -[ #A #D #i #H destruct +[ #B #A #i #H destruct | #p #A #C #_ #i #H destruct | #p #B #D #A #_ #i #H destruct | #p #B #A #C #_ #i #H destruct @@ -48,7 +48,7 @@ qed-. lemma lsred_inv_beta: ∀p,M,N. M ⇀[p] N → ∀D,C. @D.C = M → ◊ = p → ∃∃A. 𝛌.A = C & [⬐D] A = N. #p #M #N * -p -M -N -[ #A #D #D0 #C0 #H #_ destruct /2 width=3/ +[ #B #A #D0 #C0 #H #_ destruct /2 width=3/ | #p #A #C #_ #D0 #C0 #H destruct | #p #B #D #A #_ #D0 #C0 #_ #H destruct | #p #B #A #C #_ #D0 #C0 #_ #H destruct @@ -58,7 +58,7 @@ qed-. lemma lsred_inv_abst: ∀p,M,N. M ⇀[p] N → ∀A. 𝛌.A = M → ∃∃C. A ⇀[p] C & 𝛌.C = N. #p #M #N * -p -M -N -[ #A #D #A0 #H destruct +[ #B #A #A0 #H destruct | #p #A #C #HAC #A0 #H destruct /2 width=3/ | #p #B #D #A #_ #A0 #H destruct | #p #B #A #C #_ #A0 #H destruct @@ -68,7 +68,7 @@ qed-. lemma lsred_inv_appl_sn: ∀p,M,N. M ⇀[p] N → ∀B,A,q. @B.A = M → true::q = p → ∃∃D. B ⇀[q] D & @D.A = N. #p #M #N * -p -M -N -[ #A #D #B0 #A0 #p0 #_ #H destruct +[ #B #A #B0 #A0 #p0 #_ #H destruct | #p #A #C #_ #B0 #D0 #p0 #H destruct | #p #B #D #A #HBD #B0 #A0 #p0 #H1 #H2 destruct /2 width=3/ | #p #B #A #C #_ #B0 #A0 #p0 #_ #H destruct @@ -78,7 +78,7 @@ qed-. lemma lsred_inv_appl_dx: ∀p,M,N. M ⇀[p] N → ∀B,A,q. @B.A = M → false::q = p → ∃∃C. A ⇀[q] C & @B.C = N. #p #M #N * -p -M -N -[ #A #D #B0 #A0 #p0 #_ #H destruct +[ #B #A #B0 #A0 #p0 #_ #H destruct | #p #A #C #_ #B0 #D0 #p0 #H destruct | #p #B #D #A #_ #B0 #A0 #p0 #_ #H destruct | #p #B #A #C #HAC #B0 #A0 #p0 #H1 #H2 destruct /2 width=3/ @@ -87,7 +87,7 @@ qed-. lemma lsred_fwd_mult: ∀p,M,N. M ⇀[p] N → #{N} < #{M} * #{M}. #p #M #N #H elim H -p -M -N -[ #A #D @(le_to_lt_to_lt … (#{A}*#{D})) // +[ #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 @@ -101,12 +101,12 @@ qed-. lemma lsred_lift: ∀p. liftable (lsred p). #p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/ -#A #D #d dsubst_dsubst_ge // +#D2 #A #d >dsubst_dsubst_ge // qed. theorem lsred_mono: ∀p. singlevalued … (lsred p). #p #M #N1 #H elim H -p -M -N1 -[ #A #D #N2 #H elim (lsred_inv_beta … H ????) -H [4,5: // |2,3: skip ] #A0 #H1 #H2 destruct // (**) (* simplify line *) +[ #B #A #N2 #H elim (lsred_inv_beta … H ????) -H [4,5: // |2,3: skip ] #A0 #H1 #H2 destruct // (**) (* simplify line *) | #p #A #C #_ #IHAC #N2 #H elim (lsred_inv_abst … H ??) -H [3: // |2: skip ] #C0 #HAC #H destruct /3 width=1/ (**) (* simplify line *) | #p #B #D #A #_ #IHBD #N2 #H elim (lsred_inv_appl_sn … H ?????) -H [5,6: // |2,3,4: skip ] #D0 #HBD #H destruct /3 width=1/ (**) (* simplify line *) | #p #B #A #C #_ #IHAC #N2 #H elim (lsred_inv_appl_dx … H ?????) -H [5,6: // |2,3,4: skip ] #C0 #HAC #H destruct /3 width=1/ (**) (* simplify line *) diff --git a/matita/matita/contribs/lambda/policy.txt b/matita/matita/contribs/lambda/policy.txt index 4d6e5bd8c..77b0fdab7 100644 --- a/matita/matita/contribs/lambda/policy.txt +++ b/matita/matita/contribs/lambda/policy.txt @@ -10,5 +10,6 @@ d, e : variable reference depth h : relocation height i, j : de Bruijn index k : relocation height +m, n : measures on terms p, q : redex pointer r, s : redex pointer sequence diff --git a/matita/matita/contribs/lambda/preamble.ma b/matita/matita/contribs/lambda/preamble.ma index 8e4b8fc96..eb0f409a5 100644 --- a/matita/matita/contribs/lambda/preamble.ma +++ b/matita/matita/contribs/lambda/preamble.ma @@ -42,6 +42,11 @@ definition confluent1: ∀A. relation A → predicate A ≝ λA,R,a0. definition confluent: ∀A. predicate (relation A) ≝ λA,R. ∀a0. confluent1 … R a0. +(* booleans *) + +definition is_false: predicate bool ≝ λb. + false = b. + (* arithmetics *) lemma lt_refl_false: ∀n. n < n → ⊥. @@ -95,3 +100,9 @@ qed. notation > "◊" non associative with precedence 90 for @{'nil}. + +let rec Allr (A:Type[0]) (R:relation A) (l:list A) on l : Prop ≝ +match l with +[ nil ⇒ True +| cons a1 l ⇒ match l with [ nil ⇒ True | cons a2 _ ⇒ R a1 a2 ∧ Allr A R l ] +]. diff --git a/matita/matita/contribs/lambda/redex_pointer.ma b/matita/matita/contribs/lambda/redex_pointer.ma index 6895ea787..721904437 100644 --- a/matita/matita/contribs/lambda/redex_pointer.ma +++ b/matita/matita/contribs/lambda/redex_pointer.ma @@ -24,11 +24,15 @@ include "term.ma". on application nodes, "false" means "proceed right" and "true" means "proceed left" *) -definition rpointer: Type[0] ≝ list bool. +definition rptr: Type[0] ≝ list bool. + +(* Note: a redex is "in the spine" when is not in the argument of an application *) +definition in_spine: predicate rptr ≝ λp. + All … is_false p. (* Note: precedence relation on redex pointers: p ≺ q to serve as base for the order relations: p < q and p ≤ q *) -inductive rpprec: relation rpointer ≝ +inductive rpprec: relation rptr ≝ | rpprec_nil : ∀b,q. rpprec (◊) (b::q) | rppprc_cons: ∀p,q. rpprec (false::p) (true::q) | rpprec_comp: ∀b,p,q. rpprec p q → rpprec (b::p) (b::q) @@ -44,9 +48,13 @@ notation "hvbox(a break ≺ b)" for @{ 'prec $a $b }. (* Note: this is p < q *) +definition rplt: relation rptr ≝ TC … rpprec. + interpretation "'less than' on redex pointers" - 'lt p q = (TC rpointer rpprec p q). + 'lt p q = (rplt p q). (* Note: this is p ≤ q *) +definition rple: relation rptr ≝ star … rpprec. + interpretation "'less or equal to' on redex pointers" - 'leq x y = (star rpointer x y). + 'leq p q = (rple p q). diff --git a/matita/matita/contribs/lambda/redex_pointer_sequence.ma b/matita/matita/contribs/lambda/redex_pointer_sequence.ma index 5b05f4796..e32c6d2ba 100644 --- a/matita/matita/contribs/lambda/redex_pointer_sequence.ma +++ b/matita/matita/contribs/lambda/redex_pointer_sequence.ma @@ -18,4 +18,12 @@ include "redex_pointer.ma". (* Policy: pointer sequence metavariables: r, s *) -definition rpseq: Type[0] \def list rpointer. +definition rpseq: Type[0] \def list rptr. + +(* Note: a "spine" computation contracts just redexes in the spine *) +definition is_spine: predicate rpseq ≝ λs. + All … in_spine s. + +(* Note: to us, a "normal" computation contracts redexes in non-decreasing positions *) +definition is_le: predicate rpseq ≝ λs. + Allr … rple s. diff --git a/matita/matita/contribs/lambda/st_computation.ma b/matita/matita/contribs/lambda/st_computation.ma new file mode 100644 index 000000000..792ab882c --- /dev/null +++ b/matita/matita/contribs/lambda/st_computation.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "hap_computation.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: ∀M,i. hap M (#i) → st M (#i) +| st_abst: ∀M,A,C. hap M (𝛌.A) → st A C → st M (𝛌.C) +| st_appl: ∀M,B,D,A,C. hap M (@B.A) → st B D → st A C → st M (@D.C) +. +