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

   1 (*#* #stop file *)
   2
   3 Require Export subst0_defs.
   4
   5       Inductive pr0 : T -> T -> Prop :=
   6 (* structural rules *)
   7          | pr0_refl  : (t:?) (pr0 t t)
   8          | pr0_thin  : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
   9                        (k:?) (pr0 (TTail k u1 t1) (TTail k u2 t2))
  10 (* axiom rules *)
  11          | pr0_beta  : (k,v1,v2:?) (pr0 v1 v2) -> (t1,t2:?) (pr0 t1 t2) ->
  12                        (pr0 (TTail (Flat Appl) v1 (TTail (Bind Abst) k t1))
  13                             (TTail (Bind Abbr) v2 t2))
  14          | pr0_gamma : (b:?) ~b=Abst -> (v1,v2:?) (pr0 v1 v2) ->
  15                        (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
  16                        (pr0 (TTail (Flat Appl) v1 (TTail (Bind b) u1 t1))
  17                             (TTail (Bind b) u2 (TTail (Flat Appl) (lift (1) (0) v2) t2)))
  18          | pr0_delta : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
  19                        (w:?) (subst0 (0) u2 t2 w) ->
  20                        (pr0 (TTail (Bind Abbr) u1 t1) (TTail (Bind Abbr) u2 w))
  21          | pr0_zeta  : (b:?) ~b=Abst -> (t1,t2:?) (pr0 t1 t2) ->
  22                        (u:?) (pr0 (TTail (Bind b) u (lift (1) (0) t1)) t2)
  23          | pr0_eps   : (t1,t2:?) (pr0 t1 t2) ->
  24                        (u:?) (pr0 (TTail (Flat Cast) u t1) t2).
  25
  26       Hint pr0 : ltlc := Constructors pr0.
  27
  28    Section pr0_gen. (********************************************************)
  29
  30       Theorem pr0_gen_sort : (x:?; n:?) (pr0 (TSort n) x) -> x = (TSort n).
  31       Intros; Inversion H; XAuto.
  32       Qed.
  33
  34       Theorem pr0_gen_bref : (x:?; n:?) (pr0 (TBRef n) x) -> x = (TBRef n).
  35       Intros; Inversion H; XAuto.
  36       Qed.
  37
  38       Theorem pr0_gen_abst : (u1,t1,x:?) (pr0 (TTail (Bind Abst) u1 t1) x) ->
  39                              (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) &
  40                                          (pr0 u1 u2) & (pr0 t1 t2)
  41                              ).
  42
  43       Intros; Inversion H; Clear H.
  44 (* case 1 : pr0_refl *)
  45       XEAuto.
  46 (* case 2 : pr0_cont *)
  47       XEAuto.
  48 (* case 3 : pr0_zeta *)
  49       XElim H4; XAuto.
  50       Qed.
  51
  52       Theorem pr0_gen_appl : (u1,t1,x:?) (pr0 (TTail (Flat Appl) u1 t1) x) -> (OR
  53                              (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) &
  54                                          (pr0 u1 u2) & (pr0 t1 t2)
  55                              ) |
  56                              (EX y1 z1 u2 t2 | t1 = (TTail (Bind Abst) y1 z1) &
  57                                                x = (TTail (Bind Abbr) u2 t2) &
  58                                                (pr0 u1 u2) & (pr0 z1 t2)
  59                              ) |
  60                              (EX b y1 z1 u2 v2 t2 |
  61                                 ~b=Abst &
  62                                 t1 = (TTail (Bind b) y1 z1) &
  63                                 x = (TTail (Bind b) v2 (TTail (Flat Appl) (lift (1) (0) u2) t2)) &
  64                                 (pr0 u1 u2) & (pr0 y1 v2) & (pr0 z1 t2))
  65                              ).
  66       Intros; Inversion H; XEAuto.
  67       Qed.
  68
  69       Theorem pr0_gen_cast : (u1,t1,x:?) (pr0 (TTail (Flat Cast) u1 t1) x) ->
  70                              (EX u2 t2 | x = (TTail (Flat Cast) u2 t2) &
  71                                          (pr0 u1 u2) & (pr0 t1 t2)
  72                              ) \/
  73                             (pr0 t1 x).
  74       Intros; Inversion H; XEAuto.
  75       Qed.
  76
  77    End pr0_gen.
  78
  79       Hints Resolve pr0_gen_sort pr0_gen_bref : ltlc.
  80
  81       Tactic Definition Pr0GenBase :=
  82          Match Context With
  83             | [ H: (pr0 (TTail (Bind Abst) ?1 ?2) ?3) |- ? ] ->
  84                LApply (pr0_gen_abst ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
  85                XElim H; Intros
  86             | [ H: (pr0 (TTail (Flat Appl) ?1 ?2) ?3) |- ? ] ->
  87                LApply (pr0_gen_appl ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
  88                XElim H; Intros H; XElim H; Intros
  89             | [ H: (pr0 (TTail (Flat Cast) ?1 ?2) ?3) |- ? ] ->
  90                LApply (pr0_gen_cast ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
  91                XElim H; [ Intros H; XElim H; Intros | Intros ].