3 Require Export drop_defs.
4 Require Export pr0_defs.
6 Inductive pr2 [c:C; t1,t2:T] : Prop :=
8 | pr2_pr0 : (pr0 t1 t2) -> (pr2 c t1 t2)
10 | pr2_delta : (d:?; u:?; i:?)
11 (drop i (0) c (CTail d (Bind Abbr) u)) ->
12 (subst0 i u t1 t2) -> (pr2 c t1 t2).
14 Hint pr2 : ltlc := Constructors pr2.
16 Section pr2_gen_base. (***************************************************)
18 Theorem pr2_gen_sort : (c:?; x:?; n:?) (pr2 c (TSort n) x) ->
21 Try Subst0GenBase; XEAuto.
24 Theorem pr2_gen_bref : (c:?; x:?; n:?) (pr2 c (TBRef n) x) ->
26 (EX d u | (drop n (0) c (CTail d (Bind Abbr) u)) &
27 x = (lift (S n) (0) u)
30 Try Subst0GenBase; Try Rewrite <- H1 in H0; XEAuto.
33 Theorem pr2_gen_abst : (c:?; u1,t1,x:?)
34 (pr2 c (TTail (Bind Abst) u1 t1) x) ->
35 (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) &
36 (pr2 c u1 u2) & (b:?; u:?)
37 (pr2 (CTail c (Bind b) u) t1 t2)
40 Try Pr0GenBase; Try Subst0GenBase; XDEAuto 6.
43 Theorem pr2_gen_appl : (c:?; u1,t1,x:?)
44 (pr2 c (TTail (Flat Appl) u1 t1) x) -> (OR
45 (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) &
46 (pr2 c u1 u2) & (pr2 c t1 t2)
48 (EX y1 z1 u2 t2 | t1 = (TTail (Bind Abst) y1 z1) &
49 x = (TTail (Bind Abbr) u2 t2) &
50 (pr0 u1 u2) & (pr0 z1 t2)
52 (EX b y1 z1 u2 v2 t2 |
54 t1 = (TTail (Bind b) y1 z1) &
55 x = (TTail (Bind b) v2 (TTail (Flat Appl) (lift (1) (0) u2) t2)) &
56 (pr0 u1 u2) & (pr0 y1 v2) & (pr0 z1 t2))
59 Try Pr0GenBase; Try Subst0GenBase; XEAuto.
62 Theorem pr2_gen_cast : (c:?; u1,t1,x:?)
63 (pr2 c (TTail (Flat Cast) u1 t1) x) ->
64 (EX u2 t2 | x = (TTail (Flat Cast) u2 t2) &
65 (pr2 c u1 u2) & (pr2 c t1 t2)
69 Try Pr0GenBase; Try Subst0GenBase; XEAuto.
74 Tactic Definition Pr2GenBase :=
76 | [ H: (pr2 ?1 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] ->
77 LApply (pr2_gen_abst ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
80 Section pr2_props. (******************************************************)
82 Theorem pr2_thin_dx : (c:?; t1,t2:?) (pr2 c t1 t2) ->
83 (u:?; f:?) (pr2 c (TTail (Flat f) u t1)
84 (TTail (Flat f) u t2)).
85 Intros; Inversion H; XEAuto.
88 Theorem pr2_tail_1 : (c:?; u1,u2:?) (pr2 c u1 u2) ->
89 (k:?; t:?) (pr2 c (TTail k u1 t) (TTail k u2 t)).
90 Intros; Inversion H; XEAuto.
93 Theorem pr2_tail_2 : (c:?; u,t1,t2:?; k:?) (pr2 (CTail c k u) t1 t2) ->
94 (pr2 c (TTail k u t1) (TTail k u t2)).
96 (Inversion H; [ XAuto | Clear H ];
97 (NewInduction i; DropGenBase; [ Inversion H; XEAuto | XEAuto ])).
100 Hints Resolve pr2_tail_2 : ltlc.
102 Theorem pr2_shift : (i:?; c,e:?) (drop i (0) c e) ->
103 (t1,t2:?) (pr2 c t1 t2) ->
104 (pr2 e (app c i t1) (app c i t2)).
108 DropGenBase; Rewrite H in H0.
109 Repeat Rewrite app_O; XAuto.
112 (* case 2.1 : CSort *)
113 Intros; DropGenBase; Rewrite H0; XAuto.
114 (* case 2.2 : CTail *)
115 XElim k; Intros; Simpl; DropGenBase; XAuto.
120 Hints Resolve pr2_thin_dx pr2_tail_1 pr2_tail_2 pr2_shift : ltlc.