1 Require Export pc3_defs.
8 next_lt : (n:?) (lt n (next n));
9 base_next: (n:?) (le base n) -> (next n) = (S n)
14 (*#* #caption "current axioms for typing",
15 "well formed context sort", "well formed context binder",
16 "conversion rule", "typed sort", "typed reference to abbreviation",
17 "typed reference to abstraction", "typed binder", "typed application",
20 (*#* #cap #cap c, d, t, t0, t1, t2, w #alpha m in h, n in i, u in V, v in U *)
22 Inductive wf0 [g:G] : C -> Prop :=
23 | wf0_sort: (m:?) (wf0 g (CSort m))
24 | wf0_bind: (c:?; u,t:?) (ty0 g c u t) ->
25 (b:?) (wf0 g (CTail c (Bind b) u))
26 with ty0 [g:G] : C -> T -> T -> Prop :=
27 (* structural rules *)
28 | ty0_conv: (c:?; t2,t:?) (ty0 g c t2 t) ->
29 (u,t1:?) (ty0 g c u t1) -> (pc3 c t1 t2) ->
32 | ty0_sort: (c:?) (wf0 g c) ->
33 (m:?) (ty0 g c (TSort m) (TSort (next g m)))
34 | ty0_abbr: (c:?) (wf0 g c) ->
35 (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abbr) u)) ->
36 (t:?) (ty0 g d u t) ->
37 (ty0 g c (TLRef n) (lift (S n) (0) t))
38 | ty0_abst: (c:?) (wf0 g c) ->
39 (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abst) u)) ->
40 (t:?) (ty0 g d u t) ->
41 (ty0 g c (TLRef n) (lift (S n) (0) u))
42 | ty0_bind: (c:?; u,t:?) (ty0 g c u t) ->
43 (b:?; t1,t2:?) (ty0 g (CTail c (Bind b) u) t1 t2) ->
44 (t0:?) (ty0 g (CTail c (Bind b) u) t2 t0) ->
45 (ty0 g c (TTail (Bind b) u t1) (TTail (Bind b) u t2))
46 | ty0_appl: (c:?; w,u:?) (ty0 g c w u) ->
47 (v,t:?) (ty0 g c v (TTail (Bind Abst) u t)) ->
48 (ty0 g c (TTail (Flat Appl) w v)
49 (TTail (Flat Appl) w (TTail (Bind Abst) u t))
51 | ty0_cast: (c:?; t1,t2:?) (ty0 g c t1 t2) ->
52 (t0:?) (ty0 g c t2 t0) ->
53 (ty0 g c (TTail (Flat Cast) t2 t1) t2).
57 Hint wf0 : ltlc := Constructors wf0.
59 Hint ty0 : ltlc := Constructors ty0.
61 Section wf0_props. (******************************************************)
63 Theorem wf0_ty0: (g:?; c:?; u,t:?) (ty0 g c u t) -> (wf0 g c).
64 Intros; XElim H; XAuto.
67 Hints Resolve wf0_ty0 : ltlc.
69 Theorem wf0_drop_O: (c,e:?; h:?) (drop h (0) c e) ->
70 (g:?) (wf0 g c) -> (wf0 g e).
73 Intros; DropGenBase; Rewrite H; XAuto.
74 (* case 2 : CTail k *)
75 Intros c IHc; XElim k; (
76 XElim h; Intros; DropGenBase;
77 [ Rewrite H in H0; XAuto | Inversion H1; XEAuto ] ).
82 Hints Resolve wf0_ty0 wf0_drop_O : ltlc.
84 Tactic Definition Wf0Ty0 :=
86 [ _: (ty0 ?1 ?2 ?3 ?4) |- ? ] ->
87 LApply (wf0_ty0 ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
90 Tactic Definition Wf0DropO :=
92 | [ _: (drop ?1 (0) ?2 ?3); _: (wf0 ?4 ?2) |- ? ] ->
93 LApply (wf0_drop_O ?2 ?3 ?1); [ Intros H_x | XAuto ];
94 LApply (H_x ?4); [ Clear H_x; Intros | XAuto ].
96 Section wf0_facilities. (*************************************************)
98 Theorem wf0_drop_wf0: (g:?; c:?) (wf0 g c) ->
100 (drop h (0) c (CTail e (Bind b) u)) -> (wf0 g e).
102 Wf0DropO; Inversion H1; XEAuto.
105 Theorem ty0_drop_wf0: (g:?; c:?; t1,t2:?) (ty0 g c t1 t2) ->
107 (drop h (0) c (CTail e (Bind b) u)) -> (wf0 g e).
109 EApply wf0_drop_wf0; [ Idtac | EApply H0 ]; XEAuto.
114 Hints Resolve wf0_drop_wf0 ty0_drop_wf0 : ltlc.
116 Tactic Definition DropWf0 :=
118 | [ _: (ty0 ?1 ?2 ?3 ?4);
119 _: (drop ?5 (0) ?2 (CTail ?6 (Bind ?7) ?8)) |- ? ] ->
120 LApply (ty0_drop_wf0 ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
121 LApply (H_x ?7 ?6 ?8 ?5); [ Clear H_x; Intros | XAuto ]
123 _: (drop ?5 (0) ?2 (CTail ?6 (Bind ?7) ?8)) |- ? ] ->
124 LApply (wf0_drop_wf0 ?1 ?2); [ Intros H_x | XAuto ];
125 LApply (H_x ?7 ?6 ?8 ?5); [ Clear H_x; Intros | XAuto ].