From 6a1a5110981fcb9bfe3aa36958ee118792f65796 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 19 May 2011 10:16:44 +0000
Subject: [PATCH 1/1] Porting to new parametric TJ.

---
 matita/matita/lib/lambda/inversion.ma | 59 +++++++++++++++------------
 1 file changed, 32 insertions(+), 27 deletions(-)

diff --git a/matita/matita/lib/lambda/inversion.ma b/matita/matita/lib/lambda/inversion.ma
index b25b315e3..0c2c2a98b 100644
--- a/matita/matita/lib/lambda/inversion.ma
+++ b/matita/matita/lib/lambda/inversion.ma
@@ -12,23 +12,27 @@
 include "lambda/types.ma".
 
 (*
-inductive TJ: list T → T → T → Prop ≝
-  | ax : ∀i,j. A i j → TJ (nil T) (Sort i) (Sort j)
-  | start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 0 1)
+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 G A B → TJ G C (Sort i) → TJ (C::G) (lift A 0 1) (lift B 0 1)
-  | prod: ∀G.∀A,B.∀i,j,k. R i j k →
-     TJ G A (Sort i) → TJ (A::G) B (Sort j) → TJ G (Prod A B) (Sort k)
+     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 G F (Prod A B) → TJ G a A → TJ G (App F a) (subst B 0 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 (A::G) b B → TJ G (Prod A B) (Sort i) → TJ G (Lambda A b) (Prod A B)
-  | conv: ∀G.∀A,B,C.∀i. conv B C →
-     TJ G A B → TJ G C (Sort i) → TJ G A C
+     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 G A B → TJ G B (Sort i) → TJ G (D A) B.
-     axiom prod_inv : ∀G,M,P,Q. G ⊢ M : Prod P Q →
- ∃i. P::G ⊢ Q : Sort i. *)
+     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.
@@ -36,18 +40,19 @@ axiom lambda_lift : ∀A,B,C. lift A 0 1 = Lambda B 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: ∀M,N. conv M N → conv (lift M 0 1) (lift N 0 1).
+axiom conv_lift: ∀P,M,N. Co P M N → Co P (lift M 0 1) (lift N 0 1).
  
-axiom weak_in: ∀G.∀A,B,M,N.∀i.A::G  ⊢ M : N → G ⊢ B : Sort i → 
- (lift A 0 1)::B::G ⊢  lift M 1 1 : lift N 1 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: ∀A. conv A A.
-axiom  sym_conv: ∀A,B. conv A B → conv B A.
-axiom trans_conv: ∀A,B,C. conv A B → conv B C → conv A C.
+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.
 
-theorem prod_inv: ∀G,M,N. G ⊢ M : N → ∀A,B.M = Prod A B → 
-  ∃i,j,k. conv N (Sort k) ∧ G ⊢A : Sort i ∧ A::G ⊢B : Sort j. 
-#G #M #N #t (elim t);
+theorem prod_inv: ∀P,G,M,N. G ⊢_{P} M : N → ∀A,B.M = Prod A B → 
+  ∃i,j,k. Co P N (Sort k) ∧ G ⊢_{P} A : Sort i ∧ A::G ⊢_{P} B : Sort j. 
+#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
@@ -64,14 +69,14 @@ theorem prod_inv: ∀G,M,N. G ⊢ M : N → ∀A,B.M = Prod A B →
   |#G1 #A #B #C #i #cBC #t1 #t2 #H1 #H2 #A1 #B1 #eqA
    cases (H1 … eqA) #i * #j * #k * * #c1 #t3 #t4
    @(ex_intro … i) @(ex_intro … j) @(ex_intro … k) % //
-   % // @(trans_conv C B … c1) @sym_conv //
+   % // @(trans_conv Pts C B … c1) @sym_conv //
   |#G1 #A #B #i #t1 #t2 #_ #_ #A1 #B1 #eqA destruct
   ]
 qed.
 
-theorem abs_inv: ∀G,M,N. G ⊢ M : N → ∀A,b.M = Lambda A b → 
-  ∃i,B. conv N (Prod A B) ∧ G ⊢Prod A B: Sort i ∧ A::G ⊢b : B. 
-#G #M #N #t (elim t);
+theorem abs_inv: ∀P,G,M,N. G ⊢ _{P} M : N → ∀A,b.M = Lambda A b → 
+  ∃i,B. Co P N (Prod A B) ∧ G ⊢_{P} Prod A B: Sort i ∧ A::G ⊢_{P} b : 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
@@ -88,7 +93,7 @@ theorem abs_inv: ∀G,M,N. G ⊢ M : N → ∀A,b.M = Lambda A b →
   |#G1 #A #B #C #i #cBC #t1 #t2 #H1 #H2 #A1 #b #eqA
    cases (H1 … eqA) #i * #B1 * * #c1 #t3 #t4
    @(ex_intro … i) @(ex_intro … B1) % //
-   % // @(trans_conv C B … c1) @sym_conv //
+   % // @(trans_conv Pts C B … c1) @sym_conv //
   |#G1 #A #B #i #t1 #t2 #_ #_ #A1 #b #eqA destruct
   ]
 qed.
-- 
2.39.2