+(*#* #stop file *)
+
Require lift_gen.
Require drop_defs.
Section confluence. (*****************************************************)
-(*#* #stop macro *)
-
Tactic Definition IH :=
Match Context With
[ H1: (drop ?1 ?2 c ?3); H2: (drop ?1 ?2 c ?4) |- ? ] ->
LApply (H ?4 ?2 ?1); [ Clear H H2; Intros H | XAuto ];
LApply (H ?3); [ Clear H H1; Intros | XAuto ].
-(*#* #start macro *)
-
(*#* #caption "confluence, first case" *)
(*#* #cap #alpha c in C, x1 in C1, x2 in C2, d in i *)
Theorem drop_mono : (c,x1:?; d,h:?) (drop h d c x1) ->
(x2:?) (drop h d c x2) -> x1 = x2.
-
-(*#* #stop proof *)
-
XElim c.
(* case 1: CSort *)
Intros; Repeat DropGenBase; Rewrite H0; XAuto.
LiftGen; IH; XAuto.
Qed.
-(*#* #start proof *)
-
(*#* #caption "confluence, second case" *)
(*#* #cap #alpha c in C1, c0 in E1, e in C2, e0 in E2, u in V1, v in V2, i in k, d in i *)
(drop i (0) e (CTail e0 (Bind b) v)) &
(drop h d c0 e0)
).
-
-(*#* #stop proof *)
-
XElim i.
(* case 1 : i = 0 *)
Intros until 1.
XElim H; XEAuto.
Qed.
-(*#* #start proof *)
-
(*#* #caption "confluence, third case" *)
(*#* #cap #alpha c in C, a in C1, e in C2, i in k, d in i *)
Theorem drop_conf_ge: (i:?; a,c:?) (drop i (0) c a) ->
(e:?; h,d:?) (drop h d c e) -> (le (plus d h) i) ->
(drop (minus i h) (0) e a).
-
-(*#* #stop proof *)
-
XElim i.
(* case 1 : i = 0 *)
Intros until 1.
Rewrite <- minus_Sn_m; XEAuto.
Qed.
-(*#* #start proof *)
-
End confluence.
Section transitivity. (***************************************************)
(c1,c2:?; h:?) (drop h d c1 c2) ->
(e2:?) (drop i (0) c2 e2) ->
(EX e1 | (drop i (0) c1 e1) & (drop h (minus d i) e1 e2)).
-
-(*#* #stop proof *)
-
XElim i.
(* case 1 : i = 0 *)
Intros.
XElim IHc; XEAuto.
Qed.
-(*#* #start proof *)
-
(*#* #caption "transitivity, second case" *)
(*#* #cap #alpha c1 in C1, c2 in C, e2 in C2, d in i, i in k *)
Theorem drop_trans_ge : (i:?; c1,c2:?; d,h:?) (drop h d c1 c2) ->
(e2:?) (drop i (0) c2 e2) -> (le d i) ->
(drop (plus i h) (0) c1 e2).
-
-(*#* #stop proof *)
-
XElim i.
(* case 1: i = 0 *)
Intros.
DropGenBase; Apply drop_drop; NewInduction k; Simpl; XEAuto. (**) (* explicit constructor *)
Qed.
-(*#* #start proof *)
-
End transitivity.
-(*#* #stop macro *)
-
Tactic Definition DropDis :=
Match Context With
[ H1: (drop ?1 ?2 ?3 ?4); H2: (drop ?1 ?2 ?3 ?5) |- ? ] ->
LApply (H1 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
LApply H1; [ Clear H1; Intros | XAuto ].
-(*#* #start macro *)
-
(*#* #single *)