Merge branch 'better-list-countable' into 'master'

More efficient list encoding for Countable

See merge request !62

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