matita/matita/lib/pts_dummy/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 record pts : Type[0] ≝ {
  43   Ax: nat → nat → Prop;
  44   Re: nat → nat → nat → Prop;
  45   Co: T → T → Prop
  46   }.
  47
  48 inductive TJ (p: pts): list T → T → T → Prop ≝
  49   | ax : ∀i,j. Ax p i j → TJ p (nil T) (Sort i) (Sort j)
  50   | start: ∀G.∀A.∀i.TJ p G A (Sort i) →
  51       TJ p (A::G) (Rel 0) (lift A 0 1)
  52   | weak: ∀G.∀A,B,C.∀i.
  53      TJ p G A B → TJ p G C (Sort i) →
  54        TJ p (C::G) (lift A 0 1) (lift B 0 1)
  55   | prod: ∀G.∀A,B.∀i,j,k. Re p i j k →
  56      TJ p G A (Sort i) → TJ p (A::G) B (Sort j) →
  57        TJ p G (Prod A B) (Sort k)
  58   | app: ∀G.∀F,A,B,a.
  59      TJ p G F (Prod A B) → TJ p G a A →
  60        TJ p G (App F a) (subst B 0 a)
  61   | abs: ∀G.∀A,B,b.∀i.
  62      TJ p (A::G) b B → TJ p G (Prod A B) (Sort i) →
  63        TJ p G (Lambda A b) (Prod A B)
  64   | conv: ∀G.∀A,B,C.∀i. Co p B C →
  65      TJ p G A B → TJ p G C (Sort i) → TJ p G A C
  66   | dummy: ∀G.∀A,B.∀i.
  67      TJ p G A B → TJ p G B (Sort i) → TJ p G (D A) B.
  68
  69 interpretation "generic type judgement" 'TJT P G A B = (TJ P G A B).
  70
  71 notation "hvbox( G break  ⊢ _{P} A break : B)"
  72    non associative with precedence 45
  73    for @{'TJT $P $G $A $B}.
  74
  75 (* ninverter TJ_inv2 for TJ (%?%) : Prop. *)
  76
  77 (**** definitions ****)
  78
  79 inductive Glegal (P:pts) (G: list T) : Prop ≝
  80 glegalk : ∀A,B. G ⊢_{P} A : B → Glegal P G.
  81
  82 inductive Gterm (P:pts) (G: list T) (A:T) : Prop ≝
  83   | is_term: ∀B.G ⊢_{P} A:B → Gterm P G A
  84   | is_type: ∀B.G ⊢_{P} B:A → Gterm P G A.
  85
  86 inductive Gtype (P:pts) (G: list T) (A:T) : Prop ≝
  87 gtypek: ∀i.G ⊢_{P} A : Sort i → Gtype P G A.
  88
  89 inductive Gelement (P:pts) (G:list T) (A:T) : Prop ≝
  90 gelementk: ∀B.G ⊢_{P} A:B → Gtype P G B → Gelement P G A.
  91
  92 inductive Tlegal (P:pts) (A:T) : Prop ≝
  93 tlegalk: ∀G. Gterm P G A → Tlegal P A.
  94
  95 (*
  96 ndefinition Glegal ≝ λG: list T.∃A,B:T.TJ G A B .
  97
  98 ndefinition Gterm ≝ λG: list T.λA.∃B.TJ G A B ∨ TJ G B A.
  99
 100 ndefinition Gtype ≝ λG: list T.λA.∃i.TJ G A (Sort i).
 101
 102 ndefinition Gelement ≝ λG: list T.λA.∃B.TJ G A B ∨ Gtype G B.
 103
 104 ndefinition Tlegal ≝ λA:T.∃G: list T.Gterm G A.
 105 *)
 106
 107 (*
 108 ntheorem free_var1: ∀G.∀A,B,C. TJ G A B →
 109 subst C A
 110 #G; #i; #j; #axij; #Gleg; ncases Gleg;
 111 #A; #B; #tjAB; nelim tjAB; /2/; (* bello *) nqed.
 112 *)
 113
 114 theorem start_lemma1: ∀P,G,i,j.
 115 Ax P i j → Glegal P G → G ⊢_{P} Sort i: Sort j.
 116 #P #G #i #j #axij #Gleg (cases Gleg)
 117 #A #B #tjAB (elim tjAB) /2/
 118 (* bello *) qed.
 119
 120 theorem start_rel: ∀P,G,A,C,n,i,q.
 121 G ⊢_{P} C: Sort q → G ⊢_{P} Rel n: lift A 0 i →
 122  C::G ⊢_{P} Rel (S n): lift A 0 (S i).
 123 #P #G #A #C #n #i #p #tjC #tjn
 124  (applyS (weak P G (Rel n))) //.
 125 qed.
 126
 127 theorem start_lemma2: ∀P,G.
 128 Glegal P G → ∀n. n < |G| → G ⊢_{P} Rel n: lift (nth n T G (Rel O)) 0 (S n).
 129 #P #G #Gleg (cases Gleg) #A #B #tjAB (elim tjAB) /2/
 130   [#i #j #axij #p normalize #abs @(False_ind) @(absurd … abs) //
 131   |#G #A #i #tjA #Hind #m (cases m) /2/
 132    #p #Hle @start_rel // @Hind @le_S_S_to_le @Hle
 133   |#G #A #B #C #i #tjAB #tjC #Hind1 #_ #m (cases m)
 134      /2/ #p #Hle @start_rel // @Hind1 @le_S_S_to_le @Hle
 135   ]
 136 qed.
 137
 138 axiom conv_subst: ∀T,P,Q,N,i.Co T P Q → Co T P[i := N] Q[i := N].
 139
 140 theorem substitution_tj:
 141 ∀P,E.∀A,B,M. E ⊢_{P} M:B → ∀G,D.∀N. E = D@A::G → G ⊢_{P} N:A →
 142   ((substl D N)@G) ⊢_{P} M[|D| := N]: B[|D| := N].
 143 #Pts #E #A #B #M #tjMB (elim tjMB)
 144   [normalize #i #j #k #G #D #N (cases D)
 145     [normalize #isnil destruct
 146     |#P #L normalize #isnil destruct
 147     ]
 148   |#G #A1 #i #tjA #Hind #G1 #D (cases D)
 149     [#N #Heq #tjN >(delift (lift N O O) A1 O O O ??) //
 150      (normalize in Heq) destruct /2/
 151     |#H #L #N1 #Heq (normalize in Heq)
 152      #tjN1 normalize destruct; (applyS start) /2/
 153     ]
 154   |#G #P #Q #R #i #tjP #tjR #Hind1 #Hind2 #G1 #D #N
 155    (cases D) normalize
 156     [#Heq destruct #tjN //
 157     |#H #L #Heq #tjN1 destruct;
 158        (* napplyS weak non va *)
 159      (cut (S (length T L) = (length T L)+0+1)) [//]
 160      #Hee (applyS weak) /2/
 161     ]
 162   |#G #P #Q #i #j #k #Ax #tjP #tjQ #Hind1 #Hind2
 163    #G1 #D #N #Heq #tjN normalize @(prod … Ax);
 164     [/2/
 165     |(cut (S (length T D) = (length T D)+1)) [//]
 166      #Heq1 <Heq1 @(Hind2 ? (P::D)) normalize //
 167     ]
 168   |#G #P #Q #R #S #tjP #tjS #Hind1 #Hind2
 169    #G1 #D #N #Heq #tjN (normalize in Hind1 ⊢ %)
 170    >(plus_n_O (length ? D)) in ⊢ (? ? ? ? (? ? % ?))
 171    >(subst_lemma R S N ? 0) (applyS app) /2/
 172   |#G #P #Q #R #i #tjR #tjProd #Hind1 #Hind2
 173    #G1 #D #N #Heq #tjN normalize
 174    (applyS abs)
 175     [normalize in Hind2 /2/
 176     |(* napplyS (Hind1 G1 (P::D) N ? tjN); sistemare *)
 177      generalize in match (Hind1 G1 (P::D) N ? tjN);
 178       [#H (normalize in H) (applyS H) | normalize // ]
 179     ]
 180   |#G #P #Q #R #i #convQR #tjP #tjQ #Hind1 #Hind2
 181    #G1 #D #N #Heq #tjN
 182    @(conv …(conv_subst … convQR) ? (Hind2 …)) // @Hind1 //
 183   |#G #P #Q #i #tjP #tjQ #Hind1 #Hind2
 184    #G1 #D #N #Heq #tjN @dummy /2/
 185   ]
 186 qed.
 187
 188 lemma tj_subst_0: ∀P,G,v,w. G ⊢_{P} v : w → ∀t,u. w :: G ⊢_{P} t : u →
 189                   G ⊢_{P} t[0≝v] : u[0≝v].
 190 #P #G #v #w #Hv #t #u #Ht
 191 lapply (substitution_tj … Ht ? ([]) … Hv) normalize //
 192 qed.