\ /
V_______________________________________________________________ *)
-include "lambda/subterms.ma".
+include "lambda/par_reduction.ma".
+include "basics/star.ma".
(*
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
- ].
+inductive red : T →T → Prop ≝
+ | rbeta: ∀P,M,N. red (App (Lambda P M) N) (M[0 ≝ 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)
+ | rlamr: ∀M,N,N1. red N N1 → red(Lambda M N) (Lambda M N1)
+ | rprodl: ∀M,M1,N. red M M1 → red (Prod M N) (Prod M1 N)
+ | rprodr: ∀M,N,N1. red N N1 → red (Prod M N) (Prod M N1)
+ | d: ∀M,M1. red M M1 → red (D M) (D M1).
+
+lemma red_to_pr: ∀M,N. red M N → pr M N.
+#M #N #redMN (elim redMN) /2/
+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
+ |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).
+#M #N #P #redMNP (inversion redMNP)
+ [#P1 #M1 #N1 #eqH destruct
+ |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 %2
+ (@(ex_intro … N1)) % //
+ |#Q1 #M1 #red1 #_ #eqH destruct
+ ]
+qed.
-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) //
+lemma red_prod : ∀M,N,P. red (Prod M N) P →
+ (∃M1. P = (Prod M1 N) ∧ red M M1) ∨
+ (∃N1. P = (Prod M N1) ∧ red N N1).
+#M #N #P #redMNP (inversion redMNP)
+ [#P1 #M1 #N1 #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
+ (@(ex_intro … N1)) % //
+ |#Q1 #M1 #red1 #_ #eqH destruct
]
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) //
+lemma red_app : ∀M,N,P. red (App M N) P →
+ (∃M1,N1. M = (Lambda M1 N1) ∧ P = N1[0:=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
+ @(ex_intro … P1) @(ex_intro … M1) % //
+ |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1 %2
+ (@(ex_intro … M1)) % //
+ |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %2
+ (@(ex_intro … N1)) % //
+ |4,5,6,7:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
+ |#Q1 #M1 #red1 #_ #eqH destruct
]
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
+definition reduct ≝ λn,m. red m n.
+
+definition SN ≝ WF ? reduct.
+
+definition NF ≝ λM. ∀N. ¬ (reduct N M).
+
+theorem NF_to_SN: ∀M. NF M → SN M.
+#M #nfM % #a #red @False_ind /2/
+qed.
+
+lemma NF_Sort: ∀i. NF (Sort i).
+#i #N % #redN (inversion redN)
+ [1: #P #N #M #H destruct
+ |2,3,4,5,6,7: #N #M #P #_ #_ #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
+lemma NF_Rel: ∀i. NF (Rel i).
+#i #N % #redN (inversion redN)
+ [1: #P #N #M #H destruct
+ |2,3,4,5,6,7: #N #M #P #_ #_ #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/
+lemma red_subst : ∀N,M,M1,i. red M M1 → red M[i≝N] M1[i≝N].
+#N @Telim_size #P (cases P)
+ [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 * #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/
+ ]
+ |#P #Q #Hind #M1 #i #r1 (cases (red_prod …r1))
+ [* #P1 * #eqM1 #redP >eqM1 normalize @rprodl @Hind /2/
+ |* #P1 * #eqM1 #redP >eqM1 normalize @rprodr @Hind /2/
+ ]
+ |#P #Hind #M1 #i #r1 (cases (red_d …r1))
+ #P1 * #eqM1 #redP >eqM1 normalize @d @Hind /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
+lemma red_lift: ∀N,N1,n. red N N1 → ∀k. red (lift N k n) (lift N1 k n).
+#N #N1 #n #r1 (elim r1) normalize /2/
+qed.
+
+(* star red *)
+lemma star_appl: ∀M,M1,N. star … red M M1 →
+ star … red (App M N) (App M1 N).
+#M #M1 #N #star1 (elim star1) //
+#B #C #starMB #redBC #H @(inj … H) /2/
+qed.
+
+lemma star_appr: ∀M,N,N1. star … red N N1 →
+ star … red (App M N) (App M N1).
+#M #N #N1 #star1 (elim star1) //
+#B #C #starMB #redBC #H @(inj … H) /2/
+qed.
+
+lemma star_app: ∀M,M1,N,N1. star … red M M1 → star … red N N1 →
+ star … red (App M N) (App M1 N1).
+#M #M1 #N #N1 #redM #redN @(trans_star ??? (App M1 N)) /2/
+qed.
+
+lemma star_laml: ∀M,M1,N. star … red M M1 →
+ star … red (Lambda M N) (Lambda M1 N).
+#M #M1 #N #star1 (elim star1) //
+#B #C #starMB #redBC #H @(inj … H) /2/
+qed.
+
+lemma star_lamr: ∀M,N,N1. star … red N N1 →
+ star … red (Lambda M N) (Lambda M N1).
+#M #N #N1 #star1 (elim star1) //
+#B #C #starMB #redBC #H @(inj … H) /2/
+qed.
+
+lemma star_lam: ∀M,M1,N,N1. star … red M M1 → star … red N N1 →
+ star … red (Lambda M N) (Lambda M1 N1).
+#M #M1 #N #N1 #redM #redN @(trans_star ??? (Lambda M1 N)) /2/
+qed.
+
+lemma star_prodl: ∀M,M1,N. star … red M M1 →
+ star … red (Prod M N) (Prod M1 N).
+#M #M1 #N #star1 (elim star1) //
+#B #C #starMB #redBC #H @(inj … H) /2/
+qed.
+
+lemma star_prodr: ∀M,N,N1. star … red N N1 →
+ star … red (Prod M N) (Prod M N1).
+#M #N #N1 #star1 (elim star1) //
+#B #C #starMB #redBC #H @(inj … H) /2/
+qed.
+
+lemma star_prod: ∀M,M1,N,N1. star … red M M1 → star … red N N1 →
+ star … red (Prod M N) (Prod M1 N1).
+#M #M1 #N #N1 #redM #redN @(trans_star ??? (Prod M1 N)) /2/
+qed.
+
+lemma star_d: ∀M,M1. star … red M M1 →
+ star … red (D M) (D M1).
+#M #M1 #redM (elim redM) // #B #C #starMB #redBC #H @(inj … H) /2/
+qed.
+
+lemma red_subst1 : ∀M,N,N1,i. red N N1 →
+ (star … red) M[i≝N] M[i≝N1].
+#M (elim M)
+ [//
+ |#i #P #Q #n #r1 (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 @R_to_star /2/
+ ]
+ |#lefalse (cut (n < i)) [@not_le_to_lt /2/] #ltni
+ >(subst_rel3 … ltni) >(subst_rel3 … ltni) //
+ ]
+ |#P #Q #Hind1 #Hind2 #M1 #N1 #i #r1 normalize @star_app /2/
+ |#P #Q #Hind1 #Hind2 #M1 #N1 #i #r1 normalize @star_lam /2/
+ |#P #Q #Hind1 #Hind2 #M1 #N1 #i #r1 normalize @star_prod /2/
+ |#P #Hind #M #N #i #r1 normalize @star_d /2/
]
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
- ]
+lemma SN_d : ∀M. SN M → SN (D M).
+#M #snM (elim snM) #b #H #Hind % #a #redd (cases (red_d … redd))
+#Q * #eqa #redbQ >eqa @Hind //
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
- ]
+lemma SN_step: ∀N. SN N → ∀M. reduct M N → SN M.
+#N * #b #H #M #red @H //.
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
- ]
+lemma SN_star: ∀M,N. (star … red) N M → SN N → SN M.
+#M #N #rstar (elim rstar) //
+#Q #P #HbQ #redQP #snNQ #snN @(SN_step …redQP) /2/
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
- ]
+lemma sub_red: ∀M,N.subterm N M → ∀N1.red N N1 →
+∃M1.subterm N1 M1 ∧ red M M1.
+#M #N #subN (elim subN) /4/
+(* trsansitive case *)
+#P #Q #S #subPQ #subQS #H1 #H2 #A #redP (cases (H1 ? redP))
+#B * #subA #redQ (cases (H2 ? redQ)) #C * #subBC #redSC
+@(ex_intro … C) /3/
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
- ]
+axiom sub_star_red: ∀M,N.(star … subterm) N M → ∀N1.red N N1 →
+∃M1.subterm N1 M1 ∧ red M M1.
+
+lemma SN_subterm: ∀M. SN M → ∀N.subterm N M → SN N.
+#M #snM (elim snM) #M #snM #HindM #N #subNM % #N1 #redN
+(cases (sub_red … subNM ? redN)) #M1 *
+#subN1M1 #redMM1 @(HindM … redMM1) //
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
- ]
+lemma SN_subterm_star: ∀M. SN M → ∀N.(star … subterm N M) → SN N.
+#M #snM #N #Hstar (cases (star_inv T subterm M N)) #_ #H
+lapply (H Hstar) #Hstari (elim Hstari) //
+#M #N #_ #subNM #snM @(SN_subterm …subNM) //
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/
+definition shrink ≝ λN,M. reduct N M ∨ (TC … subterm) N M.
+
+definition SH ≝ WF ? shrink.
+
+lemma SH_subterm: ∀M. SH M → ∀N.(star … subterm) N M → SH N.
+#M #snM (elim snM) #M
+#snM #HindM #N #subNM (cases (star_case ???? subNM))
+ [#eqNM >eqNM % /2/
+ |#subsNM % #N1 *
+ [#redN (cases (sub_star_red … subNM ? redN)) #M1 *
+ #subN1M1 #redMM1 @(HindM M1) /2/
+ |#subN1 @(HindM N) /2/
+ ]
]
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/
+
+theorem SN_to_SH: ∀N. SN N → SH N.
+#N #snN (elim snN) (@Telim_size)
+#b #Hsize #snb #Hind % #a * /2/ #subab @Hsize;
+ [(elim subab)
+ [#c #subac @size_subterm //
+ |#b #c #subab #subbc #sab @(transitive_lt … sab) @size_subterm //
+ ]
+ |@SN_step @(SN_subterm_star b);
+ [% /2/ |@TC_to_star @subab] % @snb
+ |#a1 #reda1 cases(sub_star_red b a ?? reda1);
+ [#a2 * #suba1 #redba2 @(SH_subterm a2) /2/ |/2/ ]
]
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/
+lemma SH_to_SN: ∀N. SH N → SN N.
+@WF_antimonotonic /2/ qed.
+
+lemma SN_Lambda: ∀N.SN N → ∀M.SN M → SN (Lambda N M).
+#N #snN (elim snN) #P #shP #HindP #M #snM
+(* 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/
]
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/
- ]
+lemma SN_Prod: ∀N.SN N → ∀M.SN M → SN (Prod N M).
+#N #snN (elim snN) #P #shP #HindP #M #snM (elim snM)
+#Q #snQ #HindQ % #a #redH (cases (red_prod … redH))
+ [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) //
+ % /2/
+ |* #S * #eqa #redQS >eqa @(HindQ S) /2/
]
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 // ]
- ]
- ]
+lemma SN_subst: ∀i,N,M.SN M[i ≝ N] → SN M.
+#i #N (cut (∀P.SN P → ∀M.P=M[i ≝ N] → SN M));
+ [#P #H (elim H) #Q #snQ #Hind #M #eqM % #M1 #redM
+ @(Hind M1[i:=N]) // >eqM /2/
+ |#Hcut #M #snM @(Hcut … snM) //
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 //
+(*
+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
+#M #N #eqQ % #A #rA (cases (red_app … rA))
+ [*
+ [*
+ [* #M1 * #N1 * #eqH destruct
+ |* #M1 * #eqH destruct #eqA >eqA @SN_d % @snQ
]
- |* #P * #eqM2 #pr3 >eqM2 normalize @d
- @Hind // #S #P #subH @sub
- (cases (sublam … subH)) [* [* /2/ | /2/] | /3/]
- ]
+ |* #M1 * #eqA #red1 (cases (red_d …red1))
+ #M2 * #eqM1 #r2 >eqA >eqM1 @(Hind (App M2 N)) /2/
+ ]
+ |* #M2 * #eqA >eqA #r2 @(Hind (App M M2)) /2/
]
-qed.
+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 //
+lemma SN_APP: ∀P.SN P → ∀N. SN N → ∀M.
+ SN M[0:=N] → SN (App (Lambda P M) N).
+#P #snP (elim snP) #A #snA #HindA
+#N #snN (elim snN) #B #snB #HindB
+#M #snM1 (cut (SH M)) [@SN_to_SH @(SN_subst … snM1)] #shM
+(generalize in match snM1) (elim shM)
+#C #shC #HindC #snC1 % #Q #redQ (cases (red_app … redQ))
+ [*
+ [* #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/]
+ ]
+ ]
+ |* #M2 * #eqQ #r2 >eqQ @HindB // @(SN_star … snC1)
+ @red_subst1 //
]
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.
projects / helm.git / blobdiff