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 A (length T D) N)::(substl D N))
  23     ].
  24
  25 (*
  26 nlemma substl_cons: ∀A,N.∀G.
  27 substl (A::G) N = (subst_aux A (length T G) N)::(substl G N).
  28 //; nqed.
  29 *)
  30
  31 (*
  32 nlemma length_cons: ∀A.∀G. length T (A::G) = length T G + 1.
  33 /2/; nqed.*)
  34
  35 (****************************************************************)
  36
  37 naxiom A: nat → nat → Prop.
  38 naxiom R: nat → nat → nat → Prop.
  39 naxiom conv: T → T → Prop.
  40
  41 ninductive TJ: list T → T → T → Prop ≝
  42   | ax : ∀i,j. A i j → TJ (nil T) (Sort i) (Sort j)
  43   | start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 0 1)
  44   | weak: ∀G.∀A,B,C.∀i.
  45      TJ G A B → TJ G C (Sort i) → TJ (C::G) (lift A 0 1) (lift B 0 1)
  46   | prod: ∀G.∀A,B.∀i,j,k. R i j k →
  47      TJ G A (Sort i) → TJ (A::G) B (Sort j) → TJ G (Prod A B) (Sort k)
  48   | app: ∀G.∀F,A,B,a.
  49      TJ G F (Prod A B) → TJ G a A → TJ G (App F a) (subst B 0 a)
  50   | abs: ∀G.∀A,B,b.∀i.
  51      TJ (A::G) b B → TJ G (Prod A B) (Sort i) → TJ G (Lambda A b) (Prod A B)
  52   | conv: ∀G.∀A,B,C.∀i. conv B C →
  53      TJ G A B → TJ G B (Sort i) → TJ G A C.
  54
  55 notation "hvbox(G break  ⊢ A : B)" non associative with precedence 50 for @{'TJ $G $A $B}.
  56 interpretation "type judgement" 'TJ G A B = (TJ G A B).
  57
  58 (* ninverter TJ_inv2 for TJ (%?%) : Prop. *)
  59
  60 (**** definitions ****)
  61
  62 ninductive Glegal (G: list T) : Prop ≝
  63 glegalk : ∀A,B. G ⊢ A : B → Glegal G.
  64
  65 ninductive Gterm (G: list T) (A:T) : Prop ≝
  66   | is_term: ∀B.G ⊢ A:B → Gterm G A
  67   | is_type: ∀B.G ⊢ B:A → Gterm G A.
  68
  69 ninductive Gtype (G: list T) (A:T) : Prop ≝
  70 gtypek: ∀i.G ⊢ A : Sort i → Gtype G A.
  71
  72 ninductive Gelement (G:list T) (A:T) : Prop ≝
  73 gelementk: ∀B.G ⊢ A:B → Gtype G B → Gelement G A.
  74
  75 ninductive Tlegal (A:T) : Prop ≝
  76 tlegalk: ∀G. Gterm G A → Tlegal A.
  77
  78 (*
  79 ndefinition Glegal ≝ λG: list T.∃A,B:T.TJ G A B .
  80
  81 ndefinition Gterm ≝ λG: list T.λA.∃B.TJ G A B ∨ TJ G B A.
  82
  83 ndefinition Gtype ≝ λG: list T.λA.∃i.TJ G A (Sort i).
  84
  85 ndefinition Gelement ≝ λG: list T.λA.∃B.TJ G A B ∨ Gtype G B.
  86
  87 ndefinition Tlegal ≝ λA:T.∃G: list T.Gterm G A.
  88 *)
  89
  90 (*
  91 ntheorem free_var1: ∀G.∀A,B,C. TJ G A B →
  92 subst C A
  93 #G; #i; #j; #axij; #Gleg; ncases Gleg;
  94 #A; #B; #tjAB; nelim tjAB; /2/; (* bello *) nqed.
  95 *)
  96
  97 ntheorem start_lemma1: ∀G.∀i,j.
  98 A i j → Glegal G → G ⊢ Sort i: Sort j.
  99 #G; #i; #j; #axij; #Gleg; ncases Gleg;
 100 #A; #B; #tjAB; nelim tjAB; /2/;
 101 (* bello *) nqed.
 102
 103 ntheorem start_rel: ∀G.∀A.∀C.∀n,i,q.
 104 G ⊢ C: Sort q → G ⊢ Rel n: lift A 0 i → (C::G) ⊢ Rel (S n): lift A 0 (S i).
 105 #G; #A; #C; #n; #i; #p; #tjC; #tjn;
 106  napplyS (weak G (Rel n));//. (* bello *)
 107  (*
 108  nrewrite > (plus_n_O i);
 109  nrewrite > (plus_n_Sm i O);
 110  nrewrite < (lift_lift A 1 i);
 111  nrewrite > (plus_n_O n);  nrewrite > (plus_n_Sm n O);
 112  applyS (weak G (Rel n) (lift A i) C p tjn tjC). *)
 113 nqed.
 114
 115 ntheorem start_lemma2: ∀G.
 116 Glegal G → ∀n. n < |G| → G ⊢ Rel n: lift (nth n T G (Rel O)) 0 (S n).
 117 #G; #Gleg; ncases Gleg; #A; #B; #tjAB; nelim tjAB; /2/;
 118   ##[#i; #j; #axij; #p; nnormalize; #abs; napply False_ind;
 119      napply (absurd … abs); //;
 120   ##|#G; #A; #i; #tjA; #Hind; #m; ncases m; /2/;
 121      #p; #Hle; napply start_rel; //; napply Hind;
 122      napply le_S_S_to_le; napply Hle;
 123   ##|#G; #A; #B; #C; #i; #tjAB; #tjC; #Hind1; #_; #m; ncases m;
 124      /2/; #p; #Hle; napply start_rel; //;
 125      napply Hind1; napply le_S_S_to_le; napply Hle;
 126   ##]
 127 nqed.
 128
 129 (*
 130 nlet rec TJm G D on D : Prop ≝
 131   match D with
 132     [ nil ⇒ True
 133     | cons A D1 ⇒ TJ G (Rel 0) A ∧ TJm G D1
 134     ].
 135
 136 nlemma tjm1: ∀G,D.∀A. TJm G (A::D) → TJ G (Rel 0) A.
 137 #G; #D; #A; *; //; nqed.
 138
 139 ntheorem transitivity_tj: ∀D.∀A,B. TJ D A B →
 140   ∀G. Glegal G → TJm G D → TJ G A B.
 141 #D; #A; #B; #tjAB; nelim tjAB;
 142   ##[/2/;
 143   ##|/2/;
 144   ##|#E; #T; #T0; #T1; #n; #tjT; #tjT1; #H; #H1; #G; #HlegG;
 145      #tjGcons;
 146      napply weak;
 147 *)
 148 (*
 149 ntheorem substitution_tj:
 150 ∀G.∀A,B,N,M.TJ (A::G) M B → TJ G N A →
 151   TJ G (subst N M) (subst N B).
 152 #G;#A;#B;#N;#M;#tjM;
 153   napply (TJ_inv2 (A::G) M B);
 154   ##[nnormalize; /3/;
 155   ##|#G; #A; #N; #tjA; #Hind; #Heq;
 156      ndestruct;//;
 157   ##|#G; #A; #B; #C; #n; #tjA; #tjC; #Hind1; #Hind2; #Heq;
 158      ndestruct;//;
 159   ##|nnormalize; #E; #A; #B; #i; #j; #k;
 160      #Ax; #tjA; #tjB; #Hind1; #_;
 161      #Heq; #HeqB; #tjN; napply (prod ?????? Ax);
 162       ##[/2/;
 163       ##|nnormalize; napplyS weak;
 164
 165 *)
 166
 167 ntheorem substitution_tj:
 168 ∀E.∀A,B,M. E ⊢M:B → ∀G,D.∀N. E = D@A::G → G ⊢ N:A →
 169   ((substl D N)@G) ⊢ M[|D| ← N]: B[|D| ← N].
 170 #E; #A; #B; #M; #tjMB; nelim tjMB;
 171   ##[nnormalize; #i; #j; #k; #G; #D; #N; ncases D;
 172       ##[nnormalize; #isnil; ndestruct;
 173       ##|#P; #L; nnormalize; #isnil; ndestruct;
 174       ##]
 175   ##|#G; #A1; #i; #tjA; #Hind; #G1; #D; ncases D;
 176     ##[#N; #Heq; #tjN;
 177        nrewrite > (delift (lift N O O) A1 O O O ??); //;
 178        nnormalize in Heq; ndestruct;/2/;
 179     ##|#H; #L; #N1; #Heq; nnormalize in Heq;
 180        #tjN1; nnormalize; ndestruct;
 181     ncheck( let clause_829:
 182  ∀x1947: ?.
 183   ∀x1948: ?.
 184    ∀x1949: ?.
 185     ∀x1950: ?.
 186      ∀x1951: ?.
 187       eq T (lift (subst x1947 (plus x1948 x1949) x1950) x1949 x1951)
 188         (subst (lift x1947 x1949 x1951) (plus x1948 (plus x1949 x1951))
 189           x1950)
 190  ≝ λx1947:?.
 191       λx1948:?.
 192        λx1949:?.
 193         λx1950:?.
 194          λx1951:?.
 195           rewrite_l nat (plus (plus x1948 x1949) x1951)
 196             (λx:nat.
 197               eq T (lift (subst x1947 (plus x1948 x1949) x1950) x1949 x1951)
 198                 (subst (lift x1947 x1949 x1951) x x1950))
 199             (lift_subst_ijk x1950 x1947 x1951 x1948 x1949)
 200             (plus x1948 (plus x1949 x1951))
 201             (associative_plus x1948 x1949 x1951) in
 202  let clause_60: ∀x156: ?. eq nat (S x156) (plus x156 (S O))
 203   ≝ λx156:?.
 204        rewrite_r nat (plus x156 O) (λx:nat. eq nat (S x) (plus x156 (S O)))
 205          (plus_n_Sm x156 O) x156 (plus_n_O x156) in
 206   let clause_996 :
 207    eq Type
 208      (TJ (cons T (subst ? ? ?) ?) (Rel O)
 209        (subst (lift ? O (S O)) (plus ? (S O)) ?))
 210      (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
 211        (Rel O) (subst (lift H O (S O)) (S (length T L)) N1))
 212    ≝ rewrite_l nat (S (length T L))
 213          (λx:nat.
 214            eq Type
 215              (TJ
 216                (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
 217                (Rel O) (subst (lift H O (S O)) x N1))
 218              (TJ
 219                (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
 220                (Rel O) (subst (lift H O (S O)) (S (length T L)) N1)))
 221          (refl Type
 222            (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
 223              (Rel O) (subst (lift H O (S O)) (S (length T L)) N1)))
 224          (plus (length T L) (S O)) (clause_60 (length T L)) in
 225    let clause_995:
 226     eq Type
 227       (TJ (cons T (subst ? ? ?) ?) (Rel O)
 228         (subst (lift ? O (S O)) (plus ? (plus O (S O))) ?))
 229       (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
 230         (Rel O) (subst (lift H O (S O)) (S (length T L)) N1))
 231     ≝ rewrite_l nat (S O)
 232           (λx:nat.
 233             eq Type
 234               (TJ (cons T (subst ? ? ?) ?) (Rel O)
 235                 (subst (lift ? O (S O)) (plus ? x) ?))
 236               (TJ
 237                 (cons T (subst H (length T L) N1)
 238                   (append T (substl L N1) G1)) (Rel O)
 239                 (subst (lift H O (S O)) (S (length T L)) N1))) clause_996
 240           (plus O (S O)) (plus_O_n (S O)) in
 241     rewrite_r T
 242       (subst (lift ? O (S O)) (plus ? (plus O (S O))) ?)
 243       (λx:T.
 244         eq Type
 245           (TJ (cons T (subst ? (plus ? O) ?) ?) (Rel O) x)
 246           (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
 247             (Rel O) (subst (lift H O (S O)) (S (length T L)) N1)))
 248       (rewrite_l nat ?
 249         (λx:nat.
 250           eq Type
 251             (TJ (cons T (subst ? x ?) ?) (Rel O)
 252               (subst (lift ? O (S O)) (plus ? (plus O (S O))) ?))
 253             (TJ
 254               (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
 255               (Rel O) (subst (lift H O (S O)) (S (length T L)) N1)))
 256         clause_995 (plus ? O) (plus_n_O ?))
 257       (lift (subst ? (plus ? O) ?) O (S O))
 258       (clause_829 ? ? O ? (S O))
 259 ).
 260        napplyS start;
 261        (* napplyS start; *)
 262        (* napplyS start non va *)
 263        ncut (S (length T L) = ((length T L)+0+1)); ##[//##] #Heq;
 264        ncheck start.
 265        napplyS start;/2/;
 266     ##]
 267   ##|#G; #P; #Q; #R; #i; #tjP; #tjR; #Hind1; #Hind2;
 268      #G1; #D; #N; ncases D; nnormalize;
 269     ##[#Heq; ndestruct; #tjN; //;
 270     ##|#H; #L; #Heq;
 271        #tjN1; ndestruct;
 272        (* napplyS weak non va *)
 273        ncut (S (length T L) = (length T L)+0+1); ##[//##] #Heq;
 274        napplyS weak; /2/;
 275     ##]
 276   ##|#G; #P; #Q; #i; #j; #k; #Ax; #tjP; #tjQ; #Hind1; #Hind2;
 277      #G1; #D; #N; #Heq; #tjN; nnormalize;
 278      napply (prod … Ax);
 279     ##[/2/;
 280     ##|ncut (S (length T D) = (length T D)+1); ##[//##] #Heq1;
 281        nrewrite < Heq1;
 282        napply (Hind2 ? (P::D));//;
 283     ##]
 284   ##|#G; #P; #Q; #R; #S; #tjP; #tjS; #Hind1; #Hind2;
 285      #G1; #D; #N; #Heq; #tjN; nnormalize;
 286      ncheck (
 287              (subst (subst_aux  S (length T  D)  N)
 288                (subst_aux  R (length T  D)  N))
 289       ).
 290      napplyS (app (substl D N@G1) (subst_aux P (length T D) N) A (subst_aux R (length T D) N) (subst_aux S (length T D) N) ?).
 291      nlapply (subst_lemma R S N (length ? D) 0); #sl;
 292      nrewrite < (plus_n_O ?) in sl; #sl;
 293      nrewrite > sl;
 294      nauto demod;
 295      napply app; nnormalize in Hind1;/2/;
 296   ##|
 297
 298
 299
 300
 301
 302
 303