1 Require Export contexts_defs.
2 Require Export drop_defs.
3 Require Export pr0_defs.
5 (*#* #caption "current axioms for the relation $\\CprZ{}{}$",
6 "reflexivity", "compatibility"
8 (*#* #cap #cap c, c1, c2 #alpha u1 in V1, u2 in V2, k in z *)
10 Inductive cpr0 : C -> C -> Prop :=
11 | cpr0_refl : (c:?) (cpr0 c c)
12 | cpr0_comp : (c1,c2:?) (cpr0 c1 c2) -> (u1,u2:?) (pr0 u1 u2) ->
13 (k:?) (cpr0 (CTail c1 k u1) (CTail c2 k u2)).
17 Hint cpr0 : ltlc := Constructors cpr0.
19 Section cpr0_drop. (******************************************************)
21 Theorem cpr0_drop : (c1,c2:?) (cpr0 c1 c2) -> (h:?; e1:?; u1:?; k:?)
22 (drop h (0) c1 (CTail e1 k u1)) ->
23 (EX e2 u2 | (drop h (0) c2 (CTail e2 k u2)) &
24 (cpr0 e1 e2) & (pr0 u1 u2)
26 Intros until 1; XElim H.
27 (* case 1 : cpr0_refl *)
29 (* case 2 : cpr0_comp *)
31 (* case 2.1 : h = 0 *)
33 Inversion H2; Rewrite H6 in H1; Rewrite H4 in H; XEAuto.
34 (* case 2.2 : h > 0 *)
35 XElim k; Intros; DropGenBase.
36 (* case 2.2.1 : Bind *)
37 LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
39 (* case 2.2.2 : Flat *)
40 LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
44 Theorem cpr0_drop_back : (c1,c2:?) (cpr0 c2 c1) -> (h:?; e1:?; u1:?; k:?)
45 (drop h (0) c1 (CTail e1 k u1)) ->
46 (EX e2 u2 | (drop h (0) c2 (CTail e2 k u2)) &
47 (cpr0 e2 e1) & (pr0 u2 u1)
49 Intros until 1; XElim H.
50 (* case 1 : cpr0_refl *)
52 (* case 2 : cpr0_comp *)
54 (* case 2.1 : h = 0 *)
56 Inversion H2; Rewrite H6 in H1; Rewrite H4 in H; XEAuto.
57 (* case 2.2 : h > 0 *)
58 XElim k; Intros; DropGenBase.
59 (* case 2.2.1 : Bind *)
60 LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
62 (* case 2.2.2 : Flat *)
63 LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
69 Tactic Definition Cpr0Drop :=
71 | [ _: (drop ?1 (0) ?2 (CTail ?3 ?4 ?5));
72 _: (cpr0 ?2 ?6) |- ? ] ->
73 LApply (cpr0_drop ?2 ?6); [ Intros H_x | XAuto ];
74 LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
76 | [ _: (drop ?1 (0) ?2 (CTail ?3 ?4 ?5));
77 _: (cpr0 ?6 ?2) |- ? ] ->
78 LApply (cpr0_drop_back ?2 ?6); [ Intros H_x | XAuto ];
79 LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
81 | [ _: (drop ?1 (0) (CTail ?2 ?7 ?8) (CTail ?3 ?4 ?5));
82 _: (cpr0 ?2 ?6) |- ? ] ->
83 LApply (cpr0_drop (CTail ?2 ?7 ?8) (CTail ?6 ?7 ?8)); [ Intros H_x | XAuto ];
84 LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
86 | [ _: (drop ?1 (0) (CTail ?2 ?7 ?8) (CTail ?3 ?4 ?5));
87 _: (cpr0 ?6 ?2) |- ? ] ->
88 LApply (cpr0_drop_back (CTail ?2 ?7 ?8) (CTail ?6 ?7 ?8)); [ Intros H_x | XAuto ];
89 LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];