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)
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
]
(∃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
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.
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.
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.
[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/
(* 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)
|#Hcut #M #snM @(Hcut … snM) //
qed.
-lemma SN_APP: ∀P.SN P → ∀N. SN N → ∀M.
+(*
+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
+ ]
+ |* #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. *)
+
+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 (SN M)) [@(SN_subst … snM1)] #snM
-(generalize in match snM1) (elim snM)
-#C #snC #HindC #snC1 % #Q #redQ (cases (red_app … redQ))
+#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 * #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 //
- @(SN_step … snC1) /2/
- ]
- |* #M3 * #eqC #eqM2 (* TODO *)
+ [* #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.