From fb9f80d2fb30216cc0754e8e8d09206f3e3e7bb7 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 7 Mar 2011 07:29:04 +0000 Subject: [PATCH] sottotermini e confluenza (manca pr_substs). --- matita/matita/lib/lambda/reduction.ma | 456 ++++++++++++++++++++++++++ matita/matita/lib/lambda/subterms.ma | 130 ++++++++ 2 files changed, 586 insertions(+) create mode 100644 matita/matita/lib/lambda/reduction.ma create mode 100644 matita/matita/lib/lambda/subterms.ma diff --git a/matita/matita/lib/lambda/reduction.ma b/matita/matita/lib/lambda/reduction.ma new file mode 100644 index 000000000..e6d57ba6e --- /dev/null +++ b/matita/matita/lib/lambda/reduction.ma @@ -0,0 +1,456 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "lambda/subterms.ma". + +(* +inductive T : Type[0] ≝ + | Sort: nat → T + | Rel: nat → T + | App: T → T → T + | Lambda: T → T → T (* type, body *) + | Prod: T → T → T (* type, body *) + | 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. + +theorem is_lambda_to_exists: ∀M. is_lambda M = true → +∃P,N. M = Lambda P N. +#M (cases M) normalize + [1,2,6: #n #H destruct|3,5: #P #Q #H destruct + |#P #N #_ @(ex_intro … P) @(ex_intro … N) // + ] +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 → + pr (Lambda P M) (Lambda P1 M1) + | prod: ∀P,P1,M,M1. pr P P1 → pr M M1 → + pr (Prod P M) (Prod P1 M1) + | d: ∀M,M1. pr M M1 → pr (D M) (D M1). + +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 + |// + |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct + |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct + |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct + |#M #N #_ #_ #H destruct + ] +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 + |// + |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct + |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct + |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct + |#M #N #_ #_ #H destruct + ] +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) ∨ + (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 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H destruct #_ + @(ex_intro … N1) @(ex_intro … N2) /4/ + |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct + |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct + |#M #N #_ #_ #H destruct + ] +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)). +#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/ + |#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 + @(ex_intro … Q1) @(ex_intro … S1) /3/ + |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct + |#M #N #_ #_ #H destruct + ] +qed. + +lemma prProd: ∀M,N,P. pr (Prod M N) P → +∃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/ + |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct + |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct + |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct + @(ex_intro … Q1) @(ex_intro … S1) /3/ + |#M #N #_ #_ #H destruct + ] +qed. + +let rec full M ≝ + match M with + [ Sort n ⇒ Sort n + | Rel n ⇒ Rel n + | App P Q ⇒ full_app P (full Q) + | Lambda P Q ⇒ full_lam (full P) Q + | Prod P Q ⇒ Prod (full P) (full Q) + | D P ⇒ D (full P) + ] +and full_app M N ≝ + match M with + [ Sort n ⇒ App (Sort n) N + | Rel n ⇒ App (Rel n) 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) + ] +. + +axiom pr_subst_lam: ∀Q,M,M1,N,N1,n. pr (Lambda Q M) M1 → pr N N1 → + pr (Lambda Q M)[n≝N] M1[n≝N1]. +(* +#Q #M (elim M) + [#i #M1 #N #N1 #n #pr1 #pr2 + (cases (prLambda_not_dummy … pr1 ?)) // + #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1 normalize @lam // *) +(* + cases(prLambda … pr1); + [* #M2 * #N2 * * #eqM2 #pr3 #pr4 >eqM2 normalize + @lam; [@Hind1 // | @Hind2 // ] + |* #M2 * #Q1 * #eqM * #eqM1 #pr3 >eqM >eqM1 + normalize @dlam *) +(* axiom pr_subst: ∀M,M1,N,N1. pr M M1 → pr N N1 → + pr M[0≝N] M1[0≝N1]. *) + +theorem pr_subst: ∀M,M1,N,N1,n. pr M M1 → pr N N1 → + pr M[n≝N] M1[n≝N1]. +#M (elim M) + [#i #M1 #N #N1 #n #pr1 #pr2 normalize >(prSort … pr1) // + |#i #M1 #N #N1 #n #pr1 #pr2 >(prRel … pr1) + (* gran casino + normalize (cases n) // *) + |#Q #M #Hind1 #Hind2 #M1 #N #N1 #pr1 #pr2 + |#Q #M #Hind1 #Hind2 #M1 #N #N1 #n #pr1 #pr2 + @pr_subst_lam // + |#Q #M #Hind1 #Hind2 #M1 #N #N1 #n #pr1 #pr2 + (cases (prProd … pr1)) #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1 + @prod [@Hind1 // | @Hind2 // ] + |#Q #Hind #M1 #N #N1 #n #pr1 #pr2 (cases (prD … pr1)) + #M2 * #eqM1 #pr1 >eqM1 @d @Hind // + ] + +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). +#M (elim M) normalize /2/ + [#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/ + ] +qed. + +theorem pr_full: ∀M. pr M (full M). +@Telim #M (cases M) + [// + |// + |#M1 #N1 #H @pr_full_app /3/ + |#M1 #N1 #H @pr_full_lam /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 ??) // + #M1 * #N1 * * #eqQ #pr1 #pr2 >eqQ @appl; + [@(Hind (Sort n)) // |@Hind //] + |#n #P #Q #Hind #pr1 + cases (prApp_not_dummy_not_lambda … pr1 ??) // + #M1 * #N1 * * #eqQ #pr1 #pr2 >eqQ @appl; + [@(Hind (Rel n)) // |@Hind //] + |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH + cases (prApp_not_dummy_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 ??) // + #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/] + ] + ] +qed. + +theorem complete: ∀M,N. pr M N → pr N (full M). +@Telim #M (cases M) + [#n #Hind #N #prH normalize >(prSort … prH) // + |#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 + (cases (prProd …Hpr)) #M1 * #N1 * * #eqN >eqN normalize /3/ + |6:#N #Hind #P #prH normalize cases (prD … prH) + #Q * #eqP >eqP #prN @d @Hind // + ] +qed. + +theorem diamond: ∀P,Q,R. pr P Q → pr P R → ∃S. +pr Q S ∧ pr P S. +#P #Q #R #pr1 #pr2 @(ex_intro … (full P)) /3/ +qed. + + + diff --git a/matita/matita/lib/lambda/subterms.ma b/matita/matita/lib/lambda/subterms.ma new file mode 100644 index 000000000..1b18f368c --- /dev/null +++ b/matita/matita/lib/lambda/subterms.ma @@ -0,0 +1,130 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "lambda/subst.ma". + +inductive subterm : T → T → Prop ≝ + | appl : ∀M,N. subterm M (App M N) + | appr : ∀M,N. subterm N (App M N) + | lambdal : ∀M,N. subterm M (Lambda M N) + | lambdar : ∀M,N. subterm N (Lambda M N) + | prodl : ∀M,N. subterm M (Prod M N) + | prodr : ∀M,N. subterm N (Prod M N) + | sub_b : ∀M. subterm M (D M) + | sub_trans : ∀M,N,P. subterm M N → subterm N P → subterm M P. + +inverter subterm_myinv for subterm (?%). + +lemma subapp: ∀S,M,N. subterm S (App M N) → + S = M ∨ S = N ∨ subterm S M ∨ subterm S N. +#S #M #N #subH (@(subterm_myinv … subH)) + [#M1 #N1 #eqapp destruct /4/ + |#M1 #N1 #eqapp destruct /4/ + |3,4,5,6: #M1 #N1 #eqapp destruct + |#M1 #eqapp destruct + |#M1 #N1 #P #sub1 #sub2 #H1 #H2 #eqapp + (cases (H2 eqapp)) + [* [* /3/ | #subN1 %1 %2 /2/ ] + |#subN1 %2 /2/ + ] + ] +qed. + +lemma sublam: ∀S,M,N. subterm S (Lambda M N) → + S = M ∨ S = N ∨ subterm S M ∨ subterm S N. +#S #M #N #subH (@(subterm_myinv … subH)) + [1,2,5,6: #M1 #N1 #eqH destruct + |3,4:#M1 #N1 #eqH destruct /4/ + |#M1 #eqH destruct + |#M1 #N1 #P #sub1 #sub2 #H1 #H2 #eqH + (cases (H2 eqH)) + [* [* /3/ | #subN1 %1 %2 /2/ ] + |#subN1 %2 /2/ + ] + ] +qed. + +lemma subprod: ∀S,M,N. subterm S (Prod M N) → + S = M ∨ S = N ∨ subterm S M ∨ subterm S N. +#S #M #N #subH (@(subterm_myinv … subH)) + [1,2,3,4: #M1 #N1 #eqH destruct + |5,6:#M1 #N1 #eqH destruct /4/ + |#M1 #eqH destruct + |#M1 #N1 #P #sub1 #sub2 #H1 #H2 #eqH + (cases (H2 eqH)) + [* [* /3/ | #subN1 %1 %2 /2/ ] + |#subN1 %2 /2/ + ] + ] +qed. + +lemma subd: ∀S,M. subterm S (D M) → + S = M ∨ subterm S M. +#S #M #subH (@(subterm_myinv … subH)) + [1,2,3,4,5,6: #M1 #N1 #eqH destruct + |#M1 #eqH destruct /2/ + |#M1 #N1 #P #sub1 #sub2 #_ #H #eqH + (cases (H eqH)) /2/ + #subN1 %2 /2/ + ] +qed. + +lemma subsort: ∀S,n. ¬ subterm S (Sort n). +#S #n % #subH (@(subterm_myinv … subH)) + [1,2,3,4,5,6: #M1 #N1 #eqH destruct + |#M1 #eqa destruct + |/2/ + ] +qed. + +lemma subrel: ∀S,n. ¬ subterm S (Rel n). +#S #n % #subH (@(subterm_myinv … subH)) + [1,2,3,4,5,6: #M1 #N1 #eqH destruct + |#M1 #eqa destruct + |/2/ + ] +qed. + +theorem Telim: ∀P: T → Prop. (∀M. (∀N. subterm N M → P N) → P M) → + ∀M. P M. +#P #H #M (cut (P M ∧ (∀N. subterm N M → P N))) + [2: * //] +(elim M) + [#n % + [@H #N1 #subN1 @False_ind /2/ + |#N #subN1 @False_ind /2/ + ] + |#n % + [@H #N1 #subN1 @False_ind /2/ + |#N #subN1 @False_ind /2/ + ] + |#M1 #M2 * #PM1 #Hind1 * #PM2 #Hind2 + (cut (∀N.subterm N (App M1 M2) → P N)) + [#N1 #subN1 (cases (subapp … subN1)) + [* [* // | @Hind1 ] | @Hind2 ]] + #Hcut % /3/ + |#M1 #M2 * #PM1 #Hind1 * #PM2 #Hind2 + (cut (∀N.subterm N (Lambda M1 M2) → P N)) + [#N1 #subN1 (cases (sublam … subN1)) + [* [* // | @Hind1 ] | @Hind2 ]] + #Hcut % /3/ + |#M1 #M2 * #PM1 #Hind1 * #PM2 #Hind2 + (cut (∀N.subterm N (Prod M1 M2) → P N)) + [#N1 #subN1 (cases (subprod … subN1)) + [* [* // | @Hind1 ] | @Hind2 ]] + #Hcut % /3/ + |#M1 * #PM1 #Hind1 + (cut (∀N.subterm N (D M1) → P N)) + [#N1 #subN1 (cases (subd … subN1)) /2/] + #Hcut % /3/ + ] +qed. + -- 2.39.2