matita/matita/lib/finite_lambda/typing.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 "finite_lambda/reduction.ma".
  13
  14
  15 (****************************************************************)
  16
  17 inductive TJ (O: Type[0]) (D:O → FinSet): list (FType O) → T O D → FType O → Prop ≝
  18   | tval: ∀G,o,a. TJ O D G (Val O D o a) (atom O o)
  19   | trel: ∀G1,ty,G2,n. length ? G1 = n → TJ O D (G1@ty::G2) (Rel O D n) ty
  20   | tapp: ∀G,M,N,ty1,ty2. TJ O D G M (arrow O ty1 ty2) → TJ O D G N ty1 →
  21       TJ O D G (App O D M N) ty2
  22   | tlambda: ∀G,M,ty1,ty2. TJ O D (ty1::G) M ty2 →
  23       TJ O D G (Lambda O D ty1 M) (arrow O ty1 ty2)
  24   | tvec: ∀G,v,ty1,ty2.
  25       (|v| = |enum (FinSet_of_FType O D ty1)|) →
  26       (∀M. mem ? M v → TJ O D G M ty2) →
  27       TJ O D G (Vec O D ty1 v) (arrow O ty1 ty2).
  28
  29 lemma wt_to_T: ∀O,D,G,ty,a.TJ O D G (to_T O D ty a) ty.
  30 #O #D #G #ty elim ty
  31   [#o #a normalize @tval
  32   |#ty1 #ty2 #Hind1 #Hind2 normalize * #v #Hv @tvec
  33     [<Hv >length_map >length_map //
  34     |#M elim v
  35       [normalize @False_ind |#a #v1 #Hind3 * [#eqM >eqM @Hind2 |@Hind3]]
  36     ]
  37   ]
  38 qed.
  39
  40 lemma inv_rel: ∀O,D,G,n,ty.
  41   TJ O D G (Rel O D n) ty → ∃G1,G2.|G1|=n∧G=G1@ty::G2.
  42 #O #D #G #n #ty #Hrel inversion Hrel
  43   [#G1 #o #a #_ #H destruct
  44   |#G1 #ty1 #G2 #n1 #H1 #H2 #H3 #H4 destruct %{G1} %{G2} /2/
  45   |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct
  46   |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct
  47   |#G1 #v #ty3 #ty4 #_ #_ #_ #_ #H destruct
  48   ]
  49 qed.
  50
  51 lemma inv_tlambda: ∀O,D,G,M,ty1,ty2,ty3.
  52   TJ O D G (Lambda O D ty1 M) (arrow O ty2 ty3) →
  53   ty1 = ty2 ∧ TJ O D (ty2::G) M ty3.
  54 #O #D #G #M #ty1 #ty2 #ty3 #Hlam inversion Hlam
  55   [#G1 #o #a #_ #H destruct
  56   |#G1 #ty #G2 #n #_ #_ #H destruct
  57   |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct
  58   |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct % //
  59   |#G1 #v #ty3 #ty4 #_ #_ #_ #_ #H destruct
  60   ]
  61 qed.
  62
  63 lemma inv_tvec: ∀O,D,G,v,ty1,ty2,ty3.
  64    TJ O D G (Vec O D ty1 v) (arrow O ty2 ty3) →
  65   (|v| = |enum (FinSet_of_FType O D ty1)|) ∧
  66   (∀M. mem ? M v → TJ O D G M ty3).
  67 #O #D #G #v #ty1 #ty2 #ty3 #Hvec inversion Hvec
  68   [#G #o #a #_ #H destruct
  69   |#G1 #ty #G2 #n #_ #_ #H destruct
  70   |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct
  71   |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct
  72   |#G1 #v1 #ty4 #ty5 #Hv #Hmem #_ #_ #H #H1 destruct % // @Hmem
  73   ]
  74 qed.
  75
  76 (* could be generalized *)
  77 lemma weak_rel: ∀O,D,G1,G2,ty1,ty2,n. length ? G1 < n →
  78    TJ O D (G1@G2) (Rel O D n) ty1 →
  79    TJ O D (G1@ty2::G2) (Rel O D (S n)) ty1.
  80 #O #D #G1 #G2 #ty1 #ty2 #n #HG1 #Hrel lapply (inv_rel … Hrel)
  81 * #G3 * #G4 * #H1 #H2 lapply (compare_append … H2)
  82 * #G5 *
  83   [* #H3 @False_ind >H3 in HG1; >length_append >H1 #H4
  84    @(absurd … H4) @le_to_not_lt //
  85   |* #H3 #H4 >H4 >append_cons <associative_append @trel
  86    >length_append >length_append <H1 >H3 >length_append normalize
  87    >plus_n_Sm >associative_plus @eq_f //
  88   ]
  89 qed.
  90
  91 lemma strength_rel: ∀O,D,G1,G2,ty1,ty2,n. length ? G1 < n →
  92    TJ O D (G1@ty2::G2) (Rel O D n) ty1 →
  93    TJ O D (G1@G2) (Rel O D (n-1)) ty1.
  94 #O #D #G1 #G2 #ty1 #ty2 #n #HG1 #Hrel lapply (inv_rel … Hrel)
  95 * #G3 * #G4 * #H1 #H2 lapply (compare_append … H2)
  96 * #G5 *
  97   [* #H3 @False_ind >H3 in HG1; >length_append >H1 #H4
  98    @(absurd … H4) @le_to_not_lt //
  99   |lapply G5 -G5 *
 100     [>append_nil normalize * #H3 #H4 destruct @False_ind @(absurd … HG1)
 101      @le_to_not_lt //
 102     |#ty3 #G5 * #H3 normalize #H4 destruct (H4) <associative_append @trel
 103      <H1 >H3 >length_append >length_append normalize <plus_minus_associative //
 104     ]
 105   ]
 106 qed.
 107
 108 lemma no_matter: ∀O,D,G,N,tyN.
 109   TJ O D G N tyN →  ∀G1,G2,G3.G=G1@G2 → is_closed O D (|G1|) N →
 110     TJ O D (G1@G3) N tyN.
 111 #O #D #G #N #tyN #HN elim HN -HN -tyN -N -G
 112   [#G #o #a #G1 #G2 #G3 #_ #_ @tval
 113   |#G #ty #G2 #n #HG #G3 #G4 #G5 #H #HNC normalize
 114    lapply (is_closed_rel … HNC) #Hlt lapply (compare_append … H) * #G6 *
 115     [* #H1 @False_ind @(absurd ? Hlt) @le_to_not_lt <HG >H1 >length_append //
 116     |* cases G6
 117       [>append_nil normalize #H1 @False_ind
 118        @(absurd ? Hlt) @le_to_not_lt <HG >H1 //
 119       |#ty1 #G7 #H1 normalize #H2 destruct >associative_append @trel //
 120       ]
 121     ]
 122   |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #G1 #G2 #G3
 123    #Heq #Hc lapply (is_closed_app … Hc) -Hc * #HMc #HNc
 124    @(tapp … (HindM … Heq HMc) (HindN … Heq HNc))
 125   |#G #M #ty1 #ty2 #HM #HindM #G1 #G2 #G3 #Heq #Hc
 126    lapply (is_closed_lam … Hc) -Hc #HMc
 127    @tlambda @(HindM (ty1::G1) G2) [>Heq // |@HMc]
 128   |#G #v #ty1 #ty2 #Hlen #Hv #Hind #G1 #G2 #G3 #H1 #Hc @tvec
 129     [>length_map //
 130     |#M #Hmem @Hind // lapply (is_closed_vec … Hc) #Hvc @Hvc //
 131     ]
 132   ]
 133 qed.
 134
 135 lemma nth_spec: ∀A,a,d,l1,l2,n. |l1| = n → nth n A (l1@a::l2) d = a.
 136 #A #a #d #l1 elim l1 normalize
 137   [#l2 #n #Hn <Hn  //
 138   |#b #tl #Hind #l2 #m #Hm <Hm normalize @Hind //
 139   ]
 140 qed.
 141
 142 lemma wt_subst_gen: ∀O,D,G,M,tyM.
 143   TJ O D G M tyM →
 144    ∀G1,G2,N,tyN.G=(G1@tyN::G2) →
 145     TJ O D G2 N tyN → is_closed O D 0 N →
 146      TJ O D (G1@G2) (subst O D M (|G1|) N) tyM.
 147 #O #D #G #M #tyM #HM elim HM -HM -tyM -M -G
 148   [#G #o #a #G1 #G2 #N #tyN #_ #HG #_ normalize @tval
 149   |#G #ty #G2 #n #Hlen #G21 #G22 #N #tyN #HG #HN #HNc
 150    normalize cases (true_or_false (leb (|G21|) n))
 151     [#H >H cases (le_to_or_lt_eq … (leb_true_to_le … H))
 152       [#ltn >(not_eq_to_eqb_false … (lt_to_not_eq … ltn)) normalize
 153        lapply (compare_append … HG) * #G3 *
 154         [* #HG1 #HG2 @(strength_rel … tyN … ltn) <HG @trel @Hlen
 155         |* #HG >HG in ltn; >length_append #ltn @False_ind
 156          @(absurd … ltn) @le_to_not_lt >Hlen //
 157         ]
 158       |#HG21 >(eq_to_eqb_true … HG21)
 159        cut (ty = tyN)
 160         [<(nth_spec ? ty ty ? G2 … Hlen) >HG @nth_spec @HG21] #Hty >Hty
 161        normalize <HG21 @(no_matter ????? HN []) //
 162       ]
 163     |#H >H normalize lapply (compare_append … HG) * #G3 *
 164       [* #H1 @False_ind @(absurd ? Hlen) @sym_not_eq @lt_to_not_eq >H1
 165        >length_append @(lt_to_le_to_lt n (|G21|)) // @not_le_to_lt
 166        @(leb_false_to_not_le … H)
 167       |cases G3
 168         [>append_nil * #H1 @False_ind @(absurd ? Hlen) <H1 @sym_not_eq
 169          @lt_to_not_eq @not_le_to_lt @(leb_false_to_not_le … H)
 170         |#ty2 #G4 * #H1 normalize #H2 destruct >associative_append @trel //
 171         ]
 172       ]
 173     ]
 174   |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #G1 #G2 #N0 #tyN0 #eqG
 175    #HN0 #Hc normalize @(tapp … ty1)
 176     [@(HindM … eqG HN0 Hc) |@(HindN … eqG HN0 Hc)]
 177   |#G #M #ty1 #ty2 #HM #HindM #G1 #G2 #N0 #tyN0 #eqG
 178    #HN0 #Hc normalize @(tlambda … ty1) @(HindM (ty1::G1) … HN0) // >eqG //
 179   |#G #v #ty1 #ty2 #Hlen #Hv #Hind #G1 #G2 #N0 #tyN0 #eqG
 180    #HN0 #Hc normalize @(tvec … ty1)
 181     [>length_map @Hlen
 182     |#M #Hmem lapply (mem_map ????? Hmem) * #a * -Hmem #Hmem #eqM <eqM
 183      @(Hind … Hmem … eqG HN0 Hc)
 184     ]
 185   ]
 186 qed.
 187
 188 lemma wt_subst: ∀O,D,M,N,G,ty1,ty2.
 189   TJ O D (ty1::G) M ty2 →
 190   TJ O D G N ty1 → is_closed O D 0 N →
 191   TJ O D G (subst O D M 0 N) ty2.
 192 #O #D #M #N #G #ty1 #ty2 #HM #HN #Hc @(wt_subst_gen …(ty1::G) … [ ] … HN) //
 193 qed.
 194
 195 lemma subject_reduction: ∀O,D,M,M1,G,ty.
 196   TJ O D G M ty → red O D M M1 → TJ O D G M1 ty.
 197 #O #D #M #M1 #G #ty #HM lapply M1 -M1 elim HM  -HM -ty -G -M
 198   [#G #o #a #M1 #Hval elim (red_val ????? Hval)
 199   |#G #ty #G1 #n #_ #M1 #Hrel elim (red_rel ???? Hrel)
 200   |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #M1 #Hred inversion Hred
 201     [#P #M0 #N0 #Hc #H1 destruct (H1) #HM1 @(wt_subst … HN) //
 202      @(proj2 … (inv_tlambda … HM))
 203     |#ty #v #a #M0 #Ha #H1 #H2 destruct @(proj2 … (inv_tvec … HM))
 204      @(assoc_to_mem … Ha)
 205     |#M2 #M3 #N0 #Hredl #_ #H1 destruct (H1) #eqM1 @(tapp … HN) @HindM @Hredl
 206     |#M2 #M3 #N0 #Hredr #_ #H1 destruct (H1) #eqM1 @(tapp … HM) @HindN @Hredr
 207     |#ty #N0 #N1 #_ #_ #H1 destruct (H1)
 208     |#ty #M0 #H1 destruct (H1)
 209     |#ty #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1)
 210     ]
 211   |#G #P #ty1 #ty2 #HP #Hind #M1 #Hred lapply(red_lambda ????? Hred) *
 212     [* #P1 * #HredP #HM1 >HM1 @tlambda @Hind //
 213     |#HM1 >HM1 @tvec // #N #HN lapply(mem_map ????? HN)
 214      * #a * #mema #eqN <eqN -eqN @(wt_subst …HP) // @wt_to_T
 215     ]
 216   |#G #v #ty1 #ty2 #Hlen #Hv #Hind #M1 #Hred lapply(red_vec ????? Hred)
 217    * #N * #N1 * #v1 * #v2 * * #H1 #H2 #H3 >H3 @tvec
 218     [<Hlen >H2 >length_append >length_append @eq_f //
 219     |#M2 #Hmem cases (mem_append ???? Hmem) -Hmem #Hmem
 220       [@Hv >H2 @mem_append_l1 //
 221       |cases Hmem
 222         [#HM2 >HM2 -HM2 @(Hind N … H1) >H2 @mem_append_l2 %1 //
 223         |-Hmem #Hmem @Hv >H2 @mem_append_l2 %2 //
 224         ]
 225       ]
 226     ]
 227   ]
 228 qed.
 229