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

   1 Require drop_props.
   2 Require pc3_props.
   3 Require ty0_defs.
   4 Require ty0_lift.
   5
   6    Section ty0_correct. (****************************************************)
   7
   8 (*#* #caption "correctness of types" *)
   9 (*#* #cap #cap c, t1, t2  #alpha t in T3 *)
  10
  11       Theorem ty0_correct : (g:?; c:?; t1,t2:?)
  12                             (ty0 g c t1 t2) -> (EX t | (ty0 g c t2 t)).
  13
  14 (*#* #stop file *)
  15
  16       Intros; XElim H; Intros.
  17 (* case 1 : ty0_conv *)
  18       XEAuto.
  19 (* case 2 : ty0_sort *)
  20       XEAuto.
  21 (* case 3 : ty0_abbr *)
  22       XElim H2; XEAuto.
  23 (* case 4 : ty0_abst *)
  24       XEAuto.
  25 (* case 5 : ty0_bind *)
  26       XElim H4; XEAuto.
  27 (* case 6 : ty0_appl *)
  28       XElim H0; XElim H2; Intros.
  29       Ty0GenBase; XEAuto.
  30 (* case 7 : ty0_cast *)
  31       XAuto.
  32       Qed.
  33
  34    End ty0_correct.
  35
  36       Tactic Definition Ty0Correct :=
  37          Match Context With
  38             [ _: (ty0 ?1 ?2 ?3 ?4) |- ? ] ->
  39                LApply (ty0_correct ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
  40                XElim H_x; Intros.
  41
  42 (*#* #start file *)
  43
  44    Section ty0_shift. (******************************************************)
  45
  46 (*#* #caption "shift lemma for types" *)
  47 (*#* #cap #cap t1, t2 #alpha c in C1, e in C2 *)
  48
  49       Theorem ty0_shift : (h:?; c,e:?) (drop h (0) c e) ->
  50                           (g:?; t1,t2:?) (ty0 g c t1 t2) -> (wf0 g e) ->
  51                           (ty0 g e (app c h t1) (app c h t2)).
  52
  53 (*#* #stop file *)
  54
  55       XElim h.
  56 (* case 1 : h = 0 *)
  57       Intros; DropGenBase; Rewrite <- H.
  58       Repeat Rewrite app_O; XAuto.
  59 (* case 2 : h > 0 *)
  60       Intros h IHh; XElim c.
  61 (* case 2.1 : CSort *)
  62       Intros; DropGenBase; Rewrite H.
  63       Simpl; XAuto.
  64 (* case 2.2 : CTail k *)
  65       Intros c IHc; Clear IHc; XElim k; Intros; Wf0Ty0.
  66       DropGenBase; Move H0 after H2; Ty0Correct.
  67       Simpl; Apply IHh; [ Idtac | EApply ty0_bind | Idtac ]; XEAuto.
  68       Qed.
  69
  70    End ty0_shift.
  71
  72       Hints Resolve ty0_shift : ltlc.
  73
  74 (*#* #start file *)
  75
  76    Section ty0_unique. (*****************************************************)
  77
  78 (*#* #caption "uniqueness of types" *)
  79 (*#* #cap #cap c, t1, t2 #alpha u in T *)
  80
  81       Theorem ty0_unique : (g:?; c:?; u,t1:?) (ty0 g c u t1) ->
  82                            (t2:?) (ty0 g c u t2) -> (pc3 c t1 t2).
  83
  84 (*#* #stop file *)
  85
  86       Intros until 1; XElim H; Intros.
  87 (* case 1 : ty0_conv *)
  88       XEAuto.
  89 (* case 2 : ty0_sort *)
  90       Ty0GenBase; XAuto.
  91 (* case 3 : ty0_abbr *)
  92       Ty0GenBase; DropDis; Inversion H4.
  93       Rewrite H7 in H2; Rewrite H8 in H2; XEAuto.
  94 (* case 4 : ty0_abst *)
  95       Ty0GenBase; DropDis; Inversion H4.
  96       Rewrite H7 in H2; Rewrite H8 in H2; XEAuto.
  97 (* case 5 : ty0_bind *)
  98       Ty0GenBase; XEAuto.
  99 (* case 6 : ty0_appl *)
 100       Ty0GenBase; EApply pc3_t; [ Idtac | EApply H3 ]; XEAuto.
 101 (* case 7 : ty0_cast *)
 102       Ty0GenBase; XEAuto.
 103       Qed.
 104
 105    End ty0_unique.
 106
 107       Hints Resolve ty0_unique : ltlc.