matita/matita/lib/finite_lambda/terms_and_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 "basics/finset.ma".
  13 include "basics/star.ma".
  14
  15
  16 inductive FType (O:Type[0]): Type[0] ≝
  17   | atom : O → FType O
  18   | arrow : FType O → FType O → FType O.
  19
  20 inductive T (O:Type[0]) (D:O → FinSet): Type[0] ≝
  21   | Val: ∀o:O.carr (D o) → T O D        (* a value in a finset *)
  22   | Rel: nat → T O D                    (* DB index, base is 0 *)
  23   | App: T O D → T O D → T O D          (* function, argument *)
  24   | Lambda: FType O → T O D → T O D     (* type, body *)
  25   | Vec: FType O → list (T O D) → T O D (* type, body *)
  26 .
  27
  28 let rec FinSet_of_FType O (D:O→FinSet) (ty:FType O) on ty : FinSet ≝
  29   match ty with
  30   [atom o ⇒ D o
  31   |arrow ty1 ty2 ⇒ FinFun (FinSet_of_FType O D ty1) (FinSet_of_FType O D ty2)
  32   ].
  33
  34 (* size *)
  35
  36 let rec size O D (M:T O D) on M ≝
  37 match M with
  38   [Val o a ⇒ 1
  39   |Rel n ⇒ 1
  40   |App P Q ⇒ size O D P + size O D Q + 1
  41   |Lambda Ty P ⇒ size O D P + 1
  42   |Vec Ty v ⇒ foldr ?? (λx,a. size O D x + a) 0 v +1
  43   ]
  44 .
  45
  46 (* axiom pos_size: ∀M. 1 ≤ size M. *)
  47
  48 theorem Telim_size: ∀O,D.∀P: T O D → Prop.
  49  (∀M. (∀N. size O D N < size O D M → P N) → P M) → ∀M. P M.
  50 #O #D #P #H #M (cut (∀p,N. size O D N = p → P N))
  51   [2: /2/]
  52 #p @(nat_elim1 p) #m #H1 #N #sizeN @H #N0 #Hlt @(H1 (size O D N0)) //
  53 qed.
  54
  55 lemma T_elim:
  56   ∀O: Type[0].∀D:O→FinSet.∀P:T O D→Prop.
  57   (∀o:O.∀x:D o.P (Val O D o x)) →
  58   (∀n:ℕ.P(Rel O D n)) →
  59   (∀m,n:T O D.P m→P n→P (App O D m n)) →
  60   (∀Ty:FType O.∀m:T O D.P m→P(Lambda O D Ty m)) →
  61   (∀Ty:FType O.∀v:list (T O D).
  62      (∀x:T O D. mem ? x v → P x) → P(Vec O D Ty v)) →
  63   ∀x:T O D.P x.
  64 #O #D #P #Hval #Hrel #Happ #Hlam #Hvec @Telim_size #x cases x //
  65   [ (* app *) #m #n #Hind @Happ @Hind // /2 by le_minus_to_plus/
  66   | (* lam *) #ty #m #Hind @Hlam @Hind normalize //
  67   | (* vec *) #ty #v #Hind @Hvec #x lapply Hind elim v
  68     [#Hind normalize *
  69     |#hd #tl #Hind1 #Hind2 *
  70       [#Hx >Hx @Hind2 normalize //
  71       |@Hind1 #N #H @Hind2 @(lt_to_le_to_lt … H) normalize //
  72       ]
  73     ]
  74   ]
  75 qed.
  76
  77 (* since we only consider beta reduction with closed arguments we could avoid
  78 lifting. We define it for the sake of generality *)
  79
  80 (* arguments: k is the nesting depth (starts from 0), p is the lift
  81 let rec lift O D t k p on t ≝
  82   match t with
  83     [ Val o a ⇒ Val O D o a
  84     | Rel n ⇒ if (leb k n) then Rel O D (n+p) else Rel O D n
  85     | App m n ⇒ App O D (lift O D m k p) (lift O D n k p)
  86     | Lambda Ty n ⇒ Lambda O D Ty (lift O D n (S k) p)
  87     | Vec Ty v ⇒ Vec O D Ty (map ?? (λx. lift O D x k p) v)
  88     ].
  89
  90 notation "↑ ^ n ( M )" non associative with precedence 40 for @{'Lift 0 $n $M}.
  91 notation "↑ _ k ^ n ( M )" non associative with precedence 40 for @{'Lift $n $k $M}.
  92
  93 interpretation "Lift" 'Lift n k M = (lift ?? M k n).
  94
  95 let rec subst O D t k s on t ≝
  96   match t with
  97     [ Val o a ⇒ Val O D o a
  98     | Rel n ⇒ if (leb k n) then
  99         (if (eqb k n) then lift O D s 0 n else Rel O D (n-1))
 100         else(Rel O D n)
 101     | App m n ⇒ App O D (subst O D m k s) (subst O D n k s)
 102     | Lambda T n ⇒ Lambda O D T (subst O D n (S k) s)
 103     | Vec T v ⇒ Vec O D T (map ?? (λx. subst O D x k s) v)
 104     ].
 105 *)
 106
 107 (* simplified version of subst, assuming the argument s is closed *)
 108
 109 let rec subst O D t k s on t ≝
 110   match t with
 111     [ Val o a ⇒ Val O D o a
 112     | Rel n ⇒ if (leb k n) then
 113         (if (eqb k n) then (* lift O D s 0 n*) s else Rel O D (n-1))
 114         else(Rel O D n)
 115     | App m n ⇒ App O D (subst O D m k s) (subst O D n k s)
 116     | Lambda T n ⇒ Lambda O D T (subst O D n (S k) s)
 117     | Vec T v ⇒ Vec O D T (map ?? (λx. subst O D x k s) v)
 118     ].
 119 (* notation "hvbox(M break [ k ≝ N ])"
 120    non associative with precedence 90
 121    for @{'Subst1 $M $k $N}. *)
 122
 123 interpretation "Subst" 'Subst1 M k N = (subst M k N).
 124
 125 (*
 126 lemma subst_rel1: ∀O,D,A.∀k,i. i < k →
 127   (Rel O D i) [k ≝ A] = Rel O D i.
 128 #A #k #i normalize #ltik >(lt_to_leb_false … ltik) //
 129 qed.
 130
 131 lemma subst_rel2: ∀O,D, A.∀k.
 132   (Rel k) [k ≝ A] = lift A 0 k.
 133 #A #k normalize >(le_to_leb_true k k) // >(eq_to_eqb_true … (refl …)) //
 134 qed.
 135
 136 lemma subst_rel3: ∀A.∀k,i. k < i →
 137   (Rel i) [k ≝ A] = Rel (i-1).
 138 #A #k #i normalize #ltik >(le_to_leb_true k i) /2/
 139 >(not_eq_to_eqb_false k i) // @lt_to_not_eq //
 140 qed. *)
 141
 142
 143 (* closed terms ????
 144 let rec closed_k O D (t: T O D) k on t ≝
 145   match t with
 146     [ Val o a ⇒ True
 147     | Rel n ⇒ n < k
 148     | App m n ⇒ (closed_k O D m k) ∧ (closed_k O D n k)
 149     | Lambda T n ⇒ closed_k O D n (k+1)
 150     | Vec T v ⇒ closed_list O D v k
 151     ]
 152
 153 and closed_list O D (l: list (T O D)) k on l ≝
 154   match l with
 155     [ nil ⇒ True
 156     | cons hd tl ⇒ closed_k O D hd k ∧ closed_list O D tl k
 157     ]
 158 . *)
 159
 160 inductive is_closed (O:Type[0]) (D:O→FinSet): nat → T O D → Prop ≝
 161 | cval : ∀k,o,a.is_closed O D k (Val O D o a)
 162 | crel : ∀k,n. n < k → is_closed O D k (Rel O D n)
 163 | capp : ∀k,m,n. is_closed O D k m → is_closed O D k n →
 164            is_closed O D k (App O D m n)
 165 | clam : ∀T,k,m. is_closed O D (S k) m → is_closed O D k (Lambda O D T m)
 166 | cvec:  ∀T,k,v. (∀m. mem ? m v → is_closed O D k m) →
 167            is_closed O D k (Vec O D T v).
 168
 169 lemma is_closed_rel: ∀O,D,n,k.
 170   is_closed O D k (Rel O D n) → n < k.
 171 #O #D #n #k #H inversion H
 172   [#k0 #o #a #eqk #H destruct
 173   |#k0 #n0 #ltn0 #eqk #H destruct //
 174   |#k0 #M #N #_ #_ #_ #_ #_ #H destruct
 175   |#T #k0 #M #_ #_ #_ #H destruct
 176   |#T #k0 #v #_ #_ #_ #H destruct
 177   ]
 178 qed.
 179
 180 lemma is_closed_app: ∀O,D,k,M, N.
 181   is_closed O D k (App O D M N) → is_closed O D k M ∧ is_closed O D k N.
 182 #O #D #k #M #N #H inversion H
 183   [#k0 #o #a #eqk #H destruct
 184   |#k0 #n0 #ltn0 #eqk #H destruct
 185   |#k0 #M1 #N1 #HM #HN #_ #_ #_ #H1 destruct % //
 186   |#T #k0 #M #_ #_ #_ #H destruct
 187   |#T #k0 #v #_ #_ #_ #H destruct
 188   ]
 189 qed.
 190
 191 lemma is_closed_lam: ∀O,D,k,ty,M.
 192   is_closed O D k (Lambda O D ty M) → is_closed O D (S k) M.
 193 #O #D #k #ty #M #H inversion H
 194   [#k0 #o #a #eqk #H destruct
 195   |#k0 #n0 #ltn0 #eqk #H destruct
 196   |#k0 #M1 #N1 #HM #HN #_ #_ #_ #H1 destruct
 197   |#T #k0 #M1 #HM1 #_ #_ #H1 destruct //
 198   |#T #k0 #v #_ #_ #_ #H destruct
 199   ]
 200 qed.
 201
 202 lemma is_closed_vec: ∀O,D,k,ty,v.
 203   is_closed O D k (Vec O D ty v) → ∀m. mem ? m v → is_closed O D k m.
 204 #O #D #k #ty #M #H inversion H
 205   [#k0 #o #a #eqk #H destruct
 206   |#k0 #n0 #ltn0 #eqk #H destruct
 207   |#k0 #M1 #N1 #HM #HN #_ #_ #_ #H1 destruct
 208   |#T #k0 #M1 #HM1 #_ #_ #H1 destruct
 209   |#T #k0 #v #Hv #_ #_ #H1 destruct @Hv
 210   ]
 211 qed.
 212
 213 lemma is_closed_S: ∀O,D,M,m.
 214   is_closed O D m M → is_closed O D (S m) M.
 215 #O #D #M #m #H elim H //
 216   [#k #n0 #Hlt @crel @le_S //
 217   |#k #P #Q #HP #HC #H1 #H2 @capp //
 218   |#ty #k #P #HP #H1 @clam //
 219   |#ty #k #v #Hind #Hv @cvec @Hv
 220   ]
 221 qed.
 222
 223 lemma is_closed_mono: ∀O,D,M,m,n. m ≤ n →
 224   is_closed O D m M → is_closed O D n M.
 225 #O #D #M #m #n #lemn elim lemn // #i #j #H #H1 @is_closed_S @H @H1
 226 qed.
 227
 228
 229 (*** properties of lift and subst ***)
 230
 231 (*
 232 lemma lift_0: ∀O,D.∀t:T O D.∀k. lift O D t k 0 = t.
 233 #O #D #t @(T_elim … t) normalize //
 234   [#n #k cases (leb k n) normalize //
 235   |#o #v #Hind #k @eq_f lapply Hind -Hind elim v //
 236    #hd #tl #Hind #Hind1 normalize @eq_f2
 237     [@Hind1 %1 //|@Hind #x #Hx @Hind1 %2 //]
 238   ]
 239 qed.
 240
 241 lemma lift_closed: ∀O,D.∀t:T O D.∀k,p.
 242   is_closed O D k t → lift O D t k p = t.
 243 #O #D #t @(T_elim … t) normalize //
 244   [#n #k #p #H >(not_le_to_leb_false … (lt_to_not_le … (is_closed_rel … H))) //
 245   |#M #N #HindM #HindN #k #p #H lapply (is_closed_app … H) * #HcM #HcN
 246    >(HindM … HcM) >(HindN … HcN) //
 247   |#ty #M #HindM #k #p #H lapply (is_closed_lam … H) -H #H >(HindM … H) //
 248   |#ty #v #HindM #k #p #H lapply (is_closed_vec … H) -H #H @eq_f
 249    cut (∀m. mem ? m v → lift O D m k p = m)
 250     [#m #Hmem @HindM [@Hmem | @H @Hmem]] -HindM
 251    elim v // #a #tl #Hind #H1 normalize @eq_f2
 252     [@H1 %1 //|@Hind #m #Hmem @H1 %2 @Hmem]
 253   ]
 254 qed.
 255
 256 *)
 257
 258 lemma subst_closed: ∀O,D,M,N,k,i. k ≤ i →
 259   is_closed O D k M → subst O D M i N = M.
 260 #O #D #M @(T_elim … M)
 261   [#o #a normalize //
 262   |#n #N #k #j #Hlt #Hc lapply (is_closed_rel … Hc) #Hnk normalize
 263    >not_le_to_leb_false [2:@lt_to_not_le @(lt_to_le_to_lt … Hnk Hlt)] //
 264   |#P #Q #HindP #HindQ #N #k #i #ltki #Hc lapply (is_closed_app … Hc) *
 265    #HcP #HcQ normalize >(HindP … ltki HcP) >(HindQ … ltki HcQ) //
 266   |#ty #P #HindP #N #k #i #ltki #Hc lapply (is_closed_lam … Hc)
 267    #HcP normalize >(HindP … HcP) // @le_S_S @ltki
 268   |#ty #v #Hindv #N #k #i #ltki #Hc lapply (is_closed_vec … Hc)
 269    #Hcv normalize @eq_f
 270    cut (∀m:T O D.mem (T O D) m v→ subst O D m i N=m)
 271     [#m #Hmem @(Hindv … Hmem N … ltki) @Hcv @Hmem]
 272    elim v // #a #tl #Hind #H normalize @eq_f2
 273     [@H %1 //| @Hind #Hmem #Htl @H %2 @Htl]
 274   ]
 275 qed.
 276
 277 lemma subst_lemma:  ∀O,D,A,B,C,k,i. is_closed O D k B → is_closed O D i C →
 278   subst O D (subst O D A i B) (k+i) C =
 279   subst O D (subst O D A (k+S i) C) i B.
 280 #O #D #A #B #C #k @(T_elim … A) normalize
 281   [//
 282   |#n #i #HBc #HCc @(leb_elim i n) #Hle
 283     [@(eqb_elim i n) #eqni
 284       [<eqni >(lt_to_leb_false (k+(S i)) i) // normalize
 285        >(subst_closed … HBc) // >le_to_leb_true // >eq_to_eqb_true //
 286       |(cut (i < n))
 287         [cases (le_to_or_lt_eq … Hle) // #eqin @False_ind /2/] #ltin
 288        (cut (0 < n)) [@(le_to_lt_to_lt … ltin) //] #posn
 289        normalize @(leb_elim (k+i) (n-1)) #nk
 290         [@(eqb_elim (k+i) (n-1)) #H normalize
 291           [cut (k+(S i) = n); [/2 by S_pred/] #H1
 292            >(le_to_leb_true (k+(S i)) n) /2/
 293            >(eq_to_eqb_true … H1) normalize >(subst_closed … HCc) //
 294           |(cut (k+i < n-1)) [@not_eq_to_le_to_lt; //] #Hlt
 295            >(le_to_leb_true (k+(S i)) n) normalize
 296             [>(not_eq_to_eqb_false (k+(S i)) n) normalize
 297               [>le_to_leb_true [2:@lt_to_le @(le_to_lt_to_lt … Hlt) //]
 298                >not_eq_to_eqb_false // @lt_to_not_eq @(le_to_lt_to_lt … Hlt) //
 299               |@(not_to_not … H) #Hn /2 by plus_minus/
 300               ]
 301             |<plus_n_Sm @(lt_to_le_to_lt … Hlt) //
 302             ]
 303           ]
 304         |>(not_le_to_leb_false (k+(S i)) n) normalize
 305           [>(le_to_leb_true … Hle) >(not_eq_to_eqb_false … eqni) //
 306           |@(not_to_not … nk) #H @le_plus_to_minus_r //
 307           ]
 308         ]
 309       ]
 310     |(cut (n < k+i)) [@(lt_to_le_to_lt ? i) /2 by not_le_to_lt/] #ltn
 311      >not_le_to_leb_false [2: @lt_to_not_le @(transitive_lt …ltn) //] normalize
 312      >not_le_to_leb_false [2: @lt_to_not_le //] normalize
 313      >(not_le_to_leb_false … Hle) //
 314     ]
 315   |#M #N #HindM #HindN #i #HBC #HCc @eq_f2 [@HindM // |@HindN //]
 316   |#ty #M #HindM #i #HBC #HCc @eq_f >plus_n_Sm >plus_n_Sm @HindM //
 317    @is_closed_S //
 318   |#ty #v #Hindv #i #HBC #HCc @eq_f
 319    cut (∀m.mem ? m v → subst O D (subst O D m i B) (k+i) C =
 320           subst O D (subst O D m (k+S i) C) i B)
 321     [#m #Hmem @Hindv //] -Hindv elim v normalize [//]
 322    #a #tl #Hind #H @eq_f2 [@H %1 // | @Hind #m #Hmem @H %2 //]
 323   ]
 324 qed.
 325
 326