matita/matita/lib/lambda/types.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "lambda/subst.ma".
  13 include "basics/list.ma".
  14
  15
  16 (*************************** substl *****************************)
  17
  18 let rec substl (G:list T) (N:T) : list T ≝
  19   match G with
  20     [ nil ⇒ nil T
  21     | cons A D ⇒ ((subst A (length T D) N)::(substl D N))
  22     ].
  23
  24 (*
  25 nlemma substl_cons: ∀A,N.∀G.
  26 substl (A::G) N = (subst_aux A (length T G) N)::(substl G N).
  27 //; nqed.
  28 *)
  29
  30 (*start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 0 1)
  31   |
  32 nlemma length_cons: ∀A.∀G. length T (A::G) = length T G + 1.
  33 /2/; nqed.*)
  34
  35 (****************************************************************)
  36
  37 (*
  38 axiom A: nat → nat → Prop.
  39 axiom R: nat → nat → nat → Prop.
  40 axiom conv: T → T → Prop.*)
  41
  42 inductive TJ
  43  (S: nat → nat → Prop)
  44  (R: nat → nat → nat → Prop)
  45  (c: T → T → Prop) : list T → T → T → Prop ≝
  46   | ax : ∀i,j. S i j → TJ S R c (nil T) (Sort i) (Sort j)
  47   | start: ∀G.∀A.∀i.TJ S R c G A (Sort i) →
  48       TJ S R c (A::G) (Rel 0) (lift A 0 1)
  49   | weak: ∀G.∀A,B,C.∀i.
  50      TJ S R c G A B → TJ S R c G C (Sort i) →
  51        TJ S R c (C::G) (lift A 0 1) (lift B 0 1)
  52   | prod: ∀G.∀A,B.∀i,j,k. R i j k →
  53      TJ S R c G A (Sort i) → TJ S R c (A::G) B (Sort j) →
  54        TJ S R c G (Prod A B) (Sort k)
  55   | app: ∀G.∀F,A,B,a.
  56      TJ S R c G F (Prod A B) → TJ S R c G a A →
  57        TJ S R c G (App F a) (subst B 0 a)
  58   | abs: ∀G.∀A,B,b.∀i.
  59      TJ S R c (A::G) b B → TJ S R c G (Prod A B) (Sort i) →
  60        TJ S R c G (Lambda A b) (Prod A B)
  61   | conv: ∀G.∀A,B,C.∀i. c B C →
  62      TJ S R c G A B → TJ S R c G C (Sort i) → TJ S R c G A C
  63   | dummy: ∀G.∀A,B.∀i.
  64      TJ S R c G A B → TJ S R c G B (Sort i) → TJ S R c G (D A) B.
  65
  66 interpretation "type judgement" 'TJ G A B = (TJ ? ? ? G A B).
  67
  68 record pts : Type[0] ≝ {
  69   s1: nat → nat → Prop;
  70   r1: nat → nat → nat → Prop;
  71   c1: T → T → Prop
  72   }.
  73
  74 check r1.
  75 definition TJ ≝ λp:pts.c p.
  76
  77 (* ninverter TJ_inv2 for TJ (%?%) : Prop. *)
  78
  79 (**** definitions ****)
  80
  81 inductive Glegal (G: list T) : Prop ≝
  82 glegalk : ∀A,B. G ⊢ A : B → Glegal G.
  83
  84 inductive Gterm (G: list T) (A:T) : Prop ≝
  85   | is_term: ∀B.G ⊢ A:B → Gterm G A
  86   | is_type: ∀B.G ⊢ B:A → Gterm G A.
  87
  88 inductive Gtype (G: list T) (A:T) : Prop ≝
  89 gtypek: ∀i.G ⊢ A : Sort i → Gtype G A.
  90
  91 inductive Gelement (G:list T) (A:T) : Prop ≝
  92 gelementk: ∀B.G ⊢ A:B → Gtype G B → Gelement G A.
  93
  94 inductive Tlegal (A:T) : Prop ≝
  95 tlegalk: ∀G. Gterm G A → Tlegal A.
  96
  97 (*
  98 ndefinition Glegal ≝ λG: list T.∃A,B:T.TJ G A B .
  99
 100 ndefinition Gterm ≝ λG: list T.λA.∃B.TJ G A B ∨ TJ G B A.
 101
 102 ndefinition Gtype ≝ λG: list T.λA.∃i.TJ G A (Sort i).
 103
 104 ndefinition Gelement ≝ λG: list T.λA.∃B.TJ G A B ∨ Gtype G B.
 105
 106 ndefinition Tlegal ≝ λA:T.∃G: list T.Gterm G A.
 107 *)
 108
 109 (*
 110 ntheorem free_var1: ∀G.∀A,B,C. TJ G A B →
 111 subst C A
 112 #G; #i; #j; #axij; #Gleg; ncases Gleg;
 113 #A; #B; #tjAB; nelim tjAB; /2/; (* bello *) nqed.
 114 *)
 115
 116 theorem start_lemma1: ∀G.∀i,j.
 117 A i j → Glegal G → G ⊢ Sort i: Sort j.
 118 #G #i #j #axij #Gleg (cases Gleg)
 119 #A #B #tjAB (elim tjAB) /2/
 120 (* bello *) qed.
 121
 122 theorem start_rel: ∀G.∀A.∀C.∀n,i,q.
 123 G ⊢ C: Sort q → G ⊢ Rel n: lift A 0 i → (C::G) ⊢ Rel (S n): lift A 0 (S i).
 124 #G #A #C #n #i #p #tjC #tjn
 125  (applyS (weak G (Rel n))) //. (* bello *)
 126  (*
 127  nrewrite > (plus_n_O i);
 128  nrewrite > (plus_n_Sm i O);
 129  nrewrite < (lift_lift A 1 i);
 130  nrewrite > (plus_n_O n);  nrewrite > (plus_n_Sm n O);
 131  applyS (weak G (Rel n) (lift A i) C p tjn tjC). *)
 132 qed.
 133
 134 theorem start_lemma2: ∀G.
 135 Glegal G → ∀n. n < |G| → G ⊢ Rel n: lift (nth n T G (Rel O)) 0 (S n).
 136 #G #Gleg (cases Gleg) #A #B #tjAB (elim tjAB) /2/
 137   [#i #j #axij #p normalize #abs @(False_ind) @(absurd … abs) //
 138   |#G #A #i #tjA #Hind #m (cases m) /2/
 139    #p #Hle @start_rel // @Hind @le_S_S_to_le @Hle
 140   |#G #A #B #C #i #tjAB #tjC #Hind1 #_ #m (cases m)
 141      /2/ #p #Hle @start_rel // @Hind1 @le_S_S_to_le @Hle
 142   ]
 143 qed.
 144
 145 (*
 146 nlet rec TJm G D on D : Prop ≝
 147   match D with
 148     [ nil ⇒ True
 149     | cons A D1 ⇒ TJ G (Rel 0) A ∧ TJm G D1
 150     ].
 151
 152 nlemma tjm1: ∀G,D.∀A. TJm G (A::D) → TJ G (Rel 0) A.
 153 #G; #D; #A; *; //; nqed.
 154
 155 ntheorem transitivity_tj: ∀D.∀A,B. TJ D A B →
 156   ∀G. Glegal G → TJm G D → TJ G A B.
 157 #D; #A; #B; #tjAB; nelim tjAB;
 158   ##[/2/;
 159   ##|/2/;
 160   ##|#E; #T; #T0; #T1; #n; #tjT; #tjT1; #H; #H1; #G; #HlegG;
 161      #tjGcons;
 162      napply weak;
 163 *)
 164 (*
 165 ntheorem substitution_tj:
 166 ∀G.∀A,B,N,M.TJ (A::G) M B → TJ G N A →
 167   TJ G (subst N M) (subst N B).
 168 #G;#A;#B;#N;#M;#tjM;
 169   napply (TJ_inv2 (A::G) M B);
 170   ##[nnormalize; /3/;
 171   ##|#G; #A; #N; #tjA; #Hind; #Heq;
 172      ndestruct;//;
 173   ##|#G; #A; #B; #C; #n; #tjA; #tjC; #Hind1; #Hind2; #Heq;
 174      ndestruct;//;
 175   ##|nnormalize; #E; #A; #B; #i; #j; #k;
 176      #Ax; #tjA; #tjB; #Hind1; #_;
 177      #Heq; #HeqB; #tjN; napply (prod ?????? Ax);
 178       ##[/2/;
 179       ##|nnormalize; napplyS weak;
 180
 181 *)
 182
 183
 184 axiom conv_subst: ∀P,Q,N,i.conv P Q → conv P[i := N] Q[i := N].
 185
 186 theorem substitution_tj:
 187 ∀E.∀A,B,M. E ⊢M:B → ∀G,D.∀N. E = D@A::G → G ⊢ N:A →
 188   ((substl D N)@G) ⊢ M[|D| := N]: B[|D| := N].
 189 #E #A #B #M #tjMB (elim tjMB)
 190   [normalize #i #j #k #G #D #N (cases D)
 191     [normalize #isnil destruct
 192     |#P #L normalize #isnil destruct
 193     ]
 194   |#G #A1 #i #tjA #Hind #G1 #D (cases D)
 195     [#N #Heq #tjN >(delift (lift N O O) A1 O O O ??) //
 196      (normalize in Heq) destruct /2/
 197     |#H #L #N1 #Heq (normalize in Heq)
 198      #tjN1 normalize destruct; (applyS start) /2/
 199     ]
 200   |#G #P #Q #R #i #tjP #tjR #Hind1 #Hind2 #G1 #D #N
 201    (cases D) normalize
 202     [#Heq destruct #tjN //
 203     |#H #L #Heq #tjN1 destruct;
 204        (* napplyS weak non va *)
 205      (cut (S (length T L) = (length T L)+0+1)) [//]
 206      #Hee (applyS weak) /2/
 207     ]
 208   |#G #P #Q #i #j #k #Ax #tjP #tjQ #Hind1 #Hind2
 209    #G1 #D #N #Heq #tjN normalize @(prod … Ax);
 210     [/2/
 211     |(cut (S (length T D) = (length T D)+1)) [//]
 212      #Heq1 <Heq1 @(Hind2 ? (P::D)) normalize //
 213     ]
 214   |#G #P #Q #R #S #tjP #tjS #Hind1 #Hind2
 215    #G1 #D #N #Heq #tjN (normalize in Hind1 ⊢ %)
 216    >(plus_n_O (length ? D)) in ⊢ (? ? ? (? ? % ?))
 217    >(subst_lemma R S N ? 0) (applyS app) /2/
 218   |#G #P #Q #R #i #tjR #tjProd #Hind1 #Hind2
 219    #G1 #D #N #Heq #tjN normalize
 220    (applyS abs)
 221     [normalize in Hind2 /2/
 222     |(* napplyS (Hind1 G1 (P::D) N ? tjN); sistemare *)
 223      generalize in match (Hind1 G1 (P::D) N ? tjN);
 224       [#H (normalize in H) (applyS H) | normalize // ]
 225     ]
 226   |#G #P #Q #R #i #convQR #tjP #tjQ #Hind1 #Hind2
 227    #G1 #D #N #Heq #tjN
 228    @(conv …(conv_subst … convQR) ? (Hind2 …)) // @Hind1 //
 229   |#G #P #Q #i #tjP #tjQ #Hind1 #Hind2
 230    #G1 #D #N #Heq #tjN @dummy /2/
 231   ]
 232 qed.
 233
 234 lemma tj_subst_0: ∀G,v,w. G ⊢ v : w → ∀t,u. w :: G ⊢ t : u →
 235                   G ⊢ t[0≝v] : u[0≝v].
 236 #G #v #w #Hv #t #u #Ht
 237 lapply (substitution_tj … Ht ? ([]) … Hv) normalize //
 238 qed.