More efficient list encoding for Countable

This changes the encoding used for finite lists of values of countable
types to be linear instead of exponential. The encoding works by
duplicating bits of each element so that 0 -> 00 and 1 -> 11, and then
separating each element with 10. The top 1-bits are not kept since we
know a 10 is starting a new element which ends with a 1.

Fix #28

theories/countable.v

@@ -212,62 +212,16 @@ 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
-  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.
-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.
-Qed.
-Program Instance list_countable `{Countable A} : Countable (list A) :=
-  {| encode := list_encode 1; decode := list_decode [] 0 |}.
+Global Program Instance list_countable `{Countable A} : Countable (list A) :=
+  {| encode xs := positives_flatten (encode <$> xs);
+     decode p := positives ← positives_unflatten p;
+                 mapM decode positives; |}.
 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 A EqA CA xs.
+  simpl.
+  rewrite positives_unflatten_flatten.
+  simpl.
+  apply (mapM_fmap_Some _ _ _ decode_encode).
 Qed.
 
 (** ** Numbers *)

theories/list.v

@@ -354,6 +354,42 @@ Section list_set.
     end.
 End list_set.
 
+(* These next functions allow to efficiently encode lists of positives (bit strings)
+   into a single positive and go in the other direction as well. This is for
+   example used for the countable instance of lists and in namespaces.
+   The main functions are positives_flatten and positives_unflatten. *)
+Fixpoint positives_flatten_go (xs : list positive) (acc : positive) : positive :=
+  match xs with
+  | [] => acc
+  | x :: xs => positives_flatten_go xs (acc~1~0 ++ Preverse (Pdup x))
+  end.
+
+(** Flatten a list of positives into a single positive by
+    duplicating the bits of each element, so that
+    * 0 -> 00
+    * 1 -> 11
+    and then separating each element with 10. *)
+Definition positives_flatten (xs : list positive) : positive :=
+  positives_flatten_go xs 1.
+
+Fixpoint positives_unflatten_go
+        (p : positive)
+        (acc_xs : list positive)
+        (acc_elm : positive)
+  : option (list positive) :=
+  match p with
+  | 1 => Some acc_xs
+  | p'~0~0 => positives_unflatten_go p' acc_xs (acc_elm~0)
+  | p'~1~1 => positives_unflatten_go p' acc_xs (acc_elm~1)
+  | p'~1~0 => positives_unflatten_go p' (acc_elm :: acc_xs) 1
+  | _ => None
+  end%positive.
+
+(** Unflatten a positive into a list of positives, assuming the encoding
+    used by positives_flatten. *)
+Definition positives_unflatten (p : positive) : option (list positive) :=
+  positives_unflatten_go p [] 1.
+
 (** * Basic tactics on lists *)
 (** The tactic [discriminate_list] discharges a goal if it submseteq
 a list equality involving [(::)] and [(++)] of two lists that have a different
@@ -3625,6 +3661,115 @@ Instance TCForall_app {A} (P : A → Prop) xs ys :
   TCForall P xs → TCForall P ys → TCForall P (xs ++ ys).
 Proof. rewrite !TCForall_Forall. apply Forall_app_2. Qed.
 
+Section positives_flatten_unflatten.
+  Local Open Scope positive_scope.
+
+  Lemma positives_flatten_go_app xs acc :
+    positives_flatten_go xs acc = acc ++ positives_flatten_go xs 1.
+  Proof.
+    revert acc.
+    induction xs as [|x xs IH]; intros acc; simpl.
+    - reflexivity.
+    - rewrite IH.
+      rewrite (IH (6 ++ _)).
+      rewrite 2!(assoc_L (++)).
+      reflexivity.
+  Qed.
+  
+  Lemma positives_unflatten_go_app p suffix xs acc :
+    positives_unflatten_go (suffix ++ Preverse (Pdup p)) xs acc =
+    positives_unflatten_go suffix xs (acc ++ p).
+  Proof.
+    revert suffix acc.
+    induction p as [p IH|p IH|]; intros acc suffix; simpl.
+    - rewrite 2!Preverse_xI.
+      rewrite 2!(assoc_L (++)).
+      rewrite IH.
+      reflexivity.
+    - rewrite 2!Preverse_xO.
+      rewrite 2!(assoc_L (++)).
+      rewrite IH.
+      reflexivity.
+    - reflexivity.
+  Qed.
+  
+  Lemma positives_unflatten_flatten_go suffix xs acc :
+    positives_unflatten_go (suffix ++ positives_flatten_go xs 1) acc 1 =
+    positives_unflatten_go suffix (xs ++ acc) 1.
+  Proof.
+    revert suffix acc.
+    induction xs as [|x xs IH]; intros suffix acc; simpl.
+    - reflexivity.
+    - rewrite positives_flatten_go_app.
+      rewrite (assoc_L (++)).
+      rewrite IH.
+      rewrite (assoc_L (++)).
+      rewrite positives_unflatten_go_app.
+      simpl.
+      rewrite (left_id_L 1 (++)).
+      reflexivity.
+  Qed.
+  
+  Lemma positives_unflatten_flatten xs :
+    positives_unflatten (positives_flatten xs) = Some xs.
+  Proof.
+    unfold positives_flatten, positives_unflatten.
+    replace (positives_flatten_go xs 1)
+      with (1 ++ positives_flatten_go xs 1)
+      by apply (left_id_L 1 (++)).
+    rewrite positives_unflatten_flatten_go.
+    simpl.
+    rewrite (right_id_L [] (++)%list).
+    reflexivity.
+  Qed.
+  
+  Lemma positives_flatten_app xs ys :
+    positives_flatten (xs ++ ys) = positives_flatten xs ++ positives_flatten ys.
+  Proof.
+    unfold positives_flatten.
+    revert ys.
+    induction xs as [|x xs IH]; intros ys; simpl.
+    - rewrite (left_id_L 1 (++)).
+      reflexivity.
+    - rewrite positives_flatten_go_app, (positives_flatten_go_app xs).
+      rewrite IH.
+      rewrite (assoc_L (++)).
+      reflexivity.
+  Qed.
+  
+  Lemma positives_flatten_cons x xs :
+    positives_flatten (x :: xs) = 1~1~0 ++ Preverse (Pdup x) ++ positives_flatten xs.
+  Proof.
+    change (x :: xs) with ([x] ++ xs)%list.
+    rewrite positives_flatten_app.
+    rewrite (assoc_L (++)).
+    reflexivity.
+  Qed.
+  
+  Lemma positives_flatten_suffix (l k : list positive) :
+    l `suffix_of` k → ∃ q, positives_flatten k = q ++ positives_flatten l.
+  Proof.
+    intros [l' ->].
+    exists (positives_flatten l').
+    apply positives_flatten_app.
+  Qed.
+  
+  Lemma positives_flatten_suffix_eq p1 p2 (xs ys : list positive) :
+    length xs = length ys →
+    p1 ++ positives_flatten xs = p2 ++ positives_flatten ys →
+    xs = ys.
+  Proof.
+    revert p1 p2 ys; induction xs as [|x xs IH];
+      intros p1 p2 [|y ys] ?; simplify_eq/=; auto.
+    rewrite !positives_flatten_cons, !(assoc _); intros Hl.
+    assert (xs = ys) as <- by eauto; clear IH H; f_equal.
+    apply (inj (++ positives_flatten xs)) in Hl.
+    rewrite 2!Preverse_Pdup in Hl.
+    apply (Pdup_suffix_eq _ _ p1 p2) in Hl.
+    by apply (inj Preverse).
+  Qed.
+End positives_flatten_unflatten.
+
 (** * Relection over lists *)
 (** We define a simple data structure [rlist] to capture a syntactic
 representation of lists consisting of constants, applications and the nil list.

theories/namespaces.v

@@ -14,7 +14,8 @@ 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).
+Definition nclose_def (N : namespace) : coPset :=
+  coPset_suffixes (positives_flatten 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.
@@ -36,17 +37,12 @@ Section namespace.
 
   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 (positives_flatten_suffix N (ndot_def N x)) as [q' ?].
     { by exists [encode x]. }
     by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal.
   Qed.
@@ -54,8 +50,6 @@ Section namespace.
   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 +58,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]%positives_flatten_suffix_eq.
   Qed.
 
   Lemma ndot_preserve_disjoint_l N E x : ↑N ## E → ↑N.@x ## E.

theories/numbers.v

@@ -197,6 +197,23 @@ Proof Preverse_app p (1~0).
 Lemma Preverse_xI p : Preverse (p~1) = (1~1) ++ Preverse p.
 Proof Preverse_app p (1~1).
 
+Lemma Preverse_involutive p :
+  Preverse (Preverse p) = p.
+Proof.
+  induction p as [p IH|p IH|]; simpl.
+  - by rewrite Preverse_xI, Preverse_app, IH.
+  - by rewrite Preverse_xO, Preverse_app, IH.
+  - reflexivity.
+Qed.
+    
+Instance Preverse_inj : Inj (=) (=) Preverse.
+Proof.
+  intros p q eq.
+  rewrite <- (Preverse_involutive p).
+  rewrite <- (Preverse_involutive q).
+  by rewrite eq.
+Qed.
+
 Fixpoint Plength (p : positive) : nat :=
   match p with 1 => 0%nat | p~0 | p~1 => S (Plength p) end.
 Lemma Papp_length p1 p2 : Plength (p1 ++ p2) = (Plength p2 + Plength p1)%nat.
@@ -209,6 +226,59 @@ Proof.
   - intros [z ->]. lia.
 Qed.
 
+(** Duplicate the bits of a positive, i.e. 1~0~1 -> 1~0~0~1~1 and
+    1~1~0~0 -> 1~1~1~0~0~0~0 *)
+Fixpoint Pdup (p : positive) : positive :=
+  match p with
+  | 1 => 1
+  | p'~0 => (Pdup p')~0~0
+  | p'~1 => (Pdup p')~1~1
+  end.
+
+Lemma Pdup_app p q :
+  Pdup (p ++ q) = Pdup p ++ Pdup q.
+Proof.
+  revert p.
+  induction q as [p IH|p IH|]; intros q; simpl.
+  - by rewrite IH.
+  - by rewrite IH.
+  - reflexivity.
+Qed.
+
+Lemma Pdup_suffix_eq p q s1 s2 :
+  s1~1~0 ++ Pdup p = s2~1~0 ++ Pdup q → p = q.
+Proof.
+  revert q.
+  induction p as [p IH|p IH|]; intros [q|q|] eq; simplify_eq/=.
+  - by rewrite (IH q).
+  - by rewrite (IH q).
+  - reflexivity.
+Qed.
+
+Instance Pdup_inj : Inj (=) (=) Pdup.
+Proof.
+  intros p q eq.
+  apply (Pdup_suffix_eq _ _ 1 1).
+  by rewrite eq.
+Qed.
+
+Lemma Preverse_Pdup p :
+  Preverse (Pdup p) = Pdup (Preverse p).
+Proof.
+  induction p as [p IH|p IH|]; simpl.
+  - rewrite 3!Preverse_xI.
+    rewrite (assoc_L (++)).
+    rewrite IH.
+    rewrite Pdup_app.
+    reflexivity.
+  - rewrite 3!Preverse_xO.
+    rewrite (assoc_L (++)).
+    rewrite IH.
+    rewrite Pdup_app.
+    reflexivity.
+  - reflexivity.
+Qed.
+
 Close Scope positive_scope.
 
 (** * Notations and properties of [N] *)