...
 
Commits (1)
......@@ -212,62 +212,39 @@ Next Obligation.
Qed.
(** ** Lists *)
(* Lists are encoded as 1 separated sequences of 0s corresponding to the unary
representation of the elements. *)
Fixpoint list_encode `{Countable A} (acc : positive) (l : list A) : positive :=
match l with
| [] => acc
| x :: l => list_encode (Nat.iter (encode_nat x) (~0) (acc~1)) l
end.
Fixpoint list_decode `{Countable A} (acc : list A)
(n : nat) (p : positive) : option (list A) :=
match p with
| 1 => Some acc
| p~0 => list_decode acc (S n) p
| p~1 => x decode_nat n; list_decode (x :: acc) O p
Fixpoint list_encode_ (l : list positive) : positive :=
match l with [] => 1 | x :: l => prod_encode x (list_encode_ l) end.
Definition list_encode (l : list positive) : positive :=
prod_encode (Pos.of_nat (S (length l))) (list_encode_ l).
Fixpoint list_decode_ (n : nat) (p : positive) : option (list positive) :=
match n with
| O => guard (p = 1); Some []
| S n =>
x prod_decode_fst p; pl prod_decode_snd p;
l list_decode_ n pl; Some (x :: l)
end.
Lemma x0_iter_x1 n acc : Nat.iter n (~0) acc~1 = acc ++ Nat.iter n (~0) 3.
Proof. by induction n; f_equal/=. Qed.
Lemma list_encode_app' `{Countable A} (l1 l2 : list A) acc :
list_encode acc (l1 ++ l2) = list_encode acc l1 ++ list_encode 1 l2.
Definition list_decode (p : positive) : option (list positive) :=
pn prod_decode_fst p; pl prod_decode_snd p;
list_decode_ (pred (Pos.to_nat pn)) pl.
Lemma list_decode_encode l : list_decode (list_encode l) = Some l.
Proof.
revert acc; induction l1; simpl; auto.
induction l2 as [|x l IH]; intros acc; simpl; [by rewrite ?(left_id_L _ _)|].
by rewrite !(IH (Nat.iter _ _ _)), (assoc_L _), x0_iter_x1.
cut (list_decode_ (length l) (list_encode_ l) = Some l).
{ intros help. unfold list_decode, list_encode.
rewrite prod_decode_encode_fst, prod_decode_encode_snd; csimpl.
by rewrite Nat2Pos.id by done; simpl. }
induction l; simpl; auto.
by rewrite prod_decode_encode_fst, prod_decode_encode_snd; simplify_option_eq.
Qed.
Program Instance list_countable `{Countable A} : Countable (list A) :=
{| encode := list_encode 1; decode := list_decode [] 0 |}.
Program Instance list_countable `{Countable A} : Countable (list A) := {|
encode l := list_encode (encode <$> l);
decode p := list_decode p = mapM decode
|}.
Next Obligation.
intros A ??; simpl.
assert ( m acc n p, list_decode acc n (Nat.iter m (~0) p)
= list_decode acc (n + m) p) as decode_iter.
{ induction m as [|m IH]; intros acc n p; simpl; [by rewrite Nat.add_0_r|].
by rewrite IH, Nat.add_succ_r. }
cut ( l acc, list_decode acc 0 (list_encode 1 l) = Some (l ++ acc))%list.
{ by intros help l; rewrite help, (right_id_L _ _). }
induction l as [|x l IH] using @rev_ind; intros acc; [done|].
rewrite list_encode_app'; simpl; rewrite <-x0_iter_x1, decode_iter; simpl.
by rewrite decode_encode_nat; simpl; rewrite IH, <-(assoc_L _).
Qed.
Lemma list_encode_app `{Countable A} (l1 l2 : list A) :
encode (l1 ++ l2)%list = encode l1 ++ encode l2.
Proof. apply list_encode_app'. Qed.
Lemma list_encode_cons `{Countable A} x (l : list A) :
encode (x :: l) = Nat.iter (encode_nat x) (~0) 3 ++ encode l.
Proof. apply (list_encode_app' [_]). Qed.
Lemma list_encode_suffix `{Countable A} (l k : list A) :
l `suffix_of` k q, encode k = q ++ encode l.
Proof. intros [l' ->]; exists (encode l'); apply list_encode_app. Qed.
Lemma list_encode_suffix_eq `{Countable A} q1 q2 (l1 l2 : list A) :
length l1 = length l2 q1 ++ encode l1 = q2 ++ encode l2 l1 = l2.
Proof.
revert q1 q2 l2; induction l1 as [|a1 l1 IH];
intros q1 q2 [|a2 l2] ?; simplify_eq/=; auto.
rewrite !list_encode_cons, !(assoc _); intros Hl.
assert (l1 = l2) as <- by eauto; clear IH; f_equal.
apply (inj encode_nat); apply (inj (++ encode l1)) in Hl; revert Hl; clear.
generalize (encode_nat a2).
induction (encode_nat a1); intros [|?] ?; naive_solver.
intros ??? l; simpl; rewrite list_decode_encode; simpl.
apply mapM_fmap_Some; auto using decode_encode.
Qed.
(** ** Numbers *)
......
......@@ -14,7 +14,16 @@ Definition ndot_aux : seal (@ndot_def). by eexists. Qed.
Definition ndot {A A_dec A_count}:= unseal ndot_aux A A_dec A_count.
Definition ndot_eq : @ndot = @ndot_def := seal_eq ndot_aux.
Definition nclose_def (N : namespace) : coPset := coPset_suffixes (encode N).
(* Namespaces are encoded as 1 separated sequences of 0s corresponding to the
unary representation of the elements. *)
Fixpoint namespace_encode (N : namespace) : positive :=
match N with
| [] => 1
| p :: N => Nat.iter (encode_nat p) (~0) 3 ++ namespace_encode N
end%positive.
Definition nclose_def (N : namespace) : coPset :=
coPset_suffixes (namespace_encode N).
Definition nclose_aux : seal (@nclose_def). by eexists. Qed.
Instance nclose : UpClose namespace coPset := unseal nclose_aux.
Definition nclose_eq : @nclose = @nclose_def := seal_eq nclose_aux.
......@@ -30,32 +39,52 @@ Section namespace.
Implicit Types x y : A.
Implicit Types N : namespace.
Implicit Types E : coPset.
Open Scope positive_scope.
Lemma namespace_encode_app N1 N2 :
namespace_encode (N1 ++ N2)%list = namespace_encode N1 ++ namespace_encode N2.
Proof.
induction N1 as [|x N1 IH]; simpl.
- by rewrite (left_id_L _ _).
- by rewrite IH, (assoc_L _).
Qed.
Lemma namespace_encode_suffix N1 N2 :
N1 `suffix_of` N2 q, namespace_encode N2 = q ++ namespace_encode N1.
Proof.
intros [N3 ->]. exists (namespace_encode N3). apply namespace_encode_app.
Qed.
Lemma namespace_encode_suffix_eq q1 q2 N1 N2 :
length N1 = length N2
q1 ++ namespace_encode N1 = q2 ++ namespace_encode N2
N1 = N2.
Proof.
revert q1 q2 N2; induction N1 as [|a1 N1 IH];
intros q1 q2 [|a2 N2] ?; simplify_eq/=; auto.
rewrite !(assoc _); intros Hl.
assert (N1 = N2) as <- by eauto; clear IH; f_equal.
apply (inj encode_nat); apply (inj (++ namespace_encode N1)) in Hl; revert Hl; clear.
generalize (encode_nat a2).
induction (encode_nat a1); intros [|?] ?; naive_solver.
Qed.
Global Instance ndot_inj : Inj2 (=) (=) (=) (@ndot A _ _).
Proof. intros N1 x1 N2 x2; rewrite !ndot_eq; naive_solver. Qed.
Lemma nclose_nroot : nroot = (:coPset).
Proof. rewrite nclose_eq. by apply (sig_eq_pi _). Qed.
Lemma encode_nclose N : encode N (N:coPset).
Proof.
rewrite nclose_eq.
by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _).
Qed.
Lemma nclose_subseteq N x : N.@x (N : coPset).
Proof.
intros p. unfold up_close. rewrite !nclose_eq, !ndot_eq.
unfold nclose_def, ndot_def; rewrite !elem_coPset_suffixes.
intros [q ->]. destruct (list_encode_suffix N (ndot_def N x)) as [q' ?].
intros [q ->]. destruct (namespace_encode_suffix N (ndot_def N x)) as [q' ?].
{ by exists [encode x]. }
by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal.
exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal; auto.
Qed.
Lemma nclose_subseteq' E N x : N E N.@x E.
Proof. intros. etrans; eauto using nclose_subseteq. Qed.
Lemma ndot_nclose N x : encode (N.@x) (N:coPset).
Proof. apply nclose_subseteq with x, encode_nclose. Qed.
Lemma nclose_infinite N : ¬set_finite ( N : coPset).
Proof. rewrite nclose_eq. apply coPset_suffixes_infinite. Qed.
......@@ -64,7 +93,7 @@ Section namespace.
intros Hxy a. unfold up_close. rewrite !nclose_eq, !ndot_eq.
unfold nclose_def, ndot_def; rewrite !elem_coPset_suffixes.
intros [qx ->] [qy Hqy].
revert Hqy. by intros [= ?%encode_inj]%list_encode_suffix_eq.
revert Hqy. by intros [= ?%encode_inj]%namespace_encode_suffix_eq.
Qed.
Lemma ndot_preserve_disjoint_l N E x : N ## E N.@x ## E.
......