Commit 64b4548a authored by Robbert Krebbers's avatar Robbert Krebbers

Clean up Patricia trees implementation.

parent 0d69828b
......@@ -767,6 +767,15 @@ Infix "=.>*" := (Forall2 bool_le) (at level 70).
Instance: PartialOrder bool_le.
Proof. repeat split; repeat intros [|]; compute; tauto. Qed.
Lemma andb_True b1 b2 : b1 && b2 b1 b2.
Proof. destruct b1, b2; simpl; tauto. Qed.
Lemma orb_True b1 b2 : b1 || b2 b1 b2.
Proof. destruct b1, b2; simpl; tauto. Qed.
Lemma negb_True b : negb b ¬b.
Proof. destruct b; simpl; tauto. Qed.
Lemma Is_true_false (b : bool) : b = false ¬b.
Proof. now intros -> ?. Qed.
(** * Miscellaneous *)
Class Half A := half: A A.
Notation "½" := half : C_scope.
......
......@@ -21,7 +21,7 @@ be represented as a binary tree of an arbitrary size that contains [None] at
all nodes. *)
Inductive Pmap_raw (A : Type) : Type :=
| PLeaf: Pmap_raw A
| PNode: Pmap_raw A option A Pmap_raw A Pmap_raw A.
| PNode: option A Pmap_raw A Pmap_raw A Pmap_raw A.
Arguments PLeaf {_}.
Arguments PNode {_} _ _ _.
......@@ -29,234 +29,151 @@ Instance Pmap_raw_eq_dec `{∀ x y : A, Decision (x = y)} (x y : Pmap_raw A) :
Decision (x = y).
Proof. solve_decision. Defined.
(** The following decidable predicate describes non empty trees. *)
Inductive Pmap_ne {A} : Pmap_raw A Prop :=
| Pmap_ne_val l x r : Pmap_ne (PNode l (Some x) r)
| Pmap_ne_l l r : Pmap_ne l Pmap_ne (PNode l None r)
| Pmap_ne_r l r : Pmap_ne r Pmap_ne (PNode l None r).
Local Hint Constructors Pmap_ne.
Instance Pmap_ne_dec {A} : t : Pmap_raw A, Decision (Pmap_ne t).
Proof.
refine (
fix go t :=
match t return Decision (Pmap_ne t) with
| PLeaf => right _
| PNode _ (Some x) _ => left _
| PNode l Node r => cast_if_or (go l) (go r)
end); clear go; abstract first [constructor; by auto|by inversion 1].
Defined.
(** The following predicate describes well well formed trees. A tree is well
formed if it is empty or if all nodes at the bottom contain a value. *)
Inductive Pmap_wf {A} : Pmap_raw A Prop :=
| Pmap_wf_leaf : Pmap_wf PLeaf
| Pmap_wf_node l x r : Pmap_wf l Pmap_wf r Pmap_wf (PNode l (Some x) r)
| Pmap_wf_empty l r :
Pmap_wf l Pmap_wf r (Pmap_ne l Pmap_ne r) Pmap_wf (PNode l None r).
Local Hint Constructors Pmap_wf.
Instance Pmap_wf_dec {A} : t : Pmap_raw A, Decision (Pmap_wf t).
Proof.
refine (
fix go t :=
match t return Decision (Pmap_wf t) with
| PLeaf => left _
| PNode l (Some x) r => cast_if_and (go l) (go r)
| PNode l Node r =>
cast_if_and3 (decide (Pmap_ne l Pmap_ne r)) (go l) (go r)
end); clear go; abstract first [constructor; by auto|by inversion 1].
Defined.
(** Now we restrict the data type of trees to those that are well formed and
thereby obtain a data type that ensures canonicity. *)
Inductive Pmap (A : Type) : Type := PMap {
pmap_car : Pmap_raw A;
pmap_bool_prf : bool_decide (Pmap_wf pmap_car)
}.
Arguments PMap {_} _ _.
Arguments pmap_car {_} _.
Arguments pmap_bool_prf {_} _.
Definition PMap' {A} (t : Pmap_raw A) (p : Pmap_wf t) : Pmap A :=
PMap t (bool_decide_pack _ p).
Definition pmap_prf {A} (m : Pmap A) : Pmap_wf (pmap_car m) :=
bool_decide_unpack _ (pmap_bool_prf m).
Lemma Pmap_eq {A} (m1 m2 : Pmap A) : m1 = m2 pmap_car m1 = pmap_car m2.
Proof.
split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
simplify_equality'; f_equal; apply proof_irrel.
Qed.
(** * Operations on the data structure *)
Global Instance Pmap_eq_dec `{ x y : A, Decision (x = y)}
(m1 m2 : Pmap A) : Decision (m1 = m2) :=
match Pmap_raw_eq_dec (pmap_car m1) (pmap_car m2) with
| left H => left (proj2 (Pmap_eq m1 m2) H)
| right H => right (H proj1 (Pmap_eq m1 m2))
Fixpoint Pmap_wf {A} (t : Pmap_raw A) : bool :=
match t with
| PLeaf => true
| PNode None PLeaf PLeaf => false
| PNode _ l r => Pmap_wf l && Pmap_wf r
end.
Instance Pempty_raw {A} : Empty (Pmap_raw A) := PLeaf.
Global Instance Pempty {A} : Empty (Pmap A) := PMap' Pmap_wf_leaf.
Arguments Pmap_wf _ !_ / : simpl nomatch.
Lemma Pmap_wf_l {A} o (l r : Pmap_raw A) : Pmap_wf (PNode o l r) Pmap_wf l.
Proof. destruct o, l, r; simpl; rewrite ?andb_True; tauto. Qed.
Lemma Pmap_wf_r {A} o (l r : Pmap_raw A) : Pmap_wf (PNode o l r) Pmap_wf r.
Proof. destruct o, l, r; simpl; rewrite ?andb_True; tauto. Qed.
Local Hint Immediate Pmap_wf_l Pmap_wf_r.
Definition PNode' {A} (o : option A) (l r : Pmap_raw A) :=
match l, o, r with PLeaf, None, PLeaf => PLeaf | _, _, _ => PNode o l r end.
Arguments PNode' _ _ _ _ : simpl never.
Lemma PNode_wf {A} o (l r : Pmap_raw A) :
Pmap_wf l Pmap_wf r Pmap_wf (PNode' o l r).
Proof. destruct o, l, r; simpl; auto. Qed.
Local Hint Resolve PNode_wf.
(** Operations *)
Instance Pempty_raw {A} : Empty (Pmap_raw A) := PLeaf.
Instance Plookup_raw {A} : Lookup positive A (Pmap_raw A) :=
fix go (i : positive) (t : Pmap_raw A) {struct t} : option A :=
let _ : Lookup _ _ _ := @go in
match t with
| PLeaf => None
| PNode l o r =>
| PNode o l r => match i with 1 => o | i~0 => l !! i | i~1 => r !! i end
end.
Local Arguments lookup _ _ _ _ _ !_ / : simpl nomatch.
Fixpoint Psingleton_raw {A} (i : positive) (x : A) : Pmap_raw A :=
match i with
| 1 => PNode (Some x) PLeaf PLeaf
| i~0 => PNode None (Psingleton_raw i x) PLeaf
| i~1 => PNode None PLeaf (Psingleton_raw i x)
end.
Fixpoint Ppartial_alter_raw {A} (f : option A option A)
(i : positive) (t : Pmap_raw A) {struct t} : Pmap_raw A :=
match t with
| PLeaf => match f None with None => PLeaf | Some x => Psingleton_raw i x end
| PNode o l r =>
match i with
| 1 => o | i~0 => @lookup _ _ _ go i l | i~1 => @lookup _ _ _ go i r
| 1 => PNode' (f o) l r
| i~0 => PNode' o (Ppartial_alter_raw f i l) r
| i~1 => PNode' o l (Ppartial_alter_raw f i r)
end
end.
Instance Plookup {A} : Lookup positive A (Pmap A) := λ i m, pmap_car m !! i.
Lemma Plookup_empty {A} i : ( : Pmap_raw A) !! i = None.
Proof. by destruct i. Qed.
Fixpoint Pfmap_raw {A B} (f : A B) (t : Pmap_raw A) : Pmap_raw B :=
match t with
| PLeaf => PLeaf
| PNode o l r => PNode (f <$> o) (Pfmap_raw f l) (Pfmap_raw f r)
end.
Fixpoint Pto_list_raw {A} (j : positive) (t : Pmap_raw A)
(acc : list (positive * A)) : list (positive * A) :=
match t with
| PLeaf => acc
| PNode o l r => default [] o (λ x, [(Preverse j, x)]) ++
Pto_list_raw (j~0) l (Pto_list_raw (j~1) r acc)
end%list.
Fixpoint Pomap_raw {A B} (f : A option B) (t : Pmap_raw A) : Pmap_raw B :=
match t with
| PLeaf => PLeaf
| PNode o l r => PNode' (o = f) (Pomap_raw f l) (Pomap_raw f r)
end.
Fixpoint Pmerge_raw {A B C} (f : option A option B option C)
(t1 : Pmap_raw A) (t2 : Pmap_raw B) : Pmap_raw C :=
match t1, t2 with
| PLeaf, t2 => Pomap_raw (f None Some) t2
| t1, PLeaf => Pomap_raw (flip f None Some) t1
| PNode o1 l1 r1, PNode o2 l2 r2 =>
PNode' (f o1 o2) (Pmerge_raw f l1 l2) (Pmerge_raw f r1 r2)
end.
Lemma Pmap_ne_lookup {A} (t : Pmap_raw A) : Pmap_ne t i x, t !! i = Some x.
(** Proofs *)
Lemma Pmap_wf_canon {A} (t : Pmap_raw A) :
( i, t !! i = None) Pmap_wf t t = PLeaf.
Proof.
induction 1 as [? x ?| l r ? IHl | l r ? IHr].
* intros. by exists 1, x.
* destruct IHl as [i [x ?]]. by exists (i~0), x.
* destruct IHr as [i [x ?]]. by exists (i~1), x.
induction t as [|o l IHl r IHr]; intros Ht ?; auto.
assert (o = None) as -> by (apply (Ht 1)).
assert (l = PLeaf) as -> by (apply IHl; try apply (λ i, Ht (i~0)); eauto).
by assert (r = PLeaf) as -> by (apply IHr; try apply (λ i, Ht (i~1)); eauto).
Qed.
Lemma Pmap_wf_eq_get {A} (t1 t2 : Pmap_raw A) :
Pmap_wf t1 Pmap_wf t2 ( i, t1 !! i = t2 !! i) t1 = t2.
Lemma Pmap_wf_eq {A} (t1 t2 : Pmap_raw A) :
( i, t1 !! i = t2 !! i) Pmap_wf t1 Pmap_wf t2 t1 = t2.
Proof.
intros t1wf. revert t2.
induction t1wf as [| ? x ? ? IHl ? IHr | l r ? IHl ? IHr Hne1].
* destruct 1 as [| | ???? [?|?]]; intros Hget.
+ done.
+ discriminate (Hget 1).
+ destruct (Pmap_ne_lookup l) as [i [??]]; trivial.
specialize (Hget (i~0)). simpl in *. congruence.
+ destruct (Pmap_ne_lookup r) as [i [??]]; trivial.
specialize (Hget (i~1)). simpl in *. congruence.
* destruct 1; intros Hget.
+ discriminate (Hget xH).
+ f_equal.
- apply IHl; trivial. intros i. apply (Hget (i~0)).
- apply (Hget 1).
- apply IHr; trivial. intros i. apply (Hget (i~1)).
+ specialize (Hget 1). simpl in *. congruence.
* destruct 1; intros Hget.
+ destruct Hne1.
- destruct (Pmap_ne_lookup l) as [i [??]]; trivial.
specialize (Hget (i~0)); simpl in *. congruence.
- destruct (Pmap_ne_lookup r) as [i [??]]; trivial.
specialize (Hget (i~1)); simpl in *. congruence.
+ specialize (Hget 1); simpl in *. congruence.
+ f_equal.
- apply IHl; trivial. intros i. apply (Hget (i~0)).
- apply IHr; trivial. intros i. apply (Hget (i~1)).
revert t2.
induction t1 as [|o1 l1 IHl r1 IHr]; intros [|o2 l2 r2] Ht ??; simpl; auto.
* discriminate (Pmap_wf_canon (PNode o2 l2 r2)); eauto.
* discriminate (Pmap_wf_canon (PNode o1 l1 r1)); eauto.
* f_equal; [apply (Ht 1)| |].
+ apply IHl; try apply (λ x, Ht (x~0)); eauto.
+ apply IHr; try apply (λ x, Ht (x~1)); eauto.
Qed.
Lemma PNode_lookup {A} o (l r : Pmap_raw A) i :
PNode' o l r !! i = PNode o l r !! i.
Proof. by destruct i, o, l, r. Qed.
Fixpoint Psingleton_raw {A} (i : positive) (x : A) : Pmap_raw A :=
match i with
| 1 => PNode PLeaf (Some x) PLeaf
| i~0 => PNode (Psingleton_raw i x) None PLeaf
| i~1 => PNode PLeaf None (Psingleton_raw i x)
end.
Lemma Psingleton_ne {A} i (x : A) : Pmap_ne (Psingleton_raw i x).
Proof. induction i; simpl; intuition. Qed.
Local Hint Resolve Psingleton_ne.
Lemma Psingleton_wf {A} i (x : A) : Pmap_wf (Psingleton_raw i x).
Proof. induction i; simpl; intuition. Qed.
Local Hint Resolve Psingleton_wf.
Proof. induction i as [[]|[]|]; simpl; rewrite ?andb_true_r; auto. Qed.
Lemma Ppartial_alter_wf {A} f i (t : Pmap_raw A) :
Pmap_wf t Pmap_wf (Ppartial_alter_raw f i t).
Proof.
revert i; induction t as [|o l IHl r IHr]; intros i ?; simpl.
* destruct (f None); auto using Psingleton_wf.
* destruct i; simpl; eauto.
Qed.
Lemma Pfmap_wf {A B} (f : A B) t : Pmap_wf t Pmap_wf (Pfmap_raw f t).
Proof.
induction t as [|[x|] [] ? [] ?]; simpl in *; rewrite ?andb_True; intuition.
Qed.
Lemma Pomap_wf {A B} (f : A option B) t : Pmap_wf t Pmap_wf (Pomap_raw f t).
Proof. induction t; simpl; eauto. Qed.
Lemma Pmerge_wf {A B C} (f : option A option B option C) t1 t2 :
Pmap_wf t1 Pmap_wf t2 Pmap_wf (Pmerge_raw f t1 t2).
Proof. revert t2. induction t1; intros []; simpl; eauto using Pomap_wf. Qed.
Lemma Plookup_empty {A} i : ( : Pmap_raw A) !! i = None.
Proof. by destruct i. Qed.
Lemma Plookup_singleton {A} i (x : A) : Psingleton_raw i x !! i = Some x.
Proof. by induction i. Qed.
Lemma Plookup_singleton_ne {A} i j (x : A) :
i j Psingleton_raw i x !! j = None.
Proof. revert j. induction i; intros [?|?|]; simpl; auto. congruence. Qed.
Definition PNode_canon {A} (l : Pmap_raw A) (o : option A) (r : Pmap_raw A) :=
match l, o, r with PLeaf, None, PLeaf => PLeaf | _, _, _ => PNode l o r end.
Lemma PNode_canon_wf {A} (l : Pmap_raw A) (o : option A) (r : Pmap_raw A) :
Pmap_wf l Pmap_wf r Pmap_wf (PNode_canon l o r).
Proof. intros H1 H2. destruct H1, o, H2; simpl; intuition. Qed.
Local Hint Resolve PNode_canon_wf.
Lemma PNode_canon_lookup_xH {A} (l : Pmap_raw A) o (r : Pmap_raw A) :
PNode_canon l o r !! 1 = o.
Proof. by destruct l,o,r. Qed.
Lemma PNode_canon_lookup_xO {A} (l : Pmap_raw A) o (r : Pmap_raw A) i :
PNode_canon l o r !! i~0 = l !! i.
Proof. by destruct l,o,r. Qed.
Lemma PNode_canon_lookup_xI {A} (l : Pmap_raw A) o (r : Pmap_raw A) i :
PNode_canon l o r !! i~1 = r !! i.
Proof. by destruct l,o,r. Qed.
Ltac PNode_canon_rewrite := repeat first
[ rewrite PNode_canon_lookup_xH | rewrite PNode_canon_lookup_xO
| rewrite PNode_canon_lookup_xI].
Instance Ppartial_alter_raw {A} : PartialAlter positive A (Pmap_raw A) :=
fix go f i t {struct t} : Pmap_raw A :=
match t with
| PLeaf => match f None with None => PLeaf | Some x => Psingleton_raw i x end
| PNode l o r =>
match i with
| 1 => PNode_canon l (f o) r
| i~0 => PNode_canon (@partial_alter _ _ _ go f i l) o r
| i~1 => PNode_canon l o (@partial_alter _ _ _ go f i r)
end
end.
Lemma Ppartial_alter_wf {A} f i (t : Pmap_raw A) :
Pmap_wf t Pmap_wf (partial_alter f i t).
Proof.
intros twf. revert i. induction twf.
* unfold partial_alter. simpl. case (f None); intuition.
* intros [?|?|]; simpl; intuition.
* intros [?|?|]; simpl; intuition.
Qed.
Instance Ppartial_alter {A} : PartialAlter positive A (Pmap A) := λ f i m,
PMap' (partial_alter f i (pmap_car m)) (Ppartial_alter_wf f i _ (pmap_prf m)).
Proof. revert j. induction i; intros [?|?|]; simpl; auto with congruence. Qed.
Lemma Plookup_alter {A} f i (t : Pmap_raw A) :
partial_alter f i t !! i = f (t !! i).
Ppartial_alter_raw f i t !! i = f (t !! i).
Proof.
revert i. induction t.
* intros i. change (match f None with Some x => Psingleton_raw i x
| None => PLeaf end !! i = f None); destruct (f None).
+ intros. apply Plookup_singleton.
+ by destruct i.
* intros [?|?|]; simpl; by PNode_canon_rewrite.
revert i; induction t as [|o l IHl r IHr]; intros i; simpl.
* by destruct (f None); rewrite ?Plookup_singleton.
* destruct i; simpl; rewrite PNode_lookup; simpl; auto.
Qed.
Lemma Plookup_alter_ne {A} f i j (t : Pmap_raw A) :
i j partial_alter f i t !! j = t !! j.
i j Ppartial_alter_raw f i t !! j = t !! j.
Proof.
revert i j. induction t as [|l IHl ? r IHr].
* intros. change (match f None with Some x => Psingleton_raw i x
| None => PLeaf end !! j = None); destruct (f None); [|done].
intros. by apply Plookup_singleton_ne.
* intros [?|?|] [?|?|]; simpl; PNode_canon_rewrite; auto; congruence.
revert i j; induction t as [|o l IHl r IHr]; simpl.
* by intros; destruct (f None); rewrite ?Plookup_singleton_ne.
* by intros [?|?|] [?|?|] ?; simpl; rewrite ?PNode_lookup; simpl; auto.
Qed.
Instance Pfmap_raw : FMap Pmap_raw := λ A B f,
fix go t :=
match t with
| PLeaf => PLeaf | PNode l x r => PNode (go l) (f <$> x) (go r)
end.
Lemma Pfmap_ne `(f : A B) (t : Pmap_raw A) : Pmap_ne t Pmap_ne (fmap f t).
Proof. induction 1; csimpl; auto. Qed.
Local Hint Resolve Pfmap_ne.
Lemma Pfmap_wf `(f : A B) (t : Pmap_raw A) : Pmap_wf t Pmap_wf (fmap f t).
Proof. induction 1; csimpl; intuition. Qed.
Global Instance Pfmap : FMap Pmap := λ A B f m,
PMap' (f <$> pmap_car m) (Pfmap_wf f _ (pmap_prf m)).
Lemma Plookup_fmap {A B} (f : A B) (t : Pmap_raw A) i :
(f <$> t) !! i = f <$> t !! i.
Proof. revert i. induction t. done. by intros [?|?|]; simpl. Qed.
Fixpoint Pto_list_raw {A} (j : positive) (t : Pmap_raw A)
(acc : list (positive * A)) : list (positive * A) :=
match t with
| PLeaf => acc
| PNode l o r => default [] o (λ x, [(Preverse j, x)]) ++
Pto_list_raw (j~0) l (Pto_list_raw (j~1) r acc)
end%list.
Lemma Plookup_fmap {A B} (f : A B) t i : (Pfmap_raw f t) !! i = f <$> t !! i.
Proof. revert i. by induction t; intros [?|?|]; simpl. Qed.
Lemma Pelem_of_to_list {A} (t : Pmap_raw A) j i acc x :
(i,x) Pto_list_raw j t acc
( i', i = i' ++ Preverse j t !! i' = Some x) (i,x) acc.
Proof.
split.
{ revert j acc. induction t as [|l IHl [y|] r IHr]; intros j acc; simpl.
{ revert j acc. induction t as [|[y|] l IHl r IHr]; intros j acc; simpl.
* by right.
* rewrite elem_of_cons. intros [?|?]; simplify_equality.
{ left; exists 1. by rewrite (left_id_L 1 (++))%positive. }
......@@ -271,10 +188,10 @@ Proof.
left; exists (i' ~ 1). by rewrite Preverse_xI, (associative_L _). }
revert t j i acc. assert ( t j i acc,
(i, x) acc (i, x) Pto_list_raw j t acc) as help.
{ intros t; induction t as [|l IHl [y|] r IHr]; intros j i acc;
{ intros t; induction t as [|[y|] l IHl r IHr]; intros j i acc;
simpl; rewrite ?elem_of_cons; auto. }
intros t j ? acc [(i&->&Hi)|?]; [|by auto]. revert j i acc Hi.
induction t as [|l IHl [y|] r IHr]; intros j i acc ?; simpl.
induction t as [|[y|] l IHl r IHr]; intros j i acc ?; simpl.
* done.
* rewrite elem_of_cons. destruct i as [i|i|]; simplify_equality'.
+ right. apply help. specialize (IHr (j~1) i).
......@@ -292,7 +209,7 @@ Lemma Pto_list_nodup {A} j (t : Pmap_raw A) acc :
( i x, (i ++ Preverse j, x) acc t !! i = None)
NoDup acc NoDup (Pto_list_raw j t acc).
Proof.
revert j acc. induction t as [|l IHl [y|] r IHr]; simpl; intros j acc Hin ?.
revert j acc. induction t as [|[y|] l IHl r IHr]; simpl; intros j acc Hin ?.
* done.
* repeat constructor.
{ rewrite Pelem_of_to_list. intros [(i&Hi&?)|Hj].
......@@ -318,60 +235,59 @@ Proof.
apply IHr; auto. intros i x Hi.
apply (Hin (i~1) x). by rewrite Preverse_xI, (associative_L _) in Hi.
Qed.
Global Instance Pto_list {A} : FinMapToList positive A (Pmap A) := λ m,
Pto_list_raw 1 (pmap_car m) [].
Instance Pomap_raw : OMap Pmap_raw := λ A B f,
fix go t :=
match t with
| PLeaf => PLeaf | PNode l o r => PNode_canon (go l) (o = f) (go r)
end.
Lemma Pomap_wf {A B} (f : A option B) (t : Pmap_raw A) :
Pmap_wf t Pmap_wf (omap f t).
Proof. induction 1; csimpl; auto. Qed.
Local Hint Resolve Pomap_wf.
Lemma Pomap_lookup {A B} (f : A option B) (t : Pmap_raw A) i :
omap f t !! i = t !! i = f.
Lemma Pomap_lookup {A B} (f : A option B) t i :
Pomap_raw f t !! i = t !! i = f.
Proof.
revert i. induction t as [| l IHl o r IHr ]; [done |].
intros [?|?|]; csimpl; PNode_canon_rewrite; auto.
revert i. induction t as [|o l IHl r IHr]; intros [i|i|]; simpl;
rewrite ?PNode_lookup; simpl; auto.
Qed.
Lemma Pmerge_lookup {A B C} (f : option A option B option C)
(Hf : f None None = None) t1 t2 i :
Pmerge_raw f t1 t2 !! i = f (t1 !! i) (t2 !! i).
Proof.
revert t2 i; induction t1 as [|o1 l1 IHl1 r1 IHr1]; intros t2 i; simpl.
{ rewrite Pomap_lookup. by destruct (t2 !! i). }
unfold compose, flip.
destruct t2 as [|l2 o2 r2]; rewrite PNode_lookup.
* by destruct i; rewrite ?Pomap_lookup; simpl; rewrite ?Pomap_lookup;
match goal with |- ?o = _ = _ => destruct o end.
* destruct i; rewrite ?Pomap_lookup; simpl; auto.
Qed.
Global Instance Pomap: OMap Pmap := λ A B f m,
PMap' (omap f (pmap_car m)) (Pomap_wf f _ (pmap_prf m)).
Instance Pmerge_raw : Merge Pmap_raw :=
fix Pmerge_raw A B C f t1 t2 : Pmap_raw C :=
match t1, t2 with
| PLeaf, t2 => omap (f None Some) t2
| t1, PLeaf => omap (flip f None Some) t1
| PNode l1 o1 r1, PNode l2 o2 r2 =>
PNode_canon (@merge _ Pmerge_raw A B C f l1 l2)
(f o1 o2) (@merge _ Pmerge_raw A B C f r1 r2)
end.
Local Arguments omap _ _ _ _ _ _ : simpl never.
Lemma Pmerge_wf {A B C} (f : option A option B option C) t1 t2 :
Pmap_wf t1 Pmap_wf t2 Pmap_wf (merge f t1 t2).
Proof. intros t1wf. revert t2. induction t1wf; destruct 1; simpl; auto. Qed.
Global Instance Pmerge: Merge Pmap := λ A B C f m1 m2,
PMap' _ (Pmerge_wf f _ _ (pmap_prf m1) (pmap_prf m2)).
Lemma Pmerge_spec {A B C} (f : option A option B option C)
(Hf : f None None = None) (t1 : Pmap_raw A) t2 i :
merge f t1 t2 !! i = f (t1 !! i) (t2 !! i).
(** Packed version and instance of the finite map type class *)
Inductive Pmap (A : Type) : Type :=
PMap { pmap_car : Pmap_raw A; pmap_prf : Pmap_wf pmap_car }.
Arguments PMap {_} _ _.
Arguments pmap_car {_} _.
Arguments pmap_prf {_} _.
Lemma Pmap_eq {A} (m1 m2 : Pmap A) : m1 = m2 pmap_car m1 = pmap_car m2.
Proof.
revert t2 i. induction t1 as [|l1 IHl1 o1 r1 IHr1]; intros t2 i.
{ unfold merge; simpl. rewrite Pomap_lookup. by destruct (t2 !! i). }
destruct t2 as [|l2 o2 r2].
* unfold merge, Pmerge_raw. rewrite Pomap_lookup.
by destruct (PNode _ _ _ !! i).
* destruct i; simpl; by PNode_canon_rewrite.
split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
simplify_equality'; f_equal; apply proof_irrel.
Qed.
Instance Pmap_eq_dec `{ x y : A, Decision (x = y)}
(m1 m2 : Pmap A) : Decision (m1 = m2) :=
match Pmap_raw_eq_dec (pmap_car m1) (pmap_car m2) with
| left H => left (proj2 (Pmap_eq m1 m2) H)
| right H => right (H proj1 (Pmap_eq m1 m2))
end.
Instance Pempty {A} : Empty (Pmap A) := PMap I.
Instance Plookup {A} : Lookup positive A (Pmap A) := λ i m, pmap_car m !! i.
Instance Ppartial_alter {A} : PartialAlter positive A (Pmap A) := λ f i m,
PMap (partial_alter f i (pmap_car m)) (Ppartial_alter_wf f i _ (pmap_prf m)).
Instance Pfmap : FMap Pmap := λ A B f m,
PMap (f <$> pmap_car m) (Pfmap_wf f _ (pmap_prf m)).
Instance Pto_list {A} : FinMapToList positive A (Pmap A) := λ m,
Pto_list_raw 1 (pmap_car m) [].
Instance Pomap : OMap Pmap := λ A B f m,
PMap (omap f (pmap_car m)) (Pomap_wf f _ (pmap_prf m)).
Instance Pmerge : Merge Pmap := λ A B C f m1 m2,
PMap _ (Pmerge_wf f _ _ (pmap_prf m1) (pmap_prf m2)).
(** * Instantiation of the finite map interface *)
Global Instance: FinMap positive Pmap.
Instance Pmap_finmap : FinMap positive Pmap.
Proof.
split.
* intros ? [t1 ?] [t2 ?] ?. apply Pmap_eq; simpl.
apply Pmap_wf_eq_get; trivial; by apply (bool_decide_unpack _).
* by intros ? [t1 ?] [t2 ?] ?; apply Pmap_eq, Pmap_wf_eq.
* by intros ? [].
* intros ?? [??] ?. by apply Plookup_alter.
* intros ?? [??] ??. by apply Plookup_alter_ne.
......@@ -382,7 +298,7 @@ Proof.
rewrite Pelem_of_to_list, elem_of_nil.
split. by intros [(?&->&?)|]. by left; exists i.
* intros ?? ? [??] ?. by apply Pomap_lookup.
* intros ??? ?? [??] [??] ?. by apply Pmerge_spec.
* intros ??? ?? [??] [??] ?. by apply Pmerge_lookup.
Qed.
(** * Finite sets *)
......@@ -394,12 +310,12 @@ Instance: FinMapDom positive Pmap Pset := mapset_dom_spec.
(** * Fresh numbers *)
Fixpoint Pdepth {A} (m : Pmap_raw A) : nat :=
match m with
| PLeaf | PNode _ None _ => O | PNode l _ _ => S (Pdepth l)
| PLeaf | PNode None _ _ => O | PNode _ l _ => S (Pdepth l)
end.
Fixpoint Pfresh_at_depth {A} (m : Pmap_raw A) (d : nat) : option positive :=
match d, m with
| O, (PLeaf | PNode _ None _) => Some 1
| S d, PNode l _ r =>
| O, (PLeaf | PNode None _ _) => Some 1
| S d, PNode _ l r =>
match Pfresh_at_depth l d with
| Some i => Some (i~0) | None => (~1) <$> Pfresh_at_depth r d
end
......@@ -423,8 +339,8 @@ Lemma Pfresh_at_depth_fresh {A} (m : Pmap_raw A) d i :
Pfresh_at_depth m d = Some i m !! i = None.
Proof.
revert i m; induction d as [|d IH].
{ intros i [|l [] r] ?; naive_solver. }
intros i [|l o r] ?; simplify_equality'.
{ intros i [|[] l r] ?; naive_solver. }
intros i [|o l r] ?; simplify_equality'.
destruct (Pfresh_at_depth l d) as [i'|] eqn:?,
(Pfresh_at_depth r d) as [i''|] eqn:?; simplify_equality'; auto.
Qed.
......@@ -436,7 +352,7 @@ Proof.
Qed.
Lemma Pfresh_depth {A} (m : Pmap_raw A) :
m !! Pos.shiftl_nat 1 (Pdepth m) = None.
Proof. induction m as [|l IHl [x|] r IHr]; auto. Qed.
Proof. induction m as [|[x|] l IHl r IHr]; auto. Qed.
Lemma Pfresh_fresh {A} (m : Pmap A) : m !! Pfresh m = None.
Proof.
destruct m as [m ?]; unfold lookup, Plookup, Pfresh; simpl.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment