🍃 Map.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Coq.Sorting.Sorted.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.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.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.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 a b, P b → P (f k a b)) :
∀ (m : Make.t A) b, P b →
P (Make.fold f m b).
Proof.
induction m; intros.
{ exact H0. }
{ simpl.
destruct a.
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 a.
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.
induction m1; intros; simpl in ×.
{ tauto. }
{ destruct a.
destruct (IHm1 _ _ _ H0) as
[G| [z Hz]].
{ destruct (In_add_destruct G).
{ right; ∃ a; 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 k k' m 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} : Valid.t →
∀ k (s : Make.t unit), StrictlySorted.t (List.map fst s) →
Make.mem k s = true ↔ In (k,tt) s.
Proof.
intros.
induction s.
{ simpl; split; intro; (discriminate || tauto). }
{ simpl; split; intro; destruct a.
{ destruct (Make.compare_keys k k0) eqn:G.
{ left; simpl.
unfold Make.compare_keys.
destruct u; 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. }
{ right.
apply IHs; try assumption.
eapply StrictlySorted.ss_tail; exact H1.
}
}
{ destruct H2.
{ destruct u; inversion H2.
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 s)) as Hin.
{ assert (k = fst (k, tt)) as Hobv by auto.
rewrite Hobv.
apply in_map; auto.
}
pose proof (StrictlySorted.strictly_sorted_lb_correct
(List.map fst s) k0 H0 H1 k Hin) as Hc.
rewrite (Compare.Valid.sym H0) in Hc; auto. lia.
}
{ rewrite IHs; auto.
eapply StrictlySorted.ss_tail.
exact H1.
}
}
}
}
Qed.
Lemma mem_not_In `{Make.FArgs} : Valid.t →
∀ k (s : Make.t unit), StrictlySorted.t (List.map fst s) →
Make.mem k s = false ↔ ¬ In (k,tt) s.
Proof.
intros.
split; intros.
{ intro.
rewrite <- mem_In in H3; auto.
congruence.
}
{ destruct Make.mem eqn:G.
{ rewrite mem_In in G; auto.
contradiction.
}
{ 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 a b, P b → P (f k a b)) :
∀ (m : Make.t A) b, P b →
P (Make.fold f m b).
Proof.
induction m; intros.
{ exact H0. }
{ simpl.
destruct a.
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 a.
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.
induction m1; intros; simpl in ×.
{ tauto. }
{ destruct a.
destruct (IHm1 _ _ _ H0) as
[G| [z Hz]].
{ destruct (In_add_destruct G).
{ right; ∃ a; 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 k k' m 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} : Valid.t →
∀ k (s : Make.t unit), StrictlySorted.t (List.map fst s) →
Make.mem k s = true ↔ In (k,tt) s.
Proof.
intros.
induction s.
{ simpl; split; intro; (discriminate || tauto). }
{ simpl; split; intro; destruct a.
{ destruct (Make.compare_keys k k0) eqn:G.
{ left; simpl.
unfold Make.compare_keys.
destruct u; 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. }
{ right.
apply IHs; try assumption.
eapply StrictlySorted.ss_tail; exact H1.
}
}
{ destruct H2.
{ destruct u; inversion H2.
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 s)) as Hin.
{ assert (k = fst (k, tt)) as Hobv by auto.
rewrite Hobv.
apply in_map; auto.
}
pose proof (StrictlySorted.strictly_sorted_lb_correct
(List.map fst s) k0 H0 H1 k Hin) as Hc.
rewrite (Compare.Valid.sym H0) in Hc; auto. lia.
}
{ rewrite IHs; auto.
eapply StrictlySorted.ss_tail.
exact H1.
}
}
}
}
Qed.
Lemma mem_not_In `{Make.FArgs} : Valid.t →
∀ k (s : Make.t unit), StrictlySorted.t (List.map fst s) →
Make.mem k s = false ↔ ¬ In (k,tt) s.
Proof.
intros.
split; intros.
{ intro.
rewrite <- mem_In in H3; auto.
congruence.
}
{ destruct Make.mem eqn:G.
{ rewrite mem_In in G; auto.
contradiction.
}
{ reflexivity. }
}
Qed.
We can express the [mem] operation from the [find] one.
Lemma mem_from_find :
∀ {key value : Set} {Ord : COMPARABLE} (k : key)
(m : Map.Make_t Ord value),
(Map.Make Ord).(S.mem) k m =
match (Map.Make Ord).(S.find) k m with
| Some _ ⇒ true
| None ⇒ false
end.
Proof.
intros.
induction m.
{ reflexivity. }
{ simpl.
destruct a.
destruct (Make.compare_keys k k0); auto.
}
Qed.
Lemma mem_find_not_eq_none : ∀ {key value : Set} (k : key)
(Ord : COMPARABLE) (m : Map.Make_t Ord value),
(Map.Make Ord).(S.mem) k m = true →
(Map.Make Ord).(S.find (a := value)) k m ≠ None.
Proof.
intros.
induction m.
{ discriminate. }
{ simpl in ×.
destruct a.
destruct (Make.compare_keys k k0); try discriminate; auto.
}
Qed.
Lemma find_mem_eq :
∀ {key value : Set} {Ord : COMPARABLE} (k : key) (v : value)
(m : Map.Make_t Ord value),
(Map.Make Ord).(S.find) k m = Some v →
(Map.Make Ord).(S.mem) k m = true.
Proof.
intros.
induction m.
{ discriminate. }
{ simpl in ×.
destruct a.
destruct (Make.compare_keys k k0); auto.
discriminate.
}
Qed.
Lemma add_found_eq : ∀ {key value : Set} (Ord : COMPARABLE)
(m : Map.Make_t Ord value)
(k : key) (v : value),
Compare.Valid.t (fun _ ⇒ True) (fun x ⇒ x) Ord.(COMPARABLE.compare) →
(Map.Make Ord).(S.find (a := value)) k m = Some v →
(Map.Make Ord).(S.add) k v m = m.
Proof.
intros key value Ord m k v Hv Hfind.
induction m.
{ discriminate. }
{ simpl in ×.
destruct a.
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
: ∀ {key value : Set} (k : key) (Ord : COMPARABLE)
(m : Map.Make_t Ord value),
(Map.Make Ord).(S.find (a := value)) k m = None →
(Map.Make Ord).(S.mem) k m = false.
Proof.
intros.
induction m.
{ reflexivity. }
{ simpl in ×.
destruct a.
destruct (Make.compare_keys k k0) eqn:G.
{ discriminate. }
{ reflexivity. }
{ tauto. }
}
Qed.
Lemma find_add_eq_some
: ∀ {key value : Set} (k : key) (v : value) (Ord : COMPARABLE)
(m : Map.Make_t Ord value),
Compare.Valid.t (fun _ ⇒ True) (fun x ⇒ x) Ord.(COMPARABLE.compare) →
(Map.Make Ord).(S.find (a := value))
k ((Map.Make Ord).(S.add) k v m) = Some v.
Proof.
intros key value k v Ord m Hv.
induction m.
{ simpl.
unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ simpl.
destruct a.
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 :
∀ {key value : Set} (k : key) (v : value) (Ord : COMPARABLE)
(m : Map.Make_t Ord value),
Compare.Valid.t (fun _ ⇒ True) (fun x ⇒ x) Ord.(COMPARABLE.compare) →
(Map.Make Ord).(S.mem) k m = false →
(Map.Make Ord).(S.remove (a := value))
k((Map.Make Ord).(S.add) k v m) = m.
Proof.
intros key value k v Ord m Hv Hmem.
induction m.
{ simpl.
unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ destruct a.
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.
∀ {key value : Set} {Ord : COMPARABLE} (k : key)
(m : Map.Make_t Ord value),
(Map.Make Ord).(S.mem) k m =
match (Map.Make Ord).(S.find) k m with
| Some _ ⇒ true
| None ⇒ false
end.
Proof.
intros.
induction m.
{ reflexivity. }
{ simpl.
destruct a.
destruct (Make.compare_keys k k0); auto.
}
Qed.
Lemma mem_find_not_eq_none : ∀ {key value : Set} (k : key)
(Ord : COMPARABLE) (m : Map.Make_t Ord value),
(Map.Make Ord).(S.mem) k m = true →
(Map.Make Ord).(S.find (a := value)) k m ≠ None.
Proof.
intros.
induction m.
{ discriminate. }
{ simpl in ×.
destruct a.
destruct (Make.compare_keys k k0); try discriminate; auto.
}
Qed.
Lemma find_mem_eq :
∀ {key value : Set} {Ord : COMPARABLE} (k : key) (v : value)
(m : Map.Make_t Ord value),
(Map.Make Ord).(S.find) k m = Some v →
(Map.Make Ord).(S.mem) k m = true.
Proof.
intros.
induction m.
{ discriminate. }
{ simpl in ×.
destruct a.
destruct (Make.compare_keys k k0); auto.
discriminate.
}
Qed.
Lemma add_found_eq : ∀ {key value : Set} (Ord : COMPARABLE)
(m : Map.Make_t Ord value)
(k : key) (v : value),
Compare.Valid.t (fun _ ⇒ True) (fun x ⇒ x) Ord.(COMPARABLE.compare) →
(Map.Make Ord).(S.find (a := value)) k m = Some v →
(Map.Make Ord).(S.add) k v m = m.
Proof.
intros key value Ord m k v Hv Hfind.
induction m.
{ discriminate. }
{ simpl in ×.
destruct a.
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
: ∀ {key value : Set} (k : key) (Ord : COMPARABLE)
(m : Map.Make_t Ord value),
(Map.Make Ord).(S.find (a := value)) k m = None →
(Map.Make Ord).(S.mem) k m = false.
Proof.
intros.
induction m.
{ reflexivity. }
{ simpl in ×.
destruct a.
destruct (Make.compare_keys k k0) eqn:G.
{ discriminate. }
{ reflexivity. }
{ tauto. }
}
Qed.
Lemma find_add_eq_some
: ∀ {key value : Set} (k : key) (v : value) (Ord : COMPARABLE)
(m : Map.Make_t Ord value),
Compare.Valid.t (fun _ ⇒ True) (fun x ⇒ x) Ord.(COMPARABLE.compare) →
(Map.Make Ord).(S.find (a := value))
k ((Map.Make Ord).(S.add) k v m) = Some v.
Proof.
intros key value k v Ord m Hv.
induction m.
{ simpl.
unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ simpl.
destruct a.
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 :
∀ {key value : Set} (k : key) (v : value) (Ord : COMPARABLE)
(m : Map.Make_t Ord value),
Compare.Valid.t (fun _ ⇒ True) (fun x ⇒ x) Ord.(COMPARABLE.compare) →
(Map.Make Ord).(S.mem) k m = false →
(Map.Make Ord).(S.remove (a := value))
k((Map.Make Ord).(S.add) k v m) = m.
Proof.
intros key value k v Ord m Hv Hmem.
induction m.
{ simpl.
unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ destruct a.
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 :
∀ {key value : Set} (k : key) (Ord : COMPARABLE)
(m : Map.Make_t Ord value),
(Map.Make Ord).(S.find) k m = None →
(Map.Make Ord).(S.remove (a := value)) k m = m.
Proof.
intros key value k Ord m Hfind.
induction m.
{ reflexivity. }
{ destruct a; simpl in ×.
destruct (Make.compare_keys k k0).
{ discriminate. }
{ reflexivity. }
{ f_equal; auto. }
}
Qed.
Lemma add_add_eq :
∀ {key value : Set} (k : key) (v v' : value) (Ord : COMPARABLE)
(m : Map.Make_t Ord value),
Compare.Valid.t (fun _ ⇒ True) (fun x ⇒ x) Ord.(COMPARABLE.compare) →
(Map.Make Ord).(S.add (a := value)) k v
((Map.Make Ord).(S.add) k v' m) =
(Map.Make Ord).(S.add (a := value)) k v m.
Proof.
intros key value k v v' Ord m Hv.
induction m.
{ simpl.
unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ destruct a.
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 :
∀ {key value : Set} (k : key) (v : value) (Ord : COMPARABLE)
(m : Map.Make_t Ord value),
Compare.Valid.t (fun _ ⇒ True) (fun x ⇒ x) Ord.(COMPARABLE.compare) →
(Map.Make Ord).(S.mem)
k ((Map.Make Ord).(S.add) k v m) = true.
Proof.
intros key value k v Ord m Hv.
induction m; simpl in ×.
{ unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ destruct a; 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: ∀ {key value : Set}
(k k' : key) (v : value) (Ord : COMPARABLE)
(m : Map.Make_t Ord value),
Compare.Valid.t (fun _ ⇒ True) (fun x ⇒ x) Ord.(COMPARABLE.compare) →
k ≠ k' →
((Map.Make Ord).(S.find (a := value)) k
((Map.Make Ord).(S.add) k' v m)) =
((Map.Make Ord).(S.find (a := value)) k m).
Proof.
intros key value k k' v Ord m 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 a; 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. }
}
{ rewrite (@Valid.compare_keys_Lt_trans _
(@Make.Build_FArgs key Ord) Hv _ _ _ G0 G); auto.
}
{ destruct (Make.compare_keys k k0); auto. }
}
{ destruct (Make.compare_keys k k0); auto. }
}
Qed.
Lemma find_add_compare_int : ∀ {value : Set}
(k k' : int) (v' : value) (Ord : COMPARABLE)
(m : Map.Make_t Ord value),
Compare.Valid.t (fun _ ⇒ True) (fun x ⇒ x) Ord.(COMPARABLE.compare) →
(Map.Make Ord).(S.find (a := value))
k ((Map.Make Ord).(S.add) k' v' m) =
if k =? k'
then Some v'
else (Map.Make Ord).(S.find (a := value)) k m.
Proof.
intros.
destruct (k =? k') eqn:Hkk'.
{ rewrite Z.eqb_eq in Hkk'.
rewrite Hkk'.
apply find_add_eq_some; auto.
}
{ rewrite Z.eqb_neq in Hkk'.
apply find_add_neq; auto.
}
Qed.
∀ {key value : Set} (k : key) (Ord : COMPARABLE)
(m : Map.Make_t Ord value),
(Map.Make Ord).(S.find) k m = None →
(Map.Make Ord).(S.remove (a := value)) k m = m.
Proof.
intros key value k Ord m Hfind.
induction m.
{ reflexivity. }
{ destruct a; simpl in ×.
destruct (Make.compare_keys k k0).
{ discriminate. }
{ reflexivity. }
{ f_equal; auto. }
}
Qed.
Lemma add_add_eq :
∀ {key value : Set} (k : key) (v v' : value) (Ord : COMPARABLE)
(m : Map.Make_t Ord value),
Compare.Valid.t (fun _ ⇒ True) (fun x ⇒ x) Ord.(COMPARABLE.compare) →
(Map.Make Ord).(S.add (a := value)) k v
((Map.Make Ord).(S.add) k v' m) =
(Map.Make Ord).(S.add (a := value)) k v m.
Proof.
intros key value k v v' Ord m Hv.
induction m.
{ simpl.
unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ destruct a.
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 :
∀ {key value : Set} (k : key) (v : value) (Ord : COMPARABLE)
(m : Map.Make_t Ord value),
Compare.Valid.t (fun _ ⇒ True) (fun x ⇒ x) Ord.(COMPARABLE.compare) →
(Map.Make Ord).(S.mem)
k ((Map.Make Ord).(S.add) k v m) = true.
Proof.
intros key value k v Ord m Hv.
induction m; simpl in ×.
{ unfold Make.compare_keys.
rewrite (Compare.Valid.refl Hv); auto.
}
{ destruct a; 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: ∀ {key value : Set}
(k k' : key) (v : value) (Ord : COMPARABLE)
(m : Map.Make_t Ord value),
Compare.Valid.t (fun _ ⇒ True) (fun x ⇒ x) Ord.(COMPARABLE.compare) →
k ≠ k' →
((Map.Make Ord).(S.find (a := value)) k
((Map.Make Ord).(S.add) k' v m)) =
((Map.Make Ord).(S.find (a := value)) k m).
Proof.
intros key value k k' v Ord m 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 a; 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. }
}
{ rewrite (@Valid.compare_keys_Lt_trans _
(@Make.Build_FArgs key Ord) Hv _ _ _ G0 G); auto.
}
{ destruct (Make.compare_keys k k0); auto. }
}
{ destruct (Make.compare_keys k k0); auto. }
}
Qed.
Lemma find_add_compare_int : ∀ {value : Set}
(k k' : int) (v' : value) (Ord : COMPARABLE)
(m : Map.Make_t Ord value),
Compare.Valid.t (fun _ ⇒ True) (fun x ⇒ x) Ord.(COMPARABLE.compare) →
(Map.Make Ord).(S.find (a := value))
k ((Map.Make Ord).(S.add) k' v' m) =
if k =? k'
then Some v'
else (Map.Make Ord).(S.find (a := value)) k m.
Proof.
intros.
destruct (k =? k') eqn:Hkk'.
{ rewrite Z.eqb_eq in Hkk'.
rewrite Hkk'.
apply find_add_eq_some; auto.
}
{ rewrite Z.eqb_neq in Hkk'.
apply find_add_neq; auto.
}
Qed.
Creates a map from a list of bindings.
Definition of_bindings {key value : Set} {Ord : COMPARABLE}
(l : list (key × value)) : Map.Make_t Ord value :=
List.fold_right
(fun '(k, v) m ⇒ (Map.Make Ord).(S.add) k v m)
l
(Map.Make Ord).(S.empty).
(l : list (key × value)) : Map.Make_t Ord value :=
List.fold_right
(fun '(k, v) m ⇒ (Map.Make Ord).(S.add) k v m)
l
(Map.Make Ord).(S.empty).
Relate the [find] operation in a map and its bindings list.
Lemma find_of_bindings :
∀ {key value : Set} {Ord : COMPARABLE} (k : key)
(l : list (key × value)),
Compare.Valid.t (fun _ ⇒ True) (fun x ⇒ x) Ord.(COMPARABLE.compare) →
(Map.Make Ord).(S.find) k (of_bindings l) =
List.find_map
(fun '(k', v) ⇒
if Ord.(COMPARABLE.compare) k k' =? 0 then
Some v
else
None
)
l.
Proof.
intros key value Ord k l Hv.
unfold of_bindings.
induction l.
{ reflexivity. }
{ simpl.
destruct a.
destruct (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 v _ _ Hv); auto.
intro Heq.
apply Hkk0.
rewrite Heq.
apply (Compare.Valid.refl Hv); auto.
}
}
Qed.
∀ {key value : Set} {Ord : COMPARABLE} (k : key)
(l : list (key × value)),
Compare.Valid.t (fun _ ⇒ True) (fun x ⇒ x) Ord.(COMPARABLE.compare) →
(Map.Make Ord).(S.find) k (of_bindings l) =
List.find_map
(fun '(k', v) ⇒
if Ord.(COMPARABLE.compare) k k' =? 0 then
Some v
else
None
)
l.
Proof.
intros key value Ord k l Hv.
unfold of_bindings.
induction l.
{ reflexivity. }
{ simpl.
destruct a.
destruct (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 v _ _ 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 :
∀ {key value : Set} {Ord : COMPARABLE (t := key)}
(l : list (key × value)),
Sorted.Sorted (fun '(k1,_) '(k2,_) ⇒
Ord.(COMPARABLE.compare) k1 k2 = -1) l →
(Map.Make Ord).(S.bindings) (of_bindings l) =
l.
Proof.
unfold Make; simpl.
unfold Make.bindings.
unfold of_bindings.
intros.
induction l.
{ reflexivity. }
{ destruct l.
{ destruct a; reflexivity. }
{ simpl in IHl.
destruct p.
simpl.
rewrite IHl.
{ destruct a.
simpl.
unfold Make.compare_keys.
inversion H.
inversion H3.
unfold Make.Ord.
rewrite H5; auto.
}
{ inversion H; 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 ? m **.
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.
∀ {key value : Set} {Ord : COMPARABLE (t := key)}
(l : list (key × value)),
Sorted.Sorted (fun '(k1,_) '(k2,_) ⇒
Ord.(COMPARABLE.compare) k1 k2 = -1) l →
(Map.Make Ord).(S.bindings) (of_bindings l) =
l.
Proof.
unfold Make; simpl.
unfold Make.bindings.
unfold of_bindings.
intros.
induction l.
{ reflexivity. }
{ destruct l.
{ destruct a; reflexivity. }
{ simpl in IHl.
destruct p.
simpl.
rewrite IHl.
{ destruct a.
simpl.
unfold Make.compare_keys.
inversion H.
inversion H3.
unfold Make.Ord.
rewrite H5; auto.
}
{ inversion H; 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 ? m **.
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 {key value : Set} (Ord : COMPARABLE (t := key))
(k : key) (v : value) (m : (Map.Make Ord).(S.t) value) :
(Map.Make Ord).(S.cardinal) ((Map.Make Ord).(S.add) k v m) =
(Map.Make Ord).(S.cardinal) m +i
match (Map.Make Ord).(S.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.
(k : key) (v : value) (m : (Map.Make Ord).(S.t) value) :
(Map.Make Ord).(S.cardinal) ((Map.Make Ord).(S.add) k v m) =
(Map.Make Ord).(S.cardinal) m +i
match (Map.Make Ord).(S.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 {key value : Set} (Ord : COMPARABLE (t := key))
(k : key) (m : (Map.Make Ord).(S.t) value) :
(Map.Make Ord).(S.cardinal) ((Map.Make Ord).(S.remove) k m) =
(Map.Make Ord).(S.cardinal) m -i
match (Map.Make Ord).(S.find) k m with
| None ⇒ 0
| Some _ ⇒ 1
end.
Proof.
simpl.
destruct Make.find eqn:?.
{ now apply (cardinal_remove_find_Some _ _ v). }
{ rewrite cardinal_remove_find_None by assumption.
unfold Make.cardinal.
pose proof (List.length_is_valid m).
lia.
}
Qed.
(k : key) (m : (Map.Make Ord).(S.t) value) :
(Map.Make Ord).(S.cardinal) ((Map.Make Ord).(S.remove) k m) =
(Map.Make Ord).(S.cardinal) m -i
match (Map.Make Ord).(S.find) k m with
| None ⇒ 0
| Some _ ⇒ 1
end.
Proof.
simpl.
destruct Make.find eqn:?.
{ now apply (cardinal_remove_find_Some _ _ v). }
{ 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 {key value : Set} (Ord : COMPARABLE (t := key))
(m : (Map.Make Ord).(S.t) value) :
Pervasives.Int.Valid.t ((Map.Make Ord).(S.cardinal) m).
Proof.
apply List.length_is_valid.
Qed.
(m : (Map.Make Ord).(S.t) value) :
Pervasives.Int.Valid.t ((Map.Make Ord).(S.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 {key value value' : Set} (Ord : COMPARABLE (t := key))
(k : key) (f : value → value') (map : Map.Make_t Ord value) :
(let× x := (Map.Make Ord).(S.find) k map in
Some (f x)) =
(Map.Make Ord).(S.find) k ((Map.Make Ord).(S.map) f map).
Proof.
simpl.
induction map; hauto lq: on.
Qed.
(k : key) (f : value → value') (map : Map.Make_t Ord value) :
(let× x := (Map.Make Ord).(S.find) k map in
Some (f x)) =
(Map.Make Ord).(S.find) k ((Map.Make Ord).(S.map) f map).
Proof.
simpl.
induction map; hauto lq: on.
Qed.
A reformultion of [find_map] using typeclasses.
Lemma find_map_fargs `{Map.Make.FArgs} {a b : Set}
(f : a → b) (k : Map.Make.key) (map : Map.Make.t a) :
(let× ' x := Map.Make.find k map in Some (f x)) =
Map.Make.find k (Map.Make.map f map).
Proof.
apply find_map.
Qed.
(f : a → b) (k : Map.Make.key) (map : Map.Make.t a) :
(let× ' x := Map.Make.find k map in Some (f x)) =
Map.Make.find k (Map.Make.map f map).
Proof.
apply find_map.
Qed.
Adding and mapping a function over a map are commuting.
Lemma add_map {key value value' : Set} (Ord : COMPARABLE (t := key))
(k : key) (v : value) (f : value → value') (map : Map.Make_t Ord value) :
(Map.Make Ord).(S.add) k (f v) ((Map.Make Ord).(S.map) f map) =
(Map.Make Ord).(S.map) f ((Map.Make Ord).(S.add) k v map).
Proof.
simpl.
induction map; hauto lq: on.
Qed.
(k : key) (v : value) (f : value → value') (map : Map.Make_t Ord value) :
(Map.Make Ord).(S.add) k (f v) ((Map.Make Ord).(S.map) f map) =
(Map.Make Ord).(S.map) f ((Map.Make Ord).(S.add) k v map).
Proof.
simpl.
induction map; hauto lq: on.
Qed.
A reformulation of [add_map] using typeclasses.
Lemma add_map_fargs {value value' : Set} `{Map.Make.FArgs}
(k : Map.Make.key) (v : value) (f : value → value') (map : Map.Make.t value) :
Map.Make.add k (f v) (Map.Make.map f map) =
Map.Make.map f (Map.Make.add k v map).
Proof.
apply add_map.
Qed.
(k : Map.Make.key) (v : value) (f : value → value') (map : Map.Make.t value) :
Map.Make.add k (f v) (Map.Make.map f map) =
Map.Make.map f (Map.Make.add k v map).
Proof.
apply add_map.
Qed.
The result of [Map.Make.mem] is not affected by [Map.Make.map].
Lemma mem_map_fargs {value value' : Set} `{Map.Make.FArgs}
(k : Map.Make.key) (f : value → value') (map : Map.Make.t value) :
Map.Make.mem k (Map.Make.map f map) = Map.Make.mem k map.
Proof.
induction map; [reflexivity|].
destruct a; simpl.
now destruct Map.Make.compare_keys.
Qed.
(k : Map.Make.key) (f : value → value') (map : Map.Make.t value) :
Map.Make.mem k (Map.Make.map f map) = Map.Make.mem k map.
Proof.
induction map; [reflexivity|].
destruct a; simpl.
now destruct Map.Make.compare_keys.
Qed.
Removing and mapping a function over a map are commuting.
Lemma remove_map {key value value' : Set} (Ord : COMPARABLE (t := key))
(k : key) (f : value → value') (map : Map.Make_t Ord value) :
(Map.Make Ord).(S.remove) k ((Map.Make Ord).(S.map) f map) =
(Map.Make Ord).(S.map) f ((Map.Make Ord).(S.remove) k map).
Proof.
simpl.
induction map; hauto lq: on.
Qed.
(k : key) (f : value → value') (map : Map.Make_t Ord value) :
(Map.Make Ord).(S.remove) k ((Map.Make Ord).(S.map) f map) =
(Map.Make Ord).(S.map) f ((Map.Make Ord).(S.remove) k map).
Proof.
simpl.
induction map; hauto lq: on.
Qed.
Result of the application of a [fold] after a [map] operation.
Lemma fold_map {key value value' acc : Set} (Ord : COMPARABLE (t := key))
(f : value → value') (g : key → value' → acc → acc)
(map : Map.Make_t Ord value) :
∀ (init : acc),
(Map.Make Ord).(S.fold) g ((Map.Make Ord).(S.map) f map) init =
(Map.Make Ord).(S.fold) (fun k v a ⇒ g k (f v) a) map init.
Proof.
simpl.
induction map as [|[k v] map]; simpl; sfirstorder.
Qed.
(f : value → value') (g : key → value' → acc → acc)
(map : Map.Make_t Ord value) :
∀ (init : acc),
(Map.Make Ord).(S.fold) g ((Map.Make Ord).(S.map) f map) init =
(Map.Make Ord).(S.fold) (fun k v a ⇒ g k (f v) a) map init.
Proof.
simpl.
induction map as [|[k v] map]; simpl; sfirstorder.
Qed.
Result of the application of a [fold_es] after a [map] operation.
Lemma fold_es_map {key value value' acc : Set} (Ord : COMPARABLE (t := key))
(f : value → value') (g : key → value' → acc → M? acc)
(map : Map.Make_t Ord value) :
∀ (init : acc),
(Map.Make Ord).(S.fold_es) g ((Map.Make Ord).(S.map) f map) init =
(Map.Make Ord).(S.fold_es) (fun k v a ⇒ g k (f v) a) map init.
Proof.
intros.
apply fold_map.
Qed.
Lemma In_add `{Make.FArgs} {A : Set}
(k : Make.key) (a : A) (m : Make.t A) :
In (k, a) (Make.add k a 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} (Hv : Map.Valid.t)
(k k': Make.key) (a a': A) (m : Make.t A) :
(k,a) = (k', a') ∨ (k ≠ k' ∧ In (k, a) m) →
In (k, a) (Make.add k' a' m).
Proof.
induction m; simpl; intro Hi.
{ destruct Hi; auto. induction H0; auto. }
{ destruct a0 as [k0 a0].
destruct Hi.
{ inversion H0; subst k' a'; 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, a) (Make.add k' a' 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 a; 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 a; 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 a},
In (k, a) m1 →
¬ In k (List.map fst m2) →
f k (Some a) None = Some c →
In (k, c) (Make.merge f m1 m2).
Proof.
induction m1; intros.
{ destruct H0. }
{ destruct a as [k' a'].
destruct H0.
{ simpl in ×.
assert (Make.pick_opt k m2 = (None, m2)). {
induction m2; simpl; auto.
destruct a as [k'']; simpl in ×.
destruct (Make.compare_keys k k'') eqn:?; auto.
{ apply (Valid.compare_keys_Eq Hv) in Heqc0.
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, c) (Make.merge f m1 t)). {
apply IHm1 with a0; 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 a); 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 c b},
In (k, b) m2 →
¬ In k (List.map fst m1) →
f k None (Some b) = Some c →
In (k, c) (Make.merge f m1 m2).
Proof.
induction m1; intros.
{ simpl in ×.
induction m2; simpl.
{ inversion H0. }
{ destruct H0.
{ subst a. rewrite H2. left. auto. }
{ destruct a. destruct (f k0 None (Some b0)); [right|]; auto. }
}
}
{ destruct a; simpl.
destruct (Make.pick_opt k0 m2) eqn:?.
apply (StrictlySorted.pick_opt_to_ind Hv) in Heqp.
assert (In (k, c) (Make.merge f m1 t)). {
apply IHm1 with b; 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 a) o); auto.
apply (In_add_intro Hv); 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 c a b},
In (k, a) m1 →
In (k, b) m2 →
f k (Some a) (Some b) = Some c →
In (k, c) (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 c},
In (k, c) (Make.merge f m1 m2) →
(∃ a, In (k, a) m1
∧ ¬ In k (List.map fst m2)
∧ f k (Some a) None = Some c)
∨ (∃ b, In (k, b) m2
∧ ¬ In k (List.map fst m1)
∧ f k None (Some b) = Some c)
∨ (∃ a b, In (k, a) m1 ∧ In (k, b) m2
∧ f k (Some a) (Some b) = Some c).
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 a.
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}
(Hv : Map.Valid.t)
(m : Make.t A) k v :
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 a.
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 a.
simpl; congruence.
}
Qed.
Lemma add_In `{Make.FArgs} {A : Set} (m : Make.t A)
: ∀ k v, In (k, v) (Make.add k v m).
Proof.
induction m; intros.
{ left; auto. }
{ simpl.
Tactics.destruct_pairs.
destruct Make.compare_keys; hauto.
}
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 a,
Map.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, a) m1 ∨ In (k, f k a) m2) →
In (k, f k a) (Make.fold
(fun k0 v ⇒ Make.add k0 (f k0 v)) m1 m2).
Proof.
induction m1; intros m2 k a' Hv Hss1 Hss2 Hdis Hin.
{ simpl.
destruct Hin as [[]|]; auto.
}
{ simpl.
destruct a.
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, a0) = fst (k1, b))
by auto.
rewrite H1.
apply in_map; auto.
}
}
}
destruct Hin.
{ destruct H0; try tauto.
right; inversion H0.
simpl in Hss1.
apply add_In.
}
{ 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 k v 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 b}, In (k, b) (Make.mapi f m) →
∃ a, In (k, a) m ∧ f k a = b.
Proof.
induction m; intros k b Hin.
{ destruct Hin. }
{ simpl in Hin; Tactics.destruct_pairs.
destruct Hin.
{ ∃ a; sfirstorder. }
{ destruct (IHm _ _ H0) as [a' [Ha'1 Ha'2]].
∃ a'; sfirstorder. }
}
Qed.
(f : value → value') (g : key → value' → acc → M? acc)
(map : Map.Make_t Ord value) :
∀ (init : acc),
(Map.Make Ord).(S.fold_es) g ((Map.Make Ord).(S.map) f map) init =
(Map.Make Ord).(S.fold_es) (fun k v a ⇒ g k (f v) a) map init.
Proof.
intros.
apply fold_map.
Qed.
Lemma In_add `{Make.FArgs} {A : Set}
(k : Make.key) (a : A) (m : Make.t A) :
In (k, a) (Make.add k a 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} (Hv : Map.Valid.t)
(k k': Make.key) (a a': A) (m : Make.t A) :
(k,a) = (k', a') ∨ (k ≠ k' ∧ In (k, a) m) →
In (k, a) (Make.add k' a' m).
Proof.
induction m; simpl; intro Hi.
{ destruct Hi; auto. induction H0; auto. }
{ destruct a0 as [k0 a0].
destruct Hi.
{ inversion H0; subst k' a'; 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, a) (Make.add k' a' 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 a; 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 a; 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 a},
In (k, a) m1 →
¬ In k (List.map fst m2) →
f k (Some a) None = Some c →
In (k, c) (Make.merge f m1 m2).
Proof.
induction m1; intros.
{ destruct H0. }
{ destruct a as [k' a'].
destruct H0.
{ simpl in ×.
assert (Make.pick_opt k m2 = (None, m2)). {
induction m2; simpl; auto.
destruct a as [k'']; simpl in ×.
destruct (Make.compare_keys k k'') eqn:?; auto.
{ apply (Valid.compare_keys_Eq Hv) in Heqc0.
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, c) (Make.merge f m1 t)). {
apply IHm1 with a0; 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 a); 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 c b},
In (k, b) m2 →
¬ In k (List.map fst m1) →
f k None (Some b) = Some c →
In (k, c) (Make.merge f m1 m2).
Proof.
induction m1; intros.
{ simpl in ×.
induction m2; simpl.
{ inversion H0. }
{ destruct H0.
{ subst a. rewrite H2. left. auto. }
{ destruct a. destruct (f k0 None (Some b0)); [right|]; auto. }
}
}
{ destruct a; simpl.
destruct (Make.pick_opt k0 m2) eqn:?.
apply (StrictlySorted.pick_opt_to_ind Hv) in Heqp.
assert (In (k, c) (Make.merge f m1 t)). {
apply IHm1 with b; 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 a) o); auto.
apply (In_add_intro Hv); 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 c a b},
In (k, a) m1 →
In (k, b) m2 →
f k (Some a) (Some b) = Some c →
In (k, c) (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 c},
In (k, c) (Make.merge f m1 m2) →
(∃ a, In (k, a) m1
∧ ¬ In k (List.map fst m2)
∧ f k (Some a) None = Some c)
∨ (∃ b, In (k, b) m2
∧ ¬ In k (List.map fst m1)
∧ f k None (Some b) = Some c)
∨ (∃ a b, In (k, a) m1 ∧ In (k, b) m2
∧ f k (Some a) (Some b) = Some c).
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 a.
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}
(Hv : Map.Valid.t)
(m : Make.t A) k v :
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 a.
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 a.
simpl; congruence.
}
Qed.
Lemma add_In `{Make.FArgs} {A : Set} (m : Make.t A)
: ∀ k v, In (k, v) (Make.add k v m).
Proof.
induction m; intros.
{ left; auto. }
{ simpl.
Tactics.destruct_pairs.
destruct Make.compare_keys; hauto.
}
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 a,
Map.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, a) m1 ∨ In (k, f k a) m2) →
In (k, f k a) (Make.fold
(fun k0 v ⇒ Make.add k0 (f k0 v)) m1 m2).
Proof.
induction m1; intros m2 k a' Hv Hss1 Hss2 Hdis Hin.
{ simpl.
destruct Hin as [[]|]; auto.
}
{ simpl.
destruct a.
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, a0) = fst (k1, b))
by auto.
rewrite H1.
apply in_map; auto.
}
}
}
destruct Hin.
{ destruct H0; try tauto.
right; inversion H0.
simpl in Hss1.
apply add_In.
}
{ 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 k v 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 b}, In (k, b) (Make.mapi f m) →
∃ a, In (k, a) m ∧ f k a = b.
Proof.
induction m; intros k b Hin.
{ destruct Hin. }
{ simpl in Hin; Tactics.destruct_pairs.
destruct Hin.
{ ∃ a; 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.
A reformulation of [map_list_eq].
Lemma map_list_eq_fargs `{Map.Make.FArgs} {a b : Set}
{f : Map.Make.key × a → Map.Make.key × b} (g : a → b)
(m : Map.Make.t a) : (∀ k v, f (k, v) = (k, g v)) →
Map.Make.map g m = List.map f m.
Proof.
intro; induction m; hauto.
Qed.
{f : Map.Make.key × a → Map.Make.key × b} (g : a → b)
(m : Map.Make.t a) : (∀ k v, f (k, v) = (k, g v)) →
Map.Make.map g m = List.map f m.
Proof.
intro; induction m; hauto.
Qed.
Adding a valid (w.r.t [P]) element to a map preserves [P]
Lemma make_add_preserves_P
{A B : Set}
`{Map.Make.FArgs (t := A)} (m : Map.Make.t B)
(P : (A × B) → Prop) (x : B) k :
P (k, x) →
Forall P m →
Forall P (Make.add k x 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.
{A B : Set}
`{Map.Make.FArgs (t := A)} (m : Map.Make.t B)
(P : (A × B) → Prop) (x : B) k :
P (k, x) →
Forall P m →
Forall P (Make.add k x 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
{A B : Set}
`{Map.Make.FArgs (t := A)} (m : Map.Make.t B)
(P : (A × B) → 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.
{A B : Set}
`{Map.Make.FArgs (t := A)} (m : Map.Make.t B)
(P : (A × B) → 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 {k v : Set}
`{FArgs : Make.FArgs (t := k)}
(m : list (k × v)) :
Make.of_seq_node (to_seq_node m) = m.
Proof.
induction m; [reflexivity|]; cbn.
step. now rewrite IHm.
Qed.
`{FArgs : Make.FArgs (t := k)}
(m : list (k × v)) :
Make.of_seq_node (to_seq_node m) = m.
Proof.
induction m; [reflexivity|]; cbn.
step. now rewrite IHm.
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 {k v : Set}
`{FArgs' : Map.Make.FArgs (t := k)}
(l : list (k × v)) :
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 ...] *)
assert (GOAL :
Make.add_seq_node (to_seq_node l) [(k0, v0); (k1, v1)] =
(k0, v0) :: (k1, v1) :: Make.of_seq_node (to_seq_node l)) by admit.
apply GOAL.
Admitted.
`{FArgs' : Map.Make.FArgs (t := k)}
(l : list (k × v)) :
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 ...] *)
assert (GOAL :
Make.add_seq_node (to_seq_node l) [(k0, v0); (k1, v1)] =
(k0, v0) :: (k1, v1) :: Make.of_seq_node (to_seq_node l)) by admit.
apply GOAL.
Admitted.
[add_seq_node] and [to_seq_node] are inverses
Fixpoint add_seq_node_to_seq_node_eq {k v : Set}
`{FArgs' : Map.Make.FArgs (t := k)}
(x : list (k × v)) {struct x} :
Sorted.Sorted (fun '(k1, _) '(k2, _) ⇒
Make.compare_keys k2 k1 = Datatypes.Gt) x →
Make.add_seq_node (to_seq_node x) [] = x.
Proof.
intros H_Sorted.
rewrite of_seq_node_add_seq_node_eq by assumption.
induction x; [reflexivity|]; cbn. step.
destruct x eqn:?; cbn; [reflexivity|].
cbn in ×. inversion H_Sorted as [].
inversion H0. step.
now rewrite IHx.
Qed.
`{FArgs' : Map.Make.FArgs (t := k)}
(x : list (k × v)) {struct x} :
Sorted.Sorted (fun '(k1, _) '(k2, _) ⇒
Make.compare_keys k2 k1 = Datatypes.Gt) x →
Make.add_seq_node (to_seq_node x) [] = x.
Proof.
intros H_Sorted.
rewrite of_seq_node_add_seq_node_eq by assumption.
induction x; [reflexivity|]; cbn. step.
destruct x eqn:?; cbn; [reflexivity|].
cbn in ×. inversion H_Sorted as [].
inversion H0. step.
now rewrite IHx.
Qed.
Maps order do not matter w.r.t bindings
Axiom make_bindings_rev_eq : ∀ {k v : Set}
`{FArgs' : Map.Make.FArgs (t := k)}
(map : list (k × v)),
Make.bindings map = Make.bindings (rev map).
`{FArgs' : Map.Make.FArgs (t := k)}
(map : list (k × v)),
Make.bindings map = Make.bindings (rev map).
TODO: rewrite for [fold_e] The function [fold_es] is valid.
Lemma fold_es_is_valid {k v a : Set} `{Map.Make.FArgs (t := k)}
(P : k → v → Prop)
(Q : a → Prop)
(f : k → v → a → M? a)
(map : Map.Make.t v)
(acc : a) :
Valid.t →
StrictlySorted.t (List.map fst map) →
Q acc →
(∀ k v acc, P k v → Q acc →
letP? acc' := f k v acc in Q acc') →
(∀ k v, Map.Make.find k map = Some v → P k v) →
letP? acc' := Make.fold_es f map acc in Q acc'.
Proof.
intros Hv Hsort.
unfold Make.fold_es.
unfold Make.fold_e.
intros Qacc PQf Pmap.
generalize Qacc;
generalize acc.
induction map as [|[key val] map']; [easy|].
intros; simpl.
assert (P key val) as Pkv.
{ apply Pmap.
simpl.
now rewrite Valid.compare_keys_refl.
}
pose proof (PQf key val acc0 Pkv Qacc0) as fkv.
destruct (f key val acc0) eqn:?; [|now rewrite Make_fold_shortcircuit].
simpl in fkv.
assert (∀ k' v', Make.find k' map' = 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 (IHmap' Hsort' Pmap' a0 fkv).
Admitted.
(P : k → v → Prop)
(Q : a → Prop)
(f : k → v → a → M? a)
(map : Map.Make.t v)
(acc : a) :
Valid.t →
StrictlySorted.t (List.map fst map) →
Q acc →
(∀ k v acc, P k v → Q acc →
letP? acc' := f k v acc in Q acc') →
(∀ k v, Map.Make.find k map = Some v → P k v) →
letP? acc' := Make.fold_es f map acc in Q acc'.
Proof.
intros Hv Hsort.
unfold Make.fold_es.
unfold Make.fold_e.
intros Qacc PQf Pmap.
generalize Qacc;
generalize acc.
induction map as [|[key val] map']; [easy|].
intros; simpl.
assert (P key val) as Pkv.
{ apply Pmap.
simpl.
now rewrite Valid.compare_keys_refl.
}
pose proof (PQf key val acc0 Pkv Qacc0) as fkv.
destruct (f key val acc0) eqn:?; [|now rewrite Make_fold_shortcircuit].
simpl in fkv.
assert (∀ k' v', Make.find k' map' = 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 (IHmap' Hsort' Pmap' a0 fkv).
Admitted.