Library mcertikos.invariants.INVLemmaContainer
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import Constant.
Require Import XOmega.
Require Import AbstractDataType.
Require Import ObjContainer.
Lemma empty_container_valid : Container_valid (ZMap.init Container_unused).
Proof.
constructor; simpl; intros; try rewrite ZMap.gi in *; simpl; auto; try discriminate.
Qed.
Ltac container_destruct_case_eq i :=
case_eq (zeq i 0); intros; subst;
[ | case_eq (zeq i 1); intros; subst;
[ | case_eq (zeq i 2); intros; subst;
[ | case_eq (zeq i 3); intros; subst;
[ | case_eq (zeq i 4); intros; subst;
[ | case_eq (zeq i 5); intros; subst;
[ | case_eq (zeq i 6); intros; subst;
[ | case_eq (zeq i 7); intros; subst;
[ | case_eq (zeq i 8); intros; subst]]]]]]]].
Lemma AC_init_real_container_valid: Container_valid init_real_container.
Proof.
unfold init_real_container; simpl.
constructor; simpl.
- intros.
container_destruct_case_eq i; try omega.
do 9 (rewrite ZMap.gso in H; try assumption).
rewrite ZMap.gi in H; simpl in H; inv H.
- intros.
container_destruct_case_eq i.
+ do 8 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; split; intros; assumption.
+ do 7 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; split; intros; assumption.
+ do 6 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; split; intros; assumption.
+ do 5 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; split; intros; assumption.
+ do 4 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; split; intros; assumption.
+ do 3 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; split; intros; assumption.
+ do 2 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; split; intros; assumption.
+ do 1 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; split; intros; assumption.
+ rewrite ZMap.gss; simpl in *; split; intros; assumption.
+ do 9 (rewrite ZMap.gso in H; [ | assumption]).
rewrite ZMap.gi in H; simpl in H; inv H.
- intros.
assert (720896/8 = 90112) by xomega.
assert (Integers.Int.max_unsigned = 4294967295).
{ unfold Integers.Int.max_unsigned; simpl; reflexivity. }
container_destruct_case_eq i.
+ do 8 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 7 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 6 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 5 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 4 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 3 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 2 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 1 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ rewrite ZMap.gss; simpl in *; omega.
+ do 9 (rewrite ZMap.gso in H; [ | assumption]).
rewrite ZMap.gi in H; simpl in H; inv H.
- intros.
assert (720896/8 = 90112) by xomega.
container_destruct_case_eq i.
+ do 8 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 7 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 6 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 5 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 4 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 3 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 2 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 1 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ rewrite ZMap.gss; simpl in *; omega.
+ do 9 (rewrite ZMap.gso in H; [ | assumption]).
rewrite ZMap.gi in H; simpl in H; inv H.
- intros.
container_destruct_case_eq i; try (simpl; reflexivity; fail).
do 9 (rewrite ZMap.gso in H; [ | assumption]).
rewrite ZMap.gi in H; simpl in H; inv H.
- intros.
container_destruct_case_eq i; try (simpl; repeat (constructor; simpl; try reflexivity)).
do 9 (rewrite ZMap.gso in H; [ | assumption]).
rewrite ZMap.gi in H; simpl in H; inv H.
- intros.
container_destruct_case_eq i; try (simpl; tauto; fail).
do 9 (rewrite ZMap.gso in H; [ | assumption]).
rewrite ZMap.gi in H; simpl in H; inv H.
- intros.
container_destruct_case_eq i; try (simpl; unfold init_container; simpl; repeat (constructor; simpl; auto); fail).
do 9 (rewrite ZMap.gso in H; [ | assumption]).
rewrite ZMap.gi in H; simpl in H; inv H.
- intros.
assert (720896/8 = 90112) by xomega.
assert (720896 = 0 + 90112 + 90112 + 90112 + 90112 + 90112 + 90112 + 90112 + 90112) by omega.
container_destruct_case_eq i; simpl; try (rewrite H1; repeat econstructor; simpl; eauto; try omega; fail).
do 9 (rewrite ZMap.gso in H; [ | assumption]).
rewrite ZMap.gi in H; simpl in H; inv H.
- intros.
container_destruct_case_eq i;
repeat (constructor; try intro contra; try repeat (destruct contra as [? | contra]); try omega; try inv contra).
do 9 (rewrite ZMap.gso in H; [ | assumption]).
rewrite ZMap.gi in H; simpl in H; inv H.
Qed.
Lemma AC_init_container_valid : Container_valid AC_init.
Proof.
unfold AC_init.
generalize AC_init_real_container_valid; intros; auto.
Qed.
Lemma math_false_aux:
∀ id n,
id × max_children + 1 + n = 0 →
0 ≤ id < num_proc →
0 ≤ n →
False.
Proof.
clear.
intros. omega.
Qed.
Lemma split_container_valid:
∀ id q ac
(Hvalid: Container_valid ac),
let c := ZMap.get id ac in
let child := {|
cquota := q;
cusage := 0;
cparent := id;
cchildren := nil;
cused := true |} in
let i := id × max_children + 1 + Z.of_nat (length (cchildren c)) in
let cur := {|
cquota := cquota c;
cusage := cusage c + q;
cparent := cparent c;
cchildren := i :: cchildren c;
cused := cused c |} in
∀ (Hrangei: 0 ≤ i < num_proc)
(Hj_unused: cused (ZMap.get i ac) = false)
(Hused: cused c = true)
(Hrangeq: 0 ≤ q ≤ (cquota c - cusage c)),
Container_valid (ZMap.set i child (ZMap.set id cur ac)).
Proof.
intros. inv Hvalid. subst c.
constructor; simpl; intros;
rename i0 into i´, H into Hused´.
-
destruct (zeq i´ i); try subst i´.
omega.
rewrite ZMap.gso in Hused´; auto.
destruct (zeq i´ id); try subst i´.
apply (cvalid_id _ Hused).
rewrite ZMap.gso in Hused´; auto.
-
destruct (zeq i´ i); try subst i´.
+ rewrite ZMap.gss; simpl.
split; intro Heq; subst.
× rewrite <- Heq in Hused; rewrite Hj_unused in Hused; inv Hused.
× rewrite ZMap.gss in Hused´.
eapply cvalid_id in Hused.
set (n := (length (cchildren (ZMap.get id ac)))) in ×.
specialize (Nat2Z.is_nonneg n). intros.
eapply math_false_aux in Heq; eauto. inv Heq.
+ rewrite ZMap.gso; auto.
destruct (zeq i´ id); try subst i´.
rewrite ZMap.gss; simpl; auto.
rewrite ZMap.gso; auto.
rewrite 2 ZMap.gso in Hused´; auto.
-
destruct (zeq i´ i); try subst i´.
+ rewrite ZMap.gss in *; simpl.
specialize (cvalid_quota id Hused).
specialize (cvalid_usage id Hused).
omega.
+ rewrite ZMap.gso; auto.
destruct (zeq i´ id); try subst i´.
× rewrite ZMap.gss; simpl; try omega.
apply cvalid_quota; assumption.
× rewrite 2 ZMap.gso in Hused´; auto.
rewrite ZMap.gso; auto.
-
destruct (zeq i´ i); try subst i´.
+ rewrite ZMap.gss; simpl; omega.
+ rewrite ZMap.gso; auto.
destruct (zeq i´ id); try subst i´.
× rewrite ZMap.gss; simpl; split; try omega.
apply Z.add_nonneg_nonneg; auto; try omega.
rewrite ZMap.gso in Hused´; auto; rewrite ZMap.gss in Hused´.
apply cvalid_usage; auto.
× rewrite ZMap.gso; auto.
rewrite 2 ZMap.gso in Hused´; auto.
-
destruct (zeq i´ i); try subst i´.
+ rewrite ZMap.gss; simpl.
destruct (zeq id i) as [eq|neq].
rewrite eq; rewrite ZMap.gss; auto.
rewrite ZMap.gso; auto; rewrite ZMap.gss; auto.
+ rewrite ZMap.gso in Hused´; auto.
replace (ZMap.get i´ (ZMap.set i child (ZMap.set id cur ac)))
with (ZMap.get i´ (ZMap.set id cur ac)).
× destruct (zeq i´ id); try subst i´.
{
rewrite ZMap.gss; simpl.
destruct (zeq (cparent (ZMap.get id ac)) i) as [eq1|neq1].
{
rewrite eq1; rewrite ZMap.gss; auto.
}
{
rewrite ZMap.gso; auto.
destruct (zeq (cparent (ZMap.get id ac)) id) as [eq2|neq2].
{
rewrite eq2; rewrite ZMap.gss; auto.
}
{
rewrite ZMap.gso; auto.
}
}
}
{
replace (ZMap.get i´ (ZMap.set id cur ac)) with (ZMap.get i´ ac).
{
destruct (zeq (cparent (ZMap.get i´ ac)) i) as [eq1|neq1].
{
rewrite eq1; rewrite ZMap.gss; auto.
}
{
rewrite ZMap.gso; auto.
destruct (zeq (cparent (ZMap.get i´ ac)) id) as [eq2|neq2].
{
rewrite eq2; rewrite ZMap.gss; auto.
}
{
rewrite ZMap.gso; auto.
rewrite ZMap.gso in Hused´; auto; apply cvalid_parent_used.
}
}
}
{
rewrite ZMap.gso; auto.
}
}
× symmetry; rewrite ZMap.gso; auto.
-
destruct (zeq i´ i) as [Heq|Hneq]; try subst i´.
rewrite ZMap.gss; simpl; apply Forall_nil.
rewrite ZMap.gso; auto.
destruct (zeq i´ id) as [Heq´|Hneq´]; try subst i´.
+ rewrite ZMap.gso in Hused´; auto.
rewrite ZMap.gss in Hused´ |- *; simpl.
apply Forall_cons.
rewrite ZMap.gss; auto.
apply Forall_forall; intros k Hin.
destruct (zeq k i); try subst k.
rewrite ZMap.gss; auto.
rewrite ZMap.gso; auto.
destruct (zeq k id); try subst k.
rewrite ZMap.gss; auto.
rewrite ZMap.gso; auto.
specialize (cvalid_children_used _ Hused).
rewrite Forall_forall in cvalid_children_used.
apply (cvalid_children_used k Hin).
+ rewrite 2 ZMap.gso in Hused´; auto.
rewrite ZMap.gso; auto.
apply Forall_forall; intros k Hin.
destruct (zeq k i); try subst k.
specialize (cvalid_children_used _ Hused´).
rewrite Forall_forall in cvalid_children_used.
specialize (cvalid_children_used _ Hin).
rewrite Hj_unused in cvalid_children_used; inv cvalid_children_used.
rewrite ZMap.gso; auto.
specialize (cvalid_children_used _ Hused´).
rewrite Forall_forall in cvalid_children_used.
specialize (cvalid_children_used _ Hin).
destruct (zeq k id); try subst k.
rewrite ZMap.gss; auto.
rewrite ZMap.gso; auto.
-
rename H0 into Hi´_neq.
destruct (zeq i´ i) as [Heq|Hneq]; try subst i´.
+ rewrite ZMap.gss; simpl.
destruct (zeq id i) as [Heq´|Hneq´].
rewrite Heq´ in Hused; rewrite Hj_unused in Hused; inv Hused.
rewrite ZMap.gso; auto; rewrite ZMap.gss; simpl; auto.
+ rewrite (ZMap.gso _ _ Hneq); auto.
destruct (zeq i´ id) as [Heq´|Hneq´]; try subst i´.
rewrite ZMap.gss; simpl.
destruct (zeq (cparent (ZMap.get id ac)) i) as [Heq1|Hneq1].
specialize (cvalid_parent_used id Hused); rewrite Heq1 in cvalid_parent_used.
rewrite Hj_unused in cvalid_parent_used; inv cvalid_parent_used.
rewrite ZMap.gso; auto.
destruct (zeq (cparent (ZMap.get id ac)) id) as [Heq2|Hneq2].
rewrite Heq2; rewrite ZMap.gss; simpl; right.
specialize (cvalid_parents_child id Hused Hi´_neq).
rewrite Heq2 in cvalid_parents_child; auto.
rewrite ZMap.gso; auto.
rewrite 2 ZMap.gso in Hused´; auto.
rewrite (ZMap.gso _ _ Hneq´); auto.
destruct (zeq (cparent (ZMap.get i´ ac)) i) as [Heq1|Hneq1].
specialize (cvalid_parent_used i´ Hused´); rewrite Heq1 in cvalid_parent_used.
rewrite Hj_unused in cvalid_parent_used; inv cvalid_parent_used.
rewrite ZMap.gso; auto.
destruct (zeq (cparent (ZMap.get i´ ac)) id) as [Heq2|Hneq2].
rewrite Heq2; rewrite ZMap.gss; simpl; right.
specialize (cvalid_parents_child i´ Hused´ Hi´_neq); rewrite Heq2 in cvalid_parents_child; auto.
rewrite ZMap.gso; auto.
-
destruct (zeq i´ i) as [Heq|Hneq]; try subst i´.
rewrite ZMap.gss; simpl; constructor.
rewrite ZMap.gso; auto.
destruct (zeq i´ id) as [Heq´|Hneq´]; try subst i´.
+ rewrite ZMap.gss; simpl; constructor.
rewrite ZMap.gss; auto.
apply Forall_forall; intros k Hin.
destruct (zeq k i); try subst k.
rewrite ZMap.gss; auto.
rewrite ZMap.gso; auto.
specialize (cvalid_childrens_parent _ Hused).
rewrite Forall_forall in cvalid_childrens_parent.
specialize (cvalid_childrens_parent k Hin).
destruct (zeq k id); try subst k.
rewrite ZMap.gss; auto.
rewrite ZMap.gso; auto.
+ rewrite 2 ZMap.gso in Hused´; auto.
rewrite ZMap.gso; auto.
apply Forall_forall; intros k Hin.
destruct (zeq k i); try subst k.
specialize (cvalid_children_used _ Hused´).
rewrite Forall_forall in cvalid_children_used.
specialize (cvalid_children_used _ Hin).
rewrite Hj_unused in cvalid_children_used; inv cvalid_children_used.
rewrite ZMap.gso; auto.
specialize (cvalid_childrens_parent _ Hused´).
rewrite Forall_forall in cvalid_childrens_parent.
specialize (cvalid_childrens_parent _ Hin).
destruct (zeq k id); try subst k.
rewrite ZMap.gss; auto.
rewrite ZMap.gso; auto.
-
destruct (zeq i´ i) as [Heq|Hneq]; try subst i´.
rewrite ZMap.gss; simpl; constructor; reflexivity.
rewrite ZMap.gso; auto.
destruct (zeq i´ id) as [Heq´|Hneq´]; try subst i´.
+ rewrite ZMap.gso in Hused´; auto; rewrite ZMap.gss in Hused´.
rewrite ZMap.gss; simpl; constructor.
rewrite ZMap.gss; simpl; omega.
apply cqb_notin.
apply cqb_weaken.
apply cvalid_cqb; auto.
split; try reflexivity; simpl.
specialize (cvalid_usage _ Hused); omega.
specialize (cvalid_children_used _ Hused).
rewrite Forall_forall in cvalid_children_used.
intro Hin; specialize (cvalid_children_used _ Hin).
rewrite Hj_unused in cvalid_children_used; inv cvalid_children_used.
+ rewrite 2 ZMap.gso in Hused´; auto.
rewrite ZMap.gso; auto.
apply cqb_notin.
apply cqb_weaken.
apply cvalid_cqb; auto.
split; try reflexivity; simpl.
specialize (cvalid_usage _ Hused); omega.
specialize (cvalid_children_used _ Hused´).
rewrite Forall_forall in cvalid_children_used.
intro Hin; specialize (cvalid_children_used _ Hin).
rewrite Hj_unused in cvalid_children_used; inv cvalid_children_used.
-
destruct (zeq i´ i) as [Heq|Hneq]; try subst i´.
rewrite ZMap.gss; simpl; constructor.
rewrite ZMap.gso; auto.
destruct (zeq i´ id) as [Heq´|Hneq´]; try subst i´.
rewrite ZMap.gss; simpl; constructor.
specialize (cvalid_children_used _ Hused).
rewrite Forall_forall in cvalid_children_used.
intro Hin; specialize (cvalid_children_used _ Hin).
rewrite Hj_unused in cvalid_children_used; inv cvalid_children_used.
apply cvalid_nodup; auto.
rewrite 2 ZMap.gso in Hused´; auto.
rewrite ZMap.gso; auto.
Qed.
Lemma alloc_container_valid´:
∀ i (ac: ContainerPool),
let c := ZMap.get i ac in
let cur := mkContainer (cquota c) (cusage c + 1) (cparent c)
(cchildren c) (cused c) in
Container_valid ac →
(cusage c <? cquota c) = true →
cused c = true →
Container_valid (ZMap.set i cur ac).
Proof.
intros. destruct H.
econstructor; eauto 1; simpl; intros.
-
destruct (zeq i0 i); subst.
rewrite ZMap.gss in H; auto.
rewrite ZMap.gso in H; auto.
-
destruct (zeq i0 i); subst.
rewrite ZMap.gss in H |- *; simpl.
subst c; auto.
rewrite ZMap.gso in H |- *; auto.
-
destruct (zeq i0 i); subst.
rewrite ZMap.gss in *; simpl.
apply cvalid_quota; auto.
rewrite ZMap.gso in H |- *; auto.
-
destruct (zeq i0 i); subst.
rewrite ZMap.gss in *; simpl.
rewrite Z.ltb_lt in H0.
specialize (cvalid_usage _ H); subst c; omega.
rewrite ZMap.gso in H |- *; auto.
-
destruct (zeq i0 i) as [Heq|Hneq]; subst.
rewrite ZMap.gss in *; simpl.
destruct (zeq (cparent c) i) as [Heq´|Hneq´].
rewrite Heq´; rewrite ZMap.gss; auto.
subst c; rewrite ZMap.gso; auto.
rewrite (ZMap.gso _ _ Hneq); auto; simpl.
destruct (zeq (cparent (ZMap.get i0 ac)) i) as [Heq´´|Hneq´´].
rewrite Heq´´; rewrite ZMap.gss in *; simpl; auto.
rewrite ZMap.gso in *; auto.
-
apply Forall_forall; intros i´´ Hin.
destruct (zeq i´´ i); subst.
rewrite ZMap.gss; simpl; auto.
rewrite ZMap.gso; auto.
destruct (zeq i0 i); subst.
rewrite ZMap.gss in H, Hin; simpl in H, Hin.
specialize (cvalid_children_used _ H).
rewrite Forall_forall in cvalid_children_used; auto.
rewrite ZMap.gso in H, Hin; auto.
specialize (cvalid_children_used _ H).
rewrite Forall_forall in cvalid_children_used; auto.
-
rename H2 into Hi´_neq.
destruct (zeq i0 i) as [Heq|Hneq]; subst.
rewrite ZMap.gss; simpl.
destruct (zeq (cparent c) i) as [Heq´|Hneq´].
rewrite Heq´; rewrite ZMap.gss in *; simpl.
specialize (cvalid_parents_child _ H1 Hi´_neq).
subst c; rewrite Heq´ in cvalid_parents_child; auto.
rewrite ZMap.gso; auto.
specialize (cvalid_parents_child _ H1 Hi´_neq); auto.
rewrite (ZMap.gso _ _ Hneq) in H |- *; auto.
destruct (zeq (cparent (ZMap.get i0 ac)) i) as [Heq´´|Hneq´´].
specialize (cvalid_parents_child _ H Hi´_neq).
rewrite Heq´´ in cvalid_parents_child; rewrite Heq´´; rewrite ZMap.gss; simpl; auto.
rewrite ZMap.gso; auto.
-
apply Forall_forall; intros i´´ Hin.
destruct (zeq i´´ i); subst.
rewrite ZMap.gss; simpl.
destruct (zeq i0 i); subst.
rewrite ZMap.gss in H, Hin; simpl in H, Hin.
specialize (cvalid_childrens_parent _ H).
rewrite Forall_forall in cvalid_childrens_parent; subst c; auto.
rewrite ZMap.gso in H, Hin; auto.
specialize (cvalid_childrens_parent _ H).
rewrite Forall_forall in cvalid_childrens_parent; subst c; auto.
rewrite ZMap.gso; auto.
destruct (zeq i0 i); subst.
rewrite ZMap.gss in H, Hin; simpl in H, Hin.
specialize (cvalid_childrens_parent _ H).
rewrite Forall_forall in cvalid_childrens_parent; subst c; auto.
rewrite ZMap.gso in H, Hin; auto.
specialize (cvalid_childrens_parent _ H).
rewrite Forall_forall in cvalid_childrens_parent; subst c; auto.
-
apply cqb_weaken; simpl.
destruct (zeq i0 i); subst.
rewrite ZMap.gss; simpl.
apply cqb_bound with (n1 := cusage c); try omega.
subst c; auto.
rewrite ZMap.gso in H |- *; auto.
specialize (cvalid_usage _ H1); subst c; omega.
-
destruct (zeq i0 i); subst.
rewrite ZMap.gss; simpl; subst c; auto.
rewrite ZMap.gso in H |- *; auto.
Qed.
Lemma alloc_container_valid i adt adt´ z :
Container_valid (AC adt) →
container_alloc_spec i adt = Some (adt´,z) →
Container_valid (AC adt´).
Proof.
intros. functional inversion H0.
eapply alloc_container_valid´; eauto.
subst. assumption.
Qed.
Lemma container_split_some :
∀ (d: RData) id q,
let c := ZMap.get id (AC d) in
let i := id × max_children + 1 + Z_of_nat (length (cchildren c)) in
let child := mkContainer q 0 id nil true in
ikern d = true → ihost d = true → cused (ZMap.get id (AC d)) = true →
cused (ZMap.get i (AC d)) = false →
0 ≤ i < num_proc → Z_of_nat (length (cchildren c)) < max_children →
0 ≤ q ≤ cquota c - cusage c →
let parent := mkContainer (cquota c) (cusage c + q) (cparent c) (i :: cchildren c) (cused c) in
container_split_spec id q d =
Some (d {AC: ZMap.set i child
(ZMap.set id parent (AC d))}, i).
Proof.
unfold container_split_spec; intros.
rewrite H, H0, H1, H2.
repeat (match goal with
| [ |- context [if ?a then _ else _] ] ⇒ destruct a; try omega
end); auto.
Qed.