From c42ed8044c4bb9b8eadfd6930238ff5e700df656 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 10 Mar 2011 07:41:22 +0000 Subject: [PATCH 1/1] diamond property --- matita/matita/lib/lambda/par_reduction.ma | 501 ++++++++++++++++++++++ matita/matita/lib/lambda/subst.ma | 85 +++- 2 files changed, 583 insertions(+), 3 deletions(-) create mode 100644 matita/matita/lib/lambda/par_reduction.ma diff --git a/matita/matita/lib/lambda/par_reduction.ma b/matita/matita/lib/lambda/par_reduction.ma new file mode 100644 index 000000000..6063ad955 --- /dev/null +++ b/matita/matita/lib/lambda/par_reduction.ma @@ -0,0 +1,501 @@ +(* + ||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) + ] +. + +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] + |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k + normalize @lam; [@Hind1 |@Hind2] + |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k + normalize @prod; [@Hind1 |@Hind2] + |#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) + [#i #Hind #N #M1 #N1 #n #pr1 #pr2 >(prSort … pr1) // + |#i #Hind #N #M1 #N1 #n #pr1 #pr2 >(prRel … pr1) + (cases (true_or_false (leb i n))) + [#lein (cases (le_to_or_lt_eq i n (leb_true_to_le … lein))) + [#ltin >(subst_rel1 … ltin) >(subst_rel1 … ltin) // + |#eqin >eqin >subst_rel2 >subst_rel2 /2/ + ] + |#lefalse (cut (n < i)) [@not_le_to_lt /2/] #ltni + >(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 // + ] + |* * #eqM1 #pr4 #pr5 >eqM1 @appl; + [@Hind // 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 // + ] + |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2 + (cases (prProd … pr1)) #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1 + @prod; [@Hind // normalize // | @Hind // normalize // ] + |#Q #Hind #M1 #N #N1 #n #pr1 #pr2 (cases (prD … pr1)) + #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). +#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/subst.ma b/matita/matita/lib/lambda/subst.ma index bd8c5b713..565432a9d 100644 --- a/matita/matita/lib/lambda/subst.ma +++ b/matita/matita/lib/lambda/subst.ma @@ -38,7 +38,7 @@ notation "↑ ^ n ( M )" non associative with precedence 40 for @{'Lift O $M}. notation "↑ _ k ^ n ( M )" non associative with precedence 40 for @{'Lift $n $k $M}. *) (* interpretation "Lift" 'Lift n M = (lift M n). *) -interpretation "Lift" 'Lift n k M = (lift M k n). +interpretation "Lift" 'Lift n k M = (lift M k n). let rec subst t k a ≝ match t with @@ -80,8 +80,20 @@ lemma lift_rel1: ∀i.lift (Rel i) 0 1 = Rel (S i). #i (change with (lift (Rel i) 0 1 = Rel (1 + i))) // qed. -lemma lift_lift: ∀t.∀i,j.j ≤ i → ∀h,k. - lift (lift t k i) (j+k) h = lift t k (i+h). +lemma lift_rel_lt : ∀n,k,i. i < k → lift (Rel i) k n = Rel i. +#n #k #i #ltik change with +(if_then_else ? (leb (S i) k) (Rel i) (Rel (i+n)) = Rel i) +>(le_to_leb_true … ltik) // +qed. + +lemma lift_rel_ge : ∀n,k,i. k ≤ i → lift (Rel i) k n = Rel (i+n). +#n #k #i #leki change with +(if_then_else ? (leb (S i) k) (Rel i) (Rel (i+n)) = Rel (i+n)) +>lt_to_leb_false // @le_S_S // +qed. + +lemma lift_lift: ∀t.∀m,j.j ≤ m → ∀n,k. + lift (lift t k m) (j+k) n = lift t k (m+n). #t #i #j #h (elim t) normalize // #n #h #k @(leb_elim (S n) k) #Hnk normalize [>(le_to_leb_true (S n) (j+k) ?) normalize /2/ @@ -91,6 +103,28 @@ lemma lift_lift: ∀t.∀i,j.j ≤ i → ∀h,k. ] qed. +lemma lift_lift_up: ∀n,m,t,k,i. + lift (lift t i m) (m+k+i) n = lift (lift t (k+i) n) i m. +#n #m #N (elim N) + [1,3,4,5,6: normalize // + |#p #k #i @(leb_elim i p); + [#leip >lift_rel_ge // @(leb_elim (k+i) p); + [#lekip >lift_rel_ge; + [>lift_rel_ge // >lift_rel_ge // @(transitive_le … leip) // + |>associative_plus >commutative_plus @monotonic_le_plus_l // + ] + |#lefalse (cut (p < k+i)) [@not_le_to_lt //] #ltpki + >lift_rel_lt; [|>associative_plus >commutative_plus @monotonic_lt_plus_r //] + >lift_rel_lt // >lift_rel_ge // + ] + |#lefalse (cut (p < i)) [@not_le_to_lt //] #ltpi + >lift_rel_lt // >lift_rel_lt; [|@(lt_to_le_to_lt … ltpi) //] + >lift_rel_lt; [|@(lt_to_le_to_lt … ltpi) //] + >lift_rel_lt // + ] + ] +qed. + lemma lift_lift1: ∀t.∀i,j,k. lift(lift t k j) k i = lift t k (j+i). /2/ qed. @@ -168,6 +202,51 @@ lemma lift_subst_ijk: ∀A,B.∀i,j,k. ] qed. +lemma lift_subst_up: ∀M,N,n,i,j. + lift M[i≝N] (i+j) n = (lift M (i+j+1) n)[i≝ (lift N j n)]. +#M (elim M) + [// + |#p #N #n #i #j (cases (true_or_false (leb p i))) + [#lepi (cases (le_to_or_lt_eq … (leb_true_to_le … lepi))) + [#ltpi >(subst_rel1 … ltpi) + (cut (p < i+j)) [@(lt_to_le_to_lt … ltpi) //] #ltpij + >(lift_rel_lt … ltpij); >(lift_rel_lt ?? p ?); + [>subst_rel1 // | @(lt_to_le_to_lt … ltpij) //] + |#eqpi >eqpi >subst_rel2 >lift_rel_lt; + [>subst_rel2 >(plus_n_O (i+j)) + applyS lift_lift_up + |@(le_to_lt_to_lt ? (i+j)) // + ] + ] + |#lefalse (cut (i < p)) [@not_le_to_lt /2/] #ltip + (cut (0 < p)) [@(le_to_lt_to_lt … ltip) //] #posp + >(subst_rel3 … ltip) (cases (true_or_false (leb (S p) (i+j+1)))) + [#Htrue (cut (p < i+j+1)) [@(leb_true_to_le … Htrue)] #Hlt + >lift_rel_lt; + [>lift_rel_lt // >(subst_rel3 … ltip) // | @lt_plus_to_minus //] + |#Hfalse >lift_rel_ge; + [>lift_rel_ge; + [>subst_rel3; [@eq_f /2/ | @(lt_to_le_to_lt … ltip) //] + |@not_lt_to_le @(leb_false_to_not_le … Hfalse) + ] + |@le_plus_to_minus_r @not_lt_to_le + @(leb_false_to_not_le … Hfalse) + ] + ] + ] + |#P #Q #HindP #HindQ #N #n #i #j normalize + @eq_f2; [@HindP |@HindQ ] + |#P #Q #HindP #HindQ #N #n #i #j normalize + @eq_f2; [@HindP |>associative_plus >(commutative_plus j 1) + associative_plus >(commutative_plus j 1) +