Partial modifications.

[helm.git] / matita / matita / lib / lambda / types.ma

diff --git a/matita/matita/lib/lambda/types.ma b/matita/matita/lib/lambda/types.ma
index 22abcfa3c29f430820c556546fb64b5b0c9f2ad0..d8ddb19239f1747b74df366bddcd75f973d22645 100644 (file)
--- a/matita/matita/lib/lambda/types.ma
+++ b/matita/matita/lib/lambda/types.ma
@@ -27,33 +27,52 @@ substl (A::G) N = (subst_aux A (length T G) N)::(substl G N).
 //; nqed.
 *)
 
-(*
+(*start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 0 1)
+  | 
 nlemma length_cons: ∀A.∀G. length T (A::G) = length T G + 1.
 /2/; nqed.*)
 
 (****************************************************************)
 
+(*
 axiom A: nat → nat → Prop.
 axiom R: nat → nat → nat → Prop.
-axiom conv: T → T → Prop.
-
-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)
+axiom conv: T → T → Prop.*)
+
+inductive TJ 
+ (S: nat → nat → Prop)
+ (R: nat → nat → nat → Prop)
+ (c: T → T → Prop) : list T → T → T → Prop ≝
+  | ax : ∀i,j. S i j → TJ S R c (nil T) (Sort i) (Sort j)
+  | start: ∀G.∀A.∀i.TJ S R c G A (Sort i) → 
+      TJ S R c (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)
+     TJ S R c G A B → TJ S R c G C (Sort i) → 
+       TJ S R c (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 S R c G A (Sort i) → TJ S R c (A::G) B (Sort j) → 
+       TJ S R c 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 S R c G F (Prod A B) → TJ S R c G a A → 
+       TJ S R c 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 B (Sort i) → TJ G A C
+     TJ S R c (A::G) b B → TJ S R c G (Prod A B) (Sort i) → 
+       TJ S R c G (Lambda A b) (Prod A B)
+  | conv: ∀G.∀A,B,C.∀i. c B C →
+     TJ S R c G A B → TJ S R c G C (Sort i) → TJ S R c G A C
   | dummy: ∀G.∀A,B.∀i. 
-     TJ G A B → TJ G B (Sort i) → TJ G (D A) B.
+     TJ S R c G A B → TJ S R c G B (Sort i) → TJ S R c G (D A) B.
      
-interpretation "type judgement" 'TJ G A B = (TJ G A B).
+interpretation "type judgement" 'TJ G A B = (TJ ? ? ? G A B).
+
+record pts : Type[0] ≝ {
+  s1: nat → nat → Prop;
+  r1: nat → nat → nat → Prop;
+  c1: T → T → Prop
+  }.
+
+check r1.
+definition TJ ≝ λp:pts.c p. 
 
 (* ninverter TJ_inv2 for TJ (%?%) : Prop. *)
 
@@ -115,7 +134,7 @@ qed.
 theorem start_lemma2: ∀G.
 Glegal G → ∀n. n < |G| → G ⊢ Rel n: lift (nth n T G (Rel O)) 0 (S n).
 #G #Gleg (cases Gleg) #A #B #tjAB (elim tjAB) /2/
-  [#i #j #axij #p normalize #abs @False_ind @(absurd … abs) // 
+  [#i #j #axij #p normalize #abs @(False_ind) @(absurd … abs) // 
   |#G #A #i #tjA #Hind #m (cases m) /2/
    #p #Hle @start_rel // @Hind @le_S_S_to_le @Hle
   |#G #A #B #C #i #tjAB #tjC #Hind1 #_ #m (cases m)
@@ -217,6 +236,3 @@ lemma tj_subst_0: ∀G,v,w. G ⊢ v : w → ∀t,u. w :: G ⊢ t : u →
 #G #v #w #Hv #t #u #Ht 
 lapply (substitution_tj … Ht ? ([]) … Hv) normalize //
 qed.
-
-(* weakening lemma: special case *)
-axiom tj_weak_1: ∀G,t,u. G ⊢ t : u → ∀w. w :: G ⊢ lift t 0 1 : lift u 0 1.