From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 21 Jun 2011 13:56:49 +0000 (+0000)
Subject: Some progress
X-Git-Tag: make_still_working~2425
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=18351dc3eb1f038f43aed3e7213f7246f142f770;p=helm.git

Some progress
---

diff --git a/matita/matita/lib/lambdaN/inversion.ma b/matita/matita/lib/lambdaN/inversion.ma
index 0c2c2a98b..511fa0309 100644
--- a/matita/matita/lib/lambdaN/inversion.ma
+++ b/matita/matita/lib/lambdaN/inversion.ma
@@ -9,7 +9,7 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/types.ma".
+include "lambdaN/thinning.ma".
 
 (*
 inductive TJ (p: pts): list T → T → T → Prop ≝
@@ -34,18 +34,6 @@ inductive TJ (p: pts): list T → T → T → Prop ≝
      TJ p G A B → TJ p G B (Sort i) → TJ p G (D A) B.
 *)
 
-axiom lambda_lift : ∀A,B,C. lift A 0 1 = Lambda B C →
-∃P,Q. A = Lambda P Q ∧ lift P 0 1  = B ∧ lift Q 1 1 = C.
-
-axiom prod_lift : ∀A,B,C. lift A 0 1 = Prod B C →
-∃P,Q. A = Prod P Q ∧ lift P 0 1  = B ∧ lift Q 1 1 = C.
-
-axiom conv_lift: ∀P,M,N. Co P M N → Co P (lift M 0 1) (lift N 0 1).
- 
-axiom weak_in: ∀P,G,A,B,M,N, i.
- A::G  ⊢_{P} M : N → G ⊢_{P} B : Sort i → 
-   (lift A 0 1)::B::G ⊢_{P}  lift M 1 1 : lift N 1 1.
-
 axiom refl_conv: ∀P,A. Co P A A.
 axiom  sym_conv: ∀P,A,B. Co P A B → Co P B A.
 axiom trans_conv: ∀P,A,B,C. Co P A B → Co P B C → Co P A C.
@@ -97,4 +85,22 @@ theorem abs_inv: ∀P,G,M,N. G ⊢ _{P} M : N → ∀A,b.M = Lambda A b →
   |#G1 #A #B #i #t1 #t2 #_ #_ #A1 #b #eqA destruct
   ]
 qed.
+
+theorem dummy_inv: ∀P,G,M,N. G ⊢ _{P} M: N → ∀A,B.M = D A B → 
+  Co P N B ∧ G ⊢_{P} A : B. 
+#Pts #G #M #N #t (elim t);
+  [#i #j #Aij #A #b #H destruct
+  |#G1 #P #i #t #_ #A #b #H destruct
+  |#G1 #P #Q #R #i #t1 #t2 #H1 #_ #A #b #Hl
+   cases (dummy_lift … Hl) #A1 * #b1 * * #eqP #eqA #eqb
+   cases (H1 … eqP) #c1 #t3 <eqb %
+    [@(conv_lift … c1) |<eqA @(weak … t3 t2) ]
+  |#G1 #A #B #i #j #k #Rijk #t1 #t2 #_ #_ #A1 #b #H destruct
+  |#G1 #P #A #B #C #t1 #t2 #_ #_ #A1 #b #H destruct
+  |#G1 #P #A #B #i #t1 #t2 #_ #_ #A1 #b #H destruct
+  |#G1 #A #B #C #i #cBC #t1 #t2 #H1 #H2 #A1 #b #eqA
+   cases (H1 … eqA) #c1 #t3 % // @(trans_conv Pts … c1) @sym_conv //
+  |#G1 #A #B #i #t1 #t2 #_ #_ #A1 #b #eqA destruct /2/
+  ]
+qed.
    
diff --git a/matita/matita/lib/lambdaN/subject.ma b/matita/matita/lib/lambdaN/subject.ma
index be34cb07f..e33364f6b 100644
--- a/matita/matita/lib/lambdaN/subject.ma
+++ b/matita/matita/lib/lambdaN/subject.ma
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/reduction.ma".
-include "lambda/inversion.ma". 
+include "lambdaN/reduction.ma".
+include "lambdaN/inversion.ma". 
 
 (*
 inductive T : Type[0] ≝
@@ -32,15 +32,15 @@ inductive red : T →T → Prop ≝
   | 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 lift_D: ∀M,N. lift M 0 1 = D N → 
-  ∃P. N = lift P 0 1 ∧ M = D P.   
-#M (cases M) normalize
-  [#i #N #H destruct
-  |#i #N #H destruct
-  |#A #B #N #H destruct
-  |#A #B #N #H destruct
-  |#A #B #N #H destruct
-  |#A #N #H destruct @(ex_intro … A) /2/
+lemma lift_D: ∀P,M,N. lift P 0 1 = D M N → 
+  ∃M1,N1. M = lift M1 0 1 ∧ N = lift N1 0 1 ∧ P = D M1 N1.   
+#P (cases P) normalize
+  [#i #M #N #H destruct
+  |#i #M #N #H destruct
+  |#A #B #M #N #H destruct
+  |#A #B #M #N #H destruct
+  |#A #B #M #N #H destruct
+  |#A #B #M #N #H destruct @(ex_intro … A) @(ex_intro … B) /3/
   ]
 qed. 
 
@@ -78,26 +78,25 @@ qed.
 axiom red_lift: ∀M,N. red (lift M 0 1) N → 
   ∃P. N = lift P 0 1 ∧ red M P. 
 
-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/] 
+theorem tj_d : ∀P,G,M,N,N1. G ⊢_{P} D M N1: N → G ⊢_{P} M : N.
+#Pts #G (cut (∀M,N. G ⊢_{Pts} M : N → ∀P,Q. M = D P Q → G ⊢_{Pts} P : N)) [2: /2/] 
 #M #N #t (elim t)
-  [#i #j #Aij #P #H destruct 
-  |#G1 #A #i #t1 #_ #P #H destruct
-  |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #P #H3 
-   cases (lift_D … H3) #P * #eqP #eqA >eqP @(weak … i) /2/
-  |#G1 #A #B #i #j #k #h #t1 #t2 #_ #_ #P  #H destruct
-  |#G1 #A #B #C #D #t1 #t2 #_ #_ #P  #H destruct
-  |#G1 #A #B #C #D #t1 #t2 #_ #_ #P  #H destruct
-  |#G1 #A #B #C #i #ch #t1 #t2 #H #_ #P #H
+  [#i #j #Aij #P #Q #H destruct 
+  |#G1 #A #i #t1 #_ #P #Q #H destruct
+  |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #P #Q #H3 
+   cases (lift_D … H3) #P1 * #Q1 * * #eqP #eqQ #eqA 
+   >eqP @(weak … i) /2/
+  |#G1 #A #B #i #j #k #h #t1 #t2 #_ #_ #P #Q #H destruct
+  |#G1 #A #B #C #D #t1 #t2 #_ #_ #P #Q #H destruct
+  |#G1 #A #B #C #D #t1 #t2 #_ #_ #P #Q #H destruct
+  |#G1 #A #B #C #i #ch #t1 #t2 #H #_ #P #Q #H
    @(conv… ch …t2) /2/
-  |#G1 #A #B #i #t1 #t2 #Hind1 #Hind2 #P #H destruct //
+  |#G1 #A #B #i #t1 #t2 #Hind1 #Hind2 #P #Q #H destruct //
   ]
 qed.
 
 definition red0 ≝ λM,N. M = N ∨ red M N.
 
-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 → 
@@ -218,8 +217,16 @@ theorem subject_reduction: ∀P,G,M,N. G ⊢_{P} M:N →
   |#G #A #B #i #t1 #t2 #Hind1 #Hind2 #M1 #red0d #G1 #rg
    cases red0d; 
     [#eqM1 <eqM1 @(dummy … i); [@Hind1 /2/ |@Hind2 /2/] 
-    |#redd (cases (red_d … redd)) #Q * #eqM1 #redA >eqM1
-     @(dummy … i);[@Hind1 /2/ |@Hind2 /2/]
+    |#redd (cases (red_d … redd))
+      [* #A1 * #eqM1 #redA >eqM1 
+       @(dummy … i);[@Hind1 /2/ |@Hind2 /2/]
+      |* #B1 * #eqM1 #redB >eqM1 
+       cut (G1 ⊢_{Pts} B: Sort i); [@Hind2 /2/] #sB
+       cut (G1 ⊢_{Pts} B1: Sort i); [@Hind2 /2/] #sB1
+       @(conv … B1 … i) /2/ @(dummy … i) // @(conv … B … i) /2/ 
+       @Hind1 /2/
+      ]
+    ]
   ]
 qed.
 
diff --git a/matita/matita/lib/lambdaN/thinning.ma b/matita/matita/lib/lambdaN/thinning.ma
new file mode 100644
index 000000000..1fcd6fe62
--- /dev/null
+++ b/matita/matita/lib/lambdaN/thinning.ma
@@ -0,0 +1,108 @@
+(*
+    ||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 "lambdaN/types.ma".
+
+(*
+inductive TJ (p: pts): list T → T → T → Prop ≝
+  | ax : ∀i,j. Ax p i j → TJ p (nil T) (Sort i) (Sort j)
+  | start: ∀G.∀A.∀i.TJ p G A (Sort i) → 
+      TJ p (A::G) (Rel 0) (lift A 0 1)
+  | weak: ∀G.∀A,B,C.∀i.
+     TJ p G A B → TJ p G C (Sort i) → 
+       TJ p (C::G) (lift A 0 1) (lift B 0 1)
+  | prod: ∀G.∀A,B.∀i,j,k. Re p i j k →
+     TJ p G A (Sort i) → TJ p (A::G) B (Sort j) → 
+       TJ p G (Prod A B) (Sort k)
+  | app: ∀G.∀F,A,B,a. 
+     TJ p G F (Prod A B) → TJ p G a A → 
+       TJ p G (App F a) (subst B 0 a)
+  | abs: ∀G.∀A,B,b.∀i. 
+     TJ p (A::G) b B → TJ p G (Prod A B) (Sort i) → 
+       TJ p G (Lambda A b) (Prod A B)
+  | conv: ∀G.∀A,B,C.∀i. Co p B C →
+     TJ p G A B → TJ p G C (Sort i) → TJ p G A C
+  | dummy: ∀G.∀A,B.∀i. 
+     TJ p G A B → TJ p G B (Sort i) → TJ p G (D A) B.
+*)
+
+(* the definition of liftl is tricky *)
+let rec liftl (G:list T) p : list T ≝  
+  match G with
+    [ nil ⇒ nil T
+    | cons A D ⇒ ((lift A (length ? D) p)::(liftl D p))
+    ].
+
+axiom lambda_lift : ∀A,B,C. lift A 0 1 = Lambda B C →
+∃P,Q. A = Lambda P Q ∧ lift P 0 1  = B ∧ lift Q 1 1 = C.
+
+axiom prod_lift : ∀A,B,C. lift A 0 1 = Prod B C →
+∃P,Q. A = Prod P Q ∧ lift P 0 1  = B ∧ lift Q 1 1 = C.
+
+axiom dummy_lift : ∀A,B,C. lift A 0 1 = D B C →
+∃P,Q. A = D P Q ∧ lift P 0 1  = B ∧ lift Q 0 1 = C.
+
+axiom conv_lift: ∀P,M,N,k. Co P M N → Co P (lift M k 1) (lift N k 1).
+
+lemma weak_gen: ∀P,E,M,N. E ⊢_{P} M : N → 
+∀G,D,A,i. E=D@G → G ⊢_{P} A : Sort i → 
+   (liftl D 1)@(A::G) ⊢_{P}  lift M (length ? D) 1 : lift N (length ? D) 1.
+#Pts #E #M #N #tjMN (elim tjMN)
+  [normalize #i #j #k #G #D #A #i (cases D) 
+    [normalize #isnil destruct #H @start_lemma1 //
+     @(glegalk … (start … H))
+    |#P #L normalize #isnil destruct
+    ]
+  |#G #A #i #tjA #Hind #G1 #D #A1 #j (cases D) 
+    [normalize #Heq #tjA1 <(lift_rel 0 1) @(weak …tjA1)
+     <Heq @(start … tjA)
+    |#A2 #L normalize #Heq destruct #tjA2 
+     cut (S (length ? L) = 1 + length ? L + 0) // #H >H
+     >lift_lift_up <plus_n_O @(start … i) @Hind //
+    ]
+  |#G #P #Q #R #i #tjP #tjR #Hind1 #Hind2 #G1 #D #A #j (cases D) normalize
+    [#Heq #tjA @(weak … tjA) <Heq @weak //
+    |#A1 #L #Heq destruct #tjA 
+     cut (S (length ? L) = 1 + length ? L + 0) // #H >H
+     >lift_lift_up >lift_lift_up @(weak … i);
+      [<plus_n_O @Hind1 // |@Hind2 // ]
+    ]
+  |#G #P #Q #i #j #k #Ax #tjP #tjQ #Hind1 #Hind2
+   #G1 #D #A #l #Heq #tjA normalize @(prod … Ax);
+    [/2/
+    |(cut (S (length T D) = (length T D)+1)) [//] 
+     #Heq1 <Heq1 @(Hind2 ? (P::D)) normalize //
+    ]
+  |#G #P #Q #R #S #tjP #tjS #Hind1 #Hind2
+   #G1 #D #A #l #Heq #tjA (normalize in Hind1 ⊢ %)
+   >(lift_subst_up R S 1 0 (length ? D)) @(app … (lift Q (length ? D) 1));
+    [@Hind1 // |@Hind2 //]
+  |#G #P #Q #R #i #tjR #tjProd #Hind1 #Hind2
+   #G1 #D #A #l #Heq #tjA normalize @(abs … i); 
+    [cut (∀n. S n = n +1); [//] #H <H 
+     @(Hind1 G1 (P::D) … tjA) normalize //
+    |(normalize in Hind2) @(Hind2 …tjA) //
+    ]
+  |#G #P #Q #R #i #convQR #tjP #tjQ #Hind1 #Hind2
+   #G1 #D #A #l #Heq #tjA
+   @(conv … (conv_lift … convQR) ? (Hind2 …)) // @Hind1 //
+  |#G #P #Q #i #tjP #tjQ #Hind1 #Hind2
+   #G1 #D #A #l #Heq #tjA @dummy /2/ 
+  ]
+qed.
+
+lemma weak_in: ∀P,G,A,B,M,N, i.
+ A::G  ⊢_{P} M : N → G ⊢_{P} B : Sort i → 
+   (lift A 0 1)::B::G ⊢_{P}  lift M 1 1 : lift N 1 1.
+#P #G #A #B #M #N #i #tjM #tjB 
+cut (∀A.(lift A 0 1)::B::G = (liftl (A::(nil ?)) 1)@(B::G)) // #H >H 
+@(weak_gen … tjM … tjB) //
+qed.
diff --git a/matita/matita/lib/lambdaN/types.ma b/matita/matita/lib/lambdaN/types.ma
index 0c07d2e70..7b4417232 100644
--- a/matita/matita/lib/lambdaN/types.ma
+++ b/matita/matita/lib/lambdaN/types.ma
@@ -9,7 +9,7 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/subst.ma".
+include "lambdaN/subst.ma".
 include "basics/list.ma".
 
 
@@ -64,7 +64,7 @@ inductive TJ (p: pts): list T → T → T → Prop ≝
   | conv: ∀G.∀A,B,C.∀i. Co p B C →
      TJ p G A B → TJ p G C (Sort i) → TJ p G A C
   | dummy: ∀G.∀A,B.∀i. 
-     TJ p G A B → TJ p G B (Sort i) → TJ p G (D A) B.
+     TJ p G A B → TJ p G B (Sort i) → TJ p G (D A B) B.
      
 interpretation "generic type judgement" 'TJT P G A B = (TJ P G A B).
 
@@ -133,7 +133,7 @@ Glegal P G → ∀n. n < |G| → G ⊢_{P} Rel n: lift (nth n T G (Rel O)) 0 (S
   |#G #A #B #C #i #tjAB #tjC #Hind1 #_ #m (cases m)
      /2/ #p #Hle @start_rel // @Hind1 @le_S_S_to_le @Hle
   ]
-qed.
+qed. 
 
 axiom conv_subst: ∀T,P,Q,N,i.Co T P Q → Co T P[i := N] Q[i := N].