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

   1 (*#* #stop file *)
   2
   3 Require Export ty0_defs.
   4
   5       Inductive csub0 [g:G] : C -> C -> Prop :=
   6 (* structural rules *)
   7          | csub0_sort : (n:?) (csub0 g (CSort n) (CSort n))
   8          | csub0_tail : (c1,c2:?) (csub0 g c1 c2) -> (k,u:?)
   9                         (csub0 g (CTail c1 k u) (CTail c2 k u))
  10 (* axioms *)
  11          | csub0_void : (c1,c2:?) (csub0 g c1 c2) -> (b:?) ~b=Void -> (u1,u2:?)
  12                         (csub0 g (CTail c1 (Bind Void) u1) (CTail c2 (Bind b) u2))
  13          | csub0_abst : (c1,c2:?) (csub0 g c1 c2) -> (u,t:?) (ty0 g c2 u t) ->
  14                         (csub0 g (CTail c1 (Bind Abst) t) (CTail c2 (Bind Abbr) u)).
  15
  16       Hint csub0 : ltlc := Constructors csub0.
  17
  18    Section csub0_props. (****************************************************)
  19
  20       Theorem csub0_refl : (g:?; c:?) (csub0 g c c).
  21       XElim c; XAuto.
  22       Qed.
  23
  24    End csub0_props.
  25
  26       Hints Resolve csub0_refl : ltlc.
  27
  28    Section csub0_drop. (*****************************************************)
  29
  30       Theorem csub0_drop_abbr : (g:?; n:?; c1,c2:?) (csub0 g c1 c2) -> (d1,u:?)
  31                                 (drop n (0) c1 (CTail d1 (Bind Abbr) u)) ->
  32                                 (EX d2 | (csub0 g d1 d2) &
  33                                          (drop n (0) c2 (CTail d2 (Bind Abbr) u))
  34                                 ).
  35       XElim n.
  36 (* case 1 : n = 0 *)
  37       Intros; DropGenBase; Rewrite H0 in H; Inversion H; XEAuto.
  38 (* case 2 : n > 0 *)
  39       Intros until 2; XElim H0.
  40 (* case 2.1 : csub0_sort *)
  41       Intros; Inversion H0.
  42 (* case 2.2 : csub0_tail *)
  43       XElim k; Intros; DropGenBase.
  44 (* case 2.2.1 : Bind *)
  45       LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
  46       LApply (H d1 u0); [ Clear H; Intros H | XAuto ].
  47       XElim H; XEAuto.
  48 (* case 2.2.2 : Flat *)
  49       LApply (H1 d1 u0); [ Clear H1; Intros H1 | XAuto ].
  50       XElim H1; XEAuto.
  51 (* case 2.3 : csub0_void *)
  52       Intros; DropGenBase.
  53       LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
  54       LApply (H d1 u); [ Clear H; Intros H | XAuto ].
  55       XElim H; XEAuto.
  56 (* case 2.4 : csub0_abst *)
  57       Intros; DropGenBase.
  58       LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
  59       LApply (H d1 u0); [ Clear H; Intros H | XAuto ].
  60       XElim H; XEAuto.
  61       Qed.
  62
  63       Theorem csub0_drop_abst : (g:?; n:?; c1,c2:?) (csub0 g c1 c2) -> (d1,t:?)
  64                                 (drop n (0) c1 (CTail d1 (Bind Abst) t)) ->
  65                                 (EX d2 | (csub0 g d1 d2) &
  66                                          (drop n (0) c2 (CTail d2 (Bind Abst) t))
  67
  68                                 ) \/
  69                                 (EX d2 u | (csub0 g d1 d2) &
  70                                            (drop n (0) c2 (CTail d2 (Bind Abbr) u)) &
  71                                            (ty0 g d2 u t)
  72                                 ).
  73       XElim n.
  74 (* case 1 : n = 0 *)
  75       Intros; DropGenBase; Rewrite H0 in H; Inversion H; XEAuto.
  76 (* case 2 : n > 0 *)
  77       Intros until 2; XElim H0.
  78 (* case 2.1 : csub0_sort *)
  79       Intros; Inversion H0.
  80 (* case 2.2 : csub0_tail *)
  81       XElim k; Intros; DropGenBase.
  82 (* case 2.2.1 : Bind *)
  83       LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
  84       LApply (H d1 t); [ Clear H; Intros H | XAuto ].
  85       XElim H; Intros; XElim H; XEAuto.
  86 (* case 2.2.2 : Flat *)
  87       LApply (H1 d1 t); [ Clear H1; Intros H1 | XAuto ].
  88       XElim H1; Intros; XElim H1; XEAuto.
  89 (* case 2.3 : csub0_void *)
  90       Intros; DropGenBase.
  91       LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
  92       LApply (H d1 t); [ Clear H; Intros H | XAuto ].
  93       XElim H; Intros; XElim H; XEAuto.
  94 (* case 2.4 : csub0_abst *)
  95       Intros; DropGenBase.
  96       LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
  97       LApply (H d1 t0); [ Clear H; Intros H | XAuto ].
  98       XElim H; Intros; XElim H; XEAuto.
  99       Qed.
 100
 101    End csub0_drop.
 102
 103       Tactic Definition CSub0Drop :=
 104          Match Context With
 105             | [ H1: (csub0 ?1 ?2 ?3);
 106                 H2: (drop ?4 (0) ?2 (CTail ?5 (Bind Abbr) ?6)) |- ? ] ->
 107                LApply (csub0_drop_abbr ?1 ?4 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
 108                LApply (H1 ?5 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
 109                XElim H1; Intros
 110             | [ H1: (csub0 ?1 ?2 ?3);
 111                 H2: (drop ?4 (0) ?2 (CTail ?5 (Bind Abst) ?6)) |- ? ] ->
 112                LApply (csub0_drop_abst ?1 ?4 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
 113                LApply (H1 ?5 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
 114                XElim H1; Intros H1; XElim H1; Intros.
 115
 116    Section csub0_pc3. (*****************************************************)
 117
 118       Theorem csub0_pr2 : (g:?; c1:?; t1,t2:?) (pr2 c1 t1 t2) ->
 119                           (c2:?) (csub0 g c1 c2) -> (pr2 c2 t1 t2).
 120       Intros until 1; XElim H; Intros.
 121 (* case 1 : pr2_free *)
 122       XAuto.
 123 (* case 2 : pr2_delta *)
 124       CSub0Drop; XEAuto.
 125       Qed.
 126
 127       Theorem csub0_pc2 : (g:?; c1:?; t1,t2:?) (pc2 c1 t1 t2) ->
 128                           (c2:?) (csub0 g c1 c2) -> (pc2 c2 t1 t2).
 129       Intros until 1; XElim H; Intros.
 130 (* case 1 : pc2_r *)
 131       Apply pc2_r; EApply csub0_pr2; XEAuto.
 132 (* case 2 : pc2_x *)
 133       Apply pc2_x; EApply csub0_pr2; XEAuto.
 134       Qed.
 135
 136       Theorem csub0_pc3 : (g:?; c1:?; t1,t2:?) (pc3 c1 t1 t2) ->
 137                           (c2:?) (csub0 g c1 c2) -> (pc3 c2 t1 t2).
 138       Intros until 1; XElim H; Intros.
 139 (* case 1 : pc3_r *)
 140       XAuto.
 141 (* case 2 : pc3_u *)
 142       EApply pc3_u; [ EApply csub0_pc2; XEAuto | XAuto ].
 143       Qed.
 144
 145    End csub0_pc3.
 146
 147       Hints Resolve csub0_pc3 : ltlc.
 148
 149    Section csub0_ty0. (*****************************************************)
 150
 151       Theorem csub0_ty0 : (g:?; c1:?; t1,t2:?) (ty0 g c1 t1 t2) ->
 152                           (c2:?) (wf0 g c2) -> (csub0 g c1 c2) ->
 153                           (ty0 g c2 t1 t2).
 154       Intros until 1; XElim H; Intros.
 155 (* case 1 : ty0_conv *)
 156       EApply ty0_conv; XEAuto.
 157 (* case 2 : ty0_sort *)
 158       XEAuto.
 159 (* case 3 : ty0_abbr *)
 160       CSub0Drop; EApply ty0_abbr; XEAuto.
 161 (* case 4 : ty0_abst *)
 162       CSub0Drop; [ EApply ty0_abst | EApply ty0_abbr ]; XEAuto.
 163 (* case 5 : ty0_bind *)
 164       EApply ty0_bind; XEAuto.
 165 (* case 6 : ty0_appl *)
 166       EApply ty0_appl; XEAuto.
 167 (* case 7 : ty0_cast *)
 168       EApply ty0_cast; XAuto.
 169       Qed.
 170
 171       Theorem csub0_ty0_ld : (g:?; c:?; u,v:?) (ty0 g c u v) -> (t1,t2:?)
 172                              (ty0 g (CTail c (Bind Abst) v) t1 t2) ->
 173                              (ty0 g (CTail c (Bind Abbr) u) t1 t2).
 174       Intros; EApply csub0_ty0; XEAuto.
 175       Qed.
 176
 177    End csub0_ty0.
 178
 179       Hints Resolve csub0_ty0 csub0_ty0_ld : ltlc.
 180
 181       Tactic Definition CSub0Ty0 :=
 182          Match Context With
 183             [ _: (ty0 ?1 ?2 ?4 ?); _: (ty0 ?1 ?2 ?3 ?7); _: (pc3 ?2 ?4 ?7);
 184               H: (ty0 ?1 (CTail ?2 (Bind Abst) ?4) ?5 ?6) |- ? ] ->
 185                LApply (csub0_ty0_ld ?1 ?2 ?3 ?4); [ Intros H_x | EApply ty0_conv; XEAuto ];
 186                LApply (H_x ?5 ?6); [ Clear H_x H; Intros | XAuto ].