Dummies are blocked.

diff --git a/matita/matita/lib/lambda/par_reduction.ma b/matita/matita/lib/lambda/par_reduction.ma
index 6063ad955ccb693f15938ac85d1082174e1c199a..cea1e177b8ed33fc04202bf2b2ba9fe3601cb1f3 100644 (file)
--- a/matita/matita/lib/lambda/par_reduction.ma
+++ b/matita/matita/lib/lambda/par_reduction.ma
@@ -21,25 +21,27 @@ 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
   ]. 
-  
+
+(* 
 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.
+qed.*)
 
 theorem is_lambda_to_exists: ∀M. is_lambda M = true → 
 ∃P,N. M = Lambda P N.
@@ -47,14 +49,11 @@ theorem is_lambda_to_exists: ∀M. is_lambda M = true →
   [1,2,6: #n #H destruct|3,5: #P #Q #H destruct
   |#P #N #_ @(ex_intro … P) @(ex_intro … N) //
   ]
-qed.
+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 → 
@@ -65,9 +64,7 @@ inductive pr : T →T → Prop ≝
 
 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 
+  [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
   |//
   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
@@ -78,9 +75,7 @@ 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 
+  [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
   |//
   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
@@ -91,10 +86,8 @@ 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/
+  [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
+  |#M #eqM #_ @(ex_intro … N) /2/ 
   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
@@ -102,15 +95,13 @@ lemma prD: ∀M,N. pr (D N) M → ∃P.M = D P ∧ pr N P.
   ]
 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).
+lemma prApp_not_lambda: 
+∀M,N,P. pr (App M N) P → 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 
+  [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct #_ #H1 destruct
+  |#M1 #eqM1 #_ #_ @(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
@@ -118,35 +109,14 @@ lemma prApp_not_dummy_not_lambda:
   ]
 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) ∨
+  ∃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 #eqM1 #_ @(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
@@ -155,63 +125,24 @@ lemma prApp_lambda:
   ]
 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)).
+lemma prLambda: ∀M,N,P. pr (Lambda M N) P →
+  ∃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 
-  |#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/
+  |#Q #eqQ #_ @(ex_intro … M) @(ex_intro … N) /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
+  |#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.
+qed. 
 
 lemma prProd: ∀M,N,P. pr (Prod M N) P → 
-∃M1,N1. P = Prod M1 N1 ∧ pr M M1 ∧ pr N N1.
+  ∃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/
+  |#Q #eqQ #_ @(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
@@ -225,7 +156,7 @@ let rec full M ≝
   [ Sort n ⇒ Sort n
   | Rel n ⇒ Rel n
   | App P Q ⇒ full_app P (full Q)
-  | Lambda P Q ⇒ full_lam (full P) Q
+  | Lambda P Q ⇒ Lambda (full P) (full Q)
   | Prod P Q ⇒ Prod (full P) (full Q)
   | D P ⇒ D (full P)
   ]
@@ -236,25 +167,15 @@ and full_app M 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)
+  | D P ⇒ App (D (full P)) N
   ]
 . 
 
-lemma pr_lift: ∀N,N1,n. pr N N1 → ∀k. pr (lift N k n) (lift N1 k n).
+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]
@@ -265,7 +186,7 @@ lemma pr_lift: ∀N,N1,n. pr N N1 → ∀k. pr (lift N k n) (lift N1 k n).
   |#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) 
@@ -280,45 +201,29 @@ theorem pr_subst: ∀M,M1,N,N1,n. pr M M1 → pr N N1 →
      >(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 //] 
+   (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 // 
         ]
-      ]
-    |#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 // 
-          ]
+      |* * #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 // ]
       ]
+    |#notlambda (cases (prApp_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 //
-    ]
+   #N2 * #Q1 * * #eqM1 #pr3 #pr4 >eqM1 @lam;
+    [@Hind // normalize // | @Hind // normalize // ]
   |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2
    (cases (prProd … pr1)) #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1
    @prod; [@Hind // normalize // | @Hind // normalize // ]
@@ -326,7 +231,7 @@ theorem pr_subst: ∀M,M1,N,N1,n. pr M M1 → pr N N1 →
    #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).
@@ -334,146 +239,49 @@ lemma pr_full_app: ∀M,N,N1. pr N N1 →
   [#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/
+  |#P #Hind #N1 #N2 #prN #H @appl // @d /2/ 
   ]
 qed.
 
 theorem pr_full: ∀M. pr M (full M).
-@Telim #M (cases M) 
+@Telim #M (cases M) normalize
   [// 
   |//
   |#M1 #N1 #H @pr_full_app /3/
-  |#M1 #N1 #H @pr_full_lam /3/
+  |#M1 #N1 #H normalize /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 ??) // 
+  [#n #P #Q #subH #pr1 cases (prApp_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 ??) // 
+    [@(subH (Sort n)) // |@subH //]
+  |#n #P #Q #subH #pr1 cases (prApp_not_lambda … pr1 ?) // 
    #M1 * #N1 * * #eqQ #pr1 #pr2 >eqQ @appl; 
-    [@(Hind (Rel n)) // |@Hind //]
+    [@(subH (Rel n)) // |@subH //]
   |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH
-   cases (prApp_not_dummy_not_lambda … prH ??) // 
+   cases (prApp_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 ??) // 
+   cases (prApp_lambda … prH) #M2 * #N2 *
+    [* * #eqP2 #pr1 #pr2 >eqP2 @pr_subst /3/
+    |* * #eqP2 #pr1 #pr2 >eqP2 (cases (prLambda … pr1))
+     #M3 * #M4 * * #eqM2 #pr3 #pr4 >eqM2 @beta @subH /2/
+    ]
+  |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH
+   cases (prApp_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/]
-    ]    
+  |#P #Hind #N1 #N2 #subH #pr1
+   cases (prApp_not_lambda … pr1 ?) // 
+   #M1 * #N1 * * #eqQ #pr2 #pr3 >eqQ @appl; 
+    [@(subH (D P) M1) // |@subH //]    
   ]
 qed.
 
@@ -483,11 +291,11 @@ theorem complete: ∀M,N. pr M N → pr N (full M).
   |#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 
+  |#P #P1 #Hind #N #Hpr 
+   (cases (prLambda …Hpr)) #M1 * #N1 * * #eqN >eqN normalize /3/
+  |#P #P1 #Hind #N #Hpr 
    (cases (prProd …Hpr)) #M1 * #N1 * * #eqN >eqN normalize /3/
-  |6:#N #Hind #P #prH normalize cases (prD … prH) 
+  |#N #Hind #P #prH normalize cases (prD … prH) 
    #Q * #eqP >eqP #prN @d @Hind //
   ]
 qed.
@@ -497,5 +305,3 @@ pr Q S ∧ pr P S.
 #P #Q #R #pr1 #pr2 @(ex_intro … (full P)) /3/
 qed.
 
-
-

diff --git a/matita/matita/lib/lambda/reduction.ma b/matita/matita/lib/lambda/reduction.ma
index 552969b667a13d28106baac4d30995237bba4d87..58e4e179aab1ff9e6f8fa935d257bf0749c9125e 100644 (file)
--- a/matita/matita/lib/lambda/reduction.ma
+++ b/matita/matita/lib/lambda/reduction.ma
@@ -24,8 +24,6 @@ inductive T : Type[0] ≝
 
 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)
@@ -41,25 +39,20 @@ 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
-  |#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
   ]
@@ -70,8 +63,7 @@ lemma red_prod : ∀M,N,P. red (Prod M N) P →
  (∃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 
@@ -82,19 +74,16 @@ qed.
 
 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.
@@ -112,8 +101,7 @@ 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.
@@ -121,8 +109,7 @@ 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.
@@ -132,22 +119,16 @@ lemma red_subst : ∀N,M,M1,i. red M M1 → red M[i≝N] M1[i≝N].
   [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/
@@ -314,27 +295,11 @@ lemma SN_Lambda: ∀N.SN N → ∀M.SN M → SN (Lambda N M).
 (* 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)
@@ -352,6 +317,7 @@ lemma SN_subst: ∀i,N,M.SN M[i ≝ N] → SN M.
   |#Hcut #M #snM @(Hcut … snM) //
 qed.
 
+(*
 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
@@ -366,7 +332,7 @@ cut (∀P. SN P → ∀M,N. P = App M N → SN (App (D M) N)); [|/2/]
     ]
   |* #M2 * #eqA >eqA #r2 @(Hind (App M M2)) /2/
   ]
-qed.
+qed. *)
 
 lemma  SN_APP: ∀P.SN P → ∀N. SN N → ∀M.
   SN M[0:=N] → SN (App (Lambda P M) N).
@@ -376,20 +342,11 @@ lemma  SN_APP: ∀P.SN P → ∀N. SN N → ∀M.
 (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; 
-          [%1 // |@(SN_step … snC1) /2/]
-        ]
-      |* #M3 * #eqC #eqM2 >eqM2 @SN_DAPP @HindC;
-        [%2 >eqC @inj //
-        |@(SN_subterm … snC1) >eqC normalize //
-        ]
+      [* #M3 * #eqM2 #r2 >eqM2 @HindA // % /2/
+      |* #M3 * #eqM2 #r2 >eqM2 @HindC; 
+        [%1 // |@(SN_step … snC1) /2/]
       ]
     ]
   |* #M2 * #eqQ #r2 >eqQ @HindB // @(SN_star … snC1)