diff --git a/theories/countable.v b/theories/countable.v index 4619d73b8a5e60cbdab1299ed462c1f66f173281..70d9914dd5abe8103eaf114c5c8c49e11b2a7eb3 100644 --- a/theories/countable.v +++ b/theories/countable.v @@ -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 *) diff --git a/theories/namespaces.v b/theories/namespaces.v index 78d2bedf9cc4fff05726d2e54b78961710ead853..52c12d70bfb117ff67941b375a2993d80d25350f 100644 --- a/theories/namespaces.v +++ b/theories/namespaces.v @@ -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.