🍃 Map.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Coq.Sorting.Sorted.
Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Environment.V7.Proofs.Compare.
Require TezosOfOCaml.Environment.V7.Proofs.List.
Import Map.
#[local] Transparent Map.Make.
Module Valid.
Definition t `{Make.FArgs} : Prop :=
Compare.Valid.t (fun _ ⇒ True) (fun x ⇒ x) (Make.Ord.(COMPARABLE.compare)).
Lemma compare_keys_refl `{Make.FArgs} : t →
∀ k, Make.compare_keys k k = Datatypes.Eq.
Proof.
intros Hv k.
unfold Make.compare_keys.
erewrite Compare.Valid.refl; auto.
{ exact Hv. }
{ exact I. }
Qed.
Lemma compare_keys_Lt_trans `{Make.FArgs} : t → ∀ k1 k2 k3,
Make.compare_keys k1 k2 = Datatypes.Lt →
Make.compare_keys k2 k3 = Datatypes.Lt →
Make.compare_keys k1 k3 = Datatypes.Lt.
Proof.
intros Hv k1 k2 k3 Hk1k2 Hk2k3.
unfold Make.compare_keys in ×.
destruct (Make.Ord.(COMPARABLE.compare) k1 k2 =? 0) eqn:Hz1;
[discriminate|].
destruct (Make.Ord.(COMPARABLE.compare) k1 k2 <=? 0) eqn:Hle1;
[|discriminate].
destruct (Make.Ord.(COMPARABLE.compare) k2 k3 =? 0) eqn:Hz2;
[discriminate|].
destruct (Make.Ord.(COMPARABLE.compare) k2 k3 <=? 0) eqn:Hle2;
[|discriminate].
assert (Make.Ord.(COMPARABLE.compare) k1 k3 = -1) as Hneg1.
{ rewrite Z.leb_le in ×.
rewrite Z.eqb_neq in ×.
assert (∀ x, x ≠ 0 → x ≤ 0 → x < 0) as Hfact by lia.
apply (Compare.Valid.trans_lt Hv _ k2); auto;
apply Compare.Valid.less_neg1; auto.
}
rewrite Hneg1; auto.
Qed.
Lemma compare_keys_Lt `{Make.FArgs} :
t →
∀ k k', Make.compare_keys k k' = Datatypes.Lt →
Make.Ord.(COMPARABLE.compare) k k' = -1.
Proof.
intros.
pose proof (Compare.Valid.image H0 k k' I I).
unfold Make.compare_keys in H1.
destruct (Make.Ord.(COMPARABLE.compare) k k' ) eqn:?;
simpl in *; try discriminate.
destruct p; tauto.
Qed.
Lemma compare_keys_Gt `{Make.FArgs} :
t →
∀ k k', Make.compare_keys k k' = Datatypes.Gt →
Make.Ord.(COMPARABLE.compare) k k' = 1.
Proof.
intros.
pose proof (Compare.Valid.image H0 k k' I I).
unfold Make.compare_keys in H1.
destruct (Make.Ord.(COMPARABLE.compare) k k' ) eqn:?;
simpl in *; try discriminate.
destruct p; tauto.
Qed.
Lemma compare_keys_Eq `{Make.FArgs} :
t →
∀ k k', Make.compare_keys k k' = Datatypes.Eq →
k = k'.
Proof.
intros.
unfold Make.compare_keys in ×.
destruct Z.eqb eqn:Heq;
[| destruct Z.leb; discriminate].
rewrite Z.eqb_eq in Heq.
simpl in Heq.
apply (Compare.Valid.zero H0); auto.
Qed.
End Valid.
Module StrictlySorted.
Require Import CoqOfOCaml.Settings.
Require Coq.Sorting.Sorted.
Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Environment.V7.Proofs.Compare.
Require TezosOfOCaml.Environment.V7.Proofs.List.
Import Map.
#[local] Transparent Map.Make.
Module Valid.
Definition t `{Make.FArgs} : Prop :=
Compare.Valid.t (fun _ ⇒ True) (fun x ⇒ x) (Make.Ord.(COMPARABLE.compare)).
Lemma compare_keys_refl `{Make.FArgs} : t →
∀ k, Make.compare_keys k k = Datatypes.Eq.
Proof.
intros Hv k.
unfold Make.compare_keys.
erewrite Compare.Valid.refl; auto.
{ exact Hv. }
{ exact I. }
Qed.
Lemma compare_keys_Lt_trans `{Make.FArgs} : t → ∀ k1 k2 k3,
Make.compare_keys k1 k2 = Datatypes.Lt →
Make.compare_keys k2 k3 = Datatypes.Lt →
Make.compare_keys k1 k3 = Datatypes.Lt.
Proof.
intros Hv k1 k2 k3 Hk1k2 Hk2k3.
unfold Make.compare_keys in ×.
destruct (Make.Ord.(COMPARABLE.compare) k1 k2 =? 0) eqn:Hz1;
[discriminate|].
destruct (Make.Ord.(COMPARABLE.compare) k1 k2 <=? 0) eqn:Hle1;
[|discriminate].
destruct (Make.Ord.(COMPARABLE.compare) k2 k3 =? 0) eqn:Hz2;
[discriminate|].
destruct (Make.Ord.(COMPARABLE.compare) k2 k3 <=? 0) eqn:Hle2;
[|discriminate].
assert (Make.Ord.(COMPARABLE.compare) k1 k3 = -1) as Hneg1.
{ rewrite Z.leb_le in ×.
rewrite Z.eqb_neq in ×.
assert (∀ x, x ≠ 0 → x ≤ 0 → x < 0) as Hfact by lia.
apply (Compare.Valid.trans_lt Hv _ k2); auto;
apply Compare.Valid.less_neg1; auto.
}
rewrite Hneg1; auto.
Qed.
Lemma compare_keys_Lt `{Make.FArgs} :
t →
∀ k k', Make.compare_keys k k' = Datatypes.Lt →
Make.Ord.(COMPARABLE.compare) k k' = -1.
Proof.
intros.
pose proof (Compare.Valid.image H0 k k' I I).
unfold Make.compare_keys in H1.
destruct (Make.Ord.(COMPARABLE.compare) k k' ) eqn:?;
simpl in *; try discriminate.
destruct p; tauto.
Qed.
Lemma compare_keys_Gt `{Make.FArgs} :
t →
∀ k k', Make.compare_keys k k' = Datatypes.Gt →
Make.Ord.(COMPARABLE.compare) k k' = 1.
Proof.
intros.
pose proof (Compare.Valid.image H0 k k' I I).
unfold Make.compare_keys in H1.
destruct (Make.Ord.(COMPARABLE.compare) k k' ) eqn:?;
simpl in *; try discriminate.
destruct p; tauto.
Qed.
Lemma compare_keys_Eq `{Make.FArgs} :
t →
∀ k k', Make.compare_keys k k' = Datatypes.Eq →
k = k'.
Proof.
intros.
unfold Make.compare_keys in ×.
destruct Z.eqb eqn:Heq;
[| destruct Z.leb; discriminate].
rewrite Z.eqb_eq in Heq.
simpl in Heq.
apply (Compare.Valid.zero H0); auto.
Qed.
End Valid.
Module StrictlySorted.
The list is strictly increasing w.r.t. compare and furthermore bound below
by lb. This is an auxiliary definition for strictly_sorted, using lb as
an accumulator.
Fixpoint strictly_sorted_lb {a : Set} (compare : a → a → int) (lb : a)
(xs : list a) {struct xs} : Prop :=
match xs with
| [] ⇒ True
| x :: ys ⇒
compare lb x = -1
∧ strictly_sorted_lb compare x ys
end.
(xs : list a) {struct xs} : Prop :=
match xs with
| [] ⇒ True
| x :: ys ⇒
compare lb x = -1
∧ strictly_sorted_lb compare x ys
end.
The list is strictly increasing w.r.t. compare
Definition strictly_sorted {a : Set} (compare : a → a → int)
(xs : list a) : Prop :=
match xs with
| [] ⇒ True
| x :: ys ⇒ strictly_sorted_lb compare x ys
end.
Lemma strictly_sorted_lb_weaken `{Make.FArgs} : ∀ xs x y,
Valid.t → strictly_sorted_lb Make.Ord.(COMPARABLE.compare) y xs →
Make.Ord.(COMPARABLE.compare) x y = -1 →
strictly_sorted_lb Make.Ord.(COMPARABLE.compare) x xs.
Proof.
induction xs; intros x y Hv Hss Hxy.
{ exact I. }
{ simpl; split.
destruct Hss.
apply (Compare.Valid.trans_lt Hv _ y); auto.
destruct Hss; auto.
}
Qed.
Lemma strictly_sorted_lb_correct `{Make.FArgs} : ∀ xs x,
Valid.t → strictly_sorted_lb Make.Ord.(COMPARABLE.compare) x xs →
∀ y, In y xs → Make.Ord.(COMPARABLE.compare) x y = -1.
Proof.
induction xs; intros x Hv Hss y Hin.
{ destruct Hin. }
{ destruct Hin as [Heq|Hin].
{ rewrite Heq in Hss.
simpl in Hss; tauto.
}
{ apply IHxs; auto.
simpl in Hss.
apply (strictly_sorted_lb_weaken _ _ a); tauto.
}
}
Qed.
Lemma ss_tail {a : Set} (compare : a → a → int) (x : a) (xs : list a) :
strictly_sorted compare (x :: xs) → strictly_sorted compare xs.
Proof.
intros Hss; simpl in Hss.
destruct xs.
{ exact I. }
{ simpl in *; tauto. }
Qed.
Lemma lb_find_None `{Make.FArgs} {a : Set} (k : Make.key) (m : Make.t a) :
strictly_sorted_lb Make.Ord.(COMPARABLE.compare) k (List.map fst m) →
Make.find k m = None.
Proof.
destruct m; intros.
{ reflexivity. }
{ simpl.
destruct p.
simpl in H0.
destruct H0.
unfold Make.compare_keys.
rewrite H0; reflexivity.
}
Qed.
Definition t `{Make.FArgs} (keys : list Make.key) : Prop :=
strictly_sorted (Make.Ord.(COMPARABLE.compare)) keys.
Lemma map_extensional_head `{Make.FArgs} {A : Set} :
Valid.t →
∀ (m1 m2 : Make.t A) p1 p2,
t (List.map fst (p1 :: m1)) →
t (List.map fst (p2 :: m2)) →
(∀ q, In q (p1 :: m1) ↔ In q (p2 :: m2)) →
p1 = p2.
Proof.
intros.
assert (In p1 (p2 :: m2)) by hauto.
destruct H4; auto.
assert (In p2 (p1 :: m1)) by hauto.
destruct H5; auto.
simpl in ×.
pose (in_map fst _ _ H4).
pose (in_map fst _ _ H5).
pose proof (strictly_sorted_lb_correct
_ _ H0 H1 _ i0).
pose proof (strictly_sorted_lb_correct
_ _ H0 H2 _ i).
epose (Compare.Valid.sym H0).
rewrite e in H7; auto.
rewrite H6 in H7; lia.
Qed.
Lemma map_extensional_aux `{Make.FArgs} {A : Set} :
Map.Valid.t →
∀ (m1 m2 : Make.t A) k1 k2,
strictly_sorted_lb (Make.Ord.(COMPARABLE.compare) ) k1 (List.map fst m1) →
strictly_sorted_lb (Make.Ord.(COMPARABLE.compare) ) k2 (List.map fst m2) →
(∀ p, In p m1 ↔ In p m2) →
m1 = m2.
Proof.
intro Hv.
induction m1; intros m2 k1 k2 Hm1 Hm2 Hin.
{ destruct m2; [reflexivity|].
pose (Hin p); hauto lq: on rew: off.
}
{ destruct m2.
{ pose (Hin a); hauto lq: on rew: off. }
{ assert (a = p).
eapply map_extensional_head; auto.
{ apply Hm1. }
{ apply Hm2. }
{ rewrite H0 in ×.
simpl in Hm1, Hm2.
f_equal.
eapply IHm1.
{ apply Hm1. }
{ apply Hm2. }
{ intro; split; intro.
{ assert (In p0 (p :: m2))
by (simpl in Hin; sauto lq: on).
destruct H2; auto.
rewrite <- H2 in H1.
destruct Hm1 as [Hp Hm1].
pose proof (in_map fst _ _ H1).
epose proof (strictly_sorted_lb_correct
_ _ Hv Hm1 _ H3).
rewrite (Compare.Valid.refl Hv) in H4; auto.
lia.
}
{ assert (In p0 (p :: m1))
by (simpl in Hin; sauto lq: on).
destruct H2; auto.
rewrite <- H2 in H1.
destruct Hm2 as [Hp Hm2].
pose proof (in_map fst _ _ H1).
epose proof (strictly_sorted_lb_correct
_ _ Hv Hm2 _ H3).
rewrite (Compare.Valid.refl Hv) in H4; auto.
lia.
}
}
}
}
}
Qed.
(xs : list a) : Prop :=
match xs with
| [] ⇒ True
| x :: ys ⇒ strictly_sorted_lb compare x ys
end.
Lemma strictly_sorted_lb_weaken `{Make.FArgs} : ∀ xs x y,
Valid.t → strictly_sorted_lb Make.Ord.(COMPARABLE.compare) y xs →
Make.Ord.(COMPARABLE.compare) x y = -1 →
strictly_sorted_lb Make.Ord.(COMPARABLE.compare) x xs.
Proof.
induction xs; intros x y Hv Hss Hxy.
{ exact I. }
{ simpl; split.
destruct Hss.
apply (Compare.Valid.trans_lt Hv _ y); auto.
destruct Hss; auto.
}
Qed.
Lemma strictly_sorted_lb_correct `{Make.FArgs} : ∀ xs x,
Valid.t → strictly_sorted_lb Make.Ord.(COMPARABLE.compare) x xs →
∀ y, In y xs → Make.Ord.(COMPARABLE.compare) x y = -1.
Proof.
induction xs; intros x Hv Hss y Hin.
{ destruct Hin. }
{ destruct Hin as [Heq|Hin].
{ rewrite Heq in Hss.
simpl in Hss; tauto.
}
{ apply IHxs; auto.
simpl in Hss.
apply (strictly_sorted_lb_weaken _ _ a); tauto.
}
}
Qed.
Lemma ss_tail {a : Set} (compare : a → a → int) (x : a) (xs : list a) :
strictly_sorted compare (x :: xs) → strictly_sorted compare xs.
Proof.
intros Hss; simpl in Hss.
destruct xs.
{ exact I. }
{ simpl in *; tauto. }
Qed.
Lemma lb_find_None `{Make.FArgs} {a : Set} (k : Make.key) (m : Make.t a) :
strictly_sorted_lb Make.Ord.(COMPARABLE.compare) k (List.map fst m) →
Make.find k m = None.
Proof.
destruct m; intros.
{ reflexivity. }
{ simpl.
destruct p.
simpl in H0.
destruct H0.
unfold Make.compare_keys.
rewrite H0; reflexivity.
}
Qed.
Definition t `{Make.FArgs} (keys : list Make.key) : Prop :=
strictly_sorted (Make.Ord.(COMPARABLE.compare)) keys.
Lemma map_extensional_head `{Make.FArgs} {A : Set} :
Valid.t →
∀ (m1 m2 : Make.t A) p1 p2,
t (List.map fst (p1 :: m1)) →
t (List.map fst (p2 :: m2)) →
(∀ q, In q (p1 :: m1) ↔ In q (p2 :: m2)) →
p1 = p2.
Proof.
intros.
assert (In p1 (p2 :: m2)) by hauto.
destruct H4; auto.
assert (In p2 (p1 :: m1)) by hauto.
destruct H5; auto.
simpl in ×.
pose (in_map fst _ _ H4).
pose (in_map fst _ _ H5).
pose proof (strictly_sorted_lb_correct
_ _ H0 H1 _ i0).
pose proof (strictly_sorted_lb_correct
_ _ H0 H2 _ i).
epose (Compare.Valid.sym H0).
rewrite e in H7; auto.
rewrite H6 in H7; lia.
Qed.
Lemma map_extensional_aux `{Make.FArgs} {A : Set} :
Map.Valid.t →
∀ (m1 m2 : Make.t A) k1 k2,
strictly_sorted_lb (Make.Ord.(COMPARABLE.compare) ) k1 (List.map fst m1) →
strictly_sorted_lb (Make.Ord.(COMPARABLE.compare) ) k2 (List.map fst m2) →
(∀ p, In p m1 ↔ In p m2) →
m1 = m2.
Proof.
intro Hv.
induction m1; intros m2 k1 k2 Hm1 Hm2 Hin.
{ destruct m2; [reflexivity|].
pose (Hin p); hauto lq: on rew: off.
}
{ destruct m2.
{ pose (Hin a); hauto lq: on rew: off. }
{ assert (a = p).
eapply map_extensional_head; auto.
{ apply Hm1. }
{ apply Hm2. }
{ rewrite H0 in ×.
simpl in Hm1, Hm2.
f_equal.
eapply IHm1.
{ apply Hm1. }
{ apply Hm2. }
{ intro; split; intro.
{ assert (In p0 (p :: m2))
by (simpl in Hin; sauto lq: on).
destruct H2; auto.
rewrite <- H2 in H1.
destruct Hm1 as [Hp Hm1].
pose proof (in_map fst _ _ H1).
epose proof (strictly_sorted_lb_correct
_ _ Hv Hm1 _ H3).
rewrite (Compare.Valid.refl Hv) in H4; auto.
lia.
}
{ assert (In p0 (p :: m1))
by (simpl in Hin; sauto lq: on).
destruct H2; auto.
rewrite <- H2 in H1.
destruct Hm2 as [Hp Hm2].
pose proof (in_map fst _ _ H1).
epose proof (strictly_sorted_lb_correct
_ _ Hv Hm2 _ H3).
rewrite (Compare.Valid.refl Hv) in H4; auto.
lia.
}
}
}
}
}
Qed.
Two maps are equal when their keys are sorted and
contain the same pairs.
Lemma map_extensional `{Make.FArgs} {A : Set} :
Valid.t →
∀ m1 m2 : Make.t A,
t (List.map fst m1) →
t (List.map fst m2) →
(∀ p, In p m1 ↔ In p m2) →
m1 = m2.
Proof.
destruct m1, m2; intros Hm1 Hm2 Heq.
{ reflexivity. }
{ pose (Heq p); simpl in *; tauto. }
{ pose (Heq p); simpl in *; tauto. }
{ epose map_extensional_aux.
epose (e H0 _ _ _ _ Hm1 Hm2).
assert (p = p0).
eapply map_extensional_head; auto.
apply Hm1.
apply Hm2.
rewrite H1; f_equal.
apply e0.
rewrite H1 in ×.
intro; split; intro.
{ assert (In p1 (p0 :: m2)) by hauto.
destruct H3; auto.
assert (In p m1) by congruence.
simpl in Hm1.
assert (Make.Ord.(COMPARABLE.compare) (fst p) (fst p) = -1).
eapply StrictlySorted.strictly_sorted_lb_correct; eauto.
{ apply in_map; eauto. }
{ rewrite (Compare.Valid.refl H0) in H5; auto.
lia.
}
}
{ assert (In p1 (p0 :: m1)) by hauto.
destruct H3; auto.
assert (In p m2) by congruence.
simpl in Hm2.
assert (Make.Ord.(COMPARABLE.compare) (fst p0) (fst p0) = -1).
eapply StrictlySorted.strictly_sorted_lb_correct; eauto.
{ apply in_map; congruence. }
{ rewrite (Compare.Valid.refl H0) in H5; auto.
lia.
}
}
}
Qed.
Valid.t →
∀ m1 m2 : Make.t A,
t (List.map fst m1) →
t (List.map fst m2) →
(∀ p, In p m1 ↔ In p m2) →
m1 = m2.
Proof.
destruct m1, m2; intros Hm1 Hm2 Heq.
{ reflexivity. }
{ pose (Heq p); simpl in *; tauto. }
{ pose (Heq p); simpl in *; tauto. }
{ epose map_extensional_aux.
epose (e H0 _ _ _ _ Hm1 Hm2).
assert (p = p0).
eapply map_extensional_head; auto.
apply Hm1.
apply Hm2.
rewrite H1; f_equal.
apply e0.
rewrite H1 in ×.
intro; split; intro.
{ assert (In p1 (p0 :: m2)) by hauto.
destruct H3; auto.
assert (In p m1) by congruence.
simpl in Hm1.
assert (Make.Ord.(COMPARABLE.compare) (fst p) (fst p) = -1).
eapply StrictlySorted.strictly_sorted_lb_correct; eauto.
{ apply in_map; eauto. }
{ rewrite (Compare.Valid.refl H0) in H5; auto.
lia.
}
}
{ assert (In p1 (p0 :: m1)) by hauto.
destruct H3; auto.
assert (In p m2) by congruence.
simpl in Hm2.
assert (Make.Ord.(COMPARABLE.compare) (fst p0) (fst p0) = -1).
eapply StrictlySorted.strictly_sorted_lb_correct; eauto.
{ apply in_map; congruence. }
{ rewrite (Compare.Valid.refl H0) in H5; auto.
lia.
}
}
}
Qed.
[filter_map] preserves sortedness when
keys are preserved
Lemma filter_map_ss `{Make.FArgs} {A B : Set}
(f : Make.key × A → M× (Make.key × B))
(f_pres_key : ∀ k a k' b,
f (k, a) = Some (k', b) → k = k')
(Hv : Map.Valid.t) (m : Make.t A) :
StrictlySorted.t (List.map fst m) →
StrictlySorted.t (List.map fst (filter_map f m)).
Proof.
induction m as [|x]; auto; intro Hl.
assert (t (List.map fst (filter_map f m))). {
apply IHm; destruct m; auto; induction Hl; auto.
}
clear IHm.
induction m as [|y].
{ simpl; case (f x); auto. }
{ induction Hl.
simpl in ×.
remember (f x) as fx; destruct fx;
remember (f y) as fy; destruct fy; auto;
destruct p, x; symmetry in Heqfx; apply f_pres_key in Heqfx; subst;
try (destruct p0, y; symmetry in Heqfy; apply f_pres_key in Heqfy; subst);
simpl in *; auto.
apply IHm; auto; clear IHm.
clear Heqfy b.
destruct m as [|z]; auto; simpl in ×.
induction H2.
split; auto.
apply (Compare.Valid.trans_lt Hv) with (fst y); auto.
}
Qed.
Lemma add_preserves_sorting `{Make.FArgs} {A : Set}
(Hv : Map.Valid.t) (m : Make.t A) : ∀ k v,
t (List.map fst m) →
t (List.map fst (Make.add k v m)).
Proof.
intros.
destruct m; [exact I|].
Tactics.destruct_pairs.
simpl in ×.
generalize H0.
generalize k0.
clear H0 k0.
induction m; simpl in ×.
{ intros.
destruct Make.compare_keys eqn:?.
{ exact I. }
{ simpl.
split; auto.
unfold Make.compare_keys in Heqc.
simpl in ×.
apply (Valid.compare_keys_Lt Hv); auto.
}
{ simpl.
split; auto.
rewrite (Compare.Valid.sym Hv); auto.
rewrite <- Pos2Z.opp_pos; f_equal.
apply (Valid.compare_keys_Gt Hv); auto.
}
}
{ intros.
destruct Make.compare_keys eqn:?.
{ simpl in *; split.
{ assert (k = k0) by
(apply Valid.compare_keys_Eq; auto).
rewrite <- H1 in H0; apply H0.
}
{ apply H0. }
}
{ simpl in ×.
repeat split; try tauto.
apply (Valid.compare_keys_Lt Hv); auto.
}
{ destruct a0.
destruct (Make.compare_keys k k1) eqn:?; simpl in ×.
{ simpl; split.
{ rewrite (Compare.Valid.sym Hv); auto.
rewrite <- Pos2Z.opp_pos; f_equal.
apply (Valid.compare_keys_Gt Hv); auto.
}
{ assert (k = k1) by (apply (Valid.compare_keys_Eq Hv); auto).
rewrite H1; tauto.
}
}
{ repeat split.
{ rewrite (Compare.Valid.sym Hv); auto.
rewrite <- Pos2Z.opp_pos; f_equal.
apply (Valid.compare_keys_Gt Hv); auto.
}
{ apply (Valid.compare_keys_Lt Hv); auto. }
{ tauto. }
}
{ split.
{ tauto. }
{ pose (IHm k1) as IH.
rewrite Heqc0 in IH.
apply IH; tauto.
}
}
}
}
Qed.
Inductive pick_opt_ind `{Make.FArgs} {A : Set} {Hv : Map.Valid.t} :
Make.key → Make.t A → option A → Make.t A → Prop :=
| pick_nil k : pick_opt_ind k [] None []
| pick_eq k m v : pick_opt_ind k ((k,v) :: m) (Some v) m
| pick_lt k k' v m :
Make.compare_keys k k' = Datatypes.Lt → pick_opt_ind k ((k',v) :: m) None ((k',v) :: m)
| pick_gt k k' v v' m m' :
Make.compare_keys k k' = Datatypes.Gt → pick_opt_ind k m v' m' →
pick_opt_ind k ((k',v) :: m) v' ((k',v) :: m').
Lemma pick_opt_to_ind `{Make.FArgs} {A : Set} (Hv : Map.Valid.t)
(k : Make.key) (m : Make.t A) (v : option A) (m' : Make.t A) :
Make.pick_opt k m = (v,m') → pick_opt_ind (Hv := Hv) k m v m'.
Proof.
generalize dependent k.
generalize dependent v.
generalize dependent m'.
induction m; simpl; intros.
{ inversion_clear H0; constructor. }
{ destruct a as [k'].
destruct Make.compare_keys eqn:kk.
{ inversion_clear H0.
apply (Valid.compare_keys_Eq Hv) in kk; subst.
constructor.
}
{ inversion_clear H0. constructor; auto. }
{ destruct Make.pick_opt eqn:?.
inversion H0; subst; clear H0.
econstructor 4; eauto.
}
}
Qed.
Lemma pick_opt_from_ind `{Make.FArgs} {A : Set} (Hv : Map.Valid.t)
(k : Make.key) (m : Make.t A) (v : option A) (m' : Make.t A) :
pick_opt_ind (Hv := Hv) k m v m' → Make.pick_opt k m = (v,m').
Proof.
induction 1; simpl; try (rewrite H0); auto.
{ rewrite (Valid.compare_keys_refl Hv); auto. }
{ rewrite IHpick_opt_ind; auto. }
Qed.
(f : Make.key × A → M× (Make.key × B))
(f_pres_key : ∀ k a k' b,
f (k, a) = Some (k', b) → k = k')
(Hv : Map.Valid.t) (m : Make.t A) :
StrictlySorted.t (List.map fst m) →
StrictlySorted.t (List.map fst (filter_map f m)).
Proof.
induction m as [|x]; auto; intro Hl.
assert (t (List.map fst (filter_map f m))). {
apply IHm; destruct m; auto; induction Hl; auto.
}
clear IHm.
induction m as [|y].
{ simpl; case (f x); auto. }
{ induction Hl.
simpl in ×.
remember (f x) as fx; destruct fx;
remember (f y) as fy; destruct fy; auto;
destruct p, x; symmetry in Heqfx; apply f_pres_key in Heqfx; subst;
try (destruct p0, y; symmetry in Heqfy; apply f_pres_key in Heqfy; subst);
simpl in *; auto.
apply IHm; auto; clear IHm.
clear Heqfy b.
destruct m as [|z]; auto; simpl in ×.
induction H2.
split; auto.
apply (Compare.Valid.trans_lt Hv) with (fst y); auto.
}
Qed.
Lemma add_preserves_sorting `{Make.FArgs} {A : Set}
(Hv : Map.Valid.t) (m : Make.t A) : ∀ k v,
t (List.map fst m) →
t (List.map fst (Make.add k v m)).
Proof.
intros.
destruct m; [exact I|].
Tactics.destruct_pairs.
simpl in ×.
generalize H0.
generalize k0.
clear H0 k0.
induction m; simpl in ×.
{ intros.
destruct Make.compare_keys eqn:?.
{ exact I. }
{ simpl.
split; auto.
unfold Make.compare_keys in Heqc.
simpl in ×.
apply (Valid.compare_keys_Lt Hv); auto.
}
{ simpl.
split; auto.
rewrite (Compare.Valid.sym Hv); auto.
rewrite <- Pos2Z.opp_pos; f_equal.
apply (Valid.compare_keys_Gt Hv); auto.
}
}
{ intros.
destruct Make.compare_keys eqn:?.
{ simpl in *; split.
{ assert (k = k0) by
(apply Valid.compare_keys_Eq; auto).
rewrite <- H1 in H0; apply H0.
}
{ apply H0. }
}
{ simpl in ×.
repeat split; try tauto.
apply (Valid.compare_keys_Lt Hv); auto.
}
{ destruct a0.
destruct (Make.compare_keys k k1) eqn:?; simpl in ×.
{ simpl; split.
{ rewrite (Compare.Valid.sym Hv); auto.
rewrite <- Pos2Z.opp_pos; f_equal.
apply (Valid.compare_keys_Gt Hv); auto.
}
{ assert (k = k1) by (apply (Valid.compare_keys_Eq Hv); auto).
rewrite H1; tauto.
}
}
{ repeat split.
{ rewrite (Compare.Valid.sym Hv); auto.
rewrite <- Pos2Z.opp_pos; f_equal.
apply (Valid.compare_keys_Gt Hv); auto.
}
{ apply (Valid.compare_keys_Lt Hv); auto. }
{ tauto. }
}
{ split.
{ tauto. }
{ pose (IHm k1) as IH.
rewrite Heqc0 in IH.
apply IH; tauto.
}
}
}
}
Qed.
Inductive pick_opt_ind `{Make.FArgs} {A : Set} {Hv : Map.Valid.t} :
Make.key → Make.t A → option A → Make.t A → Prop :=
| pick_nil k : pick_opt_ind k [] None []
| pick_eq k m v : pick_opt_ind k ((k,v) :: m) (Some v) m
| pick_lt k k' v m :
Make.compare_keys k k' = Datatypes.Lt → pick_opt_ind k ((k',v) :: m) None ((k',v) :: m)
| pick_gt k k' v v' m m' :
Make.compare_keys k k' = Datatypes.Gt → pick_opt_ind k m v' m' →
pick_opt_ind k ((k',v) :: m) v' ((k',v) :: m').
Lemma pick_opt_to_ind `{Make.FArgs} {A : Set} (Hv : Map.Valid.t)
(k : Make.key) (m : Make.t A) (v : option A) (m' : Make.t A) :
Make.pick_opt k m = (v,m') → pick_opt_ind (Hv := Hv) k m v m'.
Proof.
generalize dependent k.
generalize dependent v.
generalize dependent m'.
induction m; simpl; intros.
{ inversion_clear H0; constructor. }
{ destruct a as [k'].
destruct Make.compare_keys eqn:kk.
{ inversion_clear H0.
apply (Valid.compare_keys_Eq Hv) in kk; subst.
constructor.
}
{ inversion_clear H0. constructor; auto. }
{ destruct Make.pick_opt eqn:?.
inversion H0; subst; clear H0.
econstructor 4; eauto.
}
}
Qed.
Lemma pick_opt_from_ind `{Make.FArgs} {A : Set} (Hv : Map.Valid.t)
(k : Make.key) (m : Make.t A) (v : option A) (m' : Make.t A) :
pick_opt_ind (Hv := Hv) k m v m' → Make.pick_opt k m = (v,m').
Proof.
induction 1; simpl; try (rewrite H0); auto.
{ rewrite (Valid.compare_keys_refl Hv); auto. }
{ rewrite IHpick_opt_ind; auto. }
Qed.
[merge] preserves sortedness
Lemma merge_ss `{Make.FArgs} {A B C : Set}
(f : Make.key → M× A → M× B → M× C)
(Hv : Map.Valid.t) (m1 : Make.t A) :
∀ (m2 : Make.t B),
StrictlySorted.t (List.map fst m2) →
StrictlySorted.t (List.map fst
(Make.merge f m1 m2)).
Proof.
induction m1.
{ simpl; intros.
apply filter_map_ss; auto.
intros k a k' b Hf.
destruct f; inversion Hf; auto.
}
{ simpl; intros.
destruct a.
destruct Make.pick_opt eqn:?.
assert (t (List.map fst (Make.merge f m1 t1))). {
apply IHm1; clear IHm1.
apply (pick_opt_to_ind Hv) in Heqp.
induction Heqp; auto.
{ simpl in H0. destruct (List.map fst m); auto. apply H0. }
{ simpl in ×.
assert (t (List.map fst m)). {
destruct (List.map fst m); auto. apply H0.
}
specialize (IHHeqp H2); clear H2.
inversion Heqp; subst; auto.
{ induction H0. destruct (List.map fst m'); auto; induction H2.
simpl in *; split; auto.
apply (Compare.Valid.trans_lt Hv) with k; auto.
}
{ simpl in ×. induction H0; split; auto. }
}
}
{ destruct f; auto.
apply add_preserves_sorting; auto.
}
}
Qed.
End StrictlySorted.
Lemma Make_fold_lemma `{Make.FArgs} {a b : Set}
(P : b → Prop)
(f : Make.key → a → b → b)
(f_pres_P : ∀ k x y, P y → P (f k x y)) :
∀ (m : Make.t a) x, P x →
P (Make.fold f m x).
Proof.
induction m; intros.
{ exact H0. }
{ simpl.
destruct a0.
apply IHm.
apply f_pres_P; auto.
}
Qed.
Lemma In_add_destruct `{Make.FArgs} {a : Set} {m : Make.t a} :
∀ {k k' : Make.key} {v v' : a},
In (k, v) (Make.add k' v' m) →
(k', v') = (k, v) ∨ In (k, v) m.
Proof.
induction m; intros.
{ left. simpl in *; tauto. }
{ simpl in ×.
destruct a0.
destruct Make.compare_keys eqn:?.
{ destruct H0; tauto. }
{ destruct H0; tauto. }
{ destruct H0; try tauto.
destruct (IHm _ _ _ _ H0); tauto.
}
}
Qed.
Lemma In_remove_In `{Make.FArgs} {a : Set} {m : Make.t a} :
∀ {k k' : Make.key} {v : a},
In (k, v) (Make.remove k' m) →
In (k, v) m.
Proof.
induction m; sauto.
Qed.
Lemma In_fold `{Make.FArgs} {a b : Set}
(f : Make.key → a → b) (m1 : Make.t a) (m2 : Make.t b) x y :
In (x,y) (Make.fold (fun (k : Make.key) (v : a) ⇒
Make.add k (f k v)) m1 m2) →
In (x,y) m2 ∨ (∃ z, In (x, z) m1 ∧ f x z = y).
Proof.
revert m1 m2.
induction m1; intros; simpl in ×.
{ tauto. }
{ destruct a0.
destruct (IHm1 _ H0) as
[G| [z Hz]].
{ destruct (In_add_destruct G).
{ right; eexists; qauto. }
{ left; auto. }
}
{ hauto. }
}
Qed.
Lemma find_add `{Make.FArgs} {a : Set} k v (m : Make.t a) :
Valid.t → Make.find k (Make.add k v m) = Some v.
Proof.
intros.
induction m.
{ simpl.
rewrite Valid.compare_keys_refl; auto.
}
{ simpl.
destruct a0.
destruct (Make.compare_keys k k0) eqn:G.
{ simpl; rewrite Valid.compare_keys_refl; auto. }
{ simpl; rewrite Valid.compare_keys_refl; auto. }
{ simpl; rewrite G; exact IHm. }
}
Qed.
Lemma find_respects_Eq `{Make.FArgs} {a : Set} (k k' : Make.key)
(m : Make.t a) :
Valid.t → Make.compare_keys k k' = Datatypes.Eq →
Make.find k m = Make.find k' m.
Proof.
intros Hv Heq.
induction m.
{ reflexivity. }
{ simpl; destruct a0.
unfold Make.compare_keys in ×.
rewrite (Compare.Valid.congruence_left Hv k k'); auto.
{ destruct (Make.Ord.(COMPARABLE.compare) k' k0 =? 0); auto.
destruct (Make.Ord.(COMPARABLE.compare) k' k0 <=? 0); auto.
}
{ destruct (Make.Ord.(COMPARABLE.compare) k k' =? 0) eqn:G.
{ rewrite Z.eqb_eq in G.
apply (Compare.Valid.zero Hv); auto.
}
{ destruct (Make.Ord.(COMPARABLE.compare) k k' <=? 0);
try discriminate.
}
}
}
Qed.
Lemma find_update `{Make.FArgs} {a : Set} k f (m : Make.t a) :
Valid.t → StrictlySorted.t (List.map fst m) →
Make.find k (Make.update k f m) = f (Make.find k m).
Proof.
intros.
induction m.
{ unfold Make.update.
simpl.
destruct (f None); auto.
simpl; rewrite Valid.compare_keys_refl; auto.
}
{ unfold Make.update in ×.
simpl.
destruct a0.
destruct (Make.compare_keys k k0) eqn:G.
{ destruct (f (Some a0)).
{ simpl; rewrite Valid.compare_keys_refl; auto. }
{ rewrite (find_respects_Eq k k0 m H0); auto.
unfold StrictlySorted.t in H1; simpl in H1.
apply StrictlySorted.lb_find_None; auto.
}
}
{ destruct (f None).
{ simpl; rewrite Valid.compare_keys_refl; auto. }
{ simpl.
rewrite G; reflexivity.
}
}
{ destruct (f (Make.find k m)).
{ simpl.
rewrite G.
apply IHm; eapply StrictlySorted.ss_tail; exact H1.
}
{ simpl.
rewrite G.
apply IHm; eapply StrictlySorted.ss_tail; exact H1.
}
}
}
Qed.
Lemma find_singleton `{Make.FArgs} {a : Set} k (v : a) :
Valid.t → Make.find k (Make.singleton k v) = Some v.
Proof.
intros.
simpl.
rewrite Valid.compare_keys_refl; auto.
Qed.
Lemma mem_In `{Make.FArgs} {a : Set} (k : Make.key) (m : Make.t a) :
Valid.t → StrictlySorted.t (List.map fst m) →
Make.mem k m = true ↔ (∃ v, In (k,v) m).
Proof.
intros.
induction m.
{ simpl; split; intro; (discriminate || sauto). }
{ simpl; split; intro; destruct a0.
{ destruct (Make.compare_keys k k0) eqn:G.
{ eexists. left; simpl.
unfold Make.compare_keys; f_equal.
unfold Make.compare_keys in ×.
destruct (Make.Ord.(COMPARABLE.compare) k k0 =? 0) eqn:G0.
{ rewrite Z.eqb_eq in G0.
symmetry; apply (Compare.Valid.zero H0); auto.
}
{ destruct (Make.Ord.(COMPARABLE.compare) k k0 <=? 0);
discriminate.
}
}
{ discriminate. }
{ rewrite IHm in H2; destruct H2;
[|eapply StrictlySorted.ss_tail; exact H1].
eexists; right; eauto.
}
}
{ destruct H2 as [v Hv]. destruct Hv as [Hv|Hv].
{ inversion Hv.
rewrite Valid.compare_keys_refl; auto.
}
{ destruct Make.compare_keys eqn:G; auto.
{ unfold Make.compare_keys in G.
destruct (Make.Ord.(COMPARABLE.compare) k k0 =? 0);
try discriminate.
destruct (Make.Ord.(COMPARABLE.compare) k k0 <=? 0) eqn:G0;
try discriminate.
rewrite Z.leb_le in G0.
unfold StrictlySorted.t in H1.
simpl in H1.
assert (In k (List.map fst m)) as Hin.
{ assert (k = fst (k, v)) as Hobv by auto.
rewrite Hobv.
apply in_map; auto.
}
pose proof (StrictlySorted.strictly_sorted_lb_correct
(List.map fst m) k0 H0 H1 k Hin) as Hc.
rewrite (Compare.Valid.sym H0) in Hc; auto. lia.
}
{ rewrite IHm; auto.
{ ∃ v; auto. }
{ eapply StrictlySorted.ss_tail; exact H1. }
}
}
}
}
Qed.
Lemma mem_not_In `{Make.FArgs} {a : Set} (k : Make.key)
(m : Make.t a) :
Valid.t →
StrictlySorted.t (List.map fst m) →
Make.mem k m = false ↔ (∀ v, ¬ In (k, v) m).
Proof.
intros.
split; intros.
{ intro.
assert (∃ x, In (k, x) m) as Hex by firstorder.
rewrite <- mem_In in Hex; auto.
congruence.
}
{ destruct Make.mem eqn:G.
{ rewrite mem_In in G; auto.
firstorder.
}
{ reflexivity. }
}
Qed.
(f : Make.key → M× A → M× B → M× C)
(Hv : Map.Valid.t) (m1 : Make.t A) :
∀ (m2 : Make.t B),
StrictlySorted.t (List.map fst m2) →
StrictlySorted.t (List.map fst
(Make.merge f m1 m2)).
Proof.
induction m1.
{ simpl; intros.
apply filter_map_ss; auto.
intros k a k' b Hf.
destruct f; inversion Hf; auto.
}
{ simpl; intros.
destruct a.
destruct Make.pick_opt eqn:?.
assert (t (List.map fst (Make.merge f m1 t1))). {
apply IHm1; clear IHm1.
apply (pick_opt_to_ind Hv) in Heqp.
induction Heqp; auto.
{ simpl in H0. destruct (List.map fst m); auto. apply H0. }
{ simpl in ×.
assert (t (List.map fst m)). {
destruct (List.map fst m); auto. apply H0.
}
specialize (IHHeqp H2); clear H2.
inversion Heqp; subst; auto.
{ induction H0. destruct (List.map fst m'); auto; induction H2.
simpl in *; split; auto.
apply (Compare.Valid.trans_lt Hv) with k; auto.
}
{ simpl in ×. induction H0; split; auto. }
}
}
{ destruct f; auto.
apply add_preserves_sorting; auto.
}
}
Qed.
End StrictlySorted.
Lemma Make_fold_lemma `{Make.FArgs} {a b : Set}
(P : b → Prop)
(f : Make.key → a → b → b)
(f_pres_P : ∀ k x y, P y → P (f k x y)) :
∀ (m : Make.t a) x, P x →
P (Make.fold f m x).
Proof.
induction m; intros.
{ exact H0. }
{ simpl.
destruct a0.
apply IHm.
apply f_pres_P; auto.
}
Qed.
Lemma In_add_destruct `{Make.FArgs} {a : Set} {m : Make.t a} :
∀ {k k' : Make.key} {v v' : a},
In (k, v) (Make.add k' v' m) →
(k', v') = (k, v) ∨ In (k, v) m.
Proof.
induction m; intros.
{ left. simpl in *; tauto. }
{ simpl in ×.
destruct a0.
destruct Make.compare_keys eqn:?.
{ destruct H0; tauto. }
{ destruct H0; tauto. }
{ destruct H0; try tauto.
destruct (IHm _ _ _ _ H0); tauto.
}
}
Qed.
Lemma In_remove_In `{Make.FArgs} {a : Set} {m : Make.t a} :
∀ {k k' : Make.key} {v : a},
In (k, v) (Make.remove k' m) →
In (k, v) m.
Proof.
induction m; sauto.
Qed.
Lemma In_fold `{Make.FArgs} {a b : Set}
(f : Make.key → a → b) (m1 : Make.t a) (m2 : Make.t b) x y :
In (x,y) (Make.fold (fun (k : Make.key) (v : a) ⇒
Make.add k (f k v)) m1 m2) →
In (x,y) m2 ∨ (∃ z, In (x, z) m1 ∧ f x z = y).
Proof.
revert m1 m2.
induction m1; intros; simpl in ×.
{ tauto. }
{ destruct a0.
destruct (IHm1 _ H0) as
[G| [z Hz]].
{ destruct (In_add_destruct G).
{ right; eexists; qauto. }
{ left; auto. }
}
{ hauto. }
}
Qed.
Lemma find_add `{Make.FArgs} {a : Set} k v (m : Make.t a) :
Valid.t → Make.find k (Make.add k v m) = Some v.
Proof.
intros.
induction m.
{ simpl.
rewrite Valid.compare_keys_refl; auto.
}
{ simpl.
destruct a0.
destruct (Make.compare_keys k k0) eqn:G.
{ simpl; rewrite Valid.compare_keys_refl; auto. }
{ simpl; rewrite Valid.compare_keys_refl; auto. }
{ simpl; rewrite G; exact IHm. }
}
Qed.
Lemma find_respects_Eq `{Make.FArgs} {a : Set} (k k' : Make.key)
(m : Make.t a) :
Valid.t → Make.compare_keys k k' = Datatypes.Eq →
Make.find k m = Make.find k' m.
Proof.
intros Hv Heq.
induction m.
{ reflexivity. }
{ simpl; destruct a0.
unfold Make.compare_keys in ×.
rewrite (Compare.Valid.congruence_left Hv k k'); auto.
{ destruct (Make.Ord.(COMPARABLE.compare) k' k0 =? 0); auto.
destruct (Make.Ord.(COMPARABLE.compare) k' k0 <=? 0); auto.
}
{ destruct (Make.Ord.(COMPARABLE.compare) k k' =? 0) eqn:G.
{ rewrite Z.eqb_eq in G.
apply (Compare.Valid.zero Hv); auto.
}
{ destruct (Make.Ord.(COMPARABLE.compare) k k' <=? 0);
try discriminate.
}
}
}
Qed.
Lemma find_update `{Make.FArgs} {a : Set} k f (m : Make.t a) :
Valid.t → StrictlySorted.t (List.map fst m) →
Make.find k (Make.update k f m) = f (Make.find k m).
Proof.
intros.
induction m.
{ unfold Make.update.
simpl.
destruct (f None); auto.
simpl; rewrite Valid.compare_keys_refl; auto.
}
{ unfold Make.update in ×.
simpl.
destruct a0.
destruct (Make.compare_keys k k0) eqn:G.
{ destruct (f (Some a0)).
{ simpl; rewrite Valid.compare_keys_refl; auto. }
{ rewrite (find_respects_Eq k k0 m H0); auto.
unfold StrictlySorted.t in H1; simpl in H1.
apply StrictlySorted.lb_find_None; auto.
}
}
{ destruct (f None).
{ simpl; rewrite Valid.compare_keys_refl; auto. }
{ simpl.
rewrite G; reflexivity.
}
}
{ destruct (f (Make.find k m)).
{ simpl.
rewrite G.
apply IHm; eapply StrictlySorted.ss_tail; exact H1.
}
{ simpl.
rewrite G.
apply IHm; eapply StrictlySorted.ss_tail; exact H1.
}
}
}
Qed.
Lemma find_singleton `{Make.FArgs} {a : Set} k (v : a) :
Valid.t → Make.find k (Make.singleton k v) = Some v.
Proof.
intros.
simpl.
rewrite Valid.compare_keys_refl; auto.
Qed.
Lemma mem_In `{Make.FArgs} {a : Set} (k : Make.key) (m : Make.t a) :
Valid.t → StrictlySorted.t (List.map fst m) →
Make.mem k m = true ↔ (∃ v, In (k,v) m).
Proof.
intros.
induction m.
{ simpl; split; intro; (discriminate || sauto). }
{ simpl; split; intro; destruct a0.
{ destruct (Make.compare_keys k k0) eqn:G.
{ eexists. left; simpl.
unfold Make.compare_keys; f_equal.
unfold Make.compare_keys in ×.
destruct (Make.Ord.(COMPARABLE.compare) k k0 =? 0) eqn:G0.
{ rewrite Z.eqb_eq in G0.
symmetry; apply (Compare.Valid.zero H0); auto.
}
{ destruct (Make.Ord.(COMPARABLE.compare) k k0 <=? 0);
discriminate.
}
}
{ discriminate. }
{ rewrite IHm in H2; destruct H2;
[|eapply StrictlySorted.ss_tail; exact H1].
eexists; right; eauto.
}
}
{ destruct H2 as [v Hv]. destruct Hv as [Hv|Hv].
{ inversion Hv.
rewrite Valid.compare_keys_refl; auto.
}
{ destruct Make.compare_keys eqn:G; auto.
{ unfold Make.compare_keys in G.
destruct (Make.Ord.(COMPARABLE.compare) k k0 =? 0);
try discriminate.
destruct (Make.Ord.(COMPARABLE.compare) k k0 <=? 0) eqn:G0;
try discriminate.
rewrite Z.leb_le in G0.
unfold StrictlySorted.t in H1.
simpl in H1.
assert (In k (List.map fst m)) as Hin.
{ assert (k = fst (k, v)) as Hobv by auto.
rewrite Hobv.
apply in_map; auto.
}
pose proof (StrictlySorted.strictly_sorted_lb_correct
(List.map fst m) k0 H0 H1 k Hin) as Hc.
rewrite (Compare.Valid.sym H0) in Hc; auto. lia.
}
{ rewrite IHm; auto.
{ ∃ v; auto. }
{ eapply StrictlySorted.ss_tail; exact H1. }
}
}
}
}
Qed.
Lemma mem_not_In `{Make.FArgs} {a : Set} (k : Make.key)
(m : Make.t a) :
Valid.t →
StrictlySorted.t (List.map fst m) →
Make.mem k m = false ↔ (∀ v, ¬ In (k, v) m).
Proof.
intros.
split; intros.
{ intro.
assert (∃ x, In (k, x) m) as Hex by firstorder.
rewrite <- mem_In in Hex; auto.
congruence.
}
{ destruct Make.mem eqn:G.
{ rewrite mem_In in G; auto.
firstorder.
}
{ reflexivity. }
}
Qed.
We can express the [mem] operation from the [find] one.
Lemma mem_from_find `{Make.FArgs} {a : Set}
(k : Make.key) (m : Make.t a) :
Make.mem k m =
match Make.find k m with
| Some _ ⇒ true
| None ⇒ false
end.
Proof.
intros.
induction m.
{ reflexivity. }
{ simpl.
destruct a0.
destruct (Make.compare_keys k k0); auto.
}
Qed.
Lemma mem_find_not_eq_none `{Make.FArgs} {a : Set}
(k : Make.key) (m : Make.t a) :
Make.mem k m = true →
Make.find k m ≠ None.
Proof.
intros.
induction m.
{ discriminate. }
{ simpl in ×.
destruct a0.
destruct (Make.compare_keys k k0); try discriminate; auto.
}
Qed.
Lemma find_mem_eq `{Make.FArgs} {a : Set}
(k : Make.key) (v : a) (m : Make.t a) :
Make.find k m = Some v →
Make.mem k m = true.
Proof.
intros.
induction m.
{ discriminate. }
{ simpl in ×.
destruct a0.
destruct (Make.compare_keys k k0); auto.
discriminate.
}
Qed.
Lemma add_found_eq `{Make.FArgs} {a : Set}
(m : Make.t a) (k : Make.key) (v : a) :
Valid.t →
Make.find k m = Some v →
Make.add k v m = m.
Proof.
intros Hv Hfind.
induction m.
{ discriminate. }
{ simpl in ×.
destruct a0.
destruct (Make.compare_keys k k0) eqn:G.
{ inversion Hfind.
repeat f_equal.
apply (Compare.Valid.zero Hv); auto.
unfold Make.compare_keys in G.
destruct (Make.Ord.(COMPARABLE.compare) k k0 =? 0) eqn:G0.
{ rewrite Z.eqb_eq in G0; auto. }
{ destruct (Make.Ord.(COMPARABLE.compare) k k0 <=? 0); discriminate. }
}
{ discriminate. }
{ f_equal; auto. }
}
Qed.
Lemma find_eq_none_implies_mem_eq_false `{Make.FArgs}
{a : Set} (k : Make.key) (m : Make.t a) :
Make.find k m = None →
Make.mem k m = false.
Proof.
intros.
induction m.
{ reflexivity. }
{ simpl in ×.
destruct a0.
destruct (Make.compare_keys k k0) eqn:G.
{ discriminate. }
{ reflexivity. }
{ tauto. }
}
Qed.
Lemma find_add_eq_some `{Make.FArgs} {a : Set} (k : Make.key) (v : a)
(m : Make.t a) :
Valid.t → Make.find k (Make.add k v m) = Some v.
Proof.
intro Hv.
induction m.
{ simpl.
unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ simpl.
destruct a0.
destruct (Make.compare_keys k k0) eqn:G.
{ simpl.
unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ simpl.
unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ simpl.
rewrite G.
apply IHm.
}
}
Qed.
Lemma remove_add_id `{Make.FArgs} {a : Set} (k : Make.key) (v : a)
(m : Make.t a) :
Valid.t →
Make.mem k m = false → Make.remove k (Make.add k v m) = m.
Proof.
intros Hv Hmem.
induction m.
{ simpl.
unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ destruct a0.
simpl in ×.
destruct (Make.compare_keys k k0) eqn:G.
{ discriminate. }
{ simpl.
unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ simpl.
rewrite G.
f_equal; auto.
}
}
Qed.
(k : Make.key) (m : Make.t a) :
Make.mem k m =
match Make.find k m with
| Some _ ⇒ true
| None ⇒ false
end.
Proof.
intros.
induction m.
{ reflexivity. }
{ simpl.
destruct a0.
destruct (Make.compare_keys k k0); auto.
}
Qed.
Lemma mem_find_not_eq_none `{Make.FArgs} {a : Set}
(k : Make.key) (m : Make.t a) :
Make.mem k m = true →
Make.find k m ≠ None.
Proof.
intros.
induction m.
{ discriminate. }
{ simpl in ×.
destruct a0.
destruct (Make.compare_keys k k0); try discriminate; auto.
}
Qed.
Lemma find_mem_eq `{Make.FArgs} {a : Set}
(k : Make.key) (v : a) (m : Make.t a) :
Make.find k m = Some v →
Make.mem k m = true.
Proof.
intros.
induction m.
{ discriminate. }
{ simpl in ×.
destruct a0.
destruct (Make.compare_keys k k0); auto.
discriminate.
}
Qed.
Lemma add_found_eq `{Make.FArgs} {a : Set}
(m : Make.t a) (k : Make.key) (v : a) :
Valid.t →
Make.find k m = Some v →
Make.add k v m = m.
Proof.
intros Hv Hfind.
induction m.
{ discriminate. }
{ simpl in ×.
destruct a0.
destruct (Make.compare_keys k k0) eqn:G.
{ inversion Hfind.
repeat f_equal.
apply (Compare.Valid.zero Hv); auto.
unfold Make.compare_keys in G.
destruct (Make.Ord.(COMPARABLE.compare) k k0 =? 0) eqn:G0.
{ rewrite Z.eqb_eq in G0; auto. }
{ destruct (Make.Ord.(COMPARABLE.compare) k k0 <=? 0); discriminate. }
}
{ discriminate. }
{ f_equal; auto. }
}
Qed.
Lemma find_eq_none_implies_mem_eq_false `{Make.FArgs}
{a : Set} (k : Make.key) (m : Make.t a) :
Make.find k m = None →
Make.mem k m = false.
Proof.
intros.
induction m.
{ reflexivity. }
{ simpl in ×.
destruct a0.
destruct (Make.compare_keys k k0) eqn:G.
{ discriminate. }
{ reflexivity. }
{ tauto. }
}
Qed.
Lemma find_add_eq_some `{Make.FArgs} {a : Set} (k : Make.key) (v : a)
(m : Make.t a) :
Valid.t → Make.find k (Make.add k v m) = Some v.
Proof.
intro Hv.
induction m.
{ simpl.
unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ simpl.
destruct a0.
destruct (Make.compare_keys k k0) eqn:G.
{ simpl.
unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ simpl.
unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ simpl.
rewrite G.
apply IHm.
}
}
Qed.
Lemma remove_add_id `{Make.FArgs} {a : Set} (k : Make.key) (v : a)
(m : Make.t a) :
Valid.t →
Make.mem k m = false → Make.remove k (Make.add k v m) = m.
Proof.
intros Hv Hmem.
induction m.
{ simpl.
unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ destruct a0.
simpl in ×.
destruct (Make.compare_keys k k0) eqn:G.
{ discriminate. }
{ simpl.
unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ simpl.
rewrite G.
f_equal; auto.
}
}
Qed.
We do not change anything when removing an element which is not there.
Lemma remove_find_none `{Make.FArgs} {a : Set} (k : Make.key) (m : Make.t a) :
Make.find k m = None → Make.remove k m = m.
Proof.
intros Hfind.
induction m.
{ reflexivity. }
{ destruct a0; simpl in ×.
destruct (Make.compare_keys k k0).
{ discriminate. }
{ reflexivity. }
{ f_equal; auto. }
}
Qed.
Lemma add_add_eq `{Make.FArgs} {a : Set} (k : Make.key) (v v' : a)
(m : Make.t a) :
Valid.t → Make.add k v (Make.add k v' m) = Make.add k v m.
Proof.
intros Hv.
induction m.
{ simpl.
unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ destruct a0.
simpl in ×.
destruct (Make.compare_keys k k0) eqn:G; simpl.
{ unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ rewrite G.
f_equal; auto.
}
}
Qed.
Lemma mem_add_eq `{Make.FArgs} {a : Set} (k : Make.key) (v : a)
(m : Make.t a) :
Valid.t → Make.mem k (Make.add k v m) = true.
Proof.
intros Hv.
induction m; simpl in ×.
{ unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ destruct a0; simpl.
destruct (Make.compare_keys k k0) eqn:G; simpl.
{ unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ rewrite G; auto. }
}
Qed.
Lemma find_add_neq `{Make.FArgs} {a : Set} (k k' : Make.key) (v : a)
(m : Make.t a) :
Valid.t → k ≠ k' → Make.find k (Make.add k' v m) = Make.find k m.
Proof.
intros Hv Hneq.
induction m.
{ simpl.
destruct (Make.compare_keys k k') eqn:G; auto.
elim Hneq.
apply (Compare.Valid.zero Hv); auto.
unfold Make.compare_keys in G.
destruct (Make.Ord.(COMPARABLE.compare) k k' =? 0) eqn:G0.
{ apply Z.eqb_eq; auto. }
{ destruct (Make.Ord.(COMPARABLE.compare) k k' <=? 0); discriminate.
}
}
{ destruct a0; simpl in ×.
destruct (Make.compare_keys k' k0) eqn:G; simpl in ×.
{ unfold Make.compare_keys in G.
destruct (Make.Ord.(COMPARABLE.compare) k' k0 =? 0) eqn:G0.
{ rewrite Z.eqb_eq in G0.
rewrite (Compare.Valid.zero Hv _ _ I I G0).
destruct (Make.compare_keys k k0) eqn:G1; auto.
elim Hneq.
apply (Compare.Valid.zero Hv); auto.
rewrite (Compare.Valid.zero Hv _ _ I I G0).
unfold Make.compare_keys in G1.
destruct (Make.Ord.(COMPARABLE.compare) k k0 =? 0) eqn:G2.
{ rewrite <- Z.eqb_eq; auto. }
{ destruct (Make.Ord.(COMPARABLE.compare) k k0 <=? 0);
discriminate.
}
}
{ destruct (Make.Ord.(COMPARABLE.compare) k' k0 <=? 0); discriminate. }
}
{ destruct (Make.compare_keys k k') eqn:G0.
{ elim Hneq.
unfold Make.compare_keys in G0.
destruct (Make.Ord.(COMPARABLE.compare) k k' =? 0) eqn:G1.
{ rewrite Z.eqb_eq in G1.
apply (Compare.Valid.zero Hv); auto.
}
{ destruct (Make.Ord.(COMPARABLE.compare) k k' <=? 0); discriminate. }
}
{ erewrite Valid.compare_keys_Lt_trans; eauto. }
{ destruct (Make.compare_keys k k0); auto. }
}
{ destruct (Make.compare_keys k k0); auto. }
}
Qed.
Make.find k m = None → Make.remove k m = m.
Proof.
intros Hfind.
induction m.
{ reflexivity. }
{ destruct a0; simpl in ×.
destruct (Make.compare_keys k k0).
{ discriminate. }
{ reflexivity. }
{ f_equal; auto. }
}
Qed.
Lemma add_add_eq `{Make.FArgs} {a : Set} (k : Make.key) (v v' : a)
(m : Make.t a) :
Valid.t → Make.add k v (Make.add k v' m) = Make.add k v m.
Proof.
intros Hv.
induction m.
{ simpl.
unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ destruct a0.
simpl in ×.
destruct (Make.compare_keys k k0) eqn:G; simpl.
{ unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ rewrite G.
f_equal; auto.
}
}
Qed.
Lemma mem_add_eq `{Make.FArgs} {a : Set} (k : Make.key) (v : a)
(m : Make.t a) :
Valid.t → Make.mem k (Make.add k v m) = true.
Proof.
intros Hv.
induction m; simpl in ×.
{ unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ destruct a0; simpl.
destruct (Make.compare_keys k k0) eqn:G; simpl.
{ unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ rewrite G; auto. }
}
Qed.
Lemma find_add_neq `{Make.FArgs} {a : Set} (k k' : Make.key) (v : a)
(m : Make.t a) :
Valid.t → k ≠ k' → Make.find k (Make.add k' v m) = Make.find k m.
Proof.
intros Hv Hneq.
induction m.
{ simpl.
destruct (Make.compare_keys k k') eqn:G; auto.
elim Hneq.
apply (Compare.Valid.zero Hv); auto.
unfold Make.compare_keys in G.
destruct (Make.Ord.(COMPARABLE.compare) k k' =? 0) eqn:G0.
{ apply Z.eqb_eq; auto. }
{ destruct (Make.Ord.(COMPARABLE.compare) k k' <=? 0); discriminate.
}
}
{ destruct a0; simpl in ×.
destruct (Make.compare_keys k' k0) eqn:G; simpl in ×.
{ unfold Make.compare_keys in G.
destruct (Make.Ord.(COMPARABLE.compare) k' k0 =? 0) eqn:G0.
{ rewrite Z.eqb_eq in G0.
rewrite (Compare.Valid.zero Hv _ _ I I G0).
destruct (Make.compare_keys k k0) eqn:G1; auto.
elim Hneq.
apply (Compare.Valid.zero Hv); auto.
rewrite (Compare.Valid.zero Hv _ _ I I G0).
unfold Make.compare_keys in G1.
destruct (Make.Ord.(COMPARABLE.compare) k k0 =? 0) eqn:G2.
{ rewrite <- Z.eqb_eq; auto. }
{ destruct (Make.Ord.(COMPARABLE.compare) k k0 <=? 0);
discriminate.
}
}
{ destruct (Make.Ord.(COMPARABLE.compare) k' k0 <=? 0); discriminate. }
}
{ destruct (Make.compare_keys k k') eqn:G0.
{ elim Hneq.
unfold Make.compare_keys in G0.
destruct (Make.Ord.(COMPARABLE.compare) k k' =? 0) eqn:G1.
{ rewrite Z.eqb_eq in G1.
apply (Compare.Valid.zero Hv); auto.
}
{ destruct (Make.Ord.(COMPARABLE.compare) k k' <=? 0); discriminate. }
}
{ erewrite Valid.compare_keys_Lt_trans; eauto. }
{ destruct (Make.compare_keys k k0); auto. }
}
{ destruct (Make.compare_keys k k0); auto. }
}
Qed.
Creates a map from a list of bindings.
Definition of_bindings `{Make.FArgs} {a : Set}
(l : list (Make.key × a)) : Make.t a :=
List.fold_right
(fun '(k, v) m ⇒ Make.add k v m) l Make.empty.
(l : list (Make.key × a)) : Make.t a :=
List.fold_right
(fun '(k, v) m ⇒ Make.add k v m) l Make.empty.
Relate the [find] operation in a map and its bindings list.
Lemma find_of_bindings `{Make.FArgs} {a : Set} (k : Make.key)
(l : list (Make.key × a)) :
Valid.t →
Make.find k (of_bindings l) =
List.find_map
(fun '(k', v) ⇒
if Make.Ord.(COMPARABLE.compare) k k' =? 0 then
Some v
else
None
)
l.
Proof.
intros Hv.
unfold of_bindings.
induction l.
{ reflexivity. }
{ simpl.
destruct a0.
destruct (Make.Ord.(COMPARABLE.compare) k k0 =? 0) eqn:Hkk0.
{ rewrite Z.eqb_eq in Hkk0.
rewrite (Compare.Valid.zero Hv _ _ I I Hkk0).
apply find_add; auto.
}
{ rewrite Z.eqb_neq in Hkk0.
rewrite (find_add_neq k k0 a0 _ Hv); auto.
intro Heq.
apply Hkk0.
rewrite Heq.
apply (Compare.Valid.refl Hv); auto.
}
}
Qed.
(l : list (Make.key × a)) :
Valid.t →
Make.find k (of_bindings l) =
List.find_map
(fun '(k', v) ⇒
if Make.Ord.(COMPARABLE.compare) k k' =? 0 then
Some v
else
None
)
l.
Proof.
intros Hv.
unfold of_bindings.
induction l.
{ reflexivity. }
{ simpl.
destruct a0.
destruct (Make.Ord.(COMPARABLE.compare) k k0 =? 0) eqn:Hkk0.
{ rewrite Z.eqb_eq in Hkk0.
rewrite (Compare.Valid.zero Hv _ _ I I Hkk0).
apply find_add; auto.
}
{ rewrite Z.eqb_neq in Hkk0.
rewrite (find_add_neq k k0 a0 _ Hv); auto.
intro Heq.
apply Hkk0.
rewrite Heq.
apply (Compare.Valid.refl Hv); auto.
}
}
Qed.
[bindings] and [of_bindings] are inverse
Lemma bindings_of_bindings `{Make.FArgs} {a : Set}
(l : list (Make.key × a)) :
Sorted.Sorted (fun '(k1,_) '(k2,_) ⇒
Make.Ord.(COMPARABLE.compare) k1 k2 = -1) l →
Make.bindings (of_bindings l) = l.
Proof.
unfold Make; simpl.
unfold Make.bindings.
unfold of_bindings.
intros.
induction l.
{ reflexivity. }
{ destruct l.
{ destruct a0; reflexivity. }
{ simpl in IHl.
destruct p.
simpl.
rewrite IHl.
{ destruct a0.
simpl.
unfold Make.compare_keys.
inversion H0.
inversion H4.
rewrite H6; auto.
}
{ inversion H0; auto. }
}
}
Qed.
Lemma cardinal_add_find_Some `{Make.FArgs} {a : Set} (m : Make.t a) k v v' :
Map.Make.find k m = Some v' →
Map.Make.cardinal (Map.Make.add k v m) = Map.Make.cardinal m.
Proof.
intros.
induction m.
{ discriminate. }
{ simpl in ×.
destruct a0.
destruct (Make.compare_keys k k0).
{ reflexivity. }
{ discriminate. }
{ unfold Make.cardinal; simpl.
f_equal; tauto.
}
}
Qed.
Lemma cardinal_add_find_None `{Make.FArgs} {a : Set} (m : Make.t a) k v :
Map.Make.find k m = None →
Map.Make.cardinal (Map.Make.add k v m) = Map.Make.cardinal m +i 1.
Proof.
intros.
induction m.
{ reflexivity. }
{ simpl in ×.
destruct a0.
destruct (Make.compare_keys k k0); try discriminate.
{ reflexivity. }
{ unfold Make.cardinal in *; simpl.
rewrite (IHm H0); auto.
}
}
Qed.
(l : list (Make.key × a)) :
Sorted.Sorted (fun '(k1,_) '(k2,_) ⇒
Make.Ord.(COMPARABLE.compare) k1 k2 = -1) l →
Make.bindings (of_bindings l) = l.
Proof.
unfold Make; simpl.
unfold Make.bindings.
unfold of_bindings.
intros.
induction l.
{ reflexivity. }
{ destruct l.
{ destruct a0; reflexivity. }
{ simpl in IHl.
destruct p.
simpl.
rewrite IHl.
{ destruct a0.
simpl.
unfold Make.compare_keys.
inversion H0.
inversion H4.
rewrite H6; auto.
}
{ inversion H0; auto. }
}
}
Qed.
Lemma cardinal_add_find_Some `{Make.FArgs} {a : Set} (m : Make.t a) k v v' :
Map.Make.find k m = Some v' →
Map.Make.cardinal (Map.Make.add k v m) = Map.Make.cardinal m.
Proof.
intros.
induction m.
{ discriminate. }
{ simpl in ×.
destruct a0.
destruct (Make.compare_keys k k0).
{ reflexivity. }
{ discriminate. }
{ unfold Make.cardinal; simpl.
f_equal; tauto.
}
}
Qed.
Lemma cardinal_add_find_None `{Make.FArgs} {a : Set} (m : Make.t a) k v :
Map.Make.find k m = None →
Map.Make.cardinal (Map.Make.add k v m) = Map.Make.cardinal m +i 1.
Proof.
intros.
induction m.
{ reflexivity. }
{ simpl in ×.
destruct a0.
destruct (Make.compare_keys k k0); try discriminate.
{ reflexivity. }
{ unfold Make.cardinal in *; simpl.
rewrite (IHm H0); auto.
}
}
Qed.
The cardinal of a map after adding an element.
Lemma cardinal_add_find `{Make.FArgs} {a : Set} (k : Make.key) (v : a)
(m : Make.t a) :
Make.cardinal (Make.add k v m) =
Make.cardinal m +i
match Make.find k m with
| None ⇒ 1
| Some _ ⇒ 0
end.
Proof.
simpl.
destruct Make.find as [v'|] eqn:?.
{ rewrite (cardinal_add_find_Some _ _ _ v') by assumption.
unfold Make.cardinal.
pose proof (List.length_is_valid m).
lia.
}
{ now rewrite cardinal_add_find_None. }
Qed.
Lemma length_remove_find_Some `{Make.FArgs} {a : Set}
(m : Make.t a) k v :
Map.Make.find k m = Some v →
Datatypes.S (Datatypes.length (Map.Make.remove k m)) =
Datatypes.length m.
Proof.
intros.
induction m.
{ discriminate. }
{ simpl in ×.
Tactics.destruct_pairs.
destruct Make.compare_keys.
{ reflexivity. }
{ discriminate. }
{ simpl; f_equal; auto. }
}
Qed.
(m : Make.t a) :
Make.cardinal (Make.add k v m) =
Make.cardinal m +i
match Make.find k m with
| None ⇒ 1
| Some _ ⇒ 0
end.
Proof.
simpl.
destruct Make.find as [v'|] eqn:?.
{ rewrite (cardinal_add_find_Some _ _ _ v') by assumption.
unfold Make.cardinal.
pose proof (List.length_is_valid m).
lia.
}
{ now rewrite cardinal_add_find_None. }
Qed.
Lemma length_remove_find_Some `{Make.FArgs} {a : Set}
(m : Make.t a) k v :
Map.Make.find k m = Some v →
Datatypes.S (Datatypes.length (Map.Make.remove k m)) =
Datatypes.length m.
Proof.
intros.
induction m.
{ discriminate. }
{ simpl in ×.
Tactics.destruct_pairs.
destruct Make.compare_keys.
{ reflexivity. }
{ discriminate. }
{ simpl; f_equal; auto. }
}
Qed.
The cardinal of a map after removal, when the element is there.
Lemma cardinal_remove_find_Some `{Make.FArgs} {a : Set}
(m : Make.t a) k v :
Map.Make.find k m = Some v →
Map.Make.cardinal (Map.Make.remove k m) =
Map.Make.cardinal m -i 1.
Proof.
intros.
unfold Map.Make.cardinal.
induction m; simpl in ×.
{ discriminate. }
{ Tactics.destruct_pairs.
pose proof (List.length_is_valid m).
destruct Make.compare_keys; simpl; try discriminate; lia.
}
Qed.
(m : Make.t a) k v :
Map.Make.find k m = Some v →
Map.Make.cardinal (Map.Make.remove k m) =
Map.Make.cardinal m -i 1.
Proof.
intros.
unfold Map.Make.cardinal.
induction m; simpl in ×.
{ discriminate. }
{ Tactics.destruct_pairs.
pose proof (List.length_is_valid m).
destruct Make.compare_keys; simpl; try discriminate; lia.
}
Qed.
The cardinal of a map after removal, when the element is not there.
Lemma cardinal_remove_find_None `{Make.FArgs} {a : Set}
(m : Make.t a) k :
Map.Make.find k m = None →
Map.Make.cardinal (Map.Make.remove k m) =
Map.Make.cardinal m.
Proof.
intros.
unfold Map.Make.cardinal.
induction m; hauto q: on.
Qed.
(m : Make.t a) k :
Map.Make.find k m = None →
Map.Make.cardinal (Map.Make.remove k m) =
Map.Make.cardinal m.
Proof.
intros.
unfold Map.Make.cardinal.
induction m; hauto q: on.
Qed.
The cardinal of a map after removing an element.
Lemma cardinal_remove_find `{Make.FArgs} {a : Set}
(k : Make.key) (m : Make.t a) :
Make.cardinal (Make.remove k m) =
Make.cardinal m -i
match Make.find k m with
| None ⇒ 0
| Some _ ⇒ 1
end.
Proof.
simpl.
destruct Make.find eqn:?.
{ eapply cardinal_remove_find_Some; eauto. }
{ rewrite cardinal_remove_find_None by assumption.
unfold Make.cardinal.
pose proof (List.length_is_valid m).
lia.
}
Qed.
(k : Make.key) (m : Make.t a) :
Make.cardinal (Make.remove k m) =
Make.cardinal m -i
match Make.find k m with
| None ⇒ 0
| Some _ ⇒ 1
end.
Proof.
simpl.
destruct Make.find eqn:?.
{ eapply cardinal_remove_find_Some; eauto. }
{ rewrite cardinal_remove_find_None by assumption.
unfold Make.cardinal.
pose proof (List.length_is_valid m).
lia.
}
Qed.
The cardinal of a map is a valid integer.
Lemma cardinal_is_valid `{Make.FArgs} {a : Set} (m : Make.t a) :
Pervasives.Int.Valid.t (Make.cardinal m).
Proof.
apply List.length_is_valid.
Qed.
Pervasives.Int.Valid.t (Make.cardinal m).
Proof.
apply List.length_is_valid.
Qed.
Finding after a map operation is like finding before and then applying the
mapping function over the result.
Lemma find_map `{Make.FArgs} {a b : Set} (k : Make.key) (f : a → b)
(m : Make.t a) :
(let× x := Make.find k m in
Some (f x)) =
(Make.find k (Make.map f m)).
Proof.
simpl.
induction m; hauto lq: on.
Qed.
(m : Make.t a) :
(let× x := Make.find k m in
Some (f x)) =
(Make.find k (Make.map f m)).
Proof.
simpl.
induction m; hauto lq: on.
Qed.
Adding and mapping a function over a map are commuting.
Lemma add_map `{Make.FArgs} {a b : Set} (k : Make.key) (v : a) (f : a → b)
(m : Make.t a) :
Make.add k (f v) (Make.map f m) =
Make.map f (Make.add k v m).
Proof.
simpl.
induction m; hauto lq: on.
Qed.
(m : Make.t a) :
Make.add k (f v) (Make.map f m) =
Make.map f (Make.add k v m).
Proof.
simpl.
induction m; hauto lq: on.
Qed.
The result of [Map.Make.mem] is not affected by [Map.Make.map].
Lemma mem_map `{Make.FArgs} {a b : Set} (k : Make.key) (f : a → b)
(m : Make.t a) :
Make.mem k (Make.map f m) = Make.mem k m.
Proof.
induction m; [reflexivity|].
destruct a0; simpl.
now destruct Map.Make.compare_keys.
Qed.
(m : Make.t a) :
Make.mem k (Make.map f m) = Make.mem k m.
Proof.
induction m; [reflexivity|].
destruct a0; simpl.
now destruct Map.Make.compare_keys.
Qed.
Removing and mapping a function over a map are commuting.
Lemma remove_map `{Make.FArgs} {a b : Set} (k : Make.key) (f : a → b)
(m : Make.t a) :
Make.remove k (Make.map f m) =
Make.map f (Make.remove k m).
Proof.
simpl.
induction m; hauto lq: on.
Qed.
(m : Make.t a) :
Make.remove k (Make.map f m) =
Make.map f (Make.remove k m).
Proof.
simpl.
induction m; hauto lq: on.
Qed.
Result of the application of a [fold] after a [map] operation.
Lemma fold_map `{Make.FArgs} {a b acc : Set} (f : a → b)
(g : Make.key → b → acc → acc) (m : Make.t a) (init : acc) :
Make.fold g (Make.map f m) init =
Make.fold (fun k v a ⇒ g k (f v) a) m init.
Proof.
revert init.
induction m as [|[]]; simpl; sfirstorder.
Qed.
(g : Make.key → b → acc → acc) (m : Make.t a) (init : acc) :
Make.fold g (Make.map f m) init =
Make.fold (fun k v a ⇒ g k (f v) a) m init.
Proof.
revert init.
induction m as [|[]]; simpl; sfirstorder.
Qed.
Result of the application of a [fold_es] after a [map] operation.
Lemma fold_es_map `{Make.FArgs} {a b acc : Set} (f : a → b)
(g : Make.key → b → acc → M? acc) (m : Make.t a) (init : acc) :
Make.fold_es g (Make.map f m) init =
Make.fold_es (fun k v a ⇒ g k (f v) a) m init.
Proof.
intros.
apply fold_map.
Qed.
Lemma In_add `{Make.FArgs} {a : Set}
(k : Make.key) (v : a) (m : Make.t a) :
In (k, v) (Make.add k v m).
Proof.
induction m; [left; auto|].
simpl. destruct a0.
destruct Make.compare_keys eqn:?; simpl; [left|left|right]; auto.
Qed.
Lemma In_add_intro `{Make.FArgs} {a : Set} (k k': Make.key)
(v v': a) (m : Make.t a) :
Valid.t →
(k, v) = (k', v') ∨ (k ≠ k' ∧ In (k, v) m) →
In (k, v) (Make.add k' v' m).
Proof.
intro Hv.
induction m; simpl; intros Hi.
{ destruct Hi; auto. induction H0; auto. }
{ destruct a0 as [k0 a0].
destruct Hi.
{ inversion H0; subst k' v'; clear H0.
destruct (Make.compare_keys k k0) eqn:?; simpl; [left|left|right]; auto.
}
{ induction H0.
induction H1.
{ inversion H1; subst k0 a0; clear H1.
remember (Make.compare_keys k' k) as kk. symmetry in Heqkk.
destruct kk.
{ apply (Valid.compare_keys_Eq Hv) in Heqkk; subst.
contradiction H0; auto.
}
{ right; left; auto. }
{ left; auto. }
}
{ assert (In (k, v) (Make.add k' v' m)). {
apply IHm; right; auto.
}
destruct (Make.compare_keys k' k0);
[right|right; right| right]; auto.
}
}
}
Qed.
Lemma pick_opt_not_In `{Make.FArgs} {a : Set} (Hv : Map.Valid.t)
(k : Make.key) (m : Make.t a) (v : option a) (m' : Make.t a) :
StrictlySorted.t (List.map fst m) →
Make.pick_opt k m = (v,m') →
¬ In k (List.map fst m').
Proof.
intros Hss Hk F.
apply (StrictlySorted.pick_opt_to_ind Hv) in Hk.
induction Hk; simpl in *; auto.
{ induction (List.map fst m); auto; simpl in ×.
induction Hss; induction F.
{ subst. rewrite (Compare.Valid.refl Hv) in H0. inversion H0. auto. }
{ apply IHl; auto. destruct l; auto; simpl.
induction H1; split; auto.
apply (Compare.Valid.trans_lt Hv) with a0; auto.
}
}
{ induction F.
{ subst. apply (Valid.compare_keys_Lt Hv) in H0.
rewrite (Compare.Valid.refl Hv) in H0. inversion H0. auto. }
{ induction (List.map fst m); auto.
simpl in ×. induction Hss.
induction H1.
{ subst. apply (Valid.compare_keys_Lt Hv) in H0.
rewrite (Compare.Valid.sym Hv) in H0; auto.
rewrite H2 in H0; inversion H0.
}
{ apply IHl; auto.
destruct l; auto.
induction H3; simpl; split.
{ auto. apply (Compare.Valid.trans_lt Hv) with a0; auto. }
{ induction H1; auto. }
}
}
}
{ induction F.
{ subst. apply (Valid.compare_keys_Gt Hv) in H0.
rewrite (Compare.Valid.refl Hv) in H0; inversion H0; auto.
}
{ apply IHHk; auto.
destruct (List.map fst m); auto; simpl.
induction Hss; auto.
}
}
Qed.
Lemma Make_merge_In1 `{Make.FArgs} {a b c : Set}
{f : Make.key → M× a → M× b → M× c}
{Hv : Map.Valid.t} {m1 : Make.t a} {Hss : StrictlySorted.t (List.map fst m1)}
: ∀ {m2 k c v},
In (k, v) m1 →
¬ In k (List.map fst m2) →
f k (Some v) None = Some c →
In (k, c) (Make.merge f m1 m2).
Proof.
induction m1; intros.
{ destruct H0. }
{ destruct a0 as [k' a'].
destruct H0.
{ simpl in ×.
assert (Make.pick_opt k m2 = (None, m2)). {
induction m2; simpl; auto.
destruct a0 as [k'']; simpl in ×.
destruct (Make.compare_keys k k'') eqn:?; auto.
{ apply (Valid.compare_keys_Eq Hv) in Heqc1.
contradiction H1; left; auto.
}
{ assert (Make.pick_opt k m2 = (None, m2)) by auto.
rewrite H3; auto.
}
}
inversion H0; subst k' a'; clear H0.
rewrite H3, H2.
apply In_add.
}
{ simpl.
destruct (Make.pick_opt k' m2) eqn:?.
apply (StrictlySorted.pick_opt_to_ind Hv) in Heqp.
assert (In (k, c0) (Make.merge f m1 t)). {
apply IHm1 with v; auto; clear IHm1.
{ simpl in Hss; destruct (List.map fst m1); auto.
induction Hss; auto.
}
{ induction Heqp; simpl; auto.
{ intro F; apply H1; right; auto. }
{ intro F; induction F; subst.
{ apply H1; left; auto. }
{ apply IHHeqp; auto.
intro F; apply H1; right; auto.
}
}
}
}
destruct (f k' (Some a') o); auto.
apply In_add_intro; auto; right; split; auto.
simpl in Hss.
intro F; subst k'.
clear IHm1 H3.
induction m1.
{ inversion H0. }
{ induction Hss.
induction H0; subst.
{ simpl in H4. rewrite (Compare.Valid.refl Hv) in H3; auto.
inversion H3; auto.
}
{ apply IHm1; auto; clear IHm1.
{ induction (List.map fst m1); auto.
induction H4; simpl; split; auto.
apply (Compare.Valid.trans_lt Hv) with (fst a0); auto.
}
}
}
}
}
Qed.
Lemma Make_merge_In2 `{Make.FArgs} {a b c : Set}
{f : Make.key → M× a → M× b → M× c}
{Hv : Map.Valid.t} {m1 : Make.t a} {Hss : StrictlySorted.t (List.map fst m1)}
: ∀ {m2 k w v},
In (k, v) m2 →
¬ In k (List.map fst m1) →
f k None (Some v) = Some w →
In (k, w) (Make.merge f m1 m2).
Proof.
induction m1; intros.
{ simpl in ×.
induction m2; simpl.
{ inversion H0. }
{ destruct H0.
{ subst a0. rewrite H2. left. auto. }
{ destruct a0. destruct (f k0 None (Some b0)); [right|]; auto. }
}
}
{ destruct a0; simpl.
destruct (Make.pick_opt k0 m2) eqn:?.
apply (StrictlySorted.pick_opt_to_ind Hv) in Heqp.
assert (In (k, w) (Make.merge f m1 t)). {
apply IHm1 with v; auto.
{ simpl in Hss.
destruct (List.map fst m1); auto.
destruct Hss; auto.
}
{ induction Heqp; simpl in *; auto.
{ induction H0; auto.
inversion H0; subst.
contradiction H1; left; auto.
}
{ destruct H0; [left|right]; auto. }
}
{ intro F; apply H1; right; auto. }
}
destruct (f k0 (Some a0) o); auto.
apply In_add_intro; auto.
right; split; auto.
intro F; subst k0.
contradiction H1; left; auto.
}
Qed.
Lemma Make_merge_In3 `{Make.FArgs} {a b c : Set}
{f : Make.key → M× a → M× b → M× c}
{m1 : Make.t a} {Hss : StrictlySorted.t (List.map fst m1)}
: ∀ {m2 k w u v},
In (k, u) m1 →
In (k, v) m2 →
f k (Some u) (Some v) = Some w →
In (k, w) (Make.merge f m1 m2).
Proof.
intros.
Admitted.
Lemma Make_merge_In_inversion `{Make.FArgs} {a b c : Set}
{f : Make.key → M× a → M× b → M× c}
{m1 : Make.t a} : ∀ {m2 k w},
In (k, w) (Make.merge f m1 m2) →
(∃ u, In (k, u) m1
∧ ¬ In k (List.map fst m2)
∧ f k (Some u) None = Some w)
∨ (∃ v, In (k, v) m2
∧ ¬ In k (List.map fst m1)
∧ f k None (Some v) = Some w)
∨ (∃ u v, In (k, u) m1 ∧ In (k, v) m2
∧ f k (Some u) (Some v) = Some w).
Proof.
induction m1; simpl; intros.
{ destruct (List.filter_map_In_invert H0) as [x [Hx1 Hx2]].
destruct x as [k' v].
destruct f eqn:?; [|discriminate].
inversion Hx2; sauto.
}
{ destruct a0.
destruct Make.pick_opt eqn:?.
destruct f eqn:?.
{ admit. }
{ admit. }
}
Admitted.
Lemma Make_fold_shortcircuit `{Make.FArgs} {a b tr : Set}
(f : Make.key → a → Pervasives.result b tr → Pervasives.result b tr)
(f_pres_err : ∀ t k x, f k x (Pervasives.Error t) = Pervasives.Error t)
(t : tr) : ∀ m : Make.t a,
Make.fold f m (Pervasives.Error t) = Pervasives.Error t.
Proof.
unfold Make.fold.
induction m as [|[k v] m]; simpl; [reflexivity|].
congruence.
Qed.
Lemma find_In `{Make.FArgs} {a : Set}
(m : Make.t a) k v :
Valid.t →
StrictlySorted.t (List.map fst m) →
Make.find k m = Some v → In k (List.map fst m).
Proof.
(*TODO*)
Admitted.
Lemma find_not_In `{Make.FArgs} {a : Set}
(Hv : Map.Valid.t)
(m : Make.t a) k : ¬ In k (List.map fst m) →
Make.find k m = None.
Proof.
induction m; intro Hnin.
{ reflexivity. }
{ simpl.
destruct a0.
destruct Make.compare_keys eqn:?; auto.
{ elim Hnin.
left.
symmetry; apply Map.Valid.compare_keys_Eq; auto.
}
{ simpl in *; tauto. }
}
Qed.
Lemma mapi_preserves_keys `{Make.FArgs} {a b : Set}
(f : Make.key → a → b) (m : Make.t a) :
List.map fst (Make.mapi f m)
= List.map fst m.
Proof.
induction m.
{ reflexivity. }
{ destruct a0.
simpl; congruence.
}
Qed.
Definition disj {A : Set} (xs ys : list A) : Prop :=
∀ x, In x xs → ¬ In x ys.
Lemma disj_key_still_In `{Make.FArgs} {a : Set}
(Hv : Map.Valid.t)
(m : Make.t a) : ∀ p k v, ¬ In k (List.map fst m)
→ In p m → In p (Make.add k v m).
Proof.
induction m; intros.
{ destruct H1. }
{ simpl.
Tactics.destruct_pairs.
destruct Make.compare_keys eqn:?.
{ assert (k = k1) by (apply Map.Valid.compare_keys_Eq; auto).
elim H0; hauto.
}
{ right; auto. }
{ destruct H1; hauto. }
}
Qed.
Lemma In_to_In_fold `{Make.FArgs} {a b : Set}
(f : Make.key → a → b)
(m1 : Make.t a) (m2 : Make.t b) k v :
Valid.t →
StrictlySorted.t (List.map fst m1) →
StrictlySorted.t (List.map fst m2) →
disj (List.map fst m1) (List.map fst m2) →
(In (k, v) m1 ∨ In (k, f k v) m2) →
In (k, f k v) (Make.fold
(fun k0 v ⇒ Make.add k0 (f k0 v)) m1 m2).
Proof.
revert m2 k v.
induction m1; intros m2 k a' Hv Hss1 Hss2 Hdis Hin.
{ simpl.
destruct Hin as [[]|]; auto.
}
{ simpl.
destruct a0.
apply IHm1; auto.
{ eapply StrictlySorted.ss_tail; exact Hss1. }
{ apply StrictlySorted.add_preserves_sorting; auto. }
{ intros x Hx1 Hx2.
destruct (List.In_map_invert Hx1) as [[] [Hp1 Hp2]].
simpl in ×.
rewrite <- Hp1 in *; clear Hp1.
destruct (List.In_map_invert Hx2) as [[] [Hq1 Hq2]].
simpl in ×.
rewrite Hq1 in Hq2; clear Hq1.
destruct (In_add_destruct Hq2).
{ inversion H0.
rewrite <- H2 in Hp2.
pose proof (in_map fst _ _ Hp2); simpl in ×.
epose proof (StrictlySorted.strictly_sorted_lb_correct
_ _ Hv Hss1 _ H1).
rewrite (Compare.Valid.refl Hv) in H4; lia.
}
{ eapply Hdis.
{ right. apply in_map; eauto. }
{ assert (fst (k1, a1) = fst (k1, b0))
by auto.
rewrite H1.
apply in_map; auto.
}
}
}
destruct Hin.
{ destruct H0; try tauto.
right; inversion H0.
simpl in Hss1.
apply In_add.
}
{ right.
apply disj_key_still_In; auto.
intro; eapply Hdis.
{ left; reflexivity. }
{ exact H1. }
}
}
Qed.
Lemma In_mapi `{Make.FArgs} {a b : Set}
(f : Make.key → a → b) (m : Make.t a) k v :
In (k, v) m → In (k, f k v) (Make.mapi f m).
Proof.
induction m; intros Hin; destruct Hin.
{ simpl; Tactics.destruct_pairs.
left; congruence.
}
{ simpl; Tactics.destruct_pairs.
right; auto.
}
Qed.
Lemma In_mapi_invert `{Make.FArgs} {a b : Set}
{f : Make.key → a → b} {m : Make.t a} k v :
In (k, v) (Make.mapi f m) →
∃ u, In (k, u) m ∧ f k u = v.
Proof.
induction m; intros Hin.
{ destruct Hin. }
{ simpl in Hin; Tactics.destruct_pairs.
destruct Hin.
{ ∃ a0; sfirstorder. }
{ destruct (IHm H0) as [a' [Ha'1 Ha'2]].
∃ a'; sfirstorder. }
}
Qed.
(g : Make.key → b → acc → M? acc) (m : Make.t a) (init : acc) :
Make.fold_es g (Make.map f m) init =
Make.fold_es (fun k v a ⇒ g k (f v) a) m init.
Proof.
intros.
apply fold_map.
Qed.
Lemma In_add `{Make.FArgs} {a : Set}
(k : Make.key) (v : a) (m : Make.t a) :
In (k, v) (Make.add k v m).
Proof.
induction m; [left; auto|].
simpl. destruct a0.
destruct Make.compare_keys eqn:?; simpl; [left|left|right]; auto.
Qed.
Lemma In_add_intro `{Make.FArgs} {a : Set} (k k': Make.key)
(v v': a) (m : Make.t a) :
Valid.t →
(k, v) = (k', v') ∨ (k ≠ k' ∧ In (k, v) m) →
In (k, v) (Make.add k' v' m).
Proof.
intro Hv.
induction m; simpl; intros Hi.
{ destruct Hi; auto. induction H0; auto. }
{ destruct a0 as [k0 a0].
destruct Hi.
{ inversion H0; subst k' v'; clear H0.
destruct (Make.compare_keys k k0) eqn:?; simpl; [left|left|right]; auto.
}
{ induction H0.
induction H1.
{ inversion H1; subst k0 a0; clear H1.
remember (Make.compare_keys k' k) as kk. symmetry in Heqkk.
destruct kk.
{ apply (Valid.compare_keys_Eq Hv) in Heqkk; subst.
contradiction H0; auto.
}
{ right; left; auto. }
{ left; auto. }
}
{ assert (In (k, v) (Make.add k' v' m)). {
apply IHm; right; auto.
}
destruct (Make.compare_keys k' k0);
[right|right; right| right]; auto.
}
}
}
Qed.
Lemma pick_opt_not_In `{Make.FArgs} {a : Set} (Hv : Map.Valid.t)
(k : Make.key) (m : Make.t a) (v : option a) (m' : Make.t a) :
StrictlySorted.t (List.map fst m) →
Make.pick_opt k m = (v,m') →
¬ In k (List.map fst m').
Proof.
intros Hss Hk F.
apply (StrictlySorted.pick_opt_to_ind Hv) in Hk.
induction Hk; simpl in *; auto.
{ induction (List.map fst m); auto; simpl in ×.
induction Hss; induction F.
{ subst. rewrite (Compare.Valid.refl Hv) in H0. inversion H0. auto. }
{ apply IHl; auto. destruct l; auto; simpl.
induction H1; split; auto.
apply (Compare.Valid.trans_lt Hv) with a0; auto.
}
}
{ induction F.
{ subst. apply (Valid.compare_keys_Lt Hv) in H0.
rewrite (Compare.Valid.refl Hv) in H0. inversion H0. auto. }
{ induction (List.map fst m); auto.
simpl in ×. induction Hss.
induction H1.
{ subst. apply (Valid.compare_keys_Lt Hv) in H0.
rewrite (Compare.Valid.sym Hv) in H0; auto.
rewrite H2 in H0; inversion H0.
}
{ apply IHl; auto.
destruct l; auto.
induction H3; simpl; split.
{ auto. apply (Compare.Valid.trans_lt Hv) with a0; auto. }
{ induction H1; auto. }
}
}
}
{ induction F.
{ subst. apply (Valid.compare_keys_Gt Hv) in H0.
rewrite (Compare.Valid.refl Hv) in H0; inversion H0; auto.
}
{ apply IHHk; auto.
destruct (List.map fst m); auto; simpl.
induction Hss; auto.
}
}
Qed.
Lemma Make_merge_In1 `{Make.FArgs} {a b c : Set}
{f : Make.key → M× a → M× b → M× c}
{Hv : Map.Valid.t} {m1 : Make.t a} {Hss : StrictlySorted.t (List.map fst m1)}
: ∀ {m2 k c v},
In (k, v) m1 →
¬ In k (List.map fst m2) →
f k (Some v) None = Some c →
In (k, c) (Make.merge f m1 m2).
Proof.
induction m1; intros.
{ destruct H0. }
{ destruct a0 as [k' a'].
destruct H0.
{ simpl in ×.
assert (Make.pick_opt k m2 = (None, m2)). {
induction m2; simpl; auto.
destruct a0 as [k'']; simpl in ×.
destruct (Make.compare_keys k k'') eqn:?; auto.
{ apply (Valid.compare_keys_Eq Hv) in Heqc1.
contradiction H1; left; auto.
}
{ assert (Make.pick_opt k m2 = (None, m2)) by auto.
rewrite H3; auto.
}
}
inversion H0; subst k' a'; clear H0.
rewrite H3, H2.
apply In_add.
}
{ simpl.
destruct (Make.pick_opt k' m2) eqn:?.
apply (StrictlySorted.pick_opt_to_ind Hv) in Heqp.
assert (In (k, c0) (Make.merge f m1 t)). {
apply IHm1 with v; auto; clear IHm1.
{ simpl in Hss; destruct (List.map fst m1); auto.
induction Hss; auto.
}
{ induction Heqp; simpl; auto.
{ intro F; apply H1; right; auto. }
{ intro F; induction F; subst.
{ apply H1; left; auto. }
{ apply IHHeqp; auto.
intro F; apply H1; right; auto.
}
}
}
}
destruct (f k' (Some a') o); auto.
apply In_add_intro; auto; right; split; auto.
simpl in Hss.
intro F; subst k'.
clear IHm1 H3.
induction m1.
{ inversion H0. }
{ induction Hss.
induction H0; subst.
{ simpl in H4. rewrite (Compare.Valid.refl Hv) in H3; auto.
inversion H3; auto.
}
{ apply IHm1; auto; clear IHm1.
{ induction (List.map fst m1); auto.
induction H4; simpl; split; auto.
apply (Compare.Valid.trans_lt Hv) with (fst a0); auto.
}
}
}
}
}
Qed.
Lemma Make_merge_In2 `{Make.FArgs} {a b c : Set}
{f : Make.key → M× a → M× b → M× c}
{Hv : Map.Valid.t} {m1 : Make.t a} {Hss : StrictlySorted.t (List.map fst m1)}
: ∀ {m2 k w v},
In (k, v) m2 →
¬ In k (List.map fst m1) →
f k None (Some v) = Some w →
In (k, w) (Make.merge f m1 m2).
Proof.
induction m1; intros.
{ simpl in ×.
induction m2; simpl.
{ inversion H0. }
{ destruct H0.
{ subst a0. rewrite H2. left. auto. }
{ destruct a0. destruct (f k0 None (Some b0)); [right|]; auto. }
}
}
{ destruct a0; simpl.
destruct (Make.pick_opt k0 m2) eqn:?.
apply (StrictlySorted.pick_opt_to_ind Hv) in Heqp.
assert (In (k, w) (Make.merge f m1 t)). {
apply IHm1 with v; auto.
{ simpl in Hss.
destruct (List.map fst m1); auto.
destruct Hss; auto.
}
{ induction Heqp; simpl in *; auto.
{ induction H0; auto.
inversion H0; subst.
contradiction H1; left; auto.
}
{ destruct H0; [left|right]; auto. }
}
{ intro F; apply H1; right; auto. }
}
destruct (f k0 (Some a0) o); auto.
apply In_add_intro; auto.
right; split; auto.
intro F; subst k0.
contradiction H1; left; auto.
}
Qed.
Lemma Make_merge_In3 `{Make.FArgs} {a b c : Set}
{f : Make.key → M× a → M× b → M× c}
{m1 : Make.t a} {Hss : StrictlySorted.t (List.map fst m1)}
: ∀ {m2 k w u v},
In (k, u) m1 →
In (k, v) m2 →
f k (Some u) (Some v) = Some w →
In (k, w) (Make.merge f m1 m2).
Proof.
intros.
Admitted.
Lemma Make_merge_In_inversion `{Make.FArgs} {a b c : Set}
{f : Make.key → M× a → M× b → M× c}
{m1 : Make.t a} : ∀ {m2 k w},
In (k, w) (Make.merge f m1 m2) →
(∃ u, In (k, u) m1
∧ ¬ In k (List.map fst m2)
∧ f k (Some u) None = Some w)
∨ (∃ v, In (k, v) m2
∧ ¬ In k (List.map fst m1)
∧ f k None (Some v) = Some w)
∨ (∃ u v, In (k, u) m1 ∧ In (k, v) m2
∧ f k (Some u) (Some v) = Some w).
Proof.
induction m1; simpl; intros.
{ destruct (List.filter_map_In_invert H0) as [x [Hx1 Hx2]].
destruct x as [k' v].
destruct f eqn:?; [|discriminate].
inversion Hx2; sauto.
}
{ destruct a0.
destruct Make.pick_opt eqn:?.
destruct f eqn:?.
{ admit. }
{ admit. }
}
Admitted.
Lemma Make_fold_shortcircuit `{Make.FArgs} {a b tr : Set}
(f : Make.key → a → Pervasives.result b tr → Pervasives.result b tr)
(f_pres_err : ∀ t k x, f k x (Pervasives.Error t) = Pervasives.Error t)
(t : tr) : ∀ m : Make.t a,
Make.fold f m (Pervasives.Error t) = Pervasives.Error t.
Proof.
unfold Make.fold.
induction m as [|[k v] m]; simpl; [reflexivity|].
congruence.
Qed.
Lemma find_In `{Make.FArgs} {a : Set}
(m : Make.t a) k v :
Valid.t →
StrictlySorted.t (List.map fst m) →
Make.find k m = Some v → In k (List.map fst m).
Proof.
(*TODO*)
Admitted.
Lemma find_not_In `{Make.FArgs} {a : Set}
(Hv : Map.Valid.t)
(m : Make.t a) k : ¬ In k (List.map fst m) →
Make.find k m = None.
Proof.
induction m; intro Hnin.
{ reflexivity. }
{ simpl.
destruct a0.
destruct Make.compare_keys eqn:?; auto.
{ elim Hnin.
left.
symmetry; apply Map.Valid.compare_keys_Eq; auto.
}
{ simpl in *; tauto. }
}
Qed.
Lemma mapi_preserves_keys `{Make.FArgs} {a b : Set}
(f : Make.key → a → b) (m : Make.t a) :
List.map fst (Make.mapi f m)
= List.map fst m.
Proof.
induction m.
{ reflexivity. }
{ destruct a0.
simpl; congruence.
}
Qed.
Definition disj {A : Set} (xs ys : list A) : Prop :=
∀ x, In x xs → ¬ In x ys.
Lemma disj_key_still_In `{Make.FArgs} {a : Set}
(Hv : Map.Valid.t)
(m : Make.t a) : ∀ p k v, ¬ In k (List.map fst m)
→ In p m → In p (Make.add k v m).
Proof.
induction m; intros.
{ destruct H1. }
{ simpl.
Tactics.destruct_pairs.
destruct Make.compare_keys eqn:?.
{ assert (k = k1) by (apply Map.Valid.compare_keys_Eq; auto).
elim H0; hauto.
}
{ right; auto. }
{ destruct H1; hauto. }
}
Qed.
Lemma In_to_In_fold `{Make.FArgs} {a b : Set}
(f : Make.key → a → b)
(m1 : Make.t a) (m2 : Make.t b) k v :
Valid.t →
StrictlySorted.t (List.map fst m1) →
StrictlySorted.t (List.map fst m2) →
disj (List.map fst m1) (List.map fst m2) →
(In (k, v) m1 ∨ In (k, f k v) m2) →
In (k, f k v) (Make.fold
(fun k0 v ⇒ Make.add k0 (f k0 v)) m1 m2).
Proof.
revert m2 k v.
induction m1; intros m2 k a' Hv Hss1 Hss2 Hdis Hin.
{ simpl.
destruct Hin as [[]|]; auto.
}
{ simpl.
destruct a0.
apply IHm1; auto.
{ eapply StrictlySorted.ss_tail; exact Hss1. }
{ apply StrictlySorted.add_preserves_sorting; auto. }
{ intros x Hx1 Hx2.
destruct (List.In_map_invert Hx1) as [[] [Hp1 Hp2]].
simpl in ×.
rewrite <- Hp1 in *; clear Hp1.
destruct (List.In_map_invert Hx2) as [[] [Hq1 Hq2]].
simpl in ×.
rewrite Hq1 in Hq2; clear Hq1.
destruct (In_add_destruct Hq2).
{ inversion H0.
rewrite <- H2 in Hp2.
pose proof (in_map fst _ _ Hp2); simpl in ×.
epose proof (StrictlySorted.strictly_sorted_lb_correct
_ _ Hv Hss1 _ H1).
rewrite (Compare.Valid.refl Hv) in H4; lia.
}
{ eapply Hdis.
{ right. apply in_map; eauto. }
{ assert (fst (k1, a1) = fst (k1, b0))
by auto.
rewrite H1.
apply in_map; auto.
}
}
}
destruct Hin.
{ destruct H0; try tauto.
right; inversion H0.
simpl in Hss1.
apply In_add.
}
{ right.
apply disj_key_still_In; auto.
intro; eapply Hdis.
{ left; reflexivity. }
{ exact H1. }
}
}
Qed.
Lemma In_mapi `{Make.FArgs} {a b : Set}
(f : Make.key → a → b) (m : Make.t a) k v :
In (k, v) m → In (k, f k v) (Make.mapi f m).
Proof.
induction m; intros Hin; destruct Hin.
{ simpl; Tactics.destruct_pairs.
left; congruence.
}
{ simpl; Tactics.destruct_pairs.
right; auto.
}
Qed.
Lemma In_mapi_invert `{Make.FArgs} {a b : Set}
{f : Make.key → a → b} {m : Make.t a} k v :
In (k, v) (Make.mapi f m) →
∃ u, In (k, u) m ∧ f k u = v.
Proof.
induction m; intros Hin.
{ destruct Hin. }
{ simpl in Hin; Tactics.destruct_pairs.
destruct Hin.
{ ∃ a0; sfirstorder. }
{ destruct (IHm H0) as [a' [Ha'1 Ha'2]].
∃ a'; sfirstorder. }
}
Qed.
[Make.map] is equivalent to [List.map] on the value
Lemma map_list_eq `{Make.FArgs} {a b : Set}
(f : a → b) (m : Make.t a) :
Make.map f m = List.map (fun '(k, v) ⇒ (k, f v)) m.
Proof.
induction m; hauto lq:on.
Qed.
(f : a → b) (m : Make.t a) :
Make.map f m = List.map (fun '(k, v) ⇒ (k, f v)) m.
Proof.
induction m; hauto lq:on.
Qed.
Adding a valid (w.r.t [P]) element to a map preserves [P]
Lemma make_add_preserves_P `{Make.FArgs} {a : Set} (m : Make.t a)
(P : Make.key × a → Prop) (v : a) k :
P (k, v) →
Forall P m →
Forall P (Make.add k v m).
Proof.
intros H_P H_Forall.
induction m as [|? ? IHm]; [constructor; assumption|].
inversion H_Forall.
cbn. do 2 step; [now constructor..|].
constructor; [assumption|]. now apply IHm.
Qed.
(P : Make.key × a → Prop) (v : a) k :
P (k, v) →
Forall P m →
Forall P (Make.add k v m).
Proof.
intros H_P H_Forall.
induction m as [|? ? IHm]; [constructor; assumption|].
inversion H_Forall.
cbn. do 2 step; [now constructor..|].
constructor; [assumption|]. now apply IHm.
Qed.
Removing an element from a map preserves [P]
Lemma make_remove_preserves_P `{Make.FArgs} {a : Set} (m : Make.t a)
(P : Make.key × a → Prop) k :
Forall P m →
Forall P (Make.remove k m).
Proof.
intros H_Forall.
induction m as [|? ? IHm]; [constructor; assumption|].
inversion H_Forall.
cbn. do 2 step.
{ assumption. }
{ assumption. }
{ constructor; [assumption|].
now apply IHm.
}
Qed.
(P : Make.key × a → Prop) k :
Forall P m →
Forall P (Make.remove k m).
Proof.
intros H_Forall.
induction m as [|? ? IHm]; [constructor; assumption|].
inversion H_Forall.
cbn. do 2 step.
{ assumption. }
{ assumption. }
{ constructor; [assumption|].
now apply IHm.
}
Qed.
[of_seq_node] and [to_seq_node] are inverses
Lemma of_seq_node_to_seq_node_eq `{Make.FArgs} {a : Set}
(l : list (Make.key × a)) :
Make.of_seq_node (to_seq_node l) = l.
Proof.
induction l; [reflexivity|]; cbn.
step. now rewrite IHl.
Qed.
(l : list (Make.key × a)) :
Make.of_seq_node (to_seq_node l) = l.
Proof.
induction l; [reflexivity|]; cbn.
step. now rewrite IHl.
Qed.
Calling [add_seq_node] on an empty map is the
the same as creating a map with [of_seq_node]
Lemma of_seq_node_add_seq_node_eq `{Make.FArgs} {a : Set}
(l : list (Make.key × a)) :
Sorted.Sorted (fun '(k1, _) '(k2, _) ⇒
Make.compare_keys k2 k1 = Datatypes.Gt) l →
Make.add_seq_node (to_seq_node l) [] =
Make.of_seq_node (to_seq_node l).
Proof.
intros H_Sorted.
induction l; [reflexivity|]; cbn.
step; cbn in ×.
destruct l; [reflexivity|]; cbn in ×.
step.
inversion H_Sorted as [|? ? ? HRel].
inversion HRel as [|? ? H_compare_keys].
rewrite H_compare_keys.
(* I have this goal I can't apply induction because
[Map.add_seq_node] keeps accumulating the arguments
in the list, when I need something like [
(k, v) :: Map.add_seq_node ...] *)
Admitted.
(l : list (Make.key × a)) :
Sorted.Sorted (fun '(k1, _) '(k2, _) ⇒
Make.compare_keys k2 k1 = Datatypes.Gt) l →
Make.add_seq_node (to_seq_node l) [] =
Make.of_seq_node (to_seq_node l).
Proof.
intros H_Sorted.
induction l; [reflexivity|]; cbn.
step; cbn in ×.
destruct l; [reflexivity|]; cbn in ×.
step.
inversion H_Sorted as [|? ? ? HRel].
inversion HRel as [|? ? H_compare_keys].
rewrite H_compare_keys.
(* I have this goal I can't apply induction because
[Map.add_seq_node] keeps accumulating the arguments
in the list, when I need something like [
(k, v) :: Map.add_seq_node ...] *)
Admitted.
[add_seq_node] and [to_seq_node] are inverses
Fixpoint add_seq_node_to_seq_node_eq `{Make.FArgs} {a : Set}
(l : list (Make.key × a)) {struct l} :
Sorted.Sorted (fun '(k1, _) '(k2, _) ⇒
Make.compare_keys k2 k1 = Datatypes.Gt) l →
Make.add_seq_node (to_seq_node l) [] = l.
Proof.
intros H_Sorted.
rewrite of_seq_node_add_seq_node_eq by assumption.
induction l; [reflexivity|]; cbn. step.
destruct l eqn:?; cbn; [reflexivity|].
cbn in ×. inversion H_Sorted as [].
inversion H0. step.
now rewrite IHl.
Qed.
(l : list (Make.key × a)) {struct l} :
Sorted.Sorted (fun '(k1, _) '(k2, _) ⇒
Make.compare_keys k2 k1 = Datatypes.Gt) l →
Make.add_seq_node (to_seq_node l) [] = l.
Proof.
intros H_Sorted.
rewrite of_seq_node_add_seq_node_eq by assumption.
induction l; [reflexivity|]; cbn. step.
destruct l eqn:?; cbn; [reflexivity|].
cbn in ×. inversion H_Sorted as [].
inversion H0. step.
now rewrite IHl.
Qed.
Maps order do not matter w.r.t bindings
Lemma make_bindings_rev_eq `{Make.FArgs} {a : Set} (m : Make.t a) :
Make.bindings m = Make.bindings (rev m).
Admitted.
Make.bindings m = Make.bindings (rev m).
Admitted.
TODO: rewrite for [fold_e] The function [fold_es] is valid.
Lemma fold_es_is_valid `{Make.FArgs} {a acc : Set}
(P : Make.key → a → Prop)
(Q : acc → Prop)
(f : Make.key → a → acc → M? acc)
(m : Make.t a)
(init : acc) :
Valid.t →
StrictlySorted.t (List.map fst m) →
Q init →
(∀ k v init, P k v → Q init →
letP? init' := f k v init in Q init') →
(∀ k v, Map.Make.find k m = Some v → P k v) →
letP? init' := Make.fold_es f m init in Q init'.
Proof.
intros Hv Hsort.
unfold Make.fold_es.
unfold Make.fold_e.
intros Qacc PQf Pmap.
generalize Qacc;
generalize init.
induction m as [|[key val] m']; [easy|].
intros; simpl.
assert (P key val) as Pkv.
{ apply Pmap.
simpl.
now rewrite Valid.compare_keys_refl.
}
pose proof (PQf key val init0 Pkv Qacc0) as fkv.
destruct (f key val init0) eqn:?; [|now rewrite Make_fold_shortcircuit].
simpl in fkv.
assert (∀ k' v', Make.find k' m' = Some v' → P k' v') as Pmap'.
{ intros.
apply Pmap.
simpl.
simpl in Hsort.
assert (Make.Ord.(V0.Compare.COMPARABLE.compare) key k' = -1) as Hc.
{ eapply StrictlySorted.strictly_sorted_lb_correct; auto.
{ exact Hsort. }
{ eapply find_In; eauto.
admit. (*TODO*)
}
}
unfold Make.compare_keys.
rewrite (Compare.Valid.sym Hv); auto.
now rewrite Hc.
}
pose proof (StrictlySorted.ss_tail _ _ _ Hsort) as Hsort'.
exact (IHm' Hsort' Pmap' a0 fkv).
Admitted.
(P : Make.key → a → Prop)
(Q : acc → Prop)
(f : Make.key → a → acc → M? acc)
(m : Make.t a)
(init : acc) :
Valid.t →
StrictlySorted.t (List.map fst m) →
Q init →
(∀ k v init, P k v → Q init →
letP? init' := f k v init in Q init') →
(∀ k v, Map.Make.find k m = Some v → P k v) →
letP? init' := Make.fold_es f m init in Q init'.
Proof.
intros Hv Hsort.
unfold Make.fold_es.
unfold Make.fold_e.
intros Qacc PQf Pmap.
generalize Qacc;
generalize init.
induction m as [|[key val] m']; [easy|].
intros; simpl.
assert (P key val) as Pkv.
{ apply Pmap.
simpl.
now rewrite Valid.compare_keys_refl.
}
pose proof (PQf key val init0 Pkv Qacc0) as fkv.
destruct (f key val init0) eqn:?; [|now rewrite Make_fold_shortcircuit].
simpl in fkv.
assert (∀ k' v', Make.find k' m' = Some v' → P k' v') as Pmap'.
{ intros.
apply Pmap.
simpl.
simpl in Hsort.
assert (Make.Ord.(V0.Compare.COMPARABLE.compare) key k' = -1) as Hc.
{ eapply StrictlySorted.strictly_sorted_lb_correct; auto.
{ exact Hsort. }
{ eapply find_In; eauto.
admit. (*TODO*)
}
}
unfold Make.compare_keys.
rewrite (Compare.Valid.sym Hv); auto.
now rewrite Hc.
}
pose proof (StrictlySorted.ss_tail _ _ _ Hsort) as Hsort'.
exact (IHm' Hsort' Pmap' a0 fkv).
Admitted.