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

   1 Require Export subst0_defs.
   2
   3 (*#* #caption "axioms for the relation $\\PrZ{}{}$",
   4    "reflexivity", "compatibility", "$\\beta$-contraction", "$\\upsilon$-swap",
   5    "$\\delta$-expansion", "$\\zeta$-contraction", "$\\epsilon$-contraction"
   6 *)
   7 (*#* #cap #cap t, t1, t2 #alpha u in V, u1 in V1, u2 in V2, v1 in W1, v2 in W2, w in T, k in z *)
   8
   9       Inductive pr0 : T -> T -> Prop :=
  10 (* structural rules *)
  11          | pr0_refl   : (t:?) (pr0 t t)
  12          | pr0_comp   : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
  13                         (k:?) (pr0 (TTail k u1 t1) (TTail k u2 t2))
  14 (* axiom rules *)
  15          | pr0_beta   : (u,v1,v2:?) (pr0 v1 v2) -> (t1,t2:?) (pr0 t1 t2) ->
  16                         (pr0 (TTail (Flat Appl) v1 (TTail (Bind Abst) u t1))
  17                              (TTail (Bind Abbr) v2 t2))
  18          | pr0_upsilon: (b:?) ~b=Abst -> (v1,v2:?) (pr0 v1 v2) ->
  19                         (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
  20                         (pr0 (TTail (Flat Appl) v1 (TTail (Bind b) u1 t1))
  21                              (TTail (Bind b) u2 (TTail (Flat Appl) (lift (1) (0) v2) t2)))
  22          | pr0_delta  : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
  23                         (w:?) (subst0 (0) u2 t2 w) ->
  24                         (pr0 (TTail (Bind Abbr) u1 t1) (TTail (Bind Abbr) u2 w))
  25          | pr0_zeta   : (b:?) ~b=Abst -> (t1,t2:?) (pr0 t1 t2) ->
  26                         (u:?) (pr0 (TTail (Bind b) u (lift (1) (0) t1)) t2)
  27          | pr0_epsilon: (t1,t2:?) (pr0 t1 t2) ->
  28                         (u:?) (pr0 (TTail (Flat Cast) u t1) t2).
  29
  30 (*#* #stop file *)
  31
  32       Hint pr0 : ltlc := Constructors pr0.
  33
  34    Section pr0_gen_base. (***************************************************)
  35
  36       Theorem pr0_gen_sort : (x:?; n:?) (pr0 (TSort n) x) -> x = (TSort n).
  37       Intros; Inversion H; XAuto.
  38       Qed.
  39
  40       Theorem pr0_gen_lref : (x:?; n:?) (pr0 (TLRef n) x) -> x = (TLRef n).
  41       Intros; Inversion H; XAuto.
  42       Qed.
  43
  44       Theorem pr0_gen_abst : (u1,t1,x:?) (pr0 (TTail (Bind Abst) u1 t1) x) ->
  45                              (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) &
  46                                          (pr0 u1 u2) & (pr0 t1 t2)
  47                              ).
  48
  49       Intros; Inversion H; Clear H.
  50 (* case 1 : pr0_refl *)
  51       XEAuto.
  52 (* case 2 : pr0_cont *)
  53       XEAuto.
  54 (* case 3 : pr0_zeta *)
  55       XElim H4; XAuto.
  56       Qed.
  57
  58       Theorem pr0_gen_appl : (u1,t1,x:?) (pr0 (TTail (Flat Appl) u1 t1) x) -> (OR
  59                              (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) &
  60                                          (pr0 u1 u2) & (pr0 t1 t2)
  61                              ) |
  62                              (EX y1 z1 u2 t2 | t1 = (TTail (Bind Abst) y1 z1) &
  63                                                x = (TTail (Bind Abbr) u2 t2) &
  64                                                (pr0 u1 u2) & (pr0 z1 t2)
  65                              ) |
  66                              (EX b y1 z1 u2 v2 t2 |
  67                                 ~b=Abst &
  68                                 t1 = (TTail (Bind b) y1 z1) &
  69                                 x = (TTail (Bind b) v2 (TTail (Flat Appl) (lift (1) (0) u2) t2)) &
  70                                 (pr0 u1 u2) & (pr0 y1 v2) & (pr0 z1 t2))
  71                              ).
  72       Intros; Inversion H; XEAuto.
  73       Qed.
  74
  75       Theorem pr0_gen_cast : (u1,t1,x:?) (pr0 (TTail (Flat Cast) u1 t1) x) ->
  76                              (EX u2 t2 | x = (TTail (Flat Cast) u2 t2) &
  77                                          (pr0 u1 u2) & (pr0 t1 t2)
  78                              ) \/
  79                             (pr0 t1 x).
  80       Intros; Inversion H; XEAuto.
  81       Qed.
  82
  83    End pr0_gen_base.
  84
  85       Hints Resolve pr0_gen_sort pr0_gen_lref : ltlc.
  86
  87       Tactic Definition Pr0GenBase :=
  88          Match Context With
  89             | [ H: (pr0 (TSort ?1) ?2) |- ? ] ->
  90                LApply (pr0_gen_sort ?2 ?1); [ Clear H; Intros | XAuto ]
  91             | [ H: (pr0 (TLRef ?1) ?2) |- ? ] ->
  92                LApply (pr0_gen_lref ?2 ?1); [ Clear H; Intros | XAuto ]
  93             | [ H: (pr0 (TTail (Bind Abst) ?1 ?2) ?3) |- ? ] ->
  94                LApply (pr0_gen_abst ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
  95                XElim H; Intros
  96             | [ H: (pr0 (TTail (Flat Appl) ?1 ?2) ?3) |- ? ] ->
  97                LApply (pr0_gen_appl ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
  98                XElim H; Intros H; XElim H; Intros
  99             | [ H: (pr0 (TTail (Flat Cast) ?1 ?2) ?3) |- ? ] ->
 100                LApply (pr0_gen_cast ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
 101                XElim H; [ Intros H; XElim H; Intros | Intros ].