sottotermini e confluenza (manca pr_substs).

diff --git a/matita/matita/lib/lambda/reduction.ma b/matita/matita/lib/lambda/reduction.ma
new file mode 100644 (file)
index 0000000..e6d57ba
--- /dev/null
+++ b/matita/matita/lib/lambda/reduction.ma
@@ -0,0 +1,456 @@
+(*
+    ||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)
+  ]
+. 
+
+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/
+  ]
+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/subterms.ma b/matita/matita/lib/lambda/subterms.ma
new file mode 100644 (file)
index 0000000..1b18f36
--- /dev/null
+++ b/matita/matita/lib/lambda/subterms.ma
@@ -0,0 +1,130 @@
+(*
+    ||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/subst.ma".
+
+inductive subterm : T → T → Prop ≝
+  | appl : ∀M,N. subterm M (App M N)
+  | appr : ∀M,N. subterm N (App M N)
+  | lambdal : ∀M,N. subterm M (Lambda M N)
+  | lambdar : ∀M,N. subterm N (Lambda M N)
+  | prodl : ∀M,N. subterm M (Prod M N)
+  | prodr : ∀M,N. subterm N (Prod M N)
+  | sub_b : ∀M. subterm M (D M)
+  | sub_trans : ∀M,N,P. subterm M N → subterm N P → subterm M P.
+
+inverter subterm_myinv for subterm (?%).
+
+lemma subapp: ∀S,M,N. subterm S (App M N) →
+ S = M ∨ S = N ∨ subterm S M ∨ subterm S N. 
+#S #M #N #subH (@(subterm_myinv … subH))
+  [#M1 #N1 #eqapp destruct /4/
+  |#M1 #N1 #eqapp destruct /4/
+  |3,4,5,6: #M1 #N1 #eqapp destruct
+  |#M1 #eqapp destruct
+  |#M1 #N1 #P #sub1 #sub2 #H1 #H2 #eqapp
+   (cases (H2 eqapp))
+    [* [* /3/ | #subN1 %1 %2 /2/ ] 
+    |#subN1 %2 /2/
+    ]
+  ]
+qed.
+ 
+lemma sublam: ∀S,M,N. subterm S (Lambda M N) →
+ S = M ∨ S = N ∨ subterm S M ∨ subterm S N. 
+#S #M #N #subH (@(subterm_myinv … subH))
+  [1,2,5,6: #M1 #N1 #eqH destruct
+  |3,4:#M1 #N1 #eqH destruct /4/
+  |#M1 #eqH destruct
+  |#M1 #N1 #P #sub1 #sub2 #H1 #H2 #eqH
+   (cases (H2 eqH))
+    [* [* /3/ | #subN1 %1 %2 /2/ ] 
+    |#subN1 %2 /2/
+    ]
+  ]
+qed.  
+
+lemma subprod: ∀S,M,N. subterm S (Prod M N) →
+ S = M ∨ S = N ∨ subterm S M ∨ subterm S N. 
+#S #M #N #subH (@(subterm_myinv … subH))
+  [1,2,3,4: #M1 #N1 #eqH destruct
+  |5,6:#M1 #N1 #eqH destruct /4/
+  |#M1 #eqH destruct
+  |#M1 #N1 #P #sub1 #sub2 #H1 #H2 #eqH
+   (cases (H2 eqH))
+    [* [* /3/ | #subN1 %1 %2 /2/ ] 
+    |#subN1 %2 /2/
+    ]
+  ]
+qed.
+
+lemma subd: ∀S,M. subterm S (D M) →
+ S = M ∨ subterm S M. 
+#S #M #subH (@(subterm_myinv … subH))
+  [1,2,3,4,5,6: #M1 #N1 #eqH destruct
+  |#M1 #eqH destruct /2/
+  |#M1 #N1 #P #sub1 #sub2 #_ #H #eqH
+   (cases (H eqH)) /2/
+    #subN1 %2 /2/
+  ]
+qed.    
+
+lemma subsort: ∀S,n. ¬ subterm S (Sort n).
+#S #n % #subH (@(subterm_myinv … subH))
+  [1,2,3,4,5,6: #M1 #N1 #eqH destruct
+  |#M1 #eqa destruct
+  |/2/
+  ]
+qed.
+
+lemma subrel: ∀S,n. ¬ subterm S (Rel n).
+#S #n % #subH (@(subterm_myinv … subH))
+  [1,2,3,4,5,6: #M1 #N1 #eqH destruct
+  |#M1 #eqa destruct
+  |/2/
+  ]
+qed.
+
+theorem Telim: ∀P: T → Prop. (∀M. (∀N. subterm N M → P N) → P M) →
+ ∀M. P M.
+#P #H #M (cut (P M ∧ (∀N. subterm N M → P N)))
+  [2: * //]
+(elim M)
+  [#n %
+    [@H #N1 #subN1 @False_ind /2/
+    |#N #subN1 @False_ind /2/
+    ]
+  |#n %
+    [@H #N1 #subN1 @False_ind /2/
+    |#N #subN1 @False_ind /2/
+    ]
+  |#M1 #M2 * #PM1 #Hind1 * #PM2 #Hind2 
+   (cut (∀N.subterm N (App M1 M2) → P N))
+    [#N1 #subN1 (cases (subapp … subN1))
+      [* [* // | @Hind1 ] | @Hind2 ]]
+    #Hcut % /3/
+  |#M1 #M2 * #PM1 #Hind1 * #PM2 #Hind2 
+   (cut (∀N.subterm N (Lambda M1 M2) → P N))
+    [#N1 #subN1 (cases (sublam … subN1))
+      [* [* // | @Hind1 ] | @Hind2 ]]
+   #Hcut % /3/
+  |#M1 #M2 * #PM1 #Hind1 * #PM2 #Hind2 
+   (cut (∀N.subterm N (Prod M1 M2) → P N))
+    [#N1 #subN1 (cases (subprod … subN1))
+      [* [* // | @Hind1 ] | @Hind2 ]]
+   #Hcut % /3/   
+  |#M1 * #PM1 #Hind1
+   (cut (∀N.subterm N (D M1) → P N))
+    [#N1 #subN1 (cases (subd … subN1)) /2/]
+   #Hcut % /3/  
+  ]  
+qed.
+