--- /dev/null
+(*
+ ||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 <eqR #_ @(ex_intro … N) /2/
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M1 #N1 #pr #_ #H destruct #eqM @(ex_intro … N1) /2/
+ ]
+qed.
+
+lemma prApp_not_dummy_not_lambda:
+∀M,N,P. pr (App M N) P → is_dummy M = false → is_lambda M = false →
+∃M1,N1. (P = App M1 N1 ∧ pr M M1 ∧ pr N N1).
+#M #N #P #prH (inversion prH)
+ [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct #_ #_ #H1 destruct
+ |#M1 #N1 #P1 #_ #_ #H destruct #_ #H1 destruct
+ |#M #N #P1 #_ #_ #H destruct
+ |#Q #eqProd #_ #_ #_ @(ex_intro … M) @(ex_intro … N) /3/
+ |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H #H1 #_ #_ destruct
+ @(ex_intro … N1) @(ex_intro … N2) /3/
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M #N #_ #_ #H destruct
+ ]
+qed.
+
+lemma prApp_D:
+∀M,N,P. pr (App (D M) N) P →
+ (∃Q. (P = D Q ∧ pr (App M N) Q)) ∨
+ (∃M1,N1.(P = (App (D M1) N1) ∧ pr M M1 ∧ pr N N1)).
+#M #N #P #prH (inversion prH)
+ [#R #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
+ |#M1 #N1 #P1 #pr1 #_ #H destruct #eqP
+ @or_introl @(ex_intro … P1) /2/
+ |#M #N #P1 #_ #_ #H destruct
+ |#R #eqR #_ @or_intror @(ex_intro … M) @(ex_intro … N) /3/
+ |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H destruct #_
+ cases (prD … pr1) #S * #eqN1 >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 // [<eqM normalize // | @d //]
+ |@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;
+ [<plus_n_Sm <plus_n_O @Hind // >eqQ
+ @(transitive_lt ? (size (Lambda M2 N2))) normalize //
+ |@Hind // normalize //
+ ]
+ |* * #eqM1 #pr4 #pr5 >eqM1 @appl;
+ [@Hind // <eqQ normalize //
+ |@Hind // normalize //
+ ]
+ ]
+ |#notlambda (cases (prApp_not_dummy_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 //
+ ]
+ |#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.
+
+
+
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
#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/
]
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.
]
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 @HindQ]
+ |#P #Q #HindP #HindQ #N #n #i #j normalize
+ @eq_f2; [@HindP |>associative_plus >(commutative_plus j 1)
+ <associative_plus @HindQ]
+ |#P #HindP #N #n #i #j normalize
+ @eq_f @HindP
+ ]
+qed.
+
theorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k →
(lift B i (S k)) [j ≝ A] = lift B i k.
#A #B (elim B) normalize /2/
projects / helm.git / commitdiff