helm/coq-contribs/LAMBDA-TYPES/csub0_props.v

   1 (*#* #stop file *)
   2
   3 Require pc3_props.
   4 Require csub0_defs.
   5
   6    Section csub0_pc3. (*****************************************************)
   7
   8       Theorem csub0_pr2: (g:?; c1:?; t1,t2:?) (pr2 c1 t1 t2) ->
   9                          (c2:?) (csub0 g c1 c2) -> (pr2 c2 t1 t2).
  10       Intros until 1; XElim H; Intros.
  11 (* case 1: pr2_free *)
  12       XAuto.
  13 (* case 2: pr2_delta *)
  14       CSub0Drop; XEAuto.
  15       Qed.
  16
  17       Hints Resolve csub0_pr2.
  18
  19       Opaque pc3.
  20
  21       Theorem csub0_pc3: (g:?; c1:?; t1,t2:?) (pc3 c1 t1 t2) ->
  22                          (c2:?) (csub0 g c1 c2) -> (pc3 c2 t1 t2).
  23       Intros until 1; XElimUsing pc3_ind_left H; XEAuto.
  24       Qed.
  25
  26    End csub0_pc3.
  27
  28       Hints Resolve csub0_pc3 : ltlc.
  29
  30    Section csub0_ty0. (*****************************************************)
  31
  32       Theorem csub0_ty0: (g:?; c1:?; t1,t2:?) (ty0 g c1 t1 t2) ->
  33                          (c2:?) (wf0 g c2) -> (csub0 g c1 c2) ->
  34                          (ty0 g c2 t1 t2).
  35       Intros until 1; XElim H; Intros.
  36 (* case 1: ty0_conv *)
  37       EApply ty0_conv; XEAuto.
  38 (* case 2: ty0_sort *)
  39       XEAuto.
  40 (* case 3: ty0_abbr *)
  41       CSub0Drop; EApply ty0_abbr; XEAuto.
  42 (* case 4: ty0_abst *)
  43       CSub0Drop; [ EApply ty0_abst | EApply ty0_abbr ]; XEAuto.
  44 (* case 5: ty0_bind *)
  45       EApply ty0_bind; XEAuto.
  46 (* case 6: ty0_appl *)
  47       EApply ty0_appl; XEAuto.
  48 (* case 7: ty0_cast *)
  49       EApply ty0_cast; XAuto.
  50       Qed.
  51
  52       Theorem csub0_ty0_ld: (g:?; c:?; u,v:?) (ty0 g c u v) -> (t1,t2:?)
  53                             (ty0 g (CTail c (Bind Abst) v) t1 t2) ->
  54                             (ty0 g (CTail c (Bind Abbr) u) t1 t2).
  55       Intros; EApply csub0_ty0; XEAuto.
  56       Qed.
  57
  58    End csub0_ty0.
  59
  60       Hints Resolve csub0_ty0 csub0_ty0_ld : ltlc.
  61
  62       Tactic Definition CSub0Ty0 :=
  63          Match Context With
  64             [ _: (ty0 ?1 ?2 ?4 ?); _: (ty0 ?1 ?2 ?3 ?7); _: (pc3 ?2 ?4 ?7);
  65               H: (ty0 ?1 (CTail ?2 (Bind Abst) ?4) ?5 ?6) |- ? ] ->
  66                LApply (csub0_ty0_ld ?1 ?2 ?3 ?4); [ Intros H_x | EApply ty0_conv; XEAuto ];
  67                LApply (H_x ?5 ?6); [ Clear H_x H; Intros | XAuto ].