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

   1 Require Export contexts_defs.
   2 Require Export drop_defs.
   3 Require Export pr0_defs.
   4
   5 (*#* #caption "current axioms for the relation $\\CprZ{}{}$",
   6    "reflexivity", "compatibility"
   7 *)
   8 (*#* #cap #cap c, c1, c2 #alpha u1 in V1, u2 in V2, k in z *)
   9
  10       Inductive cpr0 : C -> C -> Prop :=
  11          | cpr0_refl : (c:?) (cpr0 c c)
  12          | cpr0_comp : (c1,c2:?) (cpr0 c1 c2) -> (u1,u2:?) (pr0 u1 u2) ->
  13                        (k:?) (cpr0 (CTail c1 k u1) (CTail c2 k u2)).
  14
  15 (*#* #stop file *)
  16
  17       Hint cpr0 : ltlc := Constructors cpr0.
  18
  19    Section cpr0_drop. (******************************************************)
  20
  21       Theorem cpr0_drop : (c1,c2:?) (cpr0 c1 c2) -> (h:?; e1:?; u1:?; k:?)
  22                           (drop h (0) c1 (CTail e1 k u1)) ->
  23                           (EX e2 u2 | (drop h (0) c2 (CTail e2 k u2)) &
  24                                       (cpr0 e1 e2) & (pr0 u1 u2)
  25                           ).
  26       Intros until 1; XElim H.
  27 (* case 1 : cpr0_refl *)
  28       XEAuto.
  29 (* case 2 : cpr0_comp *)
  30       XElim h.
  31 (* case 2.1 : h = 0 *)
  32       Intros; DropGenBase.
  33       Inversion H2; Rewrite H6 in H1; Rewrite H4 in H; XEAuto.
  34 (* case 2.2 : h > 0 *)
  35       XElim k; Intros; DropGenBase.
  36 (* case 2.2.1 : Bind *)
  37       LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
  38       XElim H0; XEAuto.
  39 (* case 2.2.2 : Flat *)
  40       LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
  41       XElim H0; XEAuto.
  42       Qed.
  43
  44       Theorem cpr0_drop_back : (c1,c2:?) (cpr0 c2 c1) -> (h:?; e1:?; u1:?; k:?)
  45                                (drop h (0) c1 (CTail e1 k u1)) ->
  46                                (EX e2 u2 | (drop h (0) c2 (CTail e2 k u2)) &
  47                                            (cpr0 e2 e1) & (pr0 u2 u1)
  48                                ).
  49       Intros until 1; XElim H.
  50 (* case 1 : cpr0_refl *)
  51       XEAuto.
  52 (* case 2 : cpr0_comp *)
  53       XElim h.
  54 (* case 2.1 : h = 0 *)
  55       Intros; DropGenBase.
  56       Inversion H2; Rewrite H6 in H1; Rewrite H4 in H; XEAuto.
  57 (* case 2.2 : h > 0 *)
  58       XElim k; Intros; DropGenBase.
  59 (* case 2.2.1 : Bind *)
  60       LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
  61       XElim H0; XEAuto.
  62 (* case 2.2.2 : Flat *)
  63       LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
  64       XElim H0; XEAuto.
  65       Qed.
  66
  67    End cpr0_drop.
  68
  69       Tactic Definition Cpr0Drop :=
  70          Match Context With
  71             | [ _: (drop ?1 (0) ?2 (CTail ?3 ?4 ?5));
  72                 _: (cpr0 ?2 ?6) |- ? ] ->
  73                LApply (cpr0_drop ?2 ?6); [ Intros H_x | XAuto ];
  74                LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
  75                XElim H_x; Intros
  76             | [ _: (drop ?1 (0) ?2 (CTail ?3 ?4 ?5));
  77                 _: (cpr0 ?6 ?2) |- ? ] ->
  78                LApply (cpr0_drop_back ?2 ?6); [ Intros H_x | XAuto ];
  79                LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
  80                XElim H_x; Intros
  81             | [ _: (drop ?1 (0) (CTail ?2 ?7 ?8) (CTail ?3 ?4 ?5));
  82                 _: (cpr0 ?2 ?6) |- ? ] ->
  83                LApply (cpr0_drop (CTail ?2 ?7 ?8) (CTail ?6 ?7 ?8)); [ Intros H_x | XAuto ];
  84                LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
  85                XElim H_x; Intros
  86             | [ _: (drop ?1 (0) (CTail ?2 ?7 ?8) (CTail ?3 ?4 ?5));
  87                 _: (cpr0 ?6 ?2) |- ? ] ->
  88                LApply (cpr0_drop_back (CTail ?2 ?7 ?8) (CTail ?6 ?7 ?8)); [ Intros H_x | XAuto ];
  89                LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
  90                XElim H_x; Intros.