More efficient `Countable` instance for list and make `namespaces` independent of that.

This reverts part of commit 54954f55.

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 *)

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.