1 Require Export subst0_defs.
3 (*#* #caption "axioms for the relation $\\PrZ{}{}$",
4 "reflexivity", "compatibility", "$\\beta$-contraction", "$\\upsilon$-swap",
5 "$\\delta$-expansion", "$\\zeta$-contraction", "$\\epsilon$-contraction"
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 *)
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))
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).
32 Hint pr0 : ltlc := Constructors pr0.
34 Section pr0_gen_base. (***************************************************)
36 Theorem pr0_gen_sort : (x:?; n:?) (pr0 (TSort n) x) -> x = (TSort n).
37 Intros; Inversion H; XAuto.
40 Theorem pr0_gen_lref : (x:?; n:?) (pr0 (TLRef n) x) -> x = (TLRef n).
41 Intros; Inversion H; XAuto.
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)
49 Intros; Inversion H; Clear H.
50 (* case 1 : pr0_refl *)
52 (* case 2 : pr0_cont *)
54 (* case 3 : pr0_zeta *)
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)
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)
66 (EX b y1 z1 u2 v2 t2 |
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))
72 Intros; Inversion H; XEAuto.
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)
80 Intros; Inversion H; XEAuto.
85 Hints Resolve pr0_gen_sort pr0_gen_lref : ltlc.
87 Tactic Definition Pr0GenBase :=
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 ];
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 ].