helm/software/matita/nlibrary/PTS/gpts.ma

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