X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Fsubject.ma;h=be34cb07feea60d7700d1a7b11d10dfdb8740dfc;hb=2b51cf74b9a5f37d0f91780ceae4b8f4d0ee38a1;hp=c6b0eafdb243e0785bef05fbe0b987bf30f024bb;hpb=8fa6a59d37eafaea6b21450efd679081bd83bcba;p=helm.git

diff --git a/matita/matita/lib/lambda/subject.ma b/matita/matita/lib/lambda/subject.ma
index c6b0eafdb..be34cb07f 100644
--- a/matita/matita/lib/lambda/subject.ma
+++ b/matita/matita/lib/lambda/subject.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)
@@ -46,9 +44,9 @@ lemma lift_D: ∀M,N. lift M 0 1 = D N →
   ]
 qed. 
 
-theorem type_of_type: ∀G,A,B. G ⊢ A : B → (∀i. B ≠ Sort i) →
-  ∃i. G ⊢ B : Sort i.
-#G #A #B #t (elim t)
+theorem type_of_type: ∀P,G,A,B. G ⊢_{P} A : B → (∀i. B ≠ Sort i) →
+  ∃i. G ⊢_{P} B : Sort i.
+#Pts #G #A #B #t (elim t)
   [#i #j #Aij #j @False_ind /2/ 
   |#G1 #A #i #t1 #_ #P @(ex_intro … i) @(weak … t1 t1)
   |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #H3 (cases (H1 ?) )
@@ -68,9 +66,9 @@ theorem type_of_type: ∀G,A,B. G ⊢ A : B → (∀i. B ≠ Sort i) →
   ]
 qed.
 
-lemma prod_sort : ∀G,M,P,Q. G ⊢ M :Prod P Q →
- ∃i. P::G ⊢ Q : Sort i.
-#G #M #P #Q #t cases(type_of_type …t ?);
+lemma prod_sort : ∀Pts,G,M,P,Q. G ⊢_{Pts} M :Prod P Q →
+ ∃i. P::G ⊢_{Pts} Q : Sort i.
+#Pts #G #M #P #Q #t cases(type_of_type …t ?);
   [#s #t2 cases(prod_inv … t2 …(refl …)) #s1 * #s2 * #s3 * * 
    #_ #_ #H @(ex_intro … s2) //
   | #i % #H destruct
@@ -80,8 +78,8 @@ qed.
 axiom red_lift: ∀M,N. red (lift M 0 1) N → 
   ∃P. N = lift P 0 1 ∧ red M P. 
 
-theorem tj_d : ∀G,M,N. G ⊢ D M : N → G ⊢ M : N.
-#G (cut (∀M,N. G ⊢ M : N → ∀P. M = D P → G ⊢ P : N)) [2: /2/] 
+theorem tj_d : ∀P,G,M,N. G ⊢_{P} D M : N → G ⊢_{P} M : N.
+#Pts #G (cut (∀M,N. G ⊢_{Pts} M : N → ∀P. M = D P → G ⊢_{Pts} P : N)) [2: /2/] 
 #M #N #t (elim t)
   [#i #j #Aij #P #H destruct 
   |#G1 #A #i #t1 #_ #P #H destruct
@@ -98,15 +96,13 @@ qed.
 
 definition red0 ≝ λM,N. M = N ∨ red M N.
 
-axiom conv_lift: ∀i,M,N. conv M N →
-  conv (lift M 0 i) (lift N 0 i).
-axiom red_to_conv : ∀M,N. red M N → conv M N.
-axiom refl_conv: ∀M. conv M M.
-axiom sym_conv: ∀M,N. conv M N → conv N M.
-axiom red0_to_conv : ∀M,N. red0 M N → conv M N.
-axiom conv_prod: ∀A,B,M,N. conv A B → conv M N → 
-  conv (Prod A M) (Prod B N). 
-axiom conv_subst_1: ∀M,P,Q. red P Q → conv (M[0≝Q]) (M[0≝P]).
+axiom conv_lift: ∀P,i,M,N. Co P M N →
+  Co P (lift M 0 i) (lift N 0 i).
+axiom red_to_conv : ∀P,M,N. red M N → Co P M N.
+axiom red0_to_conv : ∀P,M,N. red0 M N → Co P M N.
+axiom conv_prod: ∀P,A,B,M,N. Co P A B → Co P M N → 
+  Co P (Prod A M) (Prod B N). 
+axiom conv_subst_1: ∀Pts,M,P,Q. red P Q → Co Pts (M[0≝Q]) (M[0≝P]).
 
 inductive redG : list T → list T → Prop ≝
  | rnil : redG (nil T) (nil T)
@@ -127,33 +123,16 @@ lemma redG_nil: ∀G. redG (nil T) G → G = nil T.
 #A #B #G1 #G2 #r1 #r2 #_ #H destruct
 qed.
 
-(*
-inductive redG : list T → list T → Prop ≝
- |redT : ∀A,B,G1,G2. red A B → redG G1 G2 → 
-     redG (A::G1) (B::G2)
- |redF : ∀A,G1,G2. redG G1 G2 → redG (A::G1) (A::G2).
-
-lemma redG_inv: ∀A,G,G1. redG (A::G) G1 → 
-  ∃B. ∃G2. red0 A B ∧ redG G G2 ∧ G1 = B::G2.
-#A #G #G1 #rg (inversion rg) 
-  [#H destruct
-  |#A1 #B1 #G2 #G3 #r1 #r2 #_ #H destruct
-   #H1 @(ex_intro … B1) @(ex_intro … G3) % // % //
-  ]
-qed. *)
-
-axiom conv_prod_split: ∀A,A1,B,B1. conv (Prod A B) (Prod A1 B1) →
-conv A A1 ∧ conv B B1.
+axiom conv_prod_split: ∀P,A,A1,B,B1. 
+ Co P(Prod A B) (Prod A1 B1) → Co P A A1 ∧ Co P B B1.
 
 axiom red0_prod : ∀M,N,P. red0 (Prod M N) P → 
   (∃Q. P = Prod Q N ∧ red0 M Q) ∨
   (∃Q. P = Prod M Q ∧ red0 N Q).
-  
-axiom my_dummy: ∀G,M,N. G ⊢ M : N → G ⊢ D M : N.
 
-theorem subject_reduction: ∀G,M,N. TJ G M N → ∀M1. red0 M M1 → 
-∀G1. redG G G1 → TJ G1 M1 N.
-#G #M #N #d (elim d)
+theorem subject_reduction: ∀P,G,M,N. G ⊢_{P} M:N → 
+ ∀M1. red0 M M1 → ∀G1. redG G G1 → G1 ⊢_{P} M1:N.
+#Pts #G #M #N #d (elim d)
   [#i #j #Aij #M1 * 
     [#eqM1 <eqM1 #G1 #H >(redG_nil …H) /2/
     |#H @False_ind /2/
@@ -161,7 +140,7 @@ theorem subject_reduction: ∀G,M,N. TJ G M N → ∀M1. red0 M M1 →
   |#G1 #A #i #t1 #Hind #M1 * 
     [#eqM1 <eqM1 #G2 #H cases (redG_inv … H)
      #P * #G3 * * #r1 #r2 #eqG2 >eqG2
-     @(conv ?? (lift P O 1) ? i);
+     @(conv ??? (lift P O 1) ? i);
       [@conv_lift @sym_conv @red0_to_conv //
       |@(start … i) @Hind //
       |@(weak … (Sort i) ? i); [@Hind /2/ | @Hind //]
@@ -192,40 +171,27 @@ theorem subject_reduction: ∀G,M,N. TJ G M N → ∀M1. red0 M M1 →
     |#reda (cases (red_app …reda))
       [*
         [* 
-          [* #M2 * #N1 * #eqA #eqM1 >eqM1 #G1 #rg
-           cut (G1 ⊢ A: Prod B C); [@Hind1 /2/] #H1
+          #M2 * #N1 * #eqA #eqM1 >eqM1 #G1 #rg
+           cut (G1 ⊢_{Pts} A: Prod B C); [@Hind1 /2/] #H1
            (cases (abs_inv … H1 … eqA)) #i * #N2 * * 
            #cProd #t3 #t4 
-           (cut (conv B M2 ∧ conv C N2) ) [/2/] * #convB #convC
+           (cut (Co Pts B M2 ∧ Co Pts C N2) ) [/2/] * #convB #convC
            (cases (prod_inv … t3 … (refl …) )) #i * #j * #k * *
-           #cik #t5 #t6 (cut (G1 ⊢ P:B)) 
+           #cik #t5 #t6 (cut (G1 ⊢_{Pts} P:B)) 
             [@Hind2 /2/
-            |#Hcut cut (G1 ⊢ N1[0:=P] : N2 [0:=P]);
+            |#Hcut cut (G1 ⊢_{Pts} N1[0:=P] : N2 [0:=P]);
               [@(tj_subst_0 … M2) // @(conv … convB Hcut t5)
               |#Hcut1 cases (prod_sort … H1) #s #Csort
                @(conv … s  … Hcut1); 
                 [@conv_subst /2/ | @(tj_subst_0 … Csort) //]
               ]
             ]
-          |* #M2 * #eqA #eqM1 >eqM1 #G1 #rg
-           cut (G1 ⊢ A:Prod B C); [@Hind1 /2/] #t3
-           cases (prod_sort …t3) #i #Csort @(dummy … i);
-            [ @(app  … B);
-              [@tj_d @Hind1 /2/|@Hind2 /2/]
-            | @(tj_subst_0 … B … (Sort i));
-              [@Hind2 /2/ 
-              |//
-              ]
-            ] 
-           (* @my_dummy @(app … B); [@tj_d @Hind1 /2/|@Hind2 /2/]
-           *)          
-          ]
         |* #M2 * #eqM1 >eqM1 #H #G1 #rg @(app … B);
           [@Hind1 /2/ | @Hind2 /2/] 
         ]      
       |* #M2 * #eqM1 >eqM1 #H #G1 #rg 
-       cut (G1 ⊢ A:Prod B C); [@Hind1 /2/] #t3
-       cases (prod_sort …t3) #i #Csort @(conv ?? C[O≝ M2] … i);
+       cut (G1 ⊢_{Pts} A:Prod B C); [@Hind1 /2/] #t3
+       cases (prod_sort …t3) #i #Csort @(conv ??? C[O≝ M2] … i);
         [@conv_subst_1 //
         |@(app … B)  // @Hind2 /2/
         |@(tj_subst_0 … Csort) @Hind2 /2/
@@ -233,22 +199,18 @@ theorem subject_reduction: ∀G,M,N. TJ G M N → ∀M1. red0 M M1 →
       ]
     ]
   |#G #A #B #C #i #t1 #t2 #Hind1 #Hind2 #M2 #red0l #G1 #rg
-   cut (A::G1⊢C:B); [@Hind1 /3/] #t3
-   cut (G1 ⊢ Prod A B : Sort i); [@Hind2 /2/] #t4
+   cut (A::G1⊢_{Pts} C:B); [@Hind1 /3/] #t3
+   cut (G1 ⊢_{Pts} Prod A B : Sort i); [@Hind2 /2/] #t4
    cases red0l;
     [#eqM2 <eqM2 @(abs … t3 t4)
     |#redl (cases (red_lambda … redl))  
-      [*
-        [* #M3 * #eqM2 #redA >eqM2 
-         @(conv ?? (Prod M3 B) … t4);
+      [* #M3 * #eqM2 #redA >eqM2 
+         @(conv ??? (Prod M3 B) … t4);
           [@conv_prod /2/
           |@(abs … i); [@Hind1 /3/ |@Hind2 /3/]
           ]
         |* #M3 * #eqM3 #redC >eqM3
          @(abs … t4) @Hind1 /3/
-        ]
-      |* #Q * #eqC #eqM2 >eqM2 @(dummy … t4)
-       @(abs … t4) @tj_d @Hind1 /3/
       ]
     ]
   |#G #A #B #C #i #convBC #t1 #t2 #Hind1 #Hind2 #M1 #redA