3 Require Export subst0_defs.
5 Inductive pr0 : T -> T -> Prop :=
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))
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).
26 Hint pr0 : ltlc := Constructors pr0.
28 Section pr0_gen. (********************************************************)
30 Theorem pr0_gen_sort : (x:?; n:?) (pr0 (TSort n) x) -> x = (TSort n).
31 Intros; Inversion H; XAuto.
34 Theorem pr0_gen_bref : (x:?; n:?) (pr0 (TBRef n) x) -> x = (TBRef n).
35 Intros; Inversion H; XAuto.
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)
43 Intros; Inversion H; Clear H.
44 (* case 1 : pr0_refl *)
46 (* case 2 : pr0_cont *)
48 (* case 3 : pr0_zeta *)
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)
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)
60 (EX b y1 z1 u2 v2 t2 |
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))
66 Intros; Inversion H; XEAuto.
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)
74 Intros; Inversion H; XEAuto.
79 Hints Resolve pr0_gen_sort pr0_gen_bref : ltlc.
81 Tactic Definition Pr0GenBase :=
83 | [ H: (pr0 (TTail (Bind Abst) ?1 ?2) ?3) |- ? ] ->
84 LApply (pr0_gen_abst ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
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 ].