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

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