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

   1 Require Export pc3_defs.
   2
   3 (*#* #stop record *)
   4
   5       Record G : Set := {
   6          next     : nat -> nat;
   7          base     : nat;
   8          next_lt  : (n:?) (lt n (next n));
   9          base_next: (n:?) (le base n) -> (next n) = (S n)
  10       }.
  11
  12 (*#* #start record *)
  13
  14 (*#* #caption "current axioms for typing",
  15    "well formed context sort", "well formed context binder",
  16    "conversion rule", "typed sort", "typed reference to abbreviation",
  17    "typed reference to abstraction", "typed binder", "typed application",
  18    "typed cast"
  19 *)
  20 (*#* #cap #cap c, d, t, t0, t1, t2, w #alpha m in h, n in i, u in V, v in U *)
  21
  22       Inductive wf0 [g:G] : C -> Prop :=
  23          | wf0_sort: (m:?) (wf0 g (CSort m))
  24          | wf0_bind: (c:?; u,t:?) (ty0 g c u t) ->
  25                      (b:?) (wf0 g (CTail c (Bind b) u))
  26       with ty0 [g:G] : C -> T -> T -> Prop :=
  27 (* structural rules *)
  28          | ty0_conv: (c:?; t2,t:?) (ty0 g c t2 t) ->
  29                      (u,t1:?) (ty0 g c u t1) -> (pc3 c t1 t2) ->
  30                      (ty0 g c u t2)
  31 (* axiom rules *)
  32          | ty0_sort: (c:?) (wf0 g c) ->
  33                      (m:?) (ty0 g c (TSort m) (TSort (next g m)))
  34          | ty0_abbr: (c:?) (wf0 g c) ->
  35                      (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abbr) u)) ->
  36                      (t:?) (ty0 g d u t) ->
  37                      (ty0 g c (TLRef n) (lift (S n) (0) t))
  38          | ty0_abst: (c:?) (wf0 g c) ->
  39                      (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abst) u)) ->
  40                      (t:?) (ty0 g d u t) ->
  41                      (ty0 g c (TLRef n) (lift (S n) (0) u))
  42          | ty0_bind: (c:?; u,t:?) (ty0 g c u t) ->
  43                      (b:?; t1,t2:?) (ty0 g (CTail c (Bind b) u) t1 t2) ->
  44                      (t0:?) (ty0 g (CTail c (Bind b) u) t2 t0) ->
  45                      (ty0 g c (TTail (Bind b) u t1) (TTail (Bind b) u t2))
  46          | ty0_appl: (c:?; w,u:?) (ty0 g c w u) ->
  47                      (v,t:?) (ty0 g c v (TTail (Bind Abst) u t)) ->
  48                      (ty0 g c (TTail (Flat Appl) w v)
  49                               (TTail (Flat Appl) w (TTail (Bind Abst) u t))
  50                      )
  51          | ty0_cast: (c:?; t1,t2:?) (ty0 g c t1 t2) ->
  52                      (t0:?) (ty0 g c t2 t0) ->
  53                      (ty0 g c (TTail (Flat Cast) t2 t1) t2).
  54
  55 (*#* #stop file *)
  56
  57       Hint wf0 : ltlc := Constructors wf0.
  58
  59       Hint ty0 : ltlc := Constructors ty0.
  60
  61    Section wf0_props. (******************************************************)
  62
  63       Theorem wf0_ty0: (g:?; c:?; u,t:?) (ty0 g c u t) -> (wf0 g c).
  64       Intros; XElim H; XAuto.
  65       Qed.
  66
  67       Hints Resolve wf0_ty0 : ltlc.
  68
  69       Theorem wf0_drop_O: (c,e:?; h:?) (drop h (0) c e) ->
  70                           (g:?) (wf0 g c) -> (wf0 g e).
  71       XElim c.
  72 (* case 1 : CSort *)
  73       Intros; DropGenBase; Rewrite H; XAuto.
  74 (* case 2 : CTail k *)
  75       Intros c IHc; XElim k; (
  76       XElim h; Intros; DropGenBase;
  77       [ Rewrite H in H0; XAuto | Inversion H1; XEAuto ] ).
  78       Qed.
  79
  80    End wf0_props.
  81
  82       Hints Resolve wf0_ty0 wf0_drop_O : ltlc.
  83
  84       Tactic Definition Wf0Ty0 :=
  85          Match Context With
  86             [ _: (ty0 ?1 ?2 ?3 ?4) |- ? ] ->
  87                LApply (wf0_ty0 ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
  88                Inversion_clear H_x.
  89
  90       Tactic Definition Wf0DropO :=
  91          Match Context With
  92             | [ _: (drop ?1 (0) ?2 ?3); _: (wf0 ?4 ?2) |- ? ] ->
  93                LApply (wf0_drop_O ?2 ?3 ?1); [ Intros H_x | XAuto ];
  94                LApply (H_x ?4); [ Clear H_x; Intros | XAuto ].
  95
  96    Section wf0_facilities. (*************************************************)
  97
  98       Theorem wf0_drop_wf0: (g:?; c:?) (wf0 g c) ->
  99                             (b:?; e:?; u:?; h:?)
 100                             (drop h (0) c (CTail e (Bind b) u)) -> (wf0 g e).
 101       Intros.
 102       Wf0DropO; Inversion H1; XEAuto.
 103       Qed.
 104
 105       Theorem ty0_drop_wf0: (g:?; c:?; t1,t2:?) (ty0 g c t1 t2) ->
 106                             (b:?; e:?; u:?; h:?)
 107                             (drop h (0) c (CTail e (Bind b) u)) -> (wf0 g e).
 108       Intros.
 109       EApply wf0_drop_wf0; [ Idtac | EApply H0 ]; XEAuto.
 110       Qed.
 111
 112    End wf0_facilities.
 113
 114       Hints Resolve wf0_drop_wf0 ty0_drop_wf0 : ltlc.
 115
 116       Tactic Definition DropWf0 :=
 117          Match Context With
 118             | [ _: (ty0 ?1 ?2 ?3 ?4);
 119                 _: (drop ?5 (0) ?2 (CTail ?6 (Bind ?7) ?8)) |- ? ] ->
 120                LApply (ty0_drop_wf0 ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
 121                LApply (H_x ?7 ?6 ?8 ?5); [ Clear H_x; Intros | XAuto ]
 122             | [ _: (wf0 ?1 ?2);
 123                 _: (drop ?5 (0) ?2 (CTail ?6 (Bind ?7) ?8)) |- ? ] ->
 124                LApply (wf0_drop_wf0 ?1 ?2); [ Intros H_x | XAuto ];
 125                LApply (H_x ?7 ?6 ?8 ?5); [ Clear H_x; Intros | XAuto ].