From 0cdde6640f1e2706e1e7cd63e358254a9026c6e4 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 19 May 2011 09:58:04 +0000 Subject: [PATCH] Dummies are blocked. --- matita/matita/lib/lambda/par_reduction.ma | 334 +++++----------------- matita/matita/lib/lambda/reduction.ma | 91 ++---- 2 files changed, 94 insertions(+), 331 deletions(-) diff --git a/matita/matita/lib/lambda/par_reduction.ma b/matita/matita/lib/lambda/par_reduction.ma index 6063ad955..cea1e177b 100644 --- a/matita/matita/lib/lambda/par_reduction.ma +++ b/matita/matita/lib/lambda/par_reduction.ma @@ -21,25 +21,27 @@ inductive T : Type[0] ≝ | D: T →T . *) +(* let rec is_dummy M ≝ match M with [D P ⇒ true |_ ⇒ false - ]. + ]. *) let rec is_lambda M ≝ match M with [Lambda P Q ⇒ true |_ ⇒ false ]. - + +(* theorem is_dummy_to_exists: ∀M. is_dummy M = true → ∃N. M = D N. #M (cases M) normalize [1,2: #n #H destruct|3,4,5: #P #Q #H destruct |#N #_ @(ex_intro … N) // ] -qed. +qed.*) theorem is_lambda_to_exists: ∀M. is_lambda M = true → ∃P,N. M = Lambda P N. @@ -47,14 +49,11 @@ theorem is_lambda_to_exists: ∀M. is_lambda M = true → [1,2,6: #n #H destruct|3,5: #P #Q #H destruct |#P #N #_ @(ex_intro … P) @(ex_intro … N) // ] -qed. +qed. inductive pr : T →T → Prop ≝ | beta: ∀P,M,N,M1,N1. pr M M1 → pr N N1 → pr (App (Lambda P M) N) (M1[0 ≝ N1]) - | dapp: ∀M,N,P. pr (App M N) P → - pr (App (D M) N) (D P) - | dlam: ∀M,N,P. pr (Lambda M N) P → pr (Lambda M (D N)) (D P) | none: ∀M. pr M M | appl: ∀M,M1,N,N1. pr M M1 → pr N N1 → pr (App M N) (App M1 N1) | lam: ∀P,P1,M,M1. pr P P1 → pr M M1 → @@ -65,9 +64,7 @@ inductive pr : T →T → Prop ≝ lemma prSort: ∀M,n. pr (Sort n) M → M = Sort n. #M #n #prH (inversion prH) - [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct - |#M #N #P1 #_ #_ #H destruct - |#M #N #P1 #_ #_ #H destruct + [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct |// |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct @@ -78,9 +75,7 @@ qed. lemma prRel: ∀M,n. pr (Rel n) M → M = Rel n. #M #n #prH (inversion prH) - [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct - |#M #N #P1 #_ #_ #H destruct - |#M #N #P1 #_ #_ #H destruct + [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct |// |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct @@ -91,10 +86,8 @@ qed. lemma prD: ∀M,N. pr (D N) M → ∃P.M = D P ∧ pr N P. #M #N #prH (inversion prH) - [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct - |#M #N #P #_ #_ #H destruct - |#M #N #P1 #_ #_ #H destruct - |#R #eqR eqN1 #pr3 - @or_intror @(ex_intro … S) @(ex_intro … N2) /3/ - |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct - |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct - |#M #N #_ #_ #H destruct - ] -qed. - lemma prApp_lambda: ∀Q,M,N,P. pr (App (Lambda Q M) N) P → -∃M1,N1. (P = M1[0:=N1] ∧ pr M M1 ∧ pr N N1) ∨ + ∃M1,N1. (P = M1[0:=N1] ∧ pr M M1 ∧ pr N N1) ∨ (P = (App M1 N1) ∧ pr (Lambda Q M) M1 ∧ pr N N1). #Q #M #N #P #prH (inversion prH) [#R #M #N #M1 #N1 #pr1 #pr2 #_ #_ #H destruct #_ @(ex_intro … M1) @(ex_intro … N1) /4/ - |#M1 #N1 #P1 #_ #_ #H destruct - |#M #N #P1 #_ #_ #H destruct - |#R #eqR #_ @(ex_intro … (Lambda Q M)) @(ex_intro … N) /4/ + |#M1 #eqM1 #_ @(ex_intro … (Lambda Q M)) @(ex_intro … N) /4/ |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H destruct #_ @(ex_intro … N1) @(ex_intro … N2) /4/ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct @@ -155,63 +125,24 @@ lemma prApp_lambda: ] qed. -lemma prLambda_not_dummy: ∀M,N,P. pr (Lambda M N) P → is_dummy N = false → -∃M1,N1. (P = Lambda M1 N1 ∧ pr M M1 ∧ pr N N1). -#M #N #P #prH (inversion prH) - [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct - |#M #N #P1 #_ #_ #H destruct - |#M #N #P1 #_ #_ #H destruct #_ #eqH destruct - |#Q #eqProd #_ #_ @(ex_intro … M) @(ex_intro … N) /3/ - |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct - |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 #_ destruct - @(ex_intro … Q1) @(ex_intro … S1) /3/ - |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct - |#M #N #_ #_ #H destruct - ] -qed. - -lemma prLambda_dummy: ∀M,N,P. pr (Lambda M (D N)) P → - (∃M1,N1. P = Lambda M1 (D N1) ∧ pr M M1 ∧ pr N N1) ∨ - (∃Q. (P = D Q ∧ pr (Lambda M N) Q)). +lemma prLambda: ∀M,N,P. pr (Lambda M N) P → + ∃M1,N1. (P = Lambda M1 N1 ∧ pr M M1 ∧ pr N N1). #M #N #P #prH (inversion prH) [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct - |#M #N #P1 #_ #_ #H destruct - |#M1 #N1 #P1 #prM #_ #eqlam destruct #H @or_intror - @(ex_intro … P1) /3/ - |#Q #eqLam #_ @or_introl @(ex_intro … M) @(ex_intro … N) /3/ - |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct - |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct - cases (prD …pr2) #S2 * #eqS1 #pr3 >eqS1 @or_introl - @(ex_intro … Q1) @(ex_intro … S2) /3/ + |#Q #eqQ #_ @(ex_intro … M) @(ex_intro … N) /3/ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct - |#M #N #_ #_ #H destruct - ] -qed. - -lemma prLambda: ∀M,N,P. pr (Lambda M N) P → -(∃M1,N1. (P = Lambda M1 N1 ∧ pr M M1 ∧ pr N N1)) ∨ -(∃N1,Q. (N=D N1) ∧ (P = (D Q) ∧ pr (Lambda M N1) Q)). -#M #N #P #prH (inversion prH) - [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct - |#M #N #P1 #_ #_ #H destruct - |#M1 #N1 #P1 #prM1 #_ #eqlam #eqP destruct @or_intror - @(ex_intro … N1) @(ex_intro … P1) /3/ - |#Q #eqProd #_ @or_introl @(ex_intro … M) @(ex_intro … N) /3/ - |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct - |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct @or_introl + |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct @(ex_intro … Q1) @(ex_intro … S1) /3/ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct |#M #N #_ #_ #H destruct ] -qed. +qed. lemma prProd: ∀M,N,P. pr (Prod M N) P → -∃M1,N1. P = Prod M1 N1 ∧ pr M M1 ∧ pr N N1. + ∃M1,N1. P = Prod M1 N1 ∧ pr M M1 ∧ pr N N1. #M #N #P #prH (inversion prH) [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct - |#M #N #P1 #_ #_ #H destruct - |#M #N #P1 #_ #_ #H destruct - |#Q #eqProd #_ @(ex_intro … M) @(ex_intro … N) /3/ + |#Q #eqQ #_ @(ex_intro … M) @(ex_intro … N) /3/ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct @@ -225,7 +156,7 @@ let rec full M ≝ [ Sort n ⇒ Sort n | Rel n ⇒ Rel n | App P Q ⇒ full_app P (full Q) - | Lambda P Q ⇒ full_lam (full P) Q + | Lambda P Q ⇒ Lambda (full P) (full Q) | Prod P Q ⇒ Prod (full P) (full Q) | D P ⇒ D (full P) ] @@ -236,25 +167,15 @@ and full_app M N ≝ | App P Q ⇒ App (full_app P (full Q)) N | Lambda P Q ⇒ (full Q) [0 ≝ N] | Prod P Q ⇒ App (Prod (full P) (full Q)) N - | D P ⇒ D (full_app P N) - ] -and full_lam M N on N≝ - match N with - [ Sort n ⇒ Lambda M (Sort n) - | Rel n ⇒ Lambda M (Rel n) - | App P Q ⇒ Lambda M (full_app P (full Q)) - | Lambda P Q ⇒ Lambda M (full_lam (full P) Q) - | Prod P Q ⇒ Lambda M (Prod (full P) (full Q)) - | D P ⇒ D (full_lam M P) + | D P ⇒ App (D (full P)) N ] . -lemma pr_lift: ∀N,N1,n. pr N N1 → ∀k. pr (lift N k n) (lift N1 k n). +lemma pr_lift: ∀N,N1,n. pr N N1 → + ∀k. pr (lift N k n) (lift N1 k n). #N #N1 #n #pr1 (elim pr1) [#P #M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k normalize >lift_subst_up @beta; // - |#M1 #N1 #P #pr2 #Hind normalize #k @dapp @Hind - |#M1 #N1 #P #pr2 #Hind normalize #k @dlam @Hind |// |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k normalize @appl; [@Hind1 |@Hind2] @@ -265,7 +186,7 @@ lemma pr_lift: ∀N,N1,n. pr N N1 → ∀k. pr (lift N k n) (lift N1 k n). |#M1 #M2 #pr2 #Hind #k normalize @d // ] qed. - + theorem pr_subst: ∀M,M1,N,N1,n. pr M M1 → pr N N1 → pr M[n≝N] M1[n≝N1]. @Telim_size #P (cases P) @@ -280,45 +201,29 @@ theorem pr_subst: ∀M,M1,N,N1,n. pr M M1 → pr N N1 → >(subst_rel3 … ltni) >(subst_rel3 … ltni) // ] |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2 - (cases (true_or_false (is_dummy Q))) - [#isdummy (cases (is_dummy_to_exists … isdummy)) - #Q1 #eqM >eqM in pr1 #pr3 (cases (prApp_D … pr3)) - [* #Q2 * #eqM1 #pr4 >eqM1 @dapp @(Hind (App Q1 M)) // - >eqM normalize // - |* #M2 * #N2 * * #eqM1 #pr4 #pr5 >eqM1 @appl; - [@Hind // [eqQ in pr1 #pr3 (cases (prApp_lambda … pr3)) + #M3 * #N3 * + [* * #eqM1 #pr4 #pr5 >eqM1 + >(plus_n_O n) in ⊢ (??%) >subst_lemma @beta; + [eqQ + @(transitive_lt ? (size (Lambda M2 N2))) normalize // |@Hind // normalize // ] - ] - |#notdummy - (cases (true_or_false (is_lambda Q))) - [#islambda (cases (is_lambda_to_exists … islambda)) - #M2 * #N2 #eqQ >eqQ in pr1 #pr3 (cases (prApp_lambda … pr3)) - #M3 * #N3 * - [* * #eqM1 #pr4 #pr5 >eqM1 - >(plus_n_O n) in ⊢ (??%) >subst_lemma - @beta; - [eqQ - @(transitive_lt ? (size (Lambda M2 N2))) normalize // - |@Hind // normalize // - ] - |* * #eqM1 #pr4 #pr5 >eqM1 @appl; - [@Hind // eqM1 @appl; + [@Hind // eqM1 @appl; - [@Hind // normalize // |@Hind // normalize // ] ] + |#notlambda (cases (prApp_not_lambda … pr1 ?)) // + #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1 @appl; + [@Hind // normalize // |@Hind // normalize // ] ] |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2 (cases (prLambda … pr1)) - [* #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1 @lam; - [@Hind // normalize // | @Hind // normalize // ] - |* #N2 * #Q1 * #eqM * #eqM1 #pr3 >eqM >eqM1 @dlam - @(Hind (Lambda Q N2)) // >eqM normalize // - ] + #N2 * #Q1 * * #eqM1 #pr3 #pr4 >eqM1 @lam; + [@Hind // normalize // | @Hind // normalize // ] |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2 (cases (prProd … pr1)) #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1 @prod; [@Hind // normalize // | @Hind // normalize // ] @@ -326,7 +231,7 @@ theorem pr_subst: ∀M,M1,N,N1,n. pr M M1 → pr N N1 → #M2 * #eqM1 #pr1 >eqM1 @d @Hind // normalize // ] qed. - + lemma pr_full_app: ∀M,N,N1. pr N N1 → (∀S.subterm S M → pr S (full S)) → pr (App M N) (full_app M N1). @@ -334,146 +239,49 @@ lemma pr_full_app: ∀M,N,N1. pr N N1 → [#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @appl // @Hind1 /3/ |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @beta /2/ |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @appl // @prod /2/ - |#P #Hind #N1 #N2 #prN #H @dapp @Hind /3/ - ] -qed. - -lemma pr_full_lam: ∀M,N,N1. pr N N1 → - (∀S.subterm S M → pr S (full S)) → - pr (Lambda N M) (full_lam N1 M). -#M (elim M) normalize /2/ - [#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @lam // @pr_full_app /3/ - |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @lam // @Hind2 /3/ - |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @lam // @prod /2/ - |#P #Hind #N1 #N2 #prN #H @dlam @Hind /3/ + |#P #Hind #N1 #N2 #prN #H @appl // @d /2/ ] qed. theorem pr_full: ∀M. pr M (full M). -@Telim #M (cases M) +@Telim #M (cases M) normalize [// |// |#M1 #N1 #H @pr_full_app /3/ - |#M1 #N1 #H @pr_full_lam /3/ + |#M1 #N1 #H normalize /3/ |#M1 #N1 #H @prod /2/ |#P #H @d /2/ ] qed. - -lemma complete_beta: ∀Q,N,N1,M,M1.(* pr N N1 → *) pr N1 (full N) → - (∀S,P.subterm S (Lambda Q M) → pr S P → pr P (full S)) → - pr (Lambda Q M) M1 → pr (App M1 N1) ((full M) [O ≝ (full N)]). -#Q #N #N1 #M (elim M) - [1,2:#n #M1 #prN1 #sub #pr1 - (cases (prLambda_not_dummy … pr1 ?)) // #M2 * #N2 - * * #eqM1 #pr3 #pr4 >eqM1 @beta /3/ - |3,4,5:#M1 #M2 #_ #_ #M3 #prN1 #sub #pr1 - (cases (prLambda_not_dummy … pr1 ?)) // #M4 * #N3 - * * #eqM3 #pr3 #pr4 >eqM3 @beta /3/ - |#M1 #Hind #M2 #prN1 #sub #pr1 - (cases (prLambda_dummy … pr1)) - [* #M3 * #N3 * * #eqM2 #pr3 #pr4 >eqM2 - @beta // normalize @d @sub /2/ - |* #P * #eqM2 #pr3 >eqM2 normalize @dapp - @Hind // #S #P #subH #pr4 @sub // - (cases (sublam … subH)) [* [* /2/ | /2/] | /3/ - ] - ] -qed. -lemma complete_beta1: ∀Q,N,M,M1. - (∀N1. pr N N1 → pr N1 (full N)) → - (∀S,P.subterm S (Lambda Q M) → pr S P → pr P (full S)) → - pr (App (Lambda Q M) N) M1 → pr M1 ((full M) [O ≝ (full N)]). -#Q #N #M #M1 #prH #subH #prApp -(cases (prApp_lambda … prApp)) #M2 * #N2 * - [* * #eqM1 #pr1 #pr2 >eqM1 @pr_subst; [@subH // | @prH //] - |* * #eqM1 #pr1 #pr2 >eqM1 @(complete_beta … pr1); - [@prH // - |#S #P #subS #prS @subH // - ] - ] -qed. - lemma complete_app: ∀M,N,P. (∀S,P.subterm S (App M N) → pr S P → pr P (full S)) → pr (App M N) P → pr P (full_app M (full N)). #M (elim M) normalize - [#n #P #Q #Hind #pr1 - cases (prApp_not_dummy_not_lambda … pr1 ??) // + [#n #P #Q #subH #pr1 cases (prApp_not_lambda … pr1 ?) // #M1 * #N1 * * #eqQ #pr1 #pr2 >eqQ @appl; - [@(Hind (Sort n)) // |@Hind //] - |#n #P #Q #Hind #pr1 - cases (prApp_not_dummy_not_lambda … pr1 ??) // + [@(subH (Sort n)) // |@subH //] + |#n #P #Q #subH #pr1 cases (prApp_not_lambda … pr1 ?) // #M1 * #N1 * * #eqQ #pr1 #pr2 >eqQ @appl; - [@(Hind (Rel n)) // |@Hind //] + [@(subH (Rel n)) // |@subH //] |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH - cases (prApp_not_dummy_not_lambda … prH ??) // + cases (prApp_not_lambda … prH ?) // #M2 * #N2 * * #eqQ #pr1 #pr2 >eqQ @appl; [@Hind1 /3/ |@subH //] |#P #Q #Hind1 #Hind2 #N1 #P2 #subH #prH - @(complete_beta1 … prH); - [#N2 @subH // | #S #P1 #subS @subH - (cases (sublam … subS)) [* [* /2/ | /2/] | /2/] - ] - |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH - cases (prApp_not_dummy_not_lambda … prH ??) // + cases (prApp_lambda … prH) #M2 * #N2 * + [* * #eqP2 #pr1 #pr2 >eqP2 @pr_subst /3/ + |* * #eqP2 #pr1 #pr2 >eqP2 (cases (prLambda … pr1)) + #M3 * #M4 * * #eqM2 #pr3 #pr4 >eqM2 @beta @subH /2/ + ] + |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH + cases (prApp_not_lambda … prH ?) // #M2 * #N2 * * #eqQ #pr1 #pr2 >eqQ @appl; [@(subH (Prod P Q)) // |@subH //] - |#P #Hind #N1 #N2 #subH #prH - (cut (∀S. subterm S (App P N1) → subterm S (App (D P) N1))) - [#S #sub (cases (subapp …sub)) [* [ * /2/ | /3/] | /2/]] #Hcut - cases (prApp_D … prH); - [* #N3 * #eqN3 #pr1 >eqN3 @d @Hind // - #S #P1 #sub1 #prS @subH /2/ - |* #N3 * #N4 * * #eqN2 #prP #prN1 >eqN2 @dapp @Hind; - [#S #P1 #sub1 #prS @subH /2/ |@appl // ] - ] - ] -qed. - -lemma complete_lam: ∀M,Q,M1. - (∀S,P.subterm S (Lambda Q M) → pr S P → pr P (full S)) → - pr (Lambda Q M) M1 → pr M1 (full_lam (full Q) M). -#M (elim M) - [#n #Q #M1 #sub #pr1 normalize - (cases (prLambda_not_dummy … pr1 ?)) // #M2 * #N2 - * * #eqM1 #pr3 #pr4 >eqM1 @lam; - [@sub /2/ | @(sub (Sort n)) /2/] - |#n #Q #M1 #sub #pr1 normalize - (cases (prLambda_not_dummy … pr1 ?)) // #M2 * #N2 - * * #eqM1 #pr3 #pr4 >eqM1 @lam; - [@sub /2/ | @(sub (Rel n)) /2/] - |#M1 #M2 #_ #_ #M3 #Q #sub #pr1 - (cases (prLambda_not_dummy … pr1 ?)) // #M4 * #N3 - * * #eqM3 #pr3 #pr4 >eqM3 @lam; - [@sub // | @complete_app // #S #P1 #subS @sub - (cases (subapp …subS)) [* [* /2/ | /2/] | /3/ ] - ] - |#M1 #M2 #_ #Hind #M3 #Q #sub #pr1 - (cases (prLambda_not_dummy … pr1 ?)) // #M4 * #N3 - * * #eqM3 #pr3 #pr4 >eqM3 @lam; - [@sub // |@Hind // #S #P1 #subS @sub - (cases (sublam …subS)) [* [* /2/ | /2/] | /3/ ] - ] - |#M1 #M2 #_ #_ #M3 #Q #sub #pr1 - (cases (prLambda_not_dummy … pr1 ?)) // #M4 * #N3 - * * #eqM3 #pr3 #pr4 >eqM3 @lam; - [@sub // | (cases (prProd … pr4)) #M5 * #N4 * * #eqN3 - #pr5 #pr6 >eqN3 @prod; - [@sub /3/ | @sub /3/] - ] - |#P #Hind #Q #M2 #sub #pr1 (cases (prLambda_dummy … pr1)) - [* #M3 * #N3 * * #eqM2 #pr3 #pr4 >eqM2 normalize - @dlam @Hind; - [#S #P1 #subS @sub (cases (sublam …subS)) - [* [* /2/ | /2/ ] |/3/ ] - |@lam // - ] - |* #P * #eqM2 #pr3 >eqM2 normalize @d - @Hind // #S #P #subH @sub - (cases (sublam … subH)) [* [* /2/ | /2/] | /3/] - ] + |#P #Hind #N1 #N2 #subH #pr1 + cases (prApp_not_lambda … pr1 ?) // + #M1 * #N1 * * #eqQ #pr2 #pr3 >eqQ @appl; + [@(subH (D P) M1) // |@subH //] ] qed. @@ -483,11 +291,11 @@ theorem complete: ∀M,N. pr M N → pr N (full M). |#n #Hind #N #prH normalize >(prRel … prH) // |#M #N #Hind #Q @complete_app #S #P #subS @Hind // - | #P #P1 #Hind #N #Hpr @(complete_lam … Hpr) - #S #P #subS @Hind // - |5: #P #P1 #Hind #N #Hpr + |#P #P1 #Hind #N #Hpr + (cases (prLambda …Hpr)) #M1 * #N1 * * #eqN >eqN normalize /3/ + |#P #P1 #Hind #N #Hpr (cases (prProd …Hpr)) #M1 * #N1 * * #eqN >eqN normalize /3/ - |6:#N #Hind #P #prH normalize cases (prD … prH) + |#N #Hind #P #prH normalize cases (prD … prH) #Q * #eqP >eqP #prN @d @Hind // ] qed. @@ -497,5 +305,3 @@ pr Q S ∧ pr P S. #P #Q #R #pr1 #pr2 @(ex_intro … (full P)) /3/ qed. - - diff --git a/matita/matita/lib/lambda/reduction.ma b/matita/matita/lib/lambda/reduction.ma index 552969b66..58e4e179a 100644 --- a/matita/matita/lib/lambda/reduction.ma +++ b/matita/matita/lib/lambda/reduction.ma @@ -24,8 +24,6 @@ inductive T : Type[0] ≝ inductive red : T →T → Prop ≝ | rbeta: ∀P,M,N. red (App (Lambda P M) N) (M[0 ≝ N]) - | rdapp: ∀M,N. red (App (D M) N) (D (App M N)) - | rdlam: ∀M,N. red (Lambda M (D N)) (D (Lambda M N)) | rappl: ∀M,M1,N. red M M1 → red (App M N) (App M1 N) | rappr: ∀M,N,N1. red N N1 → red (App M N) (App M N1) | rlaml: ∀M,M1,N. red M M1 → red (Lambda M N) (Lambda M1 N) @@ -41,25 +39,20 @@ qed. lemma red_d : ∀M,P. red (D M) P → ∃N. P = D N ∧ red M N. #M #P #redMP (inversion redMP) [#P1 #M1 #N1 #eqH destruct - |#M1 #N1 #eqH destruct - |#M1 #N1 #eqH destruct - |4,5,6,7,8,9:#Q1 #Q2 #N1 #red1 #_ #eqH destruct + |2,3,4,5,6,7:#Q1 #Q2 #N1 #red1 #_ #eqH destruct |#Q1 #M1 #red1 #_ #eqH destruct #eqP @(ex_intro … M1) /2/ ] qed. lemma red_lambda : ∀M,N,P. red (Lambda M N) P → (∃M1. P = (Lambda M1 N) ∧ red M M1) ∨ - (∃N1. P = (Lambda M N1) ∧ red N N1) ∨ - (∃Q. N = D Q ∧ P = D (Lambda M Q)). + (∃N1. P = (Lambda M N1) ∧ red N N1). #M #N #P #redMNP (inversion redMNP) [#P1 #M1 #N1 #eqH destruct - |#M1 #N1 #eqH destruct - |#M1 #N1 #eqH destruct #eqP %2 (@(ex_intro … N1)) % // - |4,5,8,9:#Q1 #Q2 #N1 #red1 #_ #eqH destruct - |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1 %1 + |2,3,6,7:#Q1 #Q2 #N1 #red1 #_ #eqH destruct + |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1 (@(ex_intro … M1)) % // - |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1 %2 + |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %2 (@(ex_intro … N1)) % // |#Q1 #M1 #red1 #_ #eqH destruct ] @@ -70,8 +63,7 @@ lemma red_prod : ∀M,N,P. red (Prod M N) P → (∃N1. P = (Prod M N1) ∧ red N N1). #M #N #P #redMNP (inversion redMNP) [#P1 #M1 #N1 #eqH destruct - |2,3: #M1 #N1 #eqH destruct - |4,5,6,7:#Q1 #Q2 #N1 #red1 #_ #eqH destruct + |2,3,4,5:#Q1 #Q2 #N1 #red1 #_ #eqH destruct |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1 (@(ex_intro … M1)) % // |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %2 @@ -82,19 +74,16 @@ qed. lemma red_app : ∀M,N,P. red (App M N) P → (∃M1,N1. M = (Lambda M1 N1) ∧ P = N1[0:=N]) ∨ - (∃M1. M = (D M1) ∧ P = D (App M1 N)) ∨ (∃M1. P = (App M1 N) ∧ red M M1) ∨ (∃N1. P = (App M N1) ∧ red N N1). #M #N #P #redMNP (inversion redMNP) - [#P1 #M1 #N1 #eqH destruct #eqP %1 %1 %1 + [#P1 #M1 #N1 #eqH destruct #eqP %1 %1 @(ex_intro … P1) @(ex_intro … M1) % // - |#M1 #N1 #eqH destruct #eqP %1 %1 %2 /3/ - |#M1 #N1 #eqH destruct |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1 %2 (@(ex_intro … M1)) % // |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %2 (@(ex_intro … N1)) % // - |6,7,8,9:#Q1 #Q2 #N1 #red1 #_ #eqH destruct + |4,5,6,7:#Q1 #Q2 #N1 #red1 #_ #eqH destruct |#Q1 #M1 #red1 #_ #eqH destruct ] qed. @@ -112,8 +101,7 @@ qed. lemma NF_Sort: ∀i. NF (Sort i). #i #N % #redN (inversion redN) [1: #P #N #M #H destruct - |2,3 :#N #M #H destruct - |4,5,6,7,8,9: #N #M #P #_ #_ #H destruct + |2,3,4,5,6,7: #N #M #P #_ #_ #H destruct |#M #N #_ #_ #H destruct ] qed. @@ -121,8 +109,7 @@ qed. lemma NF_Rel: ∀i. NF (Rel i). #i #N % #redN (inversion redN) [1: #P #N #M #H destruct - |2,3 :#N #M #H destruct - |4,5,6,7,8,9: #N #M #P #_ #_ #H destruct + |2,3,4,5,6,7: #N #M #P #_ #_ #H destruct |#M #N #_ #_ #H destruct ] qed. @@ -132,22 +119,16 @@ lemma red_subst : ∀N,M,M1,i. red M M1 → red M[i≝N] M1[i≝N]. [1,2:#j #Hind #M1 #i #r1 @False_ind /2/ |#P #Q #Hind #M1 #i #r1 (cases (red_app … r1)) [* - [* - [* #M2 * #N2 * #eqP #eqM1 >eqP normalize - >eqM1 >(plus_n_O i) >(subst_lemma N2) <(plus_n_O i) - (cut (i+1 =S i)) [//] #Hcut >Hcut @rbeta - |* #M2 * #eqP #eqM1 >eqM1 >eqP normalize @rdapp - ] + [* #M2 * #N2 * #eqP #eqM1 >eqP normalize + >eqM1 >(plus_n_O i) >(subst_lemma N2) <(plus_n_O i) + (cut (i+1 =S i)) [//] #Hcut >Hcut @rbeta |* #M2 * #eqM1 #rP >eqM1 normalize @rappl @Hind /2/ ] |* #N2 * #eqM1 #rQ >eqM1 normalize @rappr @Hind /2/ ] |#P #Q #Hind #M1 #i #r1 (cases (red_lambda …r1)) - [* - [* #P1 * #eqM1 #redP >eqM1 normalize @rlaml @Hind /2/ - |* #Q1 * #eqM1 #redP >eqM1 normalize @rlamr @Hind /2/ - ] - |* #M2 * #eqQ #eqM1 >eqM1 >eqQ normalize @rdlam + [* #P1 * #eqM1 #redP >eqM1 normalize @rlaml @Hind /2/ + |* #Q1 * #eqM1 #redP >eqM1 normalize @rlamr @Hind /2/ ] |#P #Q #Hind #M1 #i #r1 (cases (red_prod …r1)) [* #P1 * #eqM1 #redP >eqM1 normalize @rprodl @Hind /2/ @@ -314,27 +295,11 @@ lemma SN_Lambda: ∀N.SN N → ∀M.SN M → SN (Lambda N M). (* for M we proceed by induction on SH *) (lapply (SN_to_SH ? snM)) #shM (elim shM) #Q #shQ #HindQ % #a #redH (cases (red_lambda … redH)) - [* - [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) // - @SH_to_SN % /2/ - |* #S * #eqa #redQS >eqa @(HindQ S) /2/ - ] - |* #S * #eqQ #eqa >eqa @SN_d @(HindQ S) /3/ + [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) // + @SH_to_SN % /2/ + |* #S * #eqa #redQS >eqa @(HindQ S) /2/ ] qed. - -(* -lemma SH_Lambda: ∀N.SH N → ∀M.SH M → SN (Lambda N M). -#N #snN (elim snN) #P #snP #HindP #M #snM (elim snM) -#Q #snQ #HindQ % #a #redH (cases (red_lambda … redH)) - [* - [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) /2/ - % /2/ - |* #S * #eqa #redQS >eqa @(HindQ S) /2/ - ] - |* #S * #eqQ #eqa >eqa @SN_d @(HindQ S) /3/ - ] -qed. *) lemma SN_Prod: ∀N.SN N → ∀M.SN M → SN (Prod N M). #N #snN (elim snN) #P #shP #HindP #M #snM (elim snM) @@ -352,6 +317,7 @@ lemma SN_subst: ∀i,N,M.SN M[i ≝ N] → SN M. |#Hcut #M #snM @(Hcut … snM) // qed. +(* lemma SN_DAPP: ∀N,M. SN (App M N) → SN (App (D M) N). cut (∀P. SN P → ∀M,N. P = App M N → SN (App (D M) N)); [|/2/] #P #snP (elim snP) #Q #snQ #Hind @@ -366,7 +332,7 @@ cut (∀P. SN P → ∀M,N. P = App M N → SN (App (D M) N)); [|/2/] ] |* #M2 * #eqA >eqA #r2 @(Hind (App M M2)) /2/ ] -qed. +qed. *) lemma SN_APP: ∀P.SN P → ∀N. SN N → ∀M. SN M[0:=N] → SN (App (Lambda P M) N). @@ -376,20 +342,11 @@ lemma SN_APP: ∀P.SN P → ∀N. SN N → ∀M. (generalize in match snM1) (elim shM) #C #shC #HindC #snC1 % #Q #redQ (cases (red_app … redQ)) [* - [* - [* #M2 * #N2 * #eqlam destruct #eqQ // - |* #M2 * #eqlam destruct - ] + [* #M2 * #N2 * #eqlam destruct #eqQ // |* #M2 * #eqQ #redlam >eqQ (cases (red_lambda …redlam)) - [* - [* #M3 * #eqM2 #r2 >eqM2 @HindA // % /2/ - |* #M3 * #eqM2 #r2 >eqM2 @HindC; - [%1 // |@(SN_step … snC1) /2/] - ] - |* #M3 * #eqC #eqM2 >eqM2 @SN_DAPP @HindC; - [%2 >eqC @inj // - |@(SN_subterm … snC1) >eqC normalize // - ] + [* #M3 * #eqM2 #r2 >eqM2 @HindA // % /2/ + |* #M3 * #eqM2 #r2 >eqM2 @HindC; + [%1 // |@(SN_step … snC1) /2/] ] ] |* #M2 * #eqQ #r2 >eqQ @HindB // @(SN_star … snC1) -- 2.39.2