tests/tactics.v

+(** Basic tests for atctics that don't import anything else
+(and hence can be run even when nothing else even builds. *)
+From Coq Require Import String.
 From stdpp Require Import tactics.
 
-Goal forall P1 P2 P3 P4 (P: Prop),
+Local Unset Mangle Names. (* for stable goal printing *)
+Local Open Scope string_scope.
+
+Goal ∀ P1 P2 P3 P4 (P: Prop),
   P1 ∨ (Is_true (P2 || P3)) ∨ P4 →
   (P1 → P) →
   (P2 → P) →
@@ -12,7 +18,7 @@ Proof.
   destruct_or? HH; [ exact (X1 HH) | exact (X2 HH) | exact (X3 HH) | exact (X4 HH) ].
 Qed.
 
-Goal forall P1 P2 P3 P4 (P: Prop),
+Goal ∀ P1 P2 P3 P4 (P: Prop),
   P1 ∨ P2 →
   P3 ∨ P4 →
   (P1 → P3 → P) →
@@ -25,7 +31,7 @@ Proof.
   destruct_or?; [ exact (X1 HH1 HH2) | exact (X3 HH1 HH2) | exact (X2 HH1 HH2) | exact (X4 HH1 HH2) ].
 Qed.
 
-Goal forall P1 P2 P3 P4 (P: Prop),
+Goal ∀ P1 P2 P3 P4 (P: Prop),
   id (P1 ∨ P2) →
   id (P3 ∨ P4) →
   (P1 → P3 → P) →
@@ -41,10 +47,367 @@ Proof.
   [ exact (X1 HH1 HH2) | exact (X2 HH1 HH2) | exact (X3 HH1 HH2) | exact (X4 HH1 HH2) ].
 Qed.
 
-Goal forall P1 P2 P3 P4,
+Goal ∀ P1 P2 P3 P4,
   P1 ∧ (Is_true (P2 && P3)) ∧ P4 →
   P1 ∧ P2 ∧ P3.
 Proof.
   intros * HH. split_and!; [ destruct_and? HH; assumption | destruct_and?; assumption | ].
   destruct_and?. Fail destruct_and!. assumption.
 Qed.
+
+(** Tests for [case_match] *)
+Goal ∀ n : nat, match n with | 0 => n = 0 | S n' => n = S n' end.
+Proof.
+  intros. by case_match.
+Restart. Proof.
+  intros. by case_match eqn:Heq; revert Heq. (* [revert Heq] checks that [Heq] exists *)
+Qed.
+
+Goal ∀ n m : nat, match n with | 0 => m = 0 | S n' => m = S n' end → n = m.
+Proof.
+  intros. by case_match.
+Restart. Proof.
+  intros. by case_match eqn:Heq; revert Heq. (* [revert Heq] checks that [Heq] exists *)
+Qed.
+
+(** Tests for [select] tactics *)
+Goal ∀ (n : nat), ∃ m : nat, True.
+Proof. intros ?. rename select nat into m. exists m. done. Qed.
+
+Goal ∀ (P : nat → Prop), P 3 → P 4 → P 4.
+Proof. intros P **. rename select (P _) into HP4. apply HP4. Qed.
+
+Goal ∀ P Q : Prop, True ∨ True → P ∨ Q → Q ∨ P.
+Proof.
+  intros P Q ??.
+  (* should select the last hypothesis *)
+  destruct select (_ ∨ _); by constructor.
+Restart. Proof.
+  intros P Q ??.
+  (* should select the last hypothesis *)
+  destruct select (_ ∨ _) as [H1|H2].
+  - right. exact H1.
+  - left. exact H2.
+Restart. Proof.
+  intros P Q ??.
+  (* should select the last hypothesis *)
+  inv select (_ ∨ _); by constructor.
+Restart. Proof.
+  intros P Q ??.
+  (* should select the last hypothesis *)
+  inv select (_ ∨ _) as [H1|H2].
+  - right. exact H1.
+  - left. exact H2.
+Restart. Proof.
+  intros P Q ??.
+  (* should select the last hypothesis *)
+  inversion select (_ ∨ _); by constructor.
+Restart. Proof.
+  intros P Q ??.
+  (* should select the last hypothesis *)
+  inversion select (_ ∨ _) as [H1|H2].
+  - right. exact H1.
+  - left. exact H2.
+Qed.
+
+(** [mk_evar] works on things that coerce to types. *)
+(** This is a feature when we have packed structures, for example Iris's [ofe]
+(fields other than the carrier omitted). *)
+Structure ofe := Ofe { ofe_car :> Type }.
+Goal ∀ A : ofe, True.
+intros A.
+let x := mk_evar A in idtac.
+Abort.
+(** More surprisingly, it also works for other coercions into a
+universe, like [Is_true : bool → Prop]. *)
+Goal True.
+let x := mk_evar true in idtac.
+Abort.
+
+(** get_head tests. *)
+Lemma test_get_head (f : nat → nat → nat → nat) : True.
+Proof.
+  let f' := get_head (f 0 1 2) in unify f f'.
+  let f' := get_head f in unify f f'.
+Abort.
+
+(** inv tests *)
+Inductive even : nat → Prop :=
+  | Even0 : even 0
+  | Even2 n : even n → even (S (S n)).
+Lemma inv_test_1 n : even (2 + n) → even n.
+Proof. intros H. inv H as [|? H']. Show. done. Qed.
+Lemma inv_test_2 (a b c d : nat) : a ≠ c → (a, b) = (c, d) → False.
+Proof.
+  (* Test taken from https://github.com/coq/coq/issues/2465 *)
+  intros DIFF EQ. inv EQ. (* Thanks to the simplify_eq this solves the goal. *)
+Qed.
+Check "inv_test_num".
+Lemma inv_test_num n : True → even (2 + n) → even n.
+Proof.
+  (* Make sure we do the same thing as [inversion_clear] when there are
+  other hypotheses before the one we invert. *)
+  inversion_clear 2 as [|? H']. Show.
+Restart. Proof.
+  inv 2 as [|? H']. Show. done.
+Qed.
+
+(** o-tactic tests *)
+Check "otest".
+Lemma otest (P Q R : nat → Prop)
+  (HPQR1 : ∀ m n, P n → Q m → R (n + m))
+  (HPQR2 : ∀ m n, P n → Q m → R (n + m) ∧ R 2)
+  (HP0 : P 0)
+  (HP1 : P 1)
+  (HQ : Q 5) : R 6.
+Proof.
+  (** Imagine we couldn't [apply] since the goal is still very different, we
+  need forward reasoning. Also we don't have proof terms for [P n] and [Q m] but
+  a short proof script can solve them. [n] needs to be specified, but [m] is
+  huge and we don't want to specify it. What do we do? The "o" family of tactics
+  for working with "o"pen terms helps. *)
+  opose proof (HPQR1 _ (S _) _ _) as HR; [exact HP1|exact HQ|]. exact HR.
+Restart. Proof.
+  (** We can have fewer [_]. *)
+  opose proof (HPQR1 _ (S _) _) as HR; [exact HP1|]. exact (HR HQ).
+Restart. Proof.
+  (** And even fewer. *)
+  opose proof (HPQR1 _ (S _)) as HR. exact (HR HP1 HQ).
+Restart. Proof.
+  (** The [*] variant automatically adds [_]. *)
+  opose proof* (HPQR1 _ (S _)) as HR; [exact HP1|exact HQ|]. exact HR.
+Restart. Proof.
+  (** Same deal for [generalize]. *)
+  ogeneralize (HPQR1 _ 1). intros HR. exact (HR HP1 HQ).
+Restart. Proof.
+  ogeneralize (HPQR1 _ 1 _); [exact HP1|]. intros HR. exact (HR HQ).
+Restart. Proof.
+  ogeneralize* (HPQR1 _ 1); [exact HP1|exact HQ|]. intros HR. exact HR.
+Restart. Proof.
+  (** [odestruct] also automatically adds subgoals until there is something
+  to destruct, as usual. Note that [edestruct] wouldn't help here,
+  it just complains that it cannot infer the placeholder. *)
+  Fail edestruct (HPQR2 _ 1).
+  odestruct (HPQR2 _ 1) as [HR1 HR2]; [exact HP1|exact HQ|]. exact HR1.
+Restart. Proof.
+  (** [ospecialize] is like [opose proof] but it reuses the name.
+  It only works on local assumptions. *)
+  Fail ospecialize (plus 0 0).
+  ospecialize (HPQR1 _ 1 _); [exact HP1|]. exact (HPQR1 HQ).
+Restart. Proof.
+  ospecialize (HPQR1 _ 1). exact (HPQR1 HP1 HQ).
+Restart. Proof.
+  ospecialize* (HPQR1 _ 1); [exact HP1|exact HQ|]. exact HPQR1.
+Qed.
+
+(** Make sure [∀] also get auto-instantiated by the [*] variant. *)
+Lemma o_tactic_with_forall (P Q R : nat → Prop) :
+  P 1 → Q 1 → (∀ n, P n → Q n → R n) → R 1.
+Proof.
+  intros HP HQ HR.
+  ospecialize* HR; [exact HP|exact HQ|exact HR].
+Restart. Proof.
+  intros HP HQ HR.
+  opose proof* HR as HR'; [exact HP|exact HQ|exact HR'].
+Qed.
+
+(* Like [inversion], this does *not* clear. *)
+Check "oinversion_test1".
+Lemma oinversion_test1 n : even (2 + n) → even n.
+Proof. intros H. oinversion H as [|n' Hn' EQ]. Show. done. Qed.
+
+Lemma oinv_test1 : ~(∀ n, even n).
+Proof. intros H. oinv (H 1). Qed.
+(* Ensure we clear the [H] if appropriate. *)
+Check "oinv_test2".
+Lemma oinv_test2 n : even (2 + n) → even n.
+Proof.
+  intros H. oinv H as [|? H']. Show. done.
+Restart. Proof.
+  oinv 1 as [|? H']. Show. done.
+Qed.
+Lemma oinv_test_num (P : Prop) n :
+  P → (P → even (2 + n)) → even n.
+Proof.
+  intros HP. oinv 1.
+  { exact HP. }
+  done.
+Qed.
+
+Check "notypeclasses_apply_error".
+Lemma notypeclasses_apply_error (P Q : Prop) : (P → Q) → Q → P.
+Proof.
+  intros H HQ. Fail notypeclasses apply H.
+Abort.
+
+(** Some tests for f_equiv. *)
+(* Similar to [f_equal], it should solve goals by [reflexivity]. *)
+Lemma test_f_equiv_refl {A} (R : relation A) `{!Equivalence R} x :
+  R x x.
+Proof. f_equiv. Qed.
+
+(* And immediately solve sub-goals by reflexivity *)
+Lemma test_f_equiv_refl_nested {A} (R : relation A) `{!Equivalence R} g x y z :
+  Proper (R ==> R ==> R) g →
+  R y z →
+  R (g x y) (g x z).
+Proof. intros ? Hyz. f_equiv. apply Hyz. Qed.
+
+(* Ensure we can handle [flip]. *)
+Lemma f_equiv_flip {A} (R : relation A) `{!PreOrder R} (f : A → A) :
+  Proper (R ==> R) f → Proper (flip R ==> flip R) f.
+Proof. intros ? ?? EQ. f_equiv. exact EQ. Qed.
+
+Section f_equiv.
+  Context `{!Equiv A, !Equiv B, !SubsetEq A}.
+
+  Lemma f_equiv1 (fn : A → B) (x1 x2 : A) :
+    Proper ((≡) ==> (≡)) fn →
+    x1 ≡ x2 →
+    fn x1 ≡ fn x2.
+  Proof. intros. f_equiv. assumption. Qed.
+
+  Lemma f_equiv2 (fn : A → B) (x1 x2 : A) :
+    Proper ((⊆) ==> (≡)) fn →
+    x1 ⊆ x2 →
+    fn x1 ≡ fn x2.
+  Proof. intros. f_equiv. assumption. Qed.
+
+  (* Ensure that we prefer the ≡. *)
+  Lemma f_equiv3 (fn : A → B) (x1 x2 : A) :
+    Proper ((≡) ==> (≡)) fn →
+    Proper ((⊆) ==> (≡)) fn →
+    x1 ≡ x2 →
+    fn x1 ≡ fn x2.
+  Proof.
+    (* The Coq tactic prefers the ⊆. *)
+    intros. Morphisms.f_equiv. Fail assumption.
+  Restart. Proof.
+    intros. f_equiv. assumption.
+  Qed.
+End f_equiv.
+
+(** Some tests for solve_proper (also testing f_equiv indirectly). *)
+
+(** Test case for #161 *)
+Lemma test_solve_proper_const {A} (R : relation A) `{!Equivalence R} x :
+  Proper (R ==> R) (λ _, x).
+Proof. solve_proper. Qed.
+
+Lemma solve_proper_flip {A} (R : relation A) `{!PreOrder R} (f : A → A) :
+  Proper (R ==> R) f → Proper (flip R ==> flip R) f.
+Proof. solve_proper. Qed.
+
+(* Test that [solve_proper_finish] uses [eassumption].
+Think of [R] being Iris's [dist]. *)
+Lemma solve_proper_finish_evar {A} (R : nat → relation A) (x y : A) :
+  R 0 x y → ∃ n, R n x y.
+Proof. intros. eexists. solve_proper. Qed.
+
+(** This is a more realistic version of the previous test, showing how such
+goals can arise for real. Needs to involve a subrelation so that the
+[eassumption] in [solve_proper_finish] doesn't already do the whole job, i.e.,
+we need the right mode for [SolveProperSubrelation]. *)
+Lemma solve_proper_finish_evar' {A} (R1 R2 : nat → relation A) (f : A → nat) :
+  (∀ n, subrelation (R2 n) (R1 n)) →
+  (∀ n, Proper (R1 n ==> eq) f) →
+  ∀ n, Proper (R2 n ==> eq) (λ x, S (f x)).
+Proof.
+  intros Hsub Hf. solve_proper_core ltac:(fun _ => eapply Hf || f_equiv).
+Qed.
+
+Definition option_rel {A} (R : relation A) (mx my : option A) :=
+  match mx, my with
+  | Some x, Some y => R x y
+  | None, None => True
+  | _, _ => False
+  end.
+Arguments option_rel : simpl never.
+Lemma solve_proper_convertible {A} (R : relation A) (x y : A) :
+  R x y → (option_rel R) (Some x) (Some y).
+Proof.
+  (* This needs [solve_proper] to use an assumption that doesn't syntactically
+  seem to be about the same variables, but actually up to conversion it exactly
+  matches the goal. *)
+  intros R'. solve_proper.
+Qed.
+
+Section tests.
+  Context {A B : Type} `{!Equiv A, !Equiv B}.
+  Context (foo : A → A) (bar : A → B) (baz : B → A → A).
+  Context `{!Proper ((≡) ==> (≡)) foo,
+            !Proper ((≡) ==> (≡)) bar,
+            !Proper ((≡) ==> (≡) ==> (≡)) baz}.
+
+  Definition test1 (x : A) := baz (bar (foo x)) x.
+  Goal Proper ((≡) ==> (≡)) test1.
+  Proof. solve_proper. Qed.
+
+  Definition test2 (b : bool) (x : A) :=
+    if b then bar (foo x) else bar x.
+  Goal ∀ b, Proper ((≡) ==> (≡)) (test2 b).
+  Proof. solve_proper. Qed.
+
+  Definition test3 (f : nat → A) :=
+    baz (bar (f 0)) (f 2).
+  Goal Proper (pointwise_relation nat (≡) ==> (≡)) test3.
+  Proof. solve_proper. Qed.
+
+  (* We mirror [discrete_fun] from Iris to have an equivalence on a function
+  space. *)
+  Definition discrete_fun {A} (B : A → Type) `{!∀ x, Equiv (B x)} := ∀ x : A, B x.
+  Local Instance discrete_fun_equiv  {A} {B : A → Type} `{!∀ x, Equiv (B x)} :
+      Equiv (discrete_fun B) :=
+    λ f g, ∀ x, f x ≡ g x.
+  Notation "A -d> B" :=
+    (@discrete_fun A (λ _, B) _) (at level 99, B at level 200, right associativity).
+  Definition test4 x (f : A -d> A) := f x.
+  Goal ∀ x, Proper ((≡) ==> (≡)) (test4 x).
+  Proof. solve_proper. Qed.
+
+  Lemma test_subrelation1 (P Q : Prop) :
+    Proper ((↔) ==> impl) id.
+  Proof. solve_proper. Qed.
+
+End tests.
+
+(** The following tests are inspired by Iris's [ofe] structure (here, simplified
+to just a type an arbitrary relation), and the discrete function space [A -d> B]
+on a Type [A] and OFE [B]. The tests occur when proving [Proper]s for
+higher-order functions, which typically occurs while defining functions using
+Iris's [fixpoint] operator. *)
+Record setoid :=
+  Setoid { setoid_car :> Type; setoid_equiv : relation setoid_car }.
+Arguments setoid_equiv {_} _ _.
+
+Definition myfun (A : Type) (B : setoid) := A → B.
+Definition myfun_equiv {A B} : relation (myfun A B) :=
+  pointwise_relation _ setoid_equiv.
+Definition myfunS (A : Type) (B : setoid) := Setoid (myfun A B) myfun_equiv.
+
+Section setoid_tests.
+  Context {A : setoid} (f : A → A) (h : A → A → A).
+  Context `{!Proper (setoid_equiv ==> setoid_equiv) f,
+            !Proper (setoid_equiv ==> setoid_equiv ==> setoid_equiv) h}.
+
+  Definition setoid_test1 (rec : myfunS nat A) : myfunS nat A :=
+    λ n, h (f (rec n)) (rec n).
+  Goal Proper (setoid_equiv ==> setoid_equiv) setoid_test1.
+  Proof. solve_proper. Qed.
+
+  Definition setoid_test2 (rec : myfunS nat (myfunS nat A)) : myfunS nat A :=
+    λ n, h (f (rec n n)) (rec n n).
+  Goal Proper (setoid_equiv ==> setoid_equiv) setoid_test2.
+  Proof. solve_proper. Qed.
+
+  Definition setoid_test3 (rec : myfunS nat A) : myfunS nat (myfunS nat A) :=
+    λ n m, h (f (rec n)) (rec m).
+  Goal Proper (setoid_equiv ==> setoid_equiv) setoid_test3.
+  Proof. solve_proper. Qed.
+End setoid_tests.
+
+(** Regression tests for [naive_solver].
+Requires a bunch of other tactics to work so it comes last in this file. *)
+Lemma naive_solver_issue_115 (P : nat → Prop) (x : nat) :
+  (∀ x', P x' → x' = 10) → P x → x + 1 = 11.
+Proof. naive_solver. Qed.

tests/tactics_more.v

+From stdpp Require Import tactics option.
+
+(** Make sure that [done] is not called recursively when solving [is_Some],
+which might leave an unresolved evar before performing ex falso. *)
+Goal False → is_Some (@None nat).
+Proof. done. Qed.
+Goal ∀ mx, mx = Some 10 → is_Some mx.
+Proof. done. Qed.
+Goal ∀ mx, Some 10 = mx → is_Some mx.
+Proof. done. Qed.

tests/telescopes.ref

-1 subgoal
+1 goal
   
   X : tele
   α, β, γ1, γ2 : X → Prop
   ============================
   accessor α β γ1 → accessor α β (λ.. x : X, γ1 x ∨ γ2 x)
-1 subgoal
+1 goal
   
   X : tele
   α, β, γ1, γ2 : X → Prop
   ============================
   ∀.. x : X, γ1 x → (λ.. x0 : X, γ1 x0 ∨ γ2 x0) x
-1 subgoal
+1 goal
   
   X : tele
   α, β, γ1, γ2 : X → Prop
@@ -18,3 +18,5 @@
   Hγ : γ1 x
   ============================
   γ1 x ∨ γ2 x
+[TEST x y : nat, x = y]
+     : Prop

tests/telescopes.v

 From stdpp Require Import tactics telescopes.
 
+Local Unset Mangle Names. (* for stable goal printing *)
+
+Section universes.
+(** This test would fail without [Unset Universe Minimization ToSet] in [telescopes.v]. *)
+Lemma texist_exist_universes (X : Type) (P : TeleS (λ _ : X, TeleO) → Prop) :
+  texist P ↔ ex P.
+Proof. by rewrite texist_exist. Qed.
+
+(** [tele_arg t] should live at the same universe
+as the types inside of [t] because [tele_arg t]
+is essentially just a (dependent) product.
+ *)
+Definition no_bump@{u} (t : tele@{u}) : Type@{u} := tele_arg@{u} t.
+
+(* Assert that telescopes are cumulatively universe polymorphic.
+   See https://gitlab.mpi-sws.org/iris/iris/-/issues/461
+ *)
+Section cumulativity.
+Monomorphic Universes Quant local.
+Monomorphic Constraint local < Quant.
+Example cumul (t : tele@{local}) : tele@{Quant} := t.
+End cumulativity.
+End universes.
+
 Section accessor.
 (* This is like Iris' accessors, but in Prop.  Just to play with telescopes. *)
 Definition accessor {X : tele} (α β γ : X → Prop) : Prop :=
@@ -28,3 +52,41 @@ Proof.
   left. done.
 Qed.
 End tests.
+End accessor.
+
+(* Type inference for tele_app-based notation.
+(Relies on [&] bidirectionality hint of tele_app.) *)
+Definition test {TT : tele} (t : TT → Prop) : Prop :=
+  ∀.. x, t x ∧ t x.
+Notation "'[TEST'  x .. z ,  P ']'" :=
+  (test (TT:=(TeleS (fun x => .. (TeleS (fun z => TeleO)) ..)))
+        (tele_app (λ x, .. (λ z, P) ..)))
+  (x binder, z binder).
+Check [TEST (x y : nat), x = y].
+
+(** [tele_arg ..] notation tests.
+    These tests mainly test type annotations and casts in the [tele_arg]
+    notations.
+    We test that Coq can typecheck literal telescope arguments in two ways:
+    - tactic unification/old unification using [exact]
+    - evarconv/new unification using [refine]
+ *)
+Example tele_arg_notation_0 : [tele].
+assert_succeeds exact [tele_arg].
+assert_succeeds refine [tele_arg].
+Abort.
+
+Example tele_arg_notation_1 : [tele (_:nat)].
+assert_succeeds exact [tele_arg 0].
+assert_succeeds refine [tele_arg 0].
+Abort.
+
+Example tele_arg_notation_2 : [tele (_ : bool) (_ : nat)].
+assert_succeeds exact [tele_arg true; 0].
+assert_succeeds refine [tele_arg true; 0].
+Abort.
+
+Example tele_arg_notation_2_dep : [tele (b : bool) (_ : if b then nat else False)].
+assert_succeeds exact [tele_arg true; 0].
+assert_succeeds refine [tele_arg true; 0].
+Abort.

tests/typeclasses.ref

+"tc_simpl_test"
+     : string
+1 goal
+  
+  P : nat → Prop
+  y : nat
+  ============================
+  P (S (S (S (S (S (S y))))))

tests/typeclasses.v

-From stdpp Require Import prelude.
+From stdpp Require Import strings.
+
+Lemma tc_simpl_test_lemma (P : nat → Prop) x y :
+  TCSimpl x y →
+  P x → P y.
+Proof. by intros ->%TCSimpl_eq. Qed.
+
+Check "tc_simpl_test".
+Lemma tc_simpl_test (P : nat → Prop) y : P (5 + S y).
+Proof.
+  apply (tc_simpl_test_lemma _ _ _ _). (* would be nicer with ssr [apply:] *)
+  Show.
+Abort.
 
 (** Check that [@Reflexive Prop ?r] picks the instance setoid_rewrite needs.
     Really, we want to set [Hint Mode Reflexive] in a way that this fails, but

tests/universes.ref

+gmap Z Z : Set
+     : Set
+gset Z : Set
+     : Set

tests/universes.v

+From stdpp Require Import gmap.
+
+(** Make sure that [gmap] and [gset] do not bump the universe. Since [Z : Set],
+the types [gmap Z Z] and [gset Z] should have universe [Set] too. *)
+
+Check (gmap Z Z : Set).
+Check (gset Z : Set).

theories/fin_map_dom.v

-(** This file provides an axiomatization of the domain function of finite
-maps. We provide such an axiomatization, instead of implementing the domain
-function in a generic way, to allow more efficient implementations. *)
-From stdpp Require Export sets fin_maps.
-Set Default Proof Using "Type*".
-
-Class FinMapDom K M D `{∀ A, Dom (M A) D, FMap M,
-    ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, PartialAlter K A (M A),
-    OMap M, Merge M, ∀ A, FinMapToList K A (M A), EqDecision K,
-    ElemOf K D, Empty D, Singleton K D,
-    Union D, Intersection D, Difference D} := {
-  finmap_dom_map :> FinMap K M;
-  finmap_dom_set :> Set_ K D;
-  elem_of_dom {A} (m : M A) i : i ∈ dom D m ↔ is_Some (m !! i)
-}.
-
-Section fin_map_dom.
-Context `{FinMapDom K M D}.
-
-Lemma lookup_lookup_total_dom `{!Inhabited A} (m : M A) i :
-  i ∈ dom D m → m !! i = Some (m !!! i).
-Proof. rewrite elem_of_dom. apply lookup_lookup_total. Qed.
-
-Lemma dom_map_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) X :
-  (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) →
-  dom D (filter P m) ≡ X.
-Proof.
-  intros HX i. rewrite elem_of_dom, HX.
-  unfold is_Some. by setoid_rewrite map_filter_lookup_Some.
-Qed.
-Lemma dom_map_filter_subseteq {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A):
-  dom D (filter P m) ⊆ dom D m.
-Proof.
-  intros ?. rewrite 2!elem_of_dom.
-  destruct 1 as [?[Eq _]%map_filter_lookup_Some]. by eexists.
-Qed.
-
-Lemma elem_of_dom_2 {A} (m : M A) i x : m !! i = Some x → i ∈ dom D m.
-Proof. rewrite elem_of_dom; eauto. Qed.
-Lemma not_elem_of_dom {A} (m : M A) i : i ∉ dom D m ↔ m !! i = None.
-Proof. by rewrite elem_of_dom, eq_None_not_Some. Qed.
-Lemma subseteq_dom {A} (m1 m2 : M A) : m1 ⊆ m2 → dom D m1 ⊆ dom D m2.
-Proof.
-  rewrite map_subseteq_spec.
-  intros ??. rewrite !elem_of_dom. inversion 1; eauto.
-Qed.
-Lemma subset_dom {A} (m1 m2 : M A) : m1 ⊂ m2 → dom D m1 ⊂ dom D m2.
-Proof.
-  intros [Hss1 Hss2]; split; [by apply subseteq_dom |].
-  contradict Hss2. rewrite map_subseteq_spec. intros i x Hi.
-  specialize (Hss2 i). rewrite !elem_of_dom in Hss2.
-  destruct Hss2; eauto. by simplify_map_eq.
-Qed.
-Lemma dom_empty {A} : dom D (@empty (M A) _) ≡ ∅.
-Proof.
-  intros x. rewrite elem_of_dom, lookup_empty, <-not_eq_None_Some. set_solver.
-Qed.
-Lemma dom_empty_inv {A} (m : M A) : dom D m ≡ ∅ → m = ∅.
-Proof.
-  intros E. apply map_empty. intros. apply not_elem_of_dom.
-  rewrite E. set_solver.
-Qed.
-Lemma dom_alter {A} f (m : M A) i : dom D (alter f i m) ≡ dom D m.
-Proof.
-  apply elem_of_equiv; intros j; rewrite !elem_of_dom; unfold is_Some.
-  destruct (decide (i = j)); simplify_map_eq/=; eauto.
-  destruct (m !! j); naive_solver.
-Qed.
-Lemma dom_insert {A} (m : M A) i x : dom D (<[i:=x]>m) ≡ {[ i ]} ∪ dom D m.
-Proof.
-  apply elem_of_equiv. intros j. rewrite elem_of_union, !elem_of_dom.
-  unfold is_Some. setoid_rewrite lookup_insert_Some.
-  destruct (decide (i = j)); set_solver.
-Qed.
-Lemma dom_insert_subseteq {A} (m : M A) i x : dom D m ⊆ dom D (<[i:=x]>m).
-Proof. rewrite (dom_insert _). set_solver. Qed.
-Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :
-  X ⊆ dom D m → X ⊆ dom D (<[i:=x]>m).
-Proof. intros. trans (dom D m); eauto using dom_insert_subseteq. Qed.
-Lemma dom_singleton {A} (i : K) (x : A) : dom D ({[i := x]} : M A) ≡ {[ i ]}.
-Proof. rewrite <-insert_empty, dom_insert, dom_empty; set_solver. Qed.
-Lemma dom_delete {A} (m : M A) i : dom D (delete i m) ≡ dom D m ∖ {[ i ]}.
-Proof.
-  apply elem_of_equiv. intros j. rewrite elem_of_difference, !elem_of_dom.
-  unfold is_Some. setoid_rewrite lookup_delete_Some. set_solver.
-Qed.
-Lemma delete_partial_alter_dom {A} (m : M A) i f :
-  i ∉ dom D m → delete i (partial_alter f i m) = m.
-Proof. rewrite not_elem_of_dom. apply delete_partial_alter. Qed.
-Lemma delete_insert_dom {A} (m : M A) i x :
-  i ∉ dom D m → delete i (<[i:=x]>m) = m.
-Proof. rewrite not_elem_of_dom. apply delete_insert. Qed.
-Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ##ₘ m2 ↔ dom D m1 ## dom D m2.
-Proof.
-  rewrite map_disjoint_spec, elem_of_disjoint.
-  setoid_rewrite elem_of_dom. unfold is_Some. naive_solver.
-Qed.
-Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 ##ₘ m2 → dom D m1 ## dom D m2.
-Proof. apply map_disjoint_dom. Qed.
-Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom D m1 ## dom D m2 → m1 ##ₘ m2.
-Proof. apply map_disjoint_dom. Qed.
-Lemma dom_union {A} (m1 m2 : M A) : dom D (m1 ∪ m2) ≡ dom D m1 ∪ dom D m2.
-Proof.
-  apply elem_of_equiv. intros i. rewrite elem_of_union, !elem_of_dom.
-  unfold is_Some. setoid_rewrite lookup_union_Some_raw.
-  destruct (m1 !! i); naive_solver.
-Qed.
-Lemma dom_intersection {A} (m1 m2: M A) : dom D (m1 ∩ m2) ≡ dom D m1 ∩ dom D m2.
-Proof.
-  apply elem_of_equiv. intros i. rewrite elem_of_intersection, !elem_of_dom.
-  unfold is_Some. setoid_rewrite lookup_intersection_Some. naive_solver.
-Qed.
-Lemma dom_difference {A} (m1 m2 : M A) : dom D (m1 ∖ m2) ≡ dom D m1 ∖ dom D m2.
-Proof.
-  apply elem_of_equiv. intros i. rewrite elem_of_difference, !elem_of_dom.
-  unfold is_Some. setoid_rewrite lookup_difference_Some.
-  destruct (m2 !! i); naive_solver.
-Qed.
-Lemma dom_fmap {A B} (f : A → B) (m : M A) : dom D (f <$> m) ≡ dom D m.
-Proof.
-  apply elem_of_equiv. intros i.
-  rewrite !elem_of_dom, lookup_fmap, <-!not_eq_None_Some.
-  destruct (m !! i); naive_solver.
-Qed.
-Lemma dom_finite {A} (m : M A) : set_finite (dom D m).
-Proof.
-  induction m using map_ind; rewrite ?dom_empty, ?dom_insert;
-    eauto using (empty_finite (C:=D)), (union_finite (C:=D)),
-    (singleton_finite (C:=D)).
-Qed.
-Global Instance dom_proper `{!Equiv A} : Proper ((≡@{M A}) ==> (≡)) (dom D).
-Proof.
-  intros m1 m2 EQm. apply elem_of_equiv. intros i.
-  rewrite !elem_of_dom, EQm. done.
-Qed.
-(** If [D] has Leibniz equality, we can show an even stronger result.  This is a
-common case e.g. when having a [gmap K A] where the key [K] has Leibniz equality
-(and thus also [gset K], the usual domain) but the value type [A] does not. *)
-Global Instance dom_proper_L `{!Equiv A, !LeibnizEquiv D} :
-  Proper ((≡@{M A}) ==> (=)) (dom D) | 0.
-Proof. intros ???. unfold_leibniz. by apply dom_proper. Qed.
-
-Section leibniz.
-  Context `{!LeibnizEquiv D}.
-  Lemma dom_map_filter_L {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) X :
-    (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) →
-    dom D (filter P m) = X.
-  Proof. unfold_leibniz. apply dom_map_filter. Qed.
-  Lemma dom_empty_L {A} : dom D (@empty (M A) _) = ∅.
-  Proof. unfold_leibniz; apply dom_empty. Qed.
-  Lemma dom_empty_inv_L {A} (m : M A) : dom D m = ∅ → m = ∅.
-  Proof. by intros; apply dom_empty_inv; unfold_leibniz. Qed.
-  Lemma dom_alter_L {A} f (m : M A) i : dom D (alter f i m) = dom D m.
-  Proof. unfold_leibniz; apply dom_alter. Qed.
-  Lemma dom_insert_L {A} (m : M A) i x : dom D (<[i:=x]>m) = {[ i ]} ∪ dom D m.
-  Proof. unfold_leibniz; apply dom_insert. Qed.
-  Lemma dom_singleton_L {A} (i : K) (x : A) : dom D ({[i := x]} : M A) = {[ i ]}.
-  Proof. unfold_leibniz; apply dom_singleton. Qed.
-  Lemma dom_delete_L {A} (m : M A) i : dom D (delete i m) = dom D m ∖ {[ i ]}.
-  Proof. unfold_leibniz; apply dom_delete. Qed.
-  Lemma dom_union_L {A} (m1 m2 : M A) : dom D (m1 ∪ m2) = dom D m1 ∪ dom D m2.
-  Proof. unfold_leibniz; apply dom_union. Qed.
-  Lemma dom_intersection_L {A} (m1 m2 : M A) :
-    dom D (m1 ∩ m2) = dom D m1 ∩ dom D m2.
-  Proof. unfold_leibniz; apply dom_intersection. Qed.
-  Lemma dom_difference_L {A} (m1 m2 : M A) : dom D (m1 ∖ m2) = dom D m1 ∖ dom D m2.
-  Proof. unfold_leibniz; apply dom_difference. Qed.
-  Lemma dom_fmap_L {A B} (f : A → B) (m : M A) : dom D (f <$> m) = dom D m.
-  Proof. unfold_leibniz; apply dom_fmap. Qed.
-End leibniz.
-
-(** * Set solver instances *)
-Global Instance set_unfold_dom_empty {A} i : SetUnfoldElemOf i (dom D (∅:M A)) False.
-Proof. constructor. by rewrite dom_empty, elem_of_empty. Qed.
-Global Instance set_unfold_dom_alter {A} f i j (m : M A) Q :
-  SetUnfoldElemOf i (dom D m) Q →
-  SetUnfoldElemOf i (dom D (alter f j m)) Q.
-Proof. constructor. by rewrite dom_alter, (set_unfold_elem_of _ (dom _ _) _). Qed.
-Global Instance set_unfold_dom_insert {A} i j x (m : M A) Q :
-  SetUnfoldElemOf i (dom D m) Q →
-  SetUnfoldElemOf i (dom D (<[j:=x]> m)) (i = j ∨ Q).
-Proof.
-  constructor. by rewrite dom_insert, elem_of_union,
-    (set_unfold_elem_of _ (dom _ _) _), elem_of_singleton.
-Qed.
-Global Instance set_unfold_dom_delete {A} i j (m : M A) Q :
-  SetUnfoldElemOf i (dom D m) Q →
-  SetUnfoldElemOf i (dom D (delete j m)) (Q ∧ i ≠ j).
-Proof.
-  constructor. by rewrite dom_delete, elem_of_difference,
-    (set_unfold_elem_of _ (dom _ _) _), elem_of_singleton.
-Qed.
-Global Instance set_unfold_dom_singleton {A} i j :
-  SetUnfoldElemOf i (dom D ({[ j := x ]} : M A)) (i = j).
-Proof. constructor. by rewrite dom_singleton, elem_of_singleton. Qed.
-Global Instance set_unfold_dom_union {A} i (m1 m2 : M A) Q1 Q2 :
-  SetUnfoldElemOf i (dom D m1) Q1 → SetUnfoldElemOf i (dom D m2) Q2 →
-  SetUnfoldElemOf i (dom D (m1 ∪ m2)) (Q1 ∨ Q2).
-Proof.
-  constructor. by rewrite dom_union, elem_of_union,
-    !(set_unfold_elem_of _ (dom _ _) _).
-Qed.
-Global Instance set_unfold_dom_intersection {A} i (m1 m2 : M A) Q1 Q2 :
-  SetUnfoldElemOf i (dom D m1) Q1 → SetUnfoldElemOf i (dom D m2) Q2 →
-  SetUnfoldElemOf i (dom D (m1 ∩ m2)) (Q1 ∧ Q2).
-Proof.
-  constructor. by rewrite dom_intersection, elem_of_intersection,
-    !(set_unfold_elem_of _ (dom _ _) _).
-Qed.
-Global Instance set_unfold_dom_difference {A} i (m1 m2 : M A) Q1 Q2 :
-  SetUnfoldElemOf i (dom D m1) Q1 → SetUnfoldElemOf i (dom D m2) Q2 →
-  SetUnfoldElemOf i (dom D (m1 ∖ m2)) (Q1 ∧ ¬Q2).
-Proof.
-  constructor. by rewrite dom_difference, elem_of_difference,
-    !(set_unfold_elem_of _ (dom _ _) _).
-Qed.
-Global Instance set_unfold_dom_fmap {A B} (f : A → B) i (m : M A) Q :
-  SetUnfoldElemOf i (dom D m) Q →
-  SetUnfoldElemOf i (dom D (f <$> m)) Q.
-Proof. constructor. by rewrite dom_fmap, (set_unfold_elem_of _ (dom _ _) _). Qed.
-End fin_map_dom.
-
-Lemma dom_seq `{FinMapDom nat M D} {A} start (xs : list A) :
-  dom D (map_seq start (M:=M A) xs) ≡ set_seq start (length xs).
-Proof.
-  revert start. induction xs as [|x xs IH]; intros start; simpl.
-  - by rewrite dom_empty.
-  - by rewrite dom_insert, IH.
-Qed.
-Lemma dom_seq_L `{FinMapDom nat M D, !LeibnizEquiv D} {A} start (xs : list A) :
-  dom D (map_seq (M:=M A) start xs) = set_seq start (length xs).
-Proof. unfold_leibniz. apply dom_seq. Qed.
-
-Instance set_unfold_dom_seq `{FinMapDom nat M D} {A} start (xs : list A) :
-  SetUnfoldElemOf i (dom D (map_seq start (M:=M A) xs)) (start ≤ i < start + length xs).
-Proof. constructor. by rewrite dom_seq, elem_of_set_seq. Qed.

theories/gmap.v

-(** This file implements finite maps and finite sets with keys of any countable
-type. The implementation is based on [Pmap]s, radix-2 search trees. *)
-From stdpp Require Export countable infinite fin_maps fin_map_dom.
-From stdpp Require Import pmap mapset propset.
-(* Set Default Proof Using "Type". *)
-
-(** * The data structure *)
-(** We pack a [Pmap] together with a proof that ensures that all keys correspond
-to codes of actual elements of the countable type. *)
-Definition gmap_wf K `{Countable K} {A} (m : Pmap A) : Prop :=
-  bool_decide (map_Forall (λ p _, encode (A:=K) <$> decode p = Some p) m).
-Record gmap K `{Countable K} A := GMap {
-  gmap_car : Pmap A;
-  gmap_prf : gmap_wf K gmap_car
-}.
-Arguments GMap {_ _ _ _} _ _ : assert.
-Arguments gmap_car {_ _ _ _} _ : assert.
-Lemma gmap_eq `{Countable K} {A} (m1 m2 : gmap K A) :
-  m1 = m2 ↔ gmap_car m1 = gmap_car m2.
-Proof.
-  split; [by intros ->|intros]. destruct m1, m2; simplify_eq/=.
-  f_equal; apply proof_irrel.
-Qed.
-Instance gmap_eq_eq `{Countable K, EqDecision A} : EqDecision (gmap K A).
-Proof.
- refine (λ m1 m2, cast_if (decide (gmap_car m1 = gmap_car m2)));
-  abstract (by rewrite gmap_eq).
-Defined.
-
-(** * Operations on the data structure *)
-Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) :=
-  λ i '(GMap m _), m !! encode i.
-Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap ∅ I.
-Global Opaque gmap_empty.
-Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A → option A) m i :
-  gmap_wf K m → gmap_wf K (partial_alter f (encode (A:=K) i) m).
-Proof.
-  unfold gmap_wf; rewrite !bool_decide_spec.
-  intros Hm p x. destruct (decide (encode i = p)) as [<-|?].
-  - rewrite decode_encode; eauto.
-  - rewrite lookup_partial_alter_ne by done. by apply Hm.
-Qed.
-
-Instance gmap_partial_alter `{Countable K} {A} :
-    PartialAlter K A (gmap K A) := λ f i '(GMap m Hm),
-  GMap (partial_alter f (encode i) m) (gmap_partial_alter_wf f m i Hm).
-
-Lemma gmap_fmap_wf `{Countable K} {A B} (f : A → B) m :
-  gmap_wf K m → gmap_wf K (f <$> m).
-Proof.
-  unfold gmap_wf; rewrite !bool_decide_spec.
-  intros ? p x. rewrite lookup_fmap, fmap_Some; intros (?&?&?); eauto.
-Qed.
-Instance gmap_fmap `{Countable K} : FMap (gmap K) := λ A B f '(GMap m Hm),
-  GMap (f <$> m) (gmap_fmap_wf f m Hm).
-Lemma gmap_omap_wf `{Countable K} {A B} (f : A → option B) m :
-  gmap_wf K m → gmap_wf K (omap f m).
-Proof.
-  unfold gmap_wf; rewrite !bool_decide_spec.
-  intros ? p x; rewrite lookup_omap, bind_Some; intros (?&?&?); eauto.
-Qed.
-Instance gmap_omap `{Countable K} : OMap (gmap K) := λ A B f '(GMap m Hm),
-  GMap (omap f m) (gmap_omap_wf f m Hm).
-Lemma gmap_merge_wf `{Countable K} {A B C}
-    (f : option A → option B → option C) m1 m2 :
-  let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
-  gmap_wf K m1 → gmap_wf K m2 → gmap_wf K (merge f' m1 m2).
-Proof.
-  intros f'; unfold gmap_wf; rewrite !bool_decide_spec.
-  intros Hm1 Hm2 p z; rewrite lookup_merge by done; intros.
-  destruct (m1 !! _) eqn:?, (m2 !! _) eqn:?; naive_solver.
-Qed.
-Instance gmap_merge `{Countable K} : Merge (gmap K) := λ A B C f '(GMap m1 Hm1) '(GMap m2 Hm2),
-  let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
-  GMap (merge f' m1 m2) (gmap_merge_wf f m1 m2 Hm1 Hm2).
-Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ '(GMap m _),
-  omap (λ '(i, x), (., x) <$> decode i) (map_to_list m).
-
-(** * Instantiation of the finite map interface *)
-Instance gmap_finmap `{Countable K} : FinMap K (gmap K).
-Proof.
-  split.
-  - unfold lookup; intros A [m1 Hm1] [m2 Hm2] Hm.
-    apply gmap_eq, map_eq; intros i; simpl in *.
-    apply bool_decide_unpack in Hm1; apply bool_decide_unpack in Hm2.
-    apply option_eq; intros x; split; intros Hi.
-    + pose proof (Hm1 i x Hi); simpl in *.
-      by destruct (decode i); simplify_eq/=; rewrite <-Hm.
-    + pose proof (Hm2 i x Hi); simpl in *.
-      by destruct (decode i); simplify_eq/=; rewrite Hm.
-  - done.
-  - intros A f [m Hm] i; apply (lookup_partial_alter f m).
-  - intros A f [m Hm] i j Hs; apply (lookup_partial_alter_ne f m).
-    by contradict Hs; apply (inj encode).
-  - intros A B f [m Hm] i; apply (lookup_fmap f m).
-  - intros A [m Hm]; unfold map_to_list; simpl.
-    apply bool_decide_unpack, map_Forall_to_list in Hm; revert Hm.
-    induction (NoDup_map_to_list m) as [|[p x] l Hpx];
-      inversion 1 as [|??? Hm']; simplify_eq/=; [by constructor|].
-    destruct (decode p) as [i|] eqn:?; simplify_eq/=; constructor; eauto.
-    rewrite elem_of_list_omap; intros ([p' x']&?&?); simplify_eq/=.
-    feed pose proof (proj1 (Forall_forall _ _) Hm' (p',x')); simpl in *; auto.
-    by destruct (decode p') as [i'|]; simplify_eq/=.
-  - intros A [m Hm] i x; unfold map_to_list, lookup; simpl.
-    apply bool_decide_unpack in Hm; rewrite elem_of_list_omap; split.
-    + intros ([p' x']&Hp'&?); apply elem_of_map_to_list in Hp'.
-      feed pose proof (Hm p' x'); simpl in *; auto.
-      by destruct (decode p') as [i'|] eqn:?; simplify_eq/=.
-    + intros; exists (encode i,x); simpl.
-      by rewrite elem_of_map_to_list, decode_encode.
-  - intros A B f [m Hm] i; apply (lookup_omap f m).
-  - intros A B C f ? [m1 Hm1] [m2 Hm2] i; unfold merge, lookup; simpl.
-    set (f' o1 o2 := match o1, o2 with None,None => None | _, _ => f o1 o2 end).
-    by rewrite lookup_merge by done; destruct (m1 !! _), (m2 !! _).
-Qed.
-
-Program Instance gmap_countable
-    `{Countable K, Countable A} : Countable (gmap K A) := {
-  encode m := encode (map_to_list m : list (K * A));
-  decode p := list_to_map <$> decode p
-}.
-Next Obligation.
-  intros K ?? A ?? m; simpl. rewrite decode_encode; simpl.
-  by rewrite list_to_map_to_list.
-Qed.
-
-(** * Curry and uncurry *)
-Definition gmap_curry `{Countable K1, Countable K2} {A} :
-    gmap K1 (gmap K2 A) → gmap (K1 * K2) A :=
-  map_fold (λ i1 m' macc,
-    map_fold (λ i2 x, <[(i1,i2):=x]>) macc m') ∅.
-Definition gmap_uncurry `{Countable K1, Countable K2} {A} :
-    gmap (K1 * K2) A → gmap K1 (gmap K2 A) :=
-  map_fold (λ '(i1, i2) x,
-    partial_alter (Some ∘ <[i2:=x]> ∘ default ∅) i1) ∅.
-
-Section curry_uncurry.
-  Context `{Countable K1, Countable K2} {A : Type}.
-
-  (* FIXME: the type annotations `option (gmap K2 A)` are silly. Maybe these are
-  a consequence of Coq bug #5735 *)
-  Lemma lookup_gmap_curry (m : gmap K1 (gmap K2 A)) i j :
-    gmap_curry m !! (i,j) = (m !! i : option (gmap K2 A)) ≫= (.!! j).
-  Proof.
-    apply (map_fold_ind (λ mr m, mr !! (i,j) = m !! i ≫= (.!! j))).
-    { by rewrite !lookup_empty. }
-    clear m; intros i' m2 m m12 Hi' IH.
-    apply (map_fold_ind (λ m2r m2, m2r !! (i,j) = <[i':=m2]> m !! i ≫= (.!! j))).
-    { rewrite IH. destruct (decide (i' = i)) as [->|].
-      - rewrite lookup_insert, Hi'; simpl; by rewrite lookup_empty.
-      - by rewrite lookup_insert_ne by done. }
-    intros j' y m2' m12' Hj' IH'. destruct (decide (i = i')) as [->|].
-    - rewrite lookup_insert; simpl. destruct (decide (j = j')) as [->|].
-      + by rewrite !lookup_insert.
-      + by rewrite !lookup_insert_ne, IH', lookup_insert by congruence.
-    - by rewrite !lookup_insert_ne, IH', lookup_insert_ne by congruence.
-  Qed.
-
-  Lemma lookup_gmap_uncurry (m : gmap (K1 * K2) A) i j :
-    (gmap_uncurry m !! i : option (gmap K2 A)) ≫= (.!! j) = m !! (i, j).
-  Proof.
-    apply (map_fold_ind (λ mr m, mr !! i ≫= (.!! j) = m !! (i, j))).
-    { by rewrite !lookup_empty. }
-    clear m; intros [i' j'] x m12 mr Hij' IH.
-    destruct (decide (i = i')) as [->|].
-    - rewrite lookup_partial_alter. destruct (decide (j = j')) as [->|].
-      + destruct (mr !! i'); simpl; by rewrite !lookup_insert.
-      + destruct (mr !! i'); simpl; by rewrite !lookup_insert_ne by congruence.
-    - by rewrite lookup_partial_alter_ne, lookup_insert_ne by congruence.
-  Qed.
-
-  Lemma lookup_gmap_uncurry_None (m : gmap (K1 * K2) A) i :
-    gmap_uncurry m !! i = None ↔ (∀ j, m !! (i, j) = None).
-  Proof.
-    apply (map_fold_ind (λ mr m, mr !! i = None ↔ (∀ j, m !! (i, j) = None)));
-      [done|].
-    clear m; intros [i' j'] x m12 mr Hij' IH.
-    destruct (decide (i = i')) as [->|].
-    - split; [by rewrite lookup_partial_alter|].
-      intros Hi. specialize (Hi j'). by rewrite lookup_insert in Hi.
-    - rewrite lookup_partial_alter_ne, IH; [|done]. apply forall_proper.
-      intros j. rewrite lookup_insert_ne; [done|congruence].
-  Qed.
-
-  Lemma gmap_curry_uncurry (m : gmap (K1 * K2) A) :
-    gmap_curry (gmap_uncurry m) = m.
-  Proof.
-   apply map_eq; intros [i j]. by rewrite lookup_gmap_curry, lookup_gmap_uncurry.
-  Qed.
-
-  Lemma gmap_uncurry_non_empty (m : gmap (K1 * K2) A) i x :
-    gmap_uncurry m !! i = Some x → x ≠ ∅.
-  Proof.
-    intros Hm ->. eapply eq_None_not_Some; [|by eexists].
-    eapply lookup_gmap_uncurry_None; intros j.
-    by rewrite <-lookup_gmap_uncurry, Hm.
-  Qed.
-
-  Lemma gmap_uncurry_curry_non_empty (m : gmap K1 (gmap K2 A)) :
-    (∀ i x, m !! i = Some x → x ≠ ∅) →
-    gmap_uncurry (gmap_curry m) = m.
-  Proof.
-    intros Hne. apply map_eq; intros i. destruct (m !! i) as [m2|] eqn:Hm.
-    - destruct (gmap_uncurry (gmap_curry m) !! i) as [m2'|] eqn:Hcurry.
-      + f_equal. apply map_eq. intros j.
-        trans ((gmap_uncurry (gmap_curry m) !! i : option (gmap _ _)) ≫= (.!! j)).
-        { by rewrite Hcurry. }
-        by rewrite lookup_gmap_uncurry, lookup_gmap_curry, Hm.
-      + rewrite lookup_gmap_uncurry_None in Hcurry.
-        exfalso; apply (Hne i m2), map_eq; [done|intros j].
-        by rewrite lookup_empty, <-(Hcurry j), lookup_gmap_curry, Hm.
-   - apply lookup_gmap_uncurry_None; intros j. by rewrite lookup_gmap_curry, Hm.
-  Qed.
-End curry_uncurry.
-
-(** * Finite sets *)
-Definition gset K `{Countable K} := mapset (gmap K).
-
-Section gset.
-  Context `{Countable K}.
-  Global Instance gset_elem_of: ElemOf K (gset K) := _.
-  Global Instance gset_empty : Empty (gset K) := _.
-  Global Instance gset_singleton : Singleton K (gset K) := _.
-  Global Instance gset_union: Union (gset K) := _.
-  Global Instance gset_intersection: Intersection (gset K) := _.
-  Global Instance gset_difference: Difference (gset K) := _.
-  Global Instance gset_elements: Elements K (gset K) := _.
-  Global Instance gset_leibniz : LeibnizEquiv (gset K) := _.
-  Global Instance gset_semi_set : SemiSet K (gset K) | 1 := _.
-  Global Instance gset_set : Set_ K (gset K) | 1 := _.
-  Global Instance gset_fin_set : FinSet K (gset K) := _.
-  Global Instance gset_eq_dec : EqDecision (gset K) := _.
-  Global Instance gset_countable : Countable (gset K) := _.
-  Global Instance gset_equiv_dec : RelDecision (≡@{gset K}) | 1 := _.
-  Global Instance gset_elem_of_dec : RelDecision (∈@{gset K}) | 1 := _.
-  Global Instance gset_disjoint_dec : RelDecision (##@{gset K}) := _.
-  Global Instance gset_subseteq_dec : RelDecision (⊆@{gset K}) := _.
-  Global Instance gset_dom {A} : Dom (gmap K A) (gset K) := mapset_dom.
-  Global Instance gset_dom_spec : FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
-
-  Definition gset_to_gmap {A} (x : A) (X : gset K) : gmap K A :=
-    (λ _, x) <$> mapset_car X.
-
-  Lemma lookup_gset_to_gmap {A} (x : A) (X : gset K) i :
-    gset_to_gmap x X !! i = guard (i ∈ X); Some x.
-  Proof.
-    destruct X as [X].
-    unfold gset_to_gmap, gset_elem_of, elem_of, mapset_elem_of; simpl.
-    rewrite lookup_fmap.
-    case_option_guard; destruct (X !! i) as [[]|]; naive_solver.
-  Qed.
-  Lemma lookup_gset_to_gmap_Some {A} (x : A) (X : gset K) i y :
-    gset_to_gmap x X !! i = Some y ↔ i ∈ X ∧ x = y.
-  Proof. rewrite lookup_gset_to_gmap. simplify_option_eq; naive_solver. Qed.
-  Lemma lookup_gset_to_gmap_None {A} (x : A) (X : gset K) i :
-    gset_to_gmap x X !! i = None ↔ i ∉ X.
-  Proof. rewrite lookup_gset_to_gmap. simplify_option_eq; naive_solver. Qed.
-
-  Lemma gset_to_gmap_empty {A} (x : A) : gset_to_gmap x ∅ = ∅.
-  Proof. apply fmap_empty. Qed.
-  Lemma gset_to_gmap_union_singleton {A} (x : A) i Y :
-    gset_to_gmap x ({[ i ]} ∪ Y) = <[i:=x]>(gset_to_gmap x Y).
-  Proof.
-    apply map_eq; intros j; apply option_eq; intros y.
-    rewrite lookup_insert_Some, !lookup_gset_to_gmap_Some, elem_of_union,
-      elem_of_singleton; destruct (decide (i = j)); intuition.
-  Qed.
-
-  Lemma fmap_gset_to_gmap {A B} (f : A → B) (X : gset K) (x : A) :
-    f <$> gset_to_gmap x X = gset_to_gmap (f x) X.
-  Proof.
-    apply map_eq; intros j. rewrite lookup_fmap, !lookup_gset_to_gmap.
-    by simplify_option_eq.
-  Qed.
-  Lemma gset_to_gmap_dom {A B} (m : gmap K A) (y : B) :
-    gset_to_gmap y (dom _ m) = const y <$> m.
-  Proof.
-    apply map_eq; intros j. rewrite lookup_fmap, lookup_gset_to_gmap.
-    destruct (m !! j) as [x|] eqn:?.
-    - by rewrite option_guard_True by (rewrite elem_of_dom; eauto).
-    - by rewrite option_guard_False by (rewrite not_elem_of_dom; eauto).
-  Qed.
-  Lemma dom_gset_to_gmap {A} (X : gset K) (x : A) :
-    dom _ (gset_to_gmap x X) = X.
-  Proof.
-    induction X as [| y X not_in IH] using set_ind_L.
-    - rewrite gset_to_gmap_empty, dom_empty_L; done.
-    - rewrite gset_to_gmap_union_singleton, dom_insert_L, IH; done.
-  Qed.
-End gset.
-
-Typeclasses Opaque gset.

theories/gmultiset.v

-From stdpp Require Import gmap.
-Set Default Proof Using "Type".
-
-Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }.
-Arguments GMultiSet {_ _ _} _ : assert.
-Arguments gmultiset_car {_ _ _} _ : assert.
-
-Instance gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
-Proof. solve_decision. Defined.
-
-Program Instance gmultiset_countable `{Countable A} :
-    Countable (gmultiset A) := {|
-  encode X := encode (gmultiset_car X); decode p := GMultiSet <$> decode p
-|}.
-Next Obligation. intros A ?? [X]; simpl. by rewrite decode_encode. Qed.
-
-Section definitions.
-  Context `{Countable A}.
-
-  Definition multiplicity (x : A) (X : gmultiset A) : nat :=
-    match gmultiset_car X !! x with Some n => S n | None => 0 end.
-  Global Instance gmultiset_elem_of : ElemOf A (gmultiset A) := λ x X,
-    0 < multiplicity x X.
-  Global Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y, ∀ x,
-    multiplicity x X ≤ multiplicity x Y.
-  Global Instance gmultiset_equiv : Equiv (gmultiset A) := λ X Y, ∀ x,
-    multiplicity x X = multiplicity x Y.
-
-  Global Instance gmultiset_elements : Elements A (gmultiset A) := λ X,
-    let (X) := X in ''(x,n) ← map_to_list X; replicate (S n) x.
-  Global Instance gmultiset_size : Size (gmultiset A) := length ∘ elements.
-
-  Global Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet ∅.
-  Global Instance gmultiset_singleton : Singleton A (gmultiset A) := λ x,
-    GMultiSet {[ x := 0 ]}.
-  Global Instance gmultiset_union : Union (gmultiset A) := λ X Y,
-    let (X) := X in let (Y) := Y in
-    GMultiSet $ union_with (λ x y, Some (x `max` y)) X Y.
-  Global Instance gmultiset_intersection : Intersection (gmultiset A) := λ X Y,
-    let (X) := X in let (Y) := Y in
-    GMultiSet $ intersection_with (λ x y, Some (x `min` y)) X Y.
-  (** Often called the "sum" *)
-  Global Instance gmultiset_disj_union : DisjUnion (gmultiset A) := λ X Y,
-    let (X) := X in let (Y) := Y in
-    GMultiSet $ union_with (λ x y, Some (S (x + y))) X Y.
-  Global Instance gmultiset_difference : Difference (gmultiset A) := λ X Y,
-    let (X) := X in let (Y) := Y in
-    GMultiSet $ difference_with (λ x y,
-      let z := x - y in guard (0 < z); Some (pred z)) X Y.
-
-  Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
-    let (X) := X in dom _ X.
-End definitions.
-
-Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
-Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
-Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference.
-Typeclasses Opaque gmultiset_dom.
-
-Section lemmas.
-Context `{Countable A}.
-Implicit Types x y : A.
-Implicit Types X Y : gmultiset A.
-
-Lemma gmultiset_eq X Y : X = Y ↔ ∀ x, multiplicity x X = multiplicity x Y.
-Proof.
-  split; [by intros ->|intros HXY].
-  destruct X as [X], Y as [Y]; f_equal; apply map_eq; intros x.
-  specialize (HXY x); unfold multiplicity in *; simpl in *.
-  repeat case_match; naive_solver.
-Qed.
-Global Instance gmultiset_leibniz : LeibnizEquiv (gmultiset A).
-Proof. intros X Y. by rewrite gmultiset_eq. Qed.
-Global Instance gmultiset_equiv_equivalence : Equivalence (≡@{gmultiset A}).
-Proof. constructor; repeat intro; naive_solver. Qed.
-
-(* Multiplicity *)
-Lemma multiplicity_empty x : multiplicity x ∅ = 0.
-Proof. done. Qed.
-Lemma multiplicity_singleton x : multiplicity x {[ x ]} = 1.
-Proof. unfold multiplicity; simpl. by rewrite lookup_singleton. Qed.
-Lemma multiplicity_singleton_ne x y : x ≠ y → multiplicity x {[ y ]} = 0.
-Proof. intros. unfold multiplicity; simpl. by rewrite lookup_singleton_ne. Qed.
-Lemma multiplicity_singleton' x y :
-  multiplicity x {[ y ]} = if decide (x = y) then 1 else 0.
-Proof.
-  destruct (decide _) as [->|].
-  - by rewrite multiplicity_singleton.
-  - by rewrite multiplicity_singleton_ne.
-Qed.
-Lemma multiplicity_union X Y x :
-  multiplicity x (X ∪ Y) = multiplicity x X `max` multiplicity x Y.
-Proof.
-  destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
-  rewrite lookup_union_with. destruct (X !! _), (Y !! _); simpl; lia.
-Qed.
-Lemma multiplicity_intersection X Y x :
-  multiplicity x (X ∩ Y) = multiplicity x X `min` multiplicity x Y.
-Proof.
-  destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
-  rewrite lookup_intersection_with. destruct (X !! _), (Y !! _); simpl; lia.
-Qed.
-Lemma multiplicity_disj_union X Y x :
-  multiplicity x (X ⊎ Y) = multiplicity x X + multiplicity x Y.
-Proof.
-  destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
-  rewrite lookup_union_with. destruct (X !! _), (Y !! _); simpl; lia.
-Qed.
-Lemma multiplicity_difference X Y x :
-  multiplicity x (X ∖ Y) = multiplicity x X - multiplicity x Y.
-Proof.
-  destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
-  rewrite lookup_difference_with.
-  destruct (X !! _), (Y !! _); simplify_option_eq; lia.
-Qed.
-
-(* Set_ *)
-Lemma elem_of_multiplicity x X : x ∈ X ↔ 0 < multiplicity x X.
-Proof. done. Qed.
-
-Global Instance gmultiset_simple_set : SemiSet A (gmultiset A).
-Proof.
-  split.
-  - intros x. rewrite elem_of_multiplicity, multiplicity_empty. lia.
-  - intros x y.
-    rewrite elem_of_multiplicity, multiplicity_singleton'.
-    destruct (decide (x = y)); intuition lia.
-  - intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. lia.
-Qed.
-Global Instance gmultiset_elem_of_dec : RelDecision (∈@{gmultiset A}).
-Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
-
-Lemma gmultiset_elem_of_disj_union X Y x : x ∈ X ⊎ Y ↔ x ∈ X ∨ x ∈ Y.
-Proof. rewrite !elem_of_multiplicity, multiplicity_disj_union. lia. Qed.
-
-Global Instance set_unfold_gmultiset_disj_union x X Y P Q :
-  SetUnfoldElemOf x X P → SetUnfoldElemOf x Y Q →
-  SetUnfoldElemOf x (X ⊎ Y) (P ∨ Q).
-Proof.
-  intros ??; constructor. rewrite gmultiset_elem_of_disj_union.
-  by rewrite <-(set_unfold_elem_of x X P), <-(set_unfold_elem_of x Y Q).
-Qed.
-
-(* Algebraic laws *)
-(** For union *)
-Global Instance gmultiset_union_comm : Comm (=@{gmultiset A}) (∪).
-Proof.
-  intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_union; lia.
-Qed.
-Global Instance gmultiset_union_assoc : Assoc (=@{gmultiset A}) (∪).
-Proof.
-  intros X Y Z. apply gmultiset_eq; intros x. rewrite !multiplicity_union; lia.
-Qed.
-Global Instance gmultiset_union_left_id : LeftId (=@{gmultiset A}) ∅ (∪).
-Proof.
-  intros X. apply gmultiset_eq; intros x.
-  by rewrite multiplicity_union, multiplicity_empty.
-Qed.
-Global Instance gmultiset_union_right_id : RightId (=@{gmultiset A}) ∅ (∪).
-Proof. intros X. by rewrite (comm_L (∪)), (left_id_L _ _). Qed.
-Global Instance gmultiset_union_idemp : IdemP (=@{gmultiset A}) (∪).
-Proof.
-  intros X. apply gmultiset_eq; intros x. rewrite !multiplicity_union; lia.
-Qed.
-
-(** For intersection *)
-Global Instance gmultiset_intersection_comm : Comm (=@{gmultiset A}) (∩).
-Proof.
-  intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_intersection; lia.
-Qed.
-Global Instance gmultiset_intersection_assoc : Assoc (=@{gmultiset A}) (∩).
-Proof.
-  intros X Y Z. apply gmultiset_eq; intros x. rewrite !multiplicity_intersection; lia.
-Qed.
-Global Instance gmultiset_intersection_left_absorb : LeftAbsorb (=@{gmultiset A}) ∅ (∩).
-Proof.
-  intros X. apply gmultiset_eq; intros x.
-  by rewrite multiplicity_intersection, multiplicity_empty.
-Qed.
-Global Instance gmultiset_intersection_right_absorb : RightAbsorb (=@{gmultiset A}) ∅ (∩).
-Proof. intros X. by rewrite (comm_L (∩)), (left_absorb_L _ _). Qed.
-Global Instance gmultiset_intersection_idemp : IdemP (=@{gmultiset A}) (∩).
-Proof.
-  intros X. apply gmultiset_eq; intros x. rewrite !multiplicity_intersection; lia.
-Qed.
-
-Lemma gmultiset_union_intersection_l X Y Z : X ∪ (Y ∩ Z) = (X ∪ Y) ∩ (X ∪ Z).
-Proof.
-  apply gmultiset_eq; intros y.
-  rewrite multiplicity_union, !multiplicity_intersection, !multiplicity_union. lia.
-Qed.
-Lemma gmultiset_union_intersection_r X Y Z : (X ∩ Y) ∪ Z = (X ∪ Z) ∩ (Y ∪ Z).
-Proof. by rewrite <-!(comm_L _ Z), gmultiset_union_intersection_l. Qed.
-Lemma gmultiset_intersection_union_l X Y Z : X ∩ (Y ∪ Z) = (X ∩ Y) ∪ (X ∩ Z).
-Proof.
-  apply gmultiset_eq; intros y.
-  rewrite multiplicity_union, !multiplicity_intersection, !multiplicity_union. lia.
-Qed.
-Lemma gmultiset_intersection_union_r X Y Z : (X ∪ Y) ∩ Z = (X ∩ Z) ∪ (Y ∩ Z).
-Proof. by rewrite <-!(comm_L _ Z), gmultiset_intersection_union_l. Qed.
-
-(** For disjoint union (aka sum) *)
-Global Instance gmultiset_disj_union_comm : Comm (=@{gmultiset A}) (⊎).
-Proof.
-  intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_disj_union; lia.
-Qed.
-Global Instance gmultiset_disj_union_assoc : Assoc (=@{gmultiset A}) (⊎).
-Proof.
-  intros X Y Z. apply gmultiset_eq; intros x. rewrite !multiplicity_disj_union; lia.
-Qed.
-Global Instance gmultiset_disj_union_left_id : LeftId (=@{gmultiset A}) ∅ (⊎).
-Proof.
-  intros X. apply gmultiset_eq; intros x.
-  by rewrite multiplicity_disj_union, multiplicity_empty.
-Qed.
-Global Instance gmultiset_disj_union_right_id : RightId (=@{gmultiset A}) ∅ (⊎).
-Proof. intros X. by rewrite (comm_L (⊎)), (left_id_L _ _). Qed.
-
-Global Instance gmultiset_disj_union_inj_1 X : Inj (=) (=) (X ⊎.).
-Proof.
-  intros Y1 Y2. rewrite !gmultiset_eq. intros HX x; generalize (HX x).
-  rewrite !multiplicity_disj_union. lia.
-Qed.
-Global Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) (.⊎ X).
-Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj (X ⊎.)). Qed.
-
-Lemma gmultiset_disj_union_intersection_l X Y Z : X ⊎ (Y ∩ Z) = (X ⊎ Y) ∩ (X ⊎ Z).
-Proof.
-  apply gmultiset_eq; intros y.
-  rewrite multiplicity_disj_union, !multiplicity_intersection,
-    !multiplicity_disj_union. lia.
-Qed.
-Lemma gmultiset_disj_union_intersection_r X Y Z : (X ∩ Y) ⊎ Z = (X ⊎ Z) ∩ (Y ⊎ Z).
-Proof. by rewrite <-!(comm_L _ Z), gmultiset_disj_union_intersection_l. Qed.
-
-Lemma gmultiset_disj_union_union_l X Y Z : X ⊎ (Y ∪ Z) = (X ⊎ Y) ∪ (X ⊎ Z).
-Proof.
-  apply gmultiset_eq; intros y.
-  rewrite multiplicity_disj_union, !multiplicity_union,
-    !multiplicity_disj_union. lia.
-Qed.
-Lemma gmultiset_disj_union_union_r X Y Z : (X ∪ Y) ⊎ Z = (X ⊎ Z) ∪ (Y ⊎ Z).
-Proof. by rewrite <-!(comm_L _ Z), gmultiset_disj_union_union_l. Qed.
-
-(** Misc *)
-Lemma gmultiset_non_empty_singleton x : {[ x ]} ≠@{gmultiset A} ∅.
-Proof.
-  rewrite gmultiset_eq. intros Hx; generalize (Hx x).
-  by rewrite multiplicity_singleton, multiplicity_empty.
-Qed.
-
-(** Conversion from lists *)
-Lemma list_to_set_disj_nil : list_to_set_disj [] =@{gmultiset A} ∅.
-Proof. done. Qed.
-Lemma list_to_set_disj_cons x l :
-  list_to_set_disj (x :: l) =@{gmultiset A} {[ x ]} ⊎ list_to_set_disj l.
-Proof. done. Qed.
-Lemma list_to_set_disj_app l1 l2 :
-  list_to_set_disj (l1 ++ l2) =@{gmultiset A} list_to_set_disj l1 ⊎ list_to_set_disj l2.
-Proof.
-  induction l1 as [|x l1 IH]; simpl.
-  - by rewrite (left_id_L _ _).
-  - by rewrite IH, (assoc_L _).
-Qed.
-Global Instance list_to_set_disj_perm :
-  Proper ((≡ₚ) ==> (=)) (list_to_set_disj (C:=gmultiset A)).
-Proof.
-  induction 1 as [|x l l' _ IH|x y l|l l' l'' _ IH1 _ IH2]; simpl; auto.
-  - by rewrite IH.
-  - by rewrite !(assoc_L _), (comm_L _ {[ x ]}).
-  - by rewrite IH1.
-Qed.
-
-(** Properties of the elements operation *)
-Lemma gmultiset_elements_empty : elements (∅ : gmultiset A) = [].
-Proof.
-  unfold elements, gmultiset_elements; simpl. by rewrite map_to_list_empty.
-Qed.
-Lemma gmultiset_elements_empty_inv X : elements X = [] → X = ∅.
-Proof.
-  destruct X as [X]; unfold elements, gmultiset_elements; simpl.
-  intros; apply (f_equal GMultiSet). destruct (map_to_list X) as [|[]] eqn:?.
-  - by apply map_to_list_empty_inv.
-  - naive_solver.
-Qed.
-Lemma gmultiset_elements_empty' X : elements X = [] ↔ X = ∅.
-Proof.
-  split; intros HX; [by apply gmultiset_elements_empty_inv|].
-  by rewrite HX, gmultiset_elements_empty.
-Qed.
-Lemma gmultiset_elements_singleton x : elements ({[ x ]} : gmultiset A) = [ x ].
-Proof.
-  unfold elements, gmultiset_elements; simpl. by rewrite map_to_list_singleton.
-Qed.
-Lemma gmultiset_elements_disj_union X Y :
-  elements (X ⊎ Y) ≡ₚ elements X ++ elements Y.
-Proof.
-  destruct X as [X], Y as [Y]; unfold elements, gmultiset_elements.
-  set (f xn := let '(x, n) := xn in replicate (S n) x); simpl.
-  revert Y; induction X as [|x n X HX IH] using map_ind; intros Y.
-  { by rewrite (left_id_L _ _ Y), map_to_list_empty. }
-  destruct (Y !! x) as [n'|] eqn:HY.
-  - rewrite <-(insert_id Y x n'), <-(insert_delete Y) by done.
-    erewrite <-insert_union_with by done.
-    rewrite !map_to_list_insert, !bind_cons
-      by (by rewrite ?lookup_union_with, ?lookup_delete, ?HX).
-    rewrite (assoc_L _), <-(comm (++) (f (_,n'))), <-!(assoc_L _), <-IH.
-    rewrite (assoc_L _). f_equiv.
-    rewrite (comm _); simpl. by rewrite replicate_plus, Permutation_middle.
-  - rewrite <-insert_union_with_l, !map_to_list_insert, !bind_cons
-      by (by rewrite ?lookup_union_with, ?HX, ?HY).
-    by rewrite <-(assoc_L (++)), <-IH.
-Qed.
-Lemma gmultiset_elem_of_elements x X : x ∈ elements X ↔ x ∈ X.
-Proof.
-  destruct X as [X]. unfold elements, gmultiset_elements.
-  set (f xn := let '(x, n) := xn in replicate (S n) x); simpl.
-  unfold elem_of at 2, gmultiset_elem_of, multiplicity; simpl.
-  rewrite elem_of_list_bind. split.
-  - intros [[??] [[<- ?]%elem_of_replicate ->%elem_of_map_to_list]]; lia.
-  - intros. destruct (X !! x) as [n|] eqn:Hx; [|lia].
-    exists (x,n); split; [|by apply elem_of_map_to_list].
-    apply elem_of_replicate; auto with lia.
-Qed.
-Lemma gmultiset_elem_of_dom x X : x ∈ dom (gset A) X ↔ x ∈ X.
-Proof.
-  unfold dom, gmultiset_dom, elem_of at 2, gmultiset_elem_of, multiplicity.
-  destruct X as [X]; simpl; rewrite elem_of_dom, <-not_eq_None_Some.
-  destruct (X !! x); naive_solver lia.
-Qed.
-
-(** Properties of the set_fold operation *)
-Lemma gmultiset_set_fold_empty {B} (f : A → B → B) (b : B) :
-  set_fold f b (∅ : gmultiset A) = b.
-Proof. by unfold set_fold; simpl; rewrite gmultiset_elements_empty. Qed.
-Lemma gmultiset_set_fold_singleton {B} (f : A → B → B) (b : B) (a : A) :
-  set_fold f b ({[a]} : gmultiset A) = f a b.
-Proof. by unfold set_fold; simpl; rewrite gmultiset_elements_singleton. Qed.
-Lemma gmultiset_set_fold_disj_union (f : A → A → A) (b : A) X Y :
-  Comm (=) f →
-  Assoc (=) f →
-  set_fold f b (X ⊎ Y) = set_fold f (set_fold f b X) Y.
-Proof.
-  intros Hcomm Hassoc. unfold set_fold; simpl.
-  by rewrite gmultiset_elements_disj_union, <- foldr_app, (comm (++)).
-Qed.
-
-(** Properties of the size operation *)
-Lemma gmultiset_size_empty : size (∅ : gmultiset A) = 0.
-Proof. done. Qed.
-Lemma gmultiset_size_empty_inv X : size X = 0 → X = ∅.
-Proof.
-  unfold size, gmultiset_size; simpl. rewrite length_zero_iff_nil.
-  apply gmultiset_elements_empty_inv.
-Qed.
-Lemma gmultiset_size_empty_iff X : size X = 0 ↔ X = ∅.
-Proof.
-  split; [apply gmultiset_size_empty_inv|].
-  by intros ->; rewrite gmultiset_size_empty.
-Qed.
-Lemma gmultiset_size_non_empty_iff X : size X ≠ 0 ↔ X ≠ ∅.
-Proof. by rewrite gmultiset_size_empty_iff. Qed.
-
-Lemma gmultiset_choose_or_empty X : (∃ x, x ∈ X) ∨ X = ∅.
-Proof.
-  destruct (elements X) as [|x l] eqn:HX; [right|left].
-  - by apply gmultiset_elements_empty_inv.
-  - exists x. rewrite <-gmultiset_elem_of_elements, HX. by left.
-Qed.
-Lemma gmultiset_choose X : X ≠ ∅ → ∃ x, x ∈ X.
-Proof. intros. by destruct (gmultiset_choose_or_empty X). Qed.
-Lemma gmultiset_size_pos_elem_of X : 0 < size X → ∃ x, x ∈ X.
-Proof.
-  intros Hsz. destruct (gmultiset_choose_or_empty X) as [|HX]; [done|].
-  contradict Hsz. rewrite HX, gmultiset_size_empty; lia.
-Qed.
-
-Lemma gmultiset_size_singleton x : size ({[ x ]} : gmultiset A) = 1.
-Proof.
-  unfold size, gmultiset_size; simpl. by rewrite gmultiset_elements_singleton.
-Qed.
-Lemma gmultiset_size_disj_union X Y : size (X ⊎ Y) = size X + size Y.
-Proof.
-  unfold size, gmultiset_size; simpl.
-  by rewrite gmultiset_elements_disj_union, app_length.
-Qed.
-
-(** Order stuff *)
-Global Instance gmultiset_po : PartialOrder (⊆@{gmultiset A}).
-Proof.
-  split; [split|].
-  - by intros X x.
-  - intros X Y Z HXY HYZ x. by trans (multiplicity x Y).
-  - intros X Y HXY HYX; apply gmultiset_eq; intros x. by apply (anti_symm (≤)).
-Qed.
-
-Lemma gmultiset_subseteq_alt X Y :
-  X ⊆ Y ↔
-  map_relation (≤) (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y).
-Proof.
-  apply forall_proper; intros x. unfold multiplicity.
-  destruct (gmultiset_car X !! x), (gmultiset_car Y !! x); naive_solver lia.
-Qed.
-Global Instance gmultiset_subseteq_dec : RelDecision (⊆@{gmultiset A}).
-Proof.
- refine (λ X Y, cast_if (decide (map_relation (≤)
-   (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y))));
-   by rewrite gmultiset_subseteq_alt.
-Defined.
-
-Lemma gmultiset_subset_subseteq X Y : X ⊂ Y → X ⊆ Y.
-Proof. apply strict_include. Qed.
-Hint Resolve gmultiset_subset_subseteq : core.
-
-Lemma gmultiset_empty_subseteq X : ∅ ⊆ X.
-Proof. intros x. rewrite multiplicity_empty. lia. Qed.
-
-Lemma gmultiset_union_subseteq_l X Y : X ⊆ X ∪ Y.
-Proof. intros x. rewrite multiplicity_union. lia. Qed.
-Lemma gmultiset_union_subseteq_r X Y : Y ⊆ X ∪ Y.
-Proof. intros x. rewrite multiplicity_union. lia. Qed.
-Lemma gmultiset_union_mono X1 X2 Y1 Y2 : X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ∪ Y1 ⊆ X2 ∪ Y2.
-Proof.
-  intros HX HY x. rewrite !multiplicity_union.
-  specialize (HX x); specialize (HY x); lia.
-Qed.
-Lemma gmultiset_union_mono_l X Y1 Y2 : Y1 ⊆ Y2 → X ∪ Y1 ⊆ X ∪ Y2.
-Proof. intros. by apply gmultiset_union_mono. Qed.
-Lemma gmultiset_union_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ∪ Y ⊆ X2 ∪ Y.
-Proof. intros. by apply gmultiset_union_mono. Qed.
-
-Lemma gmultiset_disj_union_subseteq_l X Y : X ⊆ X ⊎ Y.
-Proof. intros x. rewrite multiplicity_disj_union. lia. Qed.
-Lemma gmultiset_disj_union_subseteq_r X Y : Y ⊆ X ⊎ Y.
-Proof. intros x. rewrite multiplicity_disj_union. lia. Qed.
-Lemma gmultiset_disj_union_mono X1 X2 Y1 Y2 : X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ⊎ Y1 ⊆ X2 ⊎ Y2.
-Proof. intros ?? x. rewrite !multiplicity_disj_union. by apply Nat.add_le_mono. Qed.
-Lemma gmultiset_disj_union_mono_l X Y1 Y2 : Y1 ⊆ Y2 → X ⊎ Y1 ⊆ X ⊎ Y2.
-Proof. intros. by apply gmultiset_disj_union_mono. Qed.
-Lemma gmultiset_disj_union_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ⊎ Y ⊆ X2 ⊎ Y.
-Proof. intros. by apply gmultiset_disj_union_mono. Qed.
-
-Lemma gmultiset_subset X Y : X ⊆ Y → size X < size Y → X ⊂ Y.
-Proof. intros. apply strict_spec_alt; split; naive_solver auto with lia. Qed.
-Lemma gmultiset_disj_union_subset_l X Y : Y ≠ ∅ → X ⊂ X ⊎ Y.
-Proof.
-  intros HY%gmultiset_size_non_empty_iff.
-  apply gmultiset_subset; auto using gmultiset_disj_union_subseteq_l.
-  rewrite gmultiset_size_disj_union; lia.
-Qed.
-Lemma gmultiset_union_subset_r X Y : X ≠ ∅ → Y ⊂ X ⊎ Y.
-Proof. rewrite (comm_L (⊎)). apply gmultiset_disj_union_subset_l. Qed.
-
-Lemma gmultiset_elem_of_singleton_subseteq x X : x ∈ X ↔ {[ x ]} ⊆ X.
-Proof.
-  rewrite elem_of_multiplicity. split.
-  - intros Hx y. rewrite multiplicity_singleton'.
-    destruct (decide (y = x)); naive_solver lia.
-  - intros Hx. generalize (Hx x). rewrite multiplicity_singleton. lia.
-Qed.
-
-Lemma gmultiset_elem_of_subseteq X1 X2 x : x ∈ X1 → X1 ⊆ X2 → x ∈ X2.
-Proof. rewrite !gmultiset_elem_of_singleton_subseteq. by intros ->. Qed.
-
-Lemma gmultiset_disj_union_difference X Y : X ⊆ Y → Y = X ⊎ Y ∖ X.
-Proof.
-  intros HXY. apply gmultiset_eq; intros x; specialize (HXY x).
-  rewrite multiplicity_disj_union, multiplicity_difference; lia.
-Qed.
-Lemma gmultiset_disj_union_difference' x Y : x ∈ Y → Y = {[ x ]} ⊎ Y ∖ {[ x ]}.
-Proof.
-  intros. by apply gmultiset_disj_union_difference,
-    gmultiset_elem_of_singleton_subseteq.
-Qed.
-
-Lemma gmultiset_size_difference X Y : Y ⊆ X → size (X ∖ Y) = size X - size Y.
-Proof.
-  intros HX%gmultiset_disj_union_difference.
-  rewrite HX at 2; rewrite gmultiset_size_disj_union. lia.
-Qed.
-
-Lemma gmultiset_empty_difference X Y : Y ⊆ X → Y ∖ X = ∅.
-Proof.
-  intros HYX. unfold_leibniz. intros x.
-  rewrite multiplicity_difference, multiplicity_empty.
-  specialize (HYX x). lia.
-Qed.
-
-Lemma gmultiset_non_empty_difference X Y : X ⊂ Y → Y ∖ X ≠ ∅.
-Proof.
-  intros [_ HXY2] Hdiff; destruct HXY2; intros x.
-  generalize (f_equal (multiplicity x) Hdiff).
-  rewrite multiplicity_difference, multiplicity_empty; lia.
-Qed.
-
-Lemma gmultiset_difference_diag X : X ∖ X = ∅.
-Proof. by apply gmultiset_empty_difference. Qed.
-
-Lemma gmultiset_difference_subset X Y : X ≠ ∅ → X ⊆ Y → Y ∖ X ⊂ Y.
-Proof.
-  intros. eapply strict_transitive_l; [by apply gmultiset_union_subset_r|].
-  by rewrite <-(gmultiset_disj_union_difference X Y).
-Qed.
-
-(** Mononicity *)
-Lemma gmultiset_elements_submseteq X Y : X ⊆ Y → elements X ⊆+ elements Y.
-Proof.
-  intros ->%gmultiset_disj_union_difference. rewrite gmultiset_elements_disj_union.
-  by apply submseteq_inserts_r.
-Qed.
-
-Lemma gmultiset_subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
-Proof. intros. by apply submseteq_length, gmultiset_elements_submseteq. Qed.
-
-Lemma gmultiset_subset_size X Y : X ⊂ Y → size X < size Y.
-Proof.
-  intros HXY. assert (size (Y ∖ X) ≠ 0).
-  { by apply gmultiset_size_non_empty_iff, gmultiset_non_empty_difference. }
-  rewrite (gmultiset_disj_union_difference X Y),
-    gmultiset_size_disj_union by auto. lia.
-Qed.
-
-(** Well-foundedness *)
-Lemma gmultiset_wf : wf (⊂@{gmultiset A}).
-Proof.
-  apply (wf_projected (<) size); auto using gmultiset_subset_size, lt_wf.
-Qed.
-
-Lemma gmultiset_ind (P : gmultiset A → Prop) :
-  P ∅ → (∀ x X, P X → P ({[ x ]} ⊎ X)) → ∀ X, P X.
-Proof.
-  intros Hemp Hinsert X. induction (gmultiset_wf X) as [X _ IH].
-  destruct (gmultiset_choose_or_empty X) as [[x Hx]| ->]; auto.
-  rewrite (gmultiset_disj_union_difference' x X) by done.
-  apply Hinsert, IH, gmultiset_difference_subset,
-    gmultiset_elem_of_singleton_subseteq; auto using gmultiset_non_empty_singleton.
-Qed.
-End lemmas.

theories/numbers.v

-(** This file collects some trivial facts on the Coq types [nat] and [N] for
-natural numbers, and the type [Z] for integers. It also declares some useful
-notations. *)
-From Coq Require Export EqdepFacts PArith NArith ZArith NPeano.
-From Coq Require Import QArith Qcanon.
-From stdpp Require Export base decidable option.
-Set Default Proof Using "Type".
-Local Open Scope nat_scope.
-
-Coercion Z.of_nat : nat >-> Z.
-Instance comparison_eq_dec : EqDecision comparison.
-Proof. solve_decision. Defined.
-
-(** * Notations and properties of [nat] *)
-Arguments minus !_ !_ / : assert.
-Arguments Nat.max : simpl nomatch.
-
-Typeclasses Opaque lt.
-
-Reserved Notation "x ≤ y ≤ z" (at level 70, y at next level).
-Reserved Notation "x ≤ y < z" (at level 70, y at next level).
-Reserved Notation "x < y < z" (at level 70, y at next level).
-Reserved Notation "x < y ≤ z" (at level 70, y at next level).
-Reserved Notation "x ≤ y ≤ z ≤ z'"
-  (at level 70, y at next level, z at next level).
-
-Infix "≤" := le : nat_scope.
-Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%nat : nat_scope.
-Notation "x ≤ y < z" := (x ≤ y ∧ y < z)%nat : nat_scope.
-Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%nat : nat_scope.
-Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%nat : nat_scope.
-Notation "(≤)" := le (only parsing) : nat_scope.
-Notation "(<)" := lt (only parsing) : nat_scope.
-
-Infix "`div`" := Nat.div (at level 35) : nat_scope.
-Infix "`mod`" := Nat.modulo (at level 35) : nat_scope.
-Infix "`max`" := Nat.max (at level 35) : nat_scope.
-Infix "`min`" := Nat.min (at level 35) : nat_scope.
-
-Instance nat_eq_dec: EqDecision nat := eq_nat_dec.
-Instance nat_le_dec: RelDecision le := le_dec.
-Instance nat_lt_dec: RelDecision lt := lt_dec.
-Instance nat_inhabited: Inhabited nat := populate 0%nat.
-Instance S_inj: Inj (=) (=) S.
-Proof. by injection 1. Qed.
-Instance nat_le_po: PartialOrder (≤).
-Proof. repeat split; repeat intro; auto with lia. Qed.
-Instance nat_le_total: Total (≤).
-Proof. repeat intro; lia. Qed.
-
-Instance nat_le_pi: ∀ x y : nat, ProofIrrel (x ≤ y).
-Proof.
-  assert (∀ x y (p : x ≤ y) y' (q : x ≤ y'),
-    y = y' → eq_dep nat (le x) y p y' q) as aux.
-  { fix FIX 3. intros x ? [|y p] ? [|y' q].
-    - done.
-    - clear FIX. intros; exfalso; auto with lia.
-    - clear FIX. intros; exfalso; auto with lia.
-    - injection 1. intros Hy. by case (FIX x y p y' q Hy). }
-  intros x y p q.
-  by apply (Eqdep_dec.eq_dep_eq_dec (λ x y, decide (x = y))), aux.
-Qed.
-Instance nat_lt_pi: ∀ x y : nat, ProofIrrel (x < y).
-Proof. unfold lt. apply _. Qed.
-
-Lemma nat_le_sum (x y : nat) : x ≤ y ↔ ∃ z, y = x + z.
-Proof. split. exists (y - x); lia. intros [z ->]; lia. Qed.
-
-Lemma Nat_lt_succ_succ n : n < S (S n).
-Proof. auto with arith. Qed.
-Lemma Nat_mul_split_l n x1 x2 y1 y2 :
-  x2 < n → y2 < n → x1 * n + x2 = y1 * n + y2 → x1 = y1 ∧ x2 = y2.
-Proof.
-  intros Hx2 Hy2 E. cut (x1 = y1); [intros; subst;lia |].
-  revert y1 E. induction x1; simpl; intros [|?]; simpl; auto with lia.
-Qed.
-Lemma Nat_mul_split_r n x1 x2 y1 y2 :
-  x1 < n → y1 < n → x1 + x2 * n = y1 + y2 * n → x1 = y1 ∧ x2 = y2.
-Proof. intros. destruct (Nat_mul_split_l n x2 x1 y2 y1); auto with lia. Qed.
-
-Notation lcm := Nat.lcm.
-Notation divide := Nat.divide.
-Notation "( x | y )" := (divide x y) : nat_scope.
-Instance Nat_divide_dec : RelDecision Nat.divide.
-Proof.
-  refine (λ x y, cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff.
-Defined.
-Instance: PartialOrder divide.
-Proof.
-  repeat split; try apply _. intros ??. apply Nat.divide_antisym_nonneg; lia.
-Qed.
-Hint Extern 0 (_ | _) => reflexivity : core.
-Lemma Nat_divide_ne_0 x y : (x | y) → y ≠ 0 → x ≠ 0.
-Proof. intros Hxy Hy ->. by apply Hy, Nat.divide_0_l. Qed.
-
-Lemma Nat_iter_S {A} n (f: A → A) x : Nat.iter (S n) f x = f (Nat.iter n f x).
-Proof. done. Qed.
-Lemma Nat_iter_S_r {A} n (f: A → A) x : Nat.iter (S n) f x = Nat.iter n f (f x).
-Proof. induction n; by f_equal/=. Qed.
-Lemma Nat_iter_add {A} n1 n2 (f : A → A) x :
-  Nat.iter (n1 + n2) f x = Nat.iter n1 f (Nat.iter n2 f x).
-Proof. induction n1; by f_equal/=. Qed.
-
-Lemma Nat_iter_ind {A} (P : A → Prop) f x k :
-  P x → (∀ y, P y → P (f y)) → P (Nat.iter k f x).
-Proof. induction k; simpl; auto. Qed.
-
-
-(** * Notations and properties of [positive] *)
-Local Open Scope positive_scope.
-
-Typeclasses Opaque Pos.le.
-Typeclasses Opaque Pos.lt.
-
-Infix "≤" := Pos.le : positive_scope.
-Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z) : positive_scope.
-Notation "x ≤ y < z" := (x ≤ y ∧ y < z) : positive_scope.
-Notation "x < y ≤ z" := (x < y ∧ y ≤ z) : positive_scope.
-Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z') : positive_scope.
-Notation "(≤)" := Pos.le (only parsing) : positive_scope.
-Notation "(<)" := Pos.lt (only parsing) : positive_scope.
-Notation "(~0)" := xO (only parsing) : positive_scope.
-Notation "(~1)" := xI (only parsing) : positive_scope.
-
-Arguments Pos.of_nat : simpl never.
-Arguments Pmult : simpl never.
-
-Instance positive_eq_dec: EqDecision positive := Pos.eq_dec.
-Instance positive_le_dec: RelDecision Pos.le.
-Proof. refine (λ x y, decide ((x ?= y) ≠ Gt)). Defined.
-Instance positive_lt_dec: RelDecision Pos.lt.
-Proof. refine (λ x y, decide ((x ?= y) = Lt)). Defined.
-Instance positive_le_total: Total Pos.le.
-Proof. repeat intro; lia. Qed.
-
-Instance positive_inhabited: Inhabited positive := populate 1.
-
-Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end.
-Instance maybe_xI : Maybe xI := λ p, match p with p~1 => Some p | _ => None end.
-Instance xO_inj : Inj (=) (=) (~0).
-Proof. by injection 1. Qed.
-Instance xI_inj : Inj (=) (=) (~1).
-Proof. by injection 1. Qed.
-
-(** Since [positive] represents lists of bits, we define list operations
-on it. These operations are in reverse, as positives are treated as snoc
-lists instead of cons lists. *)
-Fixpoint Papp (p1 p2 : positive) : positive :=
-  match p2 with
-  | 1 => p1
-  | p2~0 => (Papp p1 p2)~0
-  | p2~1 => (Papp p1 p2)~1
-  end.
-Infix "++" := Papp : positive_scope.
-Notation "(++)" := Papp (only parsing) : positive_scope.
-Notation "( p ++.)" := (Papp p) (only parsing) : positive_scope.
-Notation "(.++ q )" := (λ p, Papp p q) (only parsing) : positive_scope.
-
-Fixpoint Preverse_go (p1 p2 : positive) : positive :=
-  match p2 with
-  | 1 => p1
-  | p2~0 => Preverse_go (p1~0) p2
-  | p2~1 => Preverse_go (p1~1) p2
-  end.
-Definition Preverse : positive → positive := Preverse_go 1.
-
-Global Instance Papp_1_l : LeftId (=) 1 (++).
-Proof. intros p. by induction p; intros; f_equal/=. Qed.
-Global Instance Papp_1_r : RightId (=) 1 (++).
-Proof. done. Qed.
-Global Instance Papp_assoc : Assoc (=) (++).
-Proof. intros ?? p. by induction p; intros; f_equal/=. Qed.
-Global Instance Papp_inj p : Inj (=) (=) (.++ p).
-Proof. intros ???. induction p; simplify_eq; auto. Qed.
-
-Lemma Preverse_go_app p1 p2 p3 :
-  Preverse_go p1 (p2 ++ p3) = Preverse_go p1 p3 ++ Preverse_go 1 p2.
-Proof.
-  revert p3 p1 p2.
-  cut (∀ p1 p2 p3, Preverse_go (p2 ++ p3) p1 = p2 ++ Preverse_go p3 p1).
-  { by intros go p3; induction p3; intros p1 p2; simpl; auto; rewrite <-?go. }
-  intros p1; induction p1 as [p1 IH|p1 IH|]; intros p2 p3; simpl; auto.
-  - apply (IH _ (_~1)).
-  - apply (IH _ (_~0)).
-Qed.
-Lemma Preverse_app p1 p2 : Preverse (p1 ++ p2) = Preverse p2 ++ Preverse p1.
-Proof. unfold Preverse. by rewrite Preverse_go_app. Qed.
-Lemma Preverse_xO p : Preverse (p~0) = (1~0) ++ Preverse p.
-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.
-Proof. by induction p2; f_equal/=. Qed.
-
-Lemma Plt_sum (x y : positive) : x < y ↔ ∃ z, y = x + z.
-Proof.
-  split.
-  - exists (y - x)%positive. symmetry. apply Pplus_minus. lia.
-  - 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.
-
-Local Close Scope positive_scope.
-
-(** * Notations and properties of [N] *)
-Typeclasses Opaque N.le.
-Typeclasses Opaque N.lt.
-
-Infix "≤" := N.le : N_scope.
-Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%N : N_scope.
-Notation "x ≤ y < z" := (x ≤ y ∧ y < z)%N : N_scope.
-Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%N : N_scope.
-Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%N : N_scope.
-Notation "(≤)" := N.le (only parsing) : N_scope.
-Notation "(<)" := N.lt (only parsing) : N_scope.
-
-Infix "`div`" := N.div (at level 35) : N_scope.
-Infix "`mod`" := N.modulo (at level 35) : N_scope.
-Infix "`max`" := N.max (at level 35) : N_scope.
-Infix "`min`" := N.min (at level 35) : N_scope.
-
-Arguments N.add : simpl never.
-
-Instance Npos_inj : Inj (=) (=) Npos.
-Proof. by injection 1. Qed.
-
-Instance N_eq_dec: EqDecision N := N.eq_dec.
-Program Instance N_le_dec : RelDecision N.le := λ x y,
-  match N.compare x y with Gt => right _ | _ => left _ end.
-Solve Obligations with naive_solver.
-Program Instance N_lt_dec : RelDecision N.lt := λ x y,
-  match N.compare x y with Lt => left _ | _ => right _ end.
-Solve Obligations with naive_solver.
-Instance N_inhabited: Inhabited N := populate 1%N.
-Instance N_lt_pi x y : ProofIrrel (x < y)%N.
-Proof. unfold N.lt. apply _. Qed.
-
-Instance N_le_po: PartialOrder (≤)%N.
-Proof.
-  repeat split; red. apply N.le_refl. apply N.le_trans. apply N.le_antisymm.
-Qed.
-Instance N_le_total: Total (≤)%N.
-Proof. repeat intro; lia. Qed.
-
-Hint Extern 0 (_ ≤ _)%N => reflexivity : core.
-
-(** * Notations and properties of [Z] *)
-Local Open Scope Z_scope.
-
-Typeclasses Opaque Z.le.
-Typeclasses Opaque Z.lt.
-
-Infix "≤" := Z.le : Z_scope.
-Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z) : Z_scope.
-Notation "x ≤ y < z" := (x ≤ y ∧ y < z) : Z_scope.
-Notation "x < y < z" := (x < y ∧ y < z) : Z_scope.
-Notation "x < y ≤ z" := (x < y ∧ y ≤ z) : Z_scope.
-Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z') : Z_scope.
-Notation "(≤)" := Z.le (only parsing) : Z_scope.
-Notation "(<)" := Z.lt (only parsing) : Z_scope.
-
-Infix "`div`" := Z.div (at level 35) : Z_scope.
-Infix "`mod`" := Z.modulo (at level 35) : Z_scope.
-Infix "`quot`" := Z.quot (at level 35) : Z_scope.
-Infix "`rem`" := Z.rem (at level 35) : Z_scope.
-Infix "≪" := Z.shiftl (at level 35) : Z_scope.
-Infix "≫" := Z.shiftr (at level 35) : Z_scope.
-Infix "`max`" := Z.max (at level 35) : Z_scope.
-Infix "`min`" := Z.min (at level 35) : Z_scope.
-
-Instance Zpos_inj : Inj (=) (=) Zpos.
-Proof. by injection 1. Qed.
-Instance Zneg_inj : Inj (=) (=) Zneg.
-Proof. by injection 1. Qed.
-
-Instance Z_of_nat_inj : Inj (=) (=) Z.of_nat.
-Proof. intros n1 n2. apply Nat2Z.inj. Qed.
-
-Instance Z_eq_dec: EqDecision Z := Z.eq_dec.
-Instance Z_le_dec: RelDecision Z.le := Z_le_dec.
-Instance Z_lt_dec: RelDecision Z.lt := Z_lt_dec.
-Instance Z_ge_dec: RelDecision Z.ge := Z_ge_dec.
-Instance Z_gt_dec: RelDecision Z.gt := Z_gt_dec.
-Instance Z_inhabited: Inhabited Z := populate 1.
-Instance Z_lt_pi x y : ProofIrrel (x < y).
-Proof. unfold Z.lt. apply _. Qed.
-
-Instance Z_le_po : PartialOrder (≤).
-Proof.
-  repeat split; red. apply Z.le_refl. apply Z.le_trans. apply Z.le_antisymm.
-Qed.
-Instance Z_le_total: Total Z.le.
-Proof. repeat intro; lia. Qed.
-
-Lemma Z_pow_pred_r n m : 0 < m → n * n ^ (Z.pred m) = n ^ m.
-Proof.
-  intros. rewrite <-Z.pow_succ_r, Z.succ_pred. done. by apply Z.lt_le_pred.
-Qed.
-Lemma Z_quot_range_nonneg k x y : 0 ≤ x < k → 0 < y → 0 ≤ x `quot` y < k.
-Proof.
-  intros [??] ?.
-  destruct (decide (y = 1)); subst; [rewrite Z.quot_1_r; auto |].
-  destruct (decide (x = 0)); subst; [rewrite Z.quot_0_l; auto with lia |].
-  split. apply Z.quot_pos; lia. trans x; auto. apply Z.quot_lt; lia.
-Qed.
-
-Arguments Z.pred : simpl never.
-Arguments Z.succ : simpl never.
-Arguments Z.of_nat : simpl never.
-Arguments Z.to_nat : simpl never.
-Arguments Z.mul : simpl never.
-Arguments Z.add : simpl never.
-Arguments Z.sub : simpl never.
-Arguments Z.opp : simpl never.
-Arguments Z.pow : simpl never.
-Arguments Z.div : simpl never.
-Arguments Z.modulo : simpl never.
-Arguments Z.quot : simpl never.
-Arguments Z.rem : simpl never.
-Arguments Z.shiftl : simpl never.
-Arguments Z.shiftr : simpl never.
-Arguments Z.gcd : simpl never.
-Arguments Z.lcm : simpl never.
-Arguments Z.min : simpl never.
-Arguments Z.max : simpl never.
-Arguments Z.lor : simpl never.
-Arguments Z.land : simpl never.
-Arguments Z.lxor : simpl never.
-Arguments Z.lnot : simpl never.
-Arguments Z.square : simpl never.
-Arguments Z.abs : simpl never.
-
-Lemma Z_to_nat_neq_0_pos x : Z.to_nat x ≠ 0%nat → 0 < x.
-Proof. by destruct x. Qed.
-Lemma Z_to_nat_neq_0_nonneg x : Z.to_nat x ≠ 0%nat → 0 ≤ x.
-Proof. by destruct x. Qed.
-Lemma Z_mod_pos x y : 0 < y → 0 ≤ x `mod` y.
-Proof. apply Z.mod_pos_bound. Qed.
-
-Hint Resolve Z.lt_le_incl : zpos.
-Hint Resolve Z.add_nonneg_pos Z.add_pos_nonneg Z.add_nonneg_nonneg : zpos.
-Hint Resolve Z.mul_nonneg_nonneg Z.mul_pos_pos : zpos.
-Hint Resolve Z.pow_pos_nonneg Z.pow_nonneg: zpos.
-Hint Resolve Z_mod_pos Z.div_pos : zpos.
-Hint Extern 1000 => lia : zpos.
-
-Lemma Z_to_nat_nonpos x : x ≤ 0 → Z.to_nat x = 0%nat.
-Proof. destruct x; simpl; auto using Z2Nat.inj_neg. by intros []. Qed.
-Lemma Z2Nat_inj_pow (x y : nat) : Z.of_nat (x ^ y) = x ^ y.
-Proof.
-  induction y as [|y IH]; [by rewrite Z.pow_0_r, Nat.pow_0_r|].
-  by rewrite Nat.pow_succ_r, Nat2Z.inj_succ, Z.pow_succ_r,
-    Nat2Z.inj_mul, IH by auto with zpos.
-Qed.
-Lemma Nat2Z_divide n m : (Z.of_nat n | Z.of_nat m) ↔ (n | m)%nat.
-Proof.
-  split.
-  - rewrite <-(Nat2Z.id m) at 2; intros [i ->]; exists (Z.to_nat i).
-    destruct (decide (0 ≤ i)%Z).
-    { by rewrite Z2Nat.inj_mul, Nat2Z.id by lia. }
-    by rewrite !Z_to_nat_nonpos by auto using Z.mul_nonpos_nonneg with lia.
-  - intros [i ->]. exists (Z.of_nat i). by rewrite Nat2Z.inj_mul.
-Qed.
-Lemma Z2Nat_divide n m :
-  0 ≤ n → 0 ≤ m → (Z.to_nat n | Z.to_nat m)%nat ↔ (n | m).
-Proof. intros. by rewrite <-Nat2Z_divide, !Z2Nat.id by done. Qed.
-Lemma Z2Nat_inj_div x y : Z.of_nat (x `div` y) = x `div` y.
-Proof.
-  destruct (decide (y = 0%nat)); [by subst; destruct x |].
-  apply Z.div_unique with (x `mod` y)%nat.
-  { left. rewrite <-(Nat2Z.inj_le 0), <-Nat2Z.inj_lt.
-    apply Nat.mod_bound_pos; lia. }
-  by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod.
-Qed.
-Lemma Z2Nat_inj_mod x y : Z.of_nat (x `mod` y) = x `mod` y.
-Proof.
-  destruct (decide (y = 0%nat)); [by subst; destruct x |].
-  apply Z.mod_unique with (x `div` y)%nat.
-  { left. rewrite <-(Nat2Z.inj_le 0), <-Nat2Z.inj_lt.
-    apply Nat.mod_bound_pos; lia. }
-  by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod.
-Qed.
-Lemma Nat2Z_inj_div x y :
-  0 ≤ x → 0 ≤ y →
-  Z.to_nat (x `div` y) = (Z.to_nat x `div` Z.to_nat y)%nat.
-Proof.
-  intros. destruct (decide (y = 0%nat)); [by subst; destruct x|].
-  pose proof (Z.div_pos x y).
-  apply (inj Z.of_nat). by rewrite Z2Nat_inj_div, !Z2Nat.id by lia.
-Qed.
-Lemma Nat2Z_inj_mod x y :
-  0 ≤ x → 0 ≤ y →
-  Z.to_nat (x `mod` y) = (Z.to_nat x `mod` Z.to_nat y)%nat.
-Proof.
-  intros. destruct (decide (y = 0%nat)); [by subst; destruct x|].
-  pose proof (Z_mod_pos x y).
-  apply (inj Z.of_nat). by rewrite Z2Nat_inj_mod, !Z2Nat.id by lia.
-Qed.
-Lemma Z_succ_pred_induction y (P : Z → Prop) :
-  P y →
-  (∀ x, y ≤ x → P x → P (Z.succ x)) →
-  (∀ x, x ≤ y → P x → P (Z.pred x)) →
-  (∀ x, P x).
-Proof. intros H0 HS HP. by apply (Z.order_induction' _ _ y). Qed.
-Lemma Zmod_in_range q a c :
-  q * c ≤ a < (q + 1) * c →
-  a `mod` c = a - q * c.
-Proof. intros ?. symmetry. apply Z.mod_unique_pos with q; lia. Qed.
-
-Local Close Scope Z_scope.
-
-(** * Injectivity of casts *)
-Instance N_of_nat_inj: Inj (=) (=) N.of_nat := Nat2N.inj.
-Instance nat_of_N_inj: Inj (=) (=) N.to_nat := N2Nat.inj.
-Instance nat_of_pos_inj: Inj (=) (=) Pos.to_nat := Pos2Nat.inj.
-Instance pos_of_Snat_inj: Inj (=) (=) Pos.of_succ_nat := SuccNat2Pos.inj.
-Instance Z_of_N_inj: Inj (=) (=) Z.of_N := N2Z.inj.
-(* Add others here. *)
-
-(** * Notations and properties of [Qc] *)
-Typeclasses Opaque Qcle.
-Typeclasses Opaque Qclt.
-
-Local Open Scope Qc_scope.
-Delimit Scope Qc_scope with Qc.
-Notation "1" := (Q2Qc 1) : Qc_scope.
-Notation "2" := (1+1) : Qc_scope.
-Notation "- 1" := (Qcopp 1) : Qc_scope.
-Notation "- 2" := (Qcopp 2) : Qc_scope.
-Infix "≤" := Qcle : Qc_scope.
-Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z) : Qc_scope.
-Notation "x ≤ y < z" := (x ≤ y ∧ y < z) : Qc_scope.
-Notation "x < y < z" := (x < y ∧ y < z) : Qc_scope.
-Notation "x < y ≤ z" := (x < y ∧ y ≤ z) : Qc_scope.
-Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z') : Qc_scope.
-Notation "(≤)" := Qcle (only parsing) : Qc_scope.
-Notation "(<)" := Qclt (only parsing) : Qc_scope.
-
-Hint Extern 1 (_ ≤ _) => reflexivity || discriminate : core.
-Arguments Qred : simpl never.
-
-Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
-Program Instance Qc_le_dec: RelDecision Qcle := λ x y,
-  if Qclt_le_dec y x then right _ else left _.
-Next Obligation. intros x y; apply Qclt_not_le. Qed.
-Next Obligation. done. Qed.
-Program Instance Qc_lt_dec: RelDecision Qclt := λ x y,
-  if Qclt_le_dec x y then left _ else right _.
-Next Obligation. done. Qed.
-Next Obligation. intros x y; apply Qcle_not_lt. Qed.
-Instance Qc_lt_pi x y : ProofIrrel (x < y).
-Proof. unfold Qclt. apply _. Qed.
-
-Instance Qc_le_po: PartialOrder (≤).
-Proof.
-  repeat split; red. apply Qcle_refl. apply Qcle_trans. apply Qcle_antisym.
-Qed.
-Instance Qc_lt_strict: StrictOrder (<).
-Proof.
-  split; red. intros x Hx. by destruct (Qclt_not_eq x x). apply Qclt_trans.
-Qed.
-Instance Qc_le_total: Total Qcle.
-Proof. intros x y. destruct (Qclt_le_dec x y); auto using Qclt_le_weak. Qed.
-
-Lemma Qcmult_0_l x : 0 * x = 0.
-Proof. ring. Qed.
-Lemma Qcmult_0_r x : x * 0 = 0.
-Proof. ring. Qed.
-Lemma Qcplus_diag x : (x + x)%Qc = (2 * x)%Qc.
-Proof. ring. Qed.
-Lemma Qcle_ngt (x y : Qc) : x ≤ y ↔ ¬y < x.
-Proof. split; auto using Qcle_not_lt, Qcnot_lt_le. Qed.
-Lemma Qclt_nge (x y : Qc) : x < y ↔ ¬y ≤ x.
-Proof. split; auto using Qclt_not_le, Qcnot_le_lt. Qed.
-Lemma Qcplus_le_mono_l (x y z : Qc) : x ≤ y ↔ z + x ≤ z + y.
-Proof.
-  split; intros.
-  - by apply Qcplus_le_compat.
-  - replace x with ((0 - z) + (z + x)) by ring.
-    replace y with ((0 - z) + (z + y)) by ring.
-    by apply Qcplus_le_compat.
-Qed.
-Lemma Qcplus_le_mono_r (x y z : Qc) : x ≤ y ↔ x + z ≤ y + z.
-Proof. rewrite !(Qcplus_comm _ z). apply Qcplus_le_mono_l. Qed.
-Lemma Qcplus_lt_mono_l (x y z : Qc) : x < y ↔ z + x < z + y.
-Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_l. Qed.
-Lemma Qcplus_lt_mono_r (x y z : Qc) : x < y ↔ x + z < y + z.
-Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_r. Qed.
-Instance Qcopp_inj : Inj (=) (=) Qcopp.
-Proof.
-  intros x y H. by rewrite <-(Qcopp_involutive x), H, Qcopp_involutive.
-Qed.
-Instance Qcplus_inj_r z : Inj (=) (=) (Qcplus z).
-Proof.
-  intros x y H. by apply (anti_symm (≤));rewrite (Qcplus_le_mono_l _ _ z), H.
-Qed.
-Instance Qcplus_inj_l z : Inj (=) (=) (λ x, x + z).
-Proof.
-  intros x y H. by apply (anti_symm (≤)); rewrite (Qcplus_le_mono_r _ _ z), H.
-Qed.
-Lemma Qcplus_pos_nonneg (x y : Qc) : 0 < x → 0 ≤ y → 0 < x + y.
-Proof.
-  intros. apply Qclt_le_trans with (x + 0); [by rewrite Qcplus_0_r|].
-  by apply Qcplus_le_mono_l.
-Qed.
-Lemma Qcplus_nonneg_pos (x y : Qc) : 0 ≤ x → 0 < y → 0 < x + y.
-Proof. rewrite (Qcplus_comm x). auto using Qcplus_pos_nonneg. Qed.
-Lemma Qcplus_pos_pos (x y : Qc) : 0 < x → 0 < y → 0 < x + y.
-Proof. auto using Qcplus_pos_nonneg, Qclt_le_weak. Qed.
-Lemma Qcplus_nonneg_nonneg (x y : Qc) : 0 ≤ x → 0 ≤ y → 0 ≤ x + y.
-Proof.
-  intros. trans (x + 0); [by rewrite Qcplus_0_r|].
-  by apply Qcplus_le_mono_l.
-Qed.
-Lemma Qcplus_neg_nonpos (x y : Qc) : x < 0 → y ≤ 0 → x + y < 0.
-Proof.
-  intros. apply Qcle_lt_trans with (x + 0); [|by rewrite Qcplus_0_r].
-  by apply Qcplus_le_mono_l.
-Qed.
-Lemma Qcplus_nonpos_neg (x y : Qc) : x ≤ 0 → y < 0 → x + y < 0.
-Proof. rewrite (Qcplus_comm x). auto using Qcplus_neg_nonpos. Qed.
-Lemma Qcplus_neg_neg (x y : Qc) : x < 0 → y < 0 → x + y < 0.
-Proof. auto using Qcplus_nonpos_neg, Qclt_le_weak. Qed.
-Lemma Qcplus_nonpos_nonpos (x y : Qc) : x ≤ 0 → y ≤ 0 → x + y ≤ 0.
-Proof.
-  intros. trans (x + 0); [|by rewrite Qcplus_0_r].
-  by apply Qcplus_le_mono_l.
-Qed.
-Lemma Qcmult_le_mono_nonneg_l x y z : 0 ≤ z → x ≤ y → z * x ≤ z * y.
-Proof. intros. rewrite !(Qcmult_comm z). by apply Qcmult_le_compat_r. Qed.
-Lemma Qcmult_le_mono_nonneg_r x y z : 0 ≤ z → x ≤ y → x * z ≤ y * z.
-Proof. intros. by apply Qcmult_le_compat_r. Qed.
-Lemma Qcmult_le_mono_pos_l x y z : 0 < z → x ≤ y ↔ z * x ≤ z * y.
-Proof.
-  split; auto using Qcmult_le_mono_nonneg_l, Qclt_le_weak.
-  rewrite !Qcle_ngt, !(Qcmult_comm z).
-  intuition auto using Qcmult_lt_compat_r.
-Qed.
-Lemma Qcmult_le_mono_pos_r x y z : 0 < z → x ≤ y ↔ x * z ≤ y * z.
-Proof. rewrite !(Qcmult_comm _ z). by apply Qcmult_le_mono_pos_l. Qed.
-Lemma Qcmult_lt_mono_pos_l x y z : 0 < z → x < y ↔ z * x < z * y.
-Proof. intros. by rewrite !Qclt_nge, <-Qcmult_le_mono_pos_l. Qed.
-Lemma Qcmult_lt_mono_pos_r x y z : 0 < z → x < y ↔ x * z < y * z.
-Proof. intros. by rewrite !Qclt_nge, <-Qcmult_le_mono_pos_r. Qed.
-Lemma Qcmult_pos_pos x y : 0 < x → 0 < y → 0 < x * y.
-Proof.
-  intros. apply Qcle_lt_trans with (0 * y); [by rewrite Qcmult_0_l|].
-  by apply Qcmult_lt_mono_pos_r.
-Qed.
-Lemma Qcmult_nonneg_nonneg x y : 0 ≤ x → 0 ≤ y → 0 ≤ x * y.
-Proof.
-  intros. trans (0 * y); [by rewrite Qcmult_0_l|].
-  by apply Qcmult_le_mono_nonneg_r.
-Qed.
-
-Lemma inject_Z_Qred n : Qred (inject_Z n) = inject_Z n.
-Proof. apply Qred_identity; auto using Z.gcd_1_r. Qed.
-Coercion Qc_of_Z (n : Z) : Qc := Qcmake _ (inject_Z_Qred n).
-Lemma Z2Qc_inj_0 : Qc_of_Z 0 = 0.
-Proof. by apply Qc_is_canon. Qed.
-Lemma Z2Qc_inj_1 : Qc_of_Z 1 = 1.
-Proof. by apply Qc_is_canon. Qed.
-Lemma Z2Qc_inj_2 : Qc_of_Z 2 = 2.
-Proof. by apply Qc_is_canon. Qed.
-Lemma Z2Qc_inj n m : Qc_of_Z n = Qc_of_Z m → n = m.
-Proof. by injection 1. Qed.
-Lemma Z2Qc_inj_iff n m : Qc_of_Z n = Qc_of_Z m ↔ n = m.
-Proof. split. auto using Z2Qc_inj. by intros ->. Qed.
-Lemma Z2Qc_inj_le n m : (n ≤ m)%Z ↔ Qc_of_Z n ≤ Qc_of_Z m.
-Proof. by rewrite Zle_Qle. Qed.
-Lemma Z2Qc_inj_lt n m : (n < m)%Z ↔ Qc_of_Z n < Qc_of_Z m.
-Proof. by rewrite Zlt_Qlt. Qed.
-Lemma Z2Qc_inj_add n m : Qc_of_Z (n + m) = Qc_of_Z n + Qc_of_Z m.
-Proof. apply Qc_is_canon; simpl. by rewrite Qred_correct, inject_Z_plus. Qed.
-Lemma Z2Qc_inj_mul n m : Qc_of_Z (n * m) = Qc_of_Z n * Qc_of_Z m.
-Proof. apply Qc_is_canon; simpl. by rewrite Qred_correct, inject_Z_mult. Qed.
-Lemma Z2Qc_inj_opp n : Qc_of_Z (-n) = -Qc_of_Z n.
-Proof. apply Qc_is_canon; simpl. by rewrite Qred_correct, inject_Z_opp. Qed.
-Lemma Z2Qc_inj_sub n m : Qc_of_Z (n - m) = Qc_of_Z n - Qc_of_Z m.
-Proof.
-  apply Qc_is_canon; simpl.
-  by rewrite !Qred_correct, <-inject_Z_opp, <-inject_Z_plus.
-Qed.
-Local Close Scope Qc_scope.
-
-(** * Positive rationals *)
-(** The theory of positive rationals is very incomplete. We merely provide
-some operations and theorems that are relevant for fractional permissions. *)
-Record Qp := mk_Qp { Qp_car :> Qc ; Qp_prf : (0 < Qp_car)%Qc }.
-Hint Resolve Qp_prf : core.
-Delimit Scope Qp_scope with Qp.
-Bind Scope Qp_scope with Qp.
-Arguments Qp_car _%Qp : assert.
-
-Definition Qp_one : Qp := mk_Qp 1 eq_refl.
-Program Definition Qp_plus (x y : Qp) : Qp := mk_Qp (x + y) _.
-Next Obligation. by intros x y; apply Qcplus_pos_pos. Qed.
-Definition Qp_minus (x y : Qp) : option Qp :=
-  let z := (x - y)%Qc in
-  match decide (0 < z)%Qc with left Hz => Some (mk_Qp z Hz) | _ => None end.
-Program Definition Qp_mult (x y : Qp) : Qp := mk_Qp (x * y) _.
-Next Obligation. intros x y. apply Qcmult_pos_pos; apply Qp_prf. Qed.
-
-Program Definition Qp_div (x : Qp) (y : positive) : Qp := mk_Qp (x / Zpos y) _.
-Next Obligation.
-  intros x y. unfold Qcdiv. assert (0 < Zpos y)%Qc.
-  { apply (Z2Qc_inj_lt 0%Z (Zpos y)), Pos2Z.is_pos. }
-  by rewrite (Qcmult_lt_mono_pos_r _ _ (Zpos y)%Z), Qcmult_0_l,
-    <-Qcmult_assoc, Qcmult_inv_l, Qcmult_1_r.
-Qed.
-
-Infix "+" := Qp_plus : Qp_scope.
-Infix "-" := Qp_minus : Qp_scope.
-Infix "*" := Qp_mult : Qp_scope.
-Infix "/" := Qp_div : Qp_scope.
-Notation "1" := Qp_one : Qp_scope.
-Notation "2" := (1 + 1)%Qp : Qp_scope.
-Notation "3" := (1 + 2)%Qp : Qp_scope.
-Notation "4" := (1 + 3)%Qp : Qp_scope.
-
-Lemma Qp_eq x y : x = y ↔ Qp_car x = Qp_car y.
-Proof.
-  split; [by intros ->|].
-  destruct x, y; intros; simplify_eq/=; f_equal; apply (proof_irrel _).
-Qed.
-
-Instance Qp_inhabited : Inhabited Qp := populate 1%Qp.
-Instance Qp_eq_dec : EqDecision Qp.
-Proof.
- refine (λ x y, cast_if (decide (Qp_car x = Qp_car y))); by rewrite Qp_eq.
-Defined.
-
-Instance Qp_plus_assoc : Assoc (=) Qp_plus.
-Proof. intros x y z; apply Qp_eq, Qcplus_assoc. Qed.
-Instance Qp_plus_comm : Comm (=) Qp_plus.
-Proof. intros x y; apply Qp_eq, Qcplus_comm. Qed.
-Instance Qp_plus_inj_r p : Inj (=) (=) (Qp_plus p).
-Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj (Qcplus p)). Qed.
-Instance Qp_plus_inj_l p : Inj (=) (=) (λ q, q + p)%Qp.
-Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj (λ q, q + p)%Qc). Qed.
-
-Lemma Qp_minus_diag x : (x - x)%Qp = None.
-Proof. unfold Qp_minus, Qcminus. by rewrite Qcplus_opp_r. Qed.
-Lemma Qp_op_minus x y : ((x + y) - x)%Qp = Some y.
-Proof.
-  unfold Qp_minus, Qcminus; simpl.
-  rewrite (Qcplus_comm x), <- Qcplus_assoc, Qcplus_opp_r, Qcplus_0_r.
-  destruct (decide _) as [|[]]; auto. by f_equal; apply Qp_eq.
-Qed.
-
-Instance Qp_mult_assoc : Assoc (=) Qp_mult.
-Proof. intros x y z; apply Qp_eq, Qcmult_assoc. Qed.
-Instance Qp_mult_comm : Comm (=) Qp_mult.
-Proof. intros x y; apply Qp_eq, Qcmult_comm. Qed.
-Lemma Qp_mult_plus_distr_r x y z: (x * (y + z) = x * y + x * z)%Qp.
-Proof. apply Qp_eq, Qcmult_plus_distr_r. Qed.
-Lemma Qp_mult_plus_distr_l x y z: ((x + y) * z = x * z + y * z)%Qp.
-Proof. apply Qp_eq, Qcmult_plus_distr_l. Qed.
-Lemma Qp_mult_1_l x: (1 * x)%Qp = x.
-Proof. apply Qp_eq, Qcmult_1_l. Qed.
-Lemma Qp_mult_1_r x: (x * 1)%Qp = x.
-Proof. apply Qp_eq, Qcmult_1_r. Qed.
-
-Lemma Qp_div_1 x : (x / 1 = x)%Qp.
-Proof.
-  apply Qp_eq; simpl.
-  rewrite <-(Qcmult_div_r x 1) at 2 by done. by rewrite Qcmult_1_l.
-Qed.
-Lemma Qp_div_S x y : (x / (2 * y) + x / (2 * y) = x / y)%Qp.
-Proof.
-  apply Qp_eq; simpl. unfold Qcdiv.
-  rewrite <-Qcmult_plus_distr_l, Pos2Z.inj_mul, Z2Qc_inj_mul, Z2Qc_inj_2.
-  rewrite Qcplus_diag. by field_simplify.
-Qed.
-Lemma Qp_div_2 x : (x / 2 + x / 2 = x)%Qp.
-Proof.
-  change 2%positive with (2 * 1)%positive. by rewrite Qp_div_S, Qp_div_1.
-Qed.
-Lemma Qp_half_half : (1 / 2 + 1 / 2 = 1)%Qp.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
-Lemma Qp_quarter_three_quarter : (1 / 4 + 3 / 4 = 1)%Qp.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
-Lemma Qp_three_quarter_quarter : (3 / 4 + 1 / 4 = 1)%Qp.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
-
-Lemma Qp_lt_sum (x y : Qp) : (x < y)%Qc ↔ ∃ z, y = (x + z)%Qp.
-Proof.
-  split.
-  - intros Hlt%Qclt_minus_iff. exists (mk_Qp (y - x) Hlt). apply Qp_eq; simpl.
-    unfold Qcminus. by rewrite (Qcplus_comm y), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l.
-  - intros [z ->]; simpl.
-    rewrite <-(Qcplus_0_r x) at 1. apply Qcplus_lt_mono_l, Qp_prf.
-Qed.
-
-Lemma Qp_lower_bound q1 q2 : ∃ q q1' q2', (q1 = q + q1' ∧ q2 = q + q2')%Qp.
-Proof.
-  revert q1 q2. cut (∀ q1 q2 : Qp, (q1 ≤ q2)%Qc →
-    ∃ q q1' q2', (q1 = q + q1' ∧ q2 = q + q2')%Qp).
-  { intros help q1 q2.
-    destruct (Qc_le_dec q1 q2) as [LE|LE%Qclt_nge%Qclt_le_weak]; [by eauto|].
-    destruct (help q2 q1) as (q&q1'&q2'&?&?); eauto. }
-  intros q1 q2 Hq. exists (q1 / 2)%Qp, (q1 / 2)%Qp.
-  assert (0 < q2 +- q1 */ 2)%Qc as Hq2'.
-  { eapply Qclt_le_trans; [|by apply Qcplus_le_mono_r, Hq].
-    replace (q1 +- q1 */ 2)%Qc with (q1 * (1 +- 1*/2))%Qc by ring.
-    replace 0%Qc with (0 * (1+-1*/2))%Qc by ring. by apply Qcmult_lt_compat_r. }
-  exists (mk_Qp (q2 +- q1 */ 2%Z) Hq2'). split; [by rewrite Qp_div_2|].
-  apply Qp_eq; simpl. unfold Qcdiv. ring.
-Qed.
-
-Lemma Qp_cross_split p a b c d :
-  (a + b = p → c + d = p →
-  ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d)%Qp.
-Proof.
-  intros H <-. revert a b c d H. cut (∀ a b c d : Qp,
-    (a < c)%Qc → a + b = c + d →
-    ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d)%Qp.
-  { intros help a b c d ?.
-    destruct (Qclt_le_dec a c) as [?|[?| ->%Qp_eq]%Qcle_lt_or_eq].
-    - auto.
-    - destruct (help c d a b); [done..|]. naive_solver.
-    - apply (inj (Qp_plus a)) in H as ->. destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
-      eauto 10 using (comm_L Qp_plus). }
-  intros a b c d [e ->]%Qp_lt_sum. rewrite <-(assoc_L _). intros ->%(inj (Qp_plus a)).
-  destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
-  eexists a', q, (q + e)%Qp, d'; split_and?; auto using (comm_L Qp_plus).
-  - by rewrite (assoc_L _), (comm_L Qp_plus e).
-  - by rewrite (assoc_L _), (comm_L Qp_plus a').
-Qed.
-
-Lemma Qp_bounded_split (p r : Qp) : ∃ q1 q2 : Qp, (q1 ≤ r)%Qc ∧ p = (q1 + q2)%Qp.
-Proof.
-  destruct (Qclt_le_dec r p) as [?|?].
-  - assert (0 < p +- r)%Qc as Hpos.
-    { apply (Qcplus_lt_mono_r _ _ r). rewrite <-Qcplus_assoc, (Qcplus_comm (-r)).
-      by rewrite Qcplus_opp_r, Qcplus_0_l, Qcplus_0_r. }
-    exists r, (mk_Qp _ Hpos); simpl; split; [done|].
-    apply Qp_eq; simpl. rewrite Qcplus_comm, <-Qcplus_assoc, (Qcplus_comm (-r)).
-    by rewrite Qcplus_opp_r, Qcplus_0_r.
-  - exists (p / 2)%Qp, (p / 2)%Qp; split.
-    + trans p; [|done]. apply Qclt_le_weak, Qp_lt_sum.
-      exists (p / 2)%Qp. by rewrite Qp_div_2.
-    + by rewrite Qp_div_2.
-Qed.
-
-Lemma Qp_not_plus_q_ge_1 (q: Qp): ¬ ((1 + q)%Qp ≤ 1%Qp)%Qc.
-Proof.
-  intros Hle.
-  apply (Qcplus_le_mono_l q 0 1) in Hle.
-  apply Qcle_ngt in Hle. apply Hle, Qp_prf.
-Qed.
-
-Lemma Qp_ge_0 (q: Qp): (0 ≤ q)%Qc.
-Proof. apply Qclt_le_weak, Qp_prf. Qed.
-
-(** * Helper for working with accessing lists with wrap-around
-    See also [rotate] and [rotate_take] in [list.v] *)
-(** [rotate_nat_add base offset len] computes [(base + offset) `mod`
-len]. This is useful in combination with the [rotate] function on
-lists, since the index [i] of [rotate n l] corresponds to the index
-[rotate_nat_add n i (length i)] of the original list. The definition
-uses [Z] for consistency with [rotate_nat_sub]. **)
-Definition rotate_nat_add (base offset len : nat) : nat :=
-  Z.to_nat ((base + offset) `mod` len)%Z.
-(** [rotate_nat_sub base offset len] is the inverse of [rotate_nat_add
-base offset len]. The definition needs to use modulo on [Z] instead of
-on nat since otherwise we need the sidecondition [base < len] on
-[rotate_nat_sub_add]. **)
-Definition rotate_nat_sub (base offset len : nat) : nat :=
-  Z.to_nat ((len + offset - base) `mod` len)%Z.
-
-Lemma rotate_nat_add_len_0 base offset:
-  rotate_nat_add base offset 0 = 0.
-Proof. unfold rotate_nat_add. by rewrite Zmod_0_r. Qed.
-Lemma rotate_nat_sub_len_0 base offset:
-  rotate_nat_sub base offset 0 = 0.
-Proof. unfold rotate_nat_sub. by rewrite Zmod_0_r. Qed.
-
-Lemma rotate_nat_add_add_mod base offset len:
-  rotate_nat_add base offset len =
-  rotate_nat_add (Z.to_nat (base `mod` len)%Z) offset len.
-Proof.
-  destruct len as [|i];[ by rewrite !rotate_nat_add_len_0|].
-  pose proof (Z_mod_lt base (S i)) as Hlt. unfold rotate_nat_add.
-  rewrite !Z2Nat.id by lia. by rewrite Zplus_mod_idemp_l.
-Qed.
-
-Lemma rotate_nat_add_alt base offset len:
-  base < len → offset < len →
-  rotate_nat_add base offset len =
-  if decide (base + offset < len) then base + offset else base + offset - len.
-Proof.
-  unfold rotate_nat_add. intros ??. case_decide.
-  - rewrite Z.mod_small by lia. by rewrite <-Nat2Z.inj_add, Nat2Z.id.
-  - rewrite (Zmod_in_range 1) by lia.
-    by rewrite Z.mul_1_l, <-Nat2Z.inj_add, <-Nat2Z.inj_sub,Nat2Z.id by lia.
-Qed.
-Lemma rotate_nat_sub_alt base offset len:
-  base < len → offset < len →
-  rotate_nat_sub base offset len =
-  if decide (offset < base) then len + offset - base else offset - base.
-Proof.
-  unfold rotate_nat_sub. intros ??. case_decide.
-  - rewrite Z.mod_small by lia.
-    by rewrite <-Nat2Z.inj_add, <-Nat2Z.inj_sub, Nat2Z.id by lia.
-  - rewrite (Zmod_in_range 1) by lia.
-    rewrite Z.mul_1_l, <-Nat2Z.inj_add, <-!Nat2Z.inj_sub,Nat2Z.id; lia.
-Qed.
-
-Lemma rotate_nat_add_0 base len :
-  base < len → rotate_nat_add base 0 len = base.
-Proof.
-  intros ?. unfold rotate_nat_add.
-  rewrite Z.mod_small by lia. by rewrite Z.add_0_r, Nat2Z.id.
-Qed.
-Lemma rotate_nat_sub_0 base len :
-  base < len → rotate_nat_sub base base len = 0.
-Proof. intros ?. rewrite rotate_nat_sub_alt by done. case_decide; lia. Qed.
-
-Lemma rotate_nat_add_lt base offset len :
-  0 < len → rotate_nat_add base offset len < len.
-Proof.
-  unfold rotate_nat_add. intros ?.
-  pose proof (Nat.mod_upper_bound (base + offset) len).
-  rewrite Nat2Z_inj_mod, Z2Nat.inj_add, !Nat2Z.id; lia.
-Qed.
-Lemma rotate_nat_sub_lt base offset len :
-  0 < len → rotate_nat_sub base offset len < len.
-Proof.
-  unfold rotate_nat_sub. intros ?.
-  pose proof (Z_mod_lt (len + offset - base) len).
-  apply Nat2Z.inj_lt. rewrite Z2Nat.id; lia.
-Qed.
-
-Lemma rotate_nat_add_sub base len offset:
-  offset < len →
-  rotate_nat_add base (rotate_nat_sub base offset len) len = offset.
-Proof.
-  intros ?. unfold rotate_nat_add, rotate_nat_sub.
-  rewrite Z2Nat.id by (apply Z_mod_pos; lia). rewrite Zplus_mod_idemp_r.
-  replace (base + (len + offset - base))%Z with (len + offset)%Z by lia.
-  rewrite (Zmod_in_range 1) by lia.
-  rewrite Z.mul_1_l, <-Nat2Z.inj_add, <-!Nat2Z.inj_sub,Nat2Z.id; lia.
-Qed.
-
-Lemma rotate_nat_sub_add base len offset:
-  offset < len →
-  rotate_nat_sub base (rotate_nat_add base offset len) len = offset.
-Proof.
-  intros ?. unfold rotate_nat_add, rotate_nat_sub.
-  rewrite Z2Nat.id by (apply Z_mod_pos; lia).
-  assert (∀ n, (len + n - base) = ((len - base) + n))%Z as -> by naive_solver lia.
-  rewrite Zplus_mod_idemp_r.
-  replace (len - base + (base + offset))%Z with (len + offset)%Z by lia.
-  rewrite (Zmod_in_range 1) by lia.
-  rewrite Z.mul_1_l, <-Nat2Z.inj_add, <-!Nat2Z.inj_sub,Nat2Z.id; lia.
-Qed.
-
-Lemma rotate_nat_add_add base offset len n:
-  0 < len →
-  rotate_nat_add base (offset + n) len =
-  (rotate_nat_add base offset len + n) `mod` len.
-Proof.
-  intros ?. unfold rotate_nat_add.
-  rewrite !Nat2Z_inj_mod, !Z2Nat.inj_add, !Nat2Z.id by lia.
-  by rewrite plus_assoc, Nat.add_mod_idemp_l by lia.
-Qed.
-
-Lemma rotate_nat_add_S base offset len:
-  0 < len →
-  rotate_nat_add base (S offset) len =
-  S (rotate_nat_add base offset len) `mod` len.
-Proof. intros ?. by rewrite <-Nat.add_1_r, rotate_nat_add_add, Nat.add_1_r. Qed.

theories/pmap.v

-(** This files implements an efficient implementation of finite maps whose keys
-range over Coq's data type of positive binary naturals [positive]. The
-implementation is based on Xavier Leroy's implementation of radix-2 search
-trees (uncompressed Patricia trees) and guarantees logarithmic-time operations.
-However, we extend Leroy's implementation by packing the trees into a Sigma
-type such that canonicity of representation is ensured. This is necesarry for
-Leibniz equality to become extensional. *)
-From Coq Require Import PArith.
-From stdpp Require Import mapset countable.
-From stdpp Require Export fin_maps.
-Set Default Proof Using "Type".
-
-Local Open Scope positive_scope.
-Local Hint Extern 0 (_ =@{positive} _) => congruence : core.
-Local Hint Extern 0 (_ ≠@{positive} _) => congruence : core.
-
-(** * The tree data structure *)
-(** The data type [Pmap_raw] specifies radix-2 search trees. These trees do
-not ensure canonical representations of maps. For example the empty map can
-be represented as a binary tree of an arbitrary size that contains [None] at
-all nodes. *)
-Inductive Pmap_raw (A : Type) : Type :=
-  | PLeaf: Pmap_raw A
-  | PNode: option A → Pmap_raw A → Pmap_raw A → Pmap_raw A.
-Arguments PLeaf {_} : assert.
-Arguments PNode {_} _ _ _ : assert.
-
-Instance Pmap_raw_eq_dec `{EqDecision A} : EqDecision (Pmap_raw A).
-Proof. solve_decision. Defined.
-
-Fixpoint Pmap_wf {A} (t : Pmap_raw A) : bool :=
-  match t with
-  | PLeaf => true
-  | PNode None PLeaf PLeaf => false
-  | PNode _ l r => Pmap_wf l && Pmap_wf r
-  end.
-Arguments Pmap_wf _ !_ / : simpl nomatch, assert.
-Lemma Pmap_wf_l {A} o (l r : Pmap_raw A) : Pmap_wf (PNode o l r) → Pmap_wf l.
-Proof. destruct o, l, r; simpl; rewrite ?andb_True; tauto. Qed.
-Lemma Pmap_wf_r {A} o (l r : Pmap_raw A) : Pmap_wf (PNode o l r) → Pmap_wf r.
-Proof. destruct o, l, r; simpl; rewrite ?andb_True; tauto. Qed.
-Local Hint Immediate Pmap_wf_l Pmap_wf_r : core.
-Definition PNode' {A} (o : option A) (l r : Pmap_raw A) :=
-  match l, o, r with PLeaf, None, PLeaf => PLeaf | _, _, _ => PNode o l r end.
-Arguments PNode' : simpl never.
-Lemma PNode_wf {A} o (l r : Pmap_raw A) :
-  Pmap_wf l → Pmap_wf r → Pmap_wf (PNode' o l r).
-Proof. destruct o, l, r; simpl; auto. Qed.
-Local Hint Resolve PNode_wf : core.
-
-(** Operations *)
-Instance Pempty_raw {A} : Empty (Pmap_raw A) := PLeaf.
-Instance Plookup_raw {A} : Lookup positive A (Pmap_raw A) :=
-  fix go (i : positive) (t : Pmap_raw A) {struct t} : option A :=
-  let _ : Lookup _ _ _ := @go in
-  match t with
-  | PLeaf => None
-  | PNode o l r => match i with 1 => o | i~0 => l !! i | i~1 => r !! i end
-  end.
-Local Arguments lookup _ _ _ _ _ !_ / : simpl nomatch, assert.
-Fixpoint Psingleton_raw {A} (i : positive) (x : A) : Pmap_raw A :=
-  match i with
-  | 1 => PNode (Some x) PLeaf PLeaf
-  | i~0 => PNode None (Psingleton_raw i x) PLeaf
-  | i~1 => PNode None PLeaf (Psingleton_raw i x)
-  end.
-Fixpoint Ppartial_alter_raw {A} (f : option A → option A)
-    (i : positive) (t : Pmap_raw A) {struct t} : Pmap_raw A :=
-  match t with
-  | PLeaf => match f None with None => PLeaf | Some x => Psingleton_raw i x end
-  | PNode o l r =>
-     match i with
-     | 1 => PNode' (f o) l r
-     | i~0 => PNode' o (Ppartial_alter_raw f i l) r
-     | i~1 => PNode' o l (Ppartial_alter_raw f i r)
-     end
-  end.
-Fixpoint Pfmap_raw {A B} (f : A → B) (t : Pmap_raw A) : Pmap_raw B :=
-  match t with
-  | PLeaf => PLeaf
-  | PNode o l r => PNode (f <$> o) (Pfmap_raw f l) (Pfmap_raw f r)
-  end.
-Fixpoint Pto_list_raw {A} (j : positive) (t : Pmap_raw A)
-    (acc : list (positive * A)) : list (positive * A) :=
-  match t with
-  | PLeaf => acc
-  | PNode o l r => from_option (λ x, [(Preverse j, x)]) [] o ++
-     Pto_list_raw (j~0) l (Pto_list_raw (j~1) r acc)
-  end%list.
-Fixpoint Pomap_raw {A B} (f : A → option B) (t : Pmap_raw A) : Pmap_raw B :=
-  match t with
-  | PLeaf => PLeaf
-  | PNode o l r => PNode' (o ≫= f) (Pomap_raw f l) (Pomap_raw f r)
-  end.
-Fixpoint Pmerge_raw {A B C} (f : option A → option B → option C)
-    (t1 : Pmap_raw A) (t2 : Pmap_raw B) : Pmap_raw C :=
-  match t1, t2 with
-  | PLeaf, t2 => Pomap_raw (f None ∘ Some) t2
-  | t1, PLeaf => Pomap_raw (flip f None ∘ Some) t1
-  | PNode o1 l1 r1, PNode o2 l2 r2 =>
-      PNode' (f o1 o2) (Pmerge_raw f l1 l2) (Pmerge_raw f r1 r2)
-  end.
-
-(** Proofs *)
-Lemma Pmap_wf_canon {A} (t : Pmap_raw A) :
-  (∀ i, t !! i = None) → Pmap_wf t → t = PLeaf.
-Proof.
-  induction t as [|o l IHl r IHr]; intros Ht ?; auto.
-  assert (o = None) as -> by (apply (Ht 1)).
-  assert (l = PLeaf) as -> by (apply IHl; try apply (λ i, Ht (i~0)); eauto).
-  by assert (r = PLeaf) as -> by (apply IHr; try apply (λ i, Ht (i~1)); eauto).
-Qed.
-Lemma Pmap_wf_eq {A} (t1 t2 : Pmap_raw A) :
-  (∀ i, t1 !! i = t2 !! i) → Pmap_wf t1 → Pmap_wf t2 → t1 = t2.
-Proof.
-  revert t2.
-  induction t1 as [|o1 l1 IHl r1 IHr]; intros [|o2 l2 r2] Ht ??; simpl; auto.
-  - discriminate (Pmap_wf_canon (PNode o2 l2 r2)); eauto.
-  - discriminate (Pmap_wf_canon (PNode o1 l1 r1)); eauto.
-  - f_equal; [apply (Ht 1)| |].
-    + apply IHl; try apply (λ x, Ht (x~0)); eauto.
-    + apply IHr; try apply (λ x, Ht (x~1)); eauto.
-Qed.
-Lemma PNode_lookup {A} o (l r : Pmap_raw A) i :
-  PNode' o l r !! i = PNode o l r !! i.
-Proof. by destruct i, o, l, r. Qed.
-
-Lemma Psingleton_wf {A} i (x : A) : Pmap_wf (Psingleton_raw i x).
-Proof. induction i as [[]|[]|]; simpl; rewrite ?andb_true_r; auto. Qed.
-Lemma Ppartial_alter_wf {A} f i (t : Pmap_raw A) :
-  Pmap_wf t → Pmap_wf (Ppartial_alter_raw f i t).
-Proof.
-  revert i; induction t as [|o l IHl r IHr]; intros i ?; simpl.
-  - destruct (f None); auto using Psingleton_wf.
-  - destruct i; simpl; eauto.
-Qed.
-Lemma Pfmap_wf {A B} (f : A → B) t : Pmap_wf t → Pmap_wf (Pfmap_raw f t).
-Proof.
-  induction t as [|[x|] [] ? [] ?]; simpl in *; rewrite ?andb_True; intuition.
-Qed.
-Lemma Pomap_wf {A B} (f : A → option B) t : Pmap_wf t → Pmap_wf (Pomap_raw f t).
-Proof. induction t; simpl; eauto. Qed.
-Lemma Pmerge_wf {A B C} (f : option A → option B → option C) t1 t2 :
-  Pmap_wf t1 → Pmap_wf t2 → Pmap_wf (Pmerge_raw f t1 t2).
-Proof. revert t2. induction t1; intros []; simpl; eauto using Pomap_wf. Qed.
-
-Lemma Plookup_empty {A} i : (∅ : Pmap_raw A) !! i = None.
-Proof. by destruct i. Qed.
-Lemma Plookup_singleton {A} i (x : A) : Psingleton_raw i x !! i = Some x.
-Proof. by induction i. Qed.
-Lemma Plookup_singleton_ne {A} i j (x : A) :
-  i ≠ j → Psingleton_raw i x !! j = None.
-Proof. revert j. induction i; intros [?|?|]; simpl; auto with congruence. Qed.
-Lemma Plookup_alter {A} f i (t : Pmap_raw A) :
-  Ppartial_alter_raw f i t !! i = f (t !! i).
-Proof.
-  revert i; induction t as [|o l IHl r IHr]; intros i; simpl.
-  - by destruct (f None); rewrite ?Plookup_singleton.
-  - destruct i; simpl; rewrite PNode_lookup; simpl; auto.
-Qed.
-Lemma Plookup_alter_ne {A} f i j (t : Pmap_raw A) :
-  i ≠ j → Ppartial_alter_raw f i t !! j = t !! j.
-Proof.
-  revert i j; induction t as [|o l IHl r IHr]; simpl.
-  - by intros; destruct (f None); rewrite ?Plookup_singleton_ne.
-  - by intros [?|?|] [?|?|] ?; simpl; rewrite ?PNode_lookup; simpl; auto.
-Qed.
-Lemma Plookup_fmap {A B} (f : A → B) t i : (Pfmap_raw f t) !! i = f <$> t !! i.
-Proof. revert i. by induction t; intros [?|?|]; simpl. Qed.
-Lemma Pelem_of_to_list {A} (t : Pmap_raw A) j i acc x :
-  (i,x) ∈ Pto_list_raw j t acc ↔
-    (∃ i', i = i' ++ Preverse j ∧ t !! i' = Some x) ∨ (i,x) ∈ acc.
-Proof.
-  split.
-  { revert j acc. induction t as [|[y|] l IHl r IHr]; intros j acc; simpl.
-    - by right.
-    - rewrite elem_of_cons. intros [?|?]; simplify_eq.
-      { left; exists 1. by rewrite (left_id_L 1 (++))%positive. }
-      destruct (IHl (j~0) (Pto_list_raw j~1 r acc)) as [(i'&->&?)|?]; auto.
-      { left; exists (i' ~ 0). by rewrite Preverse_xO, (assoc_L _). }
-      destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
-      left; exists (i' ~ 1). by rewrite Preverse_xI, (assoc_L _).
-    - intros.
-      destruct (IHl (j~0) (Pto_list_raw j~1 r acc)) as [(i'&->&?)|?]; auto.
-      { left; exists (i' ~ 0). by rewrite Preverse_xO, (assoc_L _). }
-      destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
-      left; exists (i' ~ 1). by rewrite Preverse_xI, (assoc_L _). }
-  revert t j i acc. assert (∀ t j i acc,
-    (i, x) ∈ acc → (i, x) ∈ Pto_list_raw j t acc) as help.
-  { intros t; induction t as [|[y|] l IHl r IHr]; intros j i acc;
-      simpl; rewrite ?elem_of_cons; auto. }
-  intros t j ? acc [(i&->&Hi)|?]; [|by auto]. revert j i acc Hi.
-  induction t as [|[y|] l IHl r IHr]; intros j i acc ?; simpl.
-  - done.
-  - rewrite elem_of_cons. destruct i as [i|i|]; simplify_eq/=.
-    + right. apply help. specialize (IHr (j~1) i).
-      rewrite Preverse_xI, (assoc_L _) in IHr. by apply IHr.
-    + right. specialize (IHl (j~0) i).
-      rewrite Preverse_xO, (assoc_L _) in IHl. by apply IHl.
-    + left. by rewrite (left_id_L 1 (++))%positive.
-  - destruct i as [i|i|]; simplify_eq/=.
-    + apply help. specialize (IHr (j~1) i).
-      rewrite Preverse_xI, (assoc_L _) in IHr. by apply IHr.
-    + specialize (IHl (j~0) i).
-      rewrite Preverse_xO, (assoc_L _) in IHl. by apply IHl.
-Qed.
-Lemma Pto_list_nodup {A} j (t : Pmap_raw A) acc :
-  (∀ i x, (i ++ Preverse j, x) ∈ acc → t !! i = None) →
-  NoDup acc → NoDup (Pto_list_raw j t acc).
-Proof.
-  revert j acc. induction t as [|[y|] l IHl r IHr]; simpl; intros j acc Hin ?.
-  - done.
-  - repeat constructor.
-    { rewrite Pelem_of_to_list. intros [(i&Hi&?)|Hj].
-      { apply (f_equal Plength) in Hi.
-        rewrite Preverse_xO, !Papp_length in Hi; simpl in *; lia. }
-      rewrite Pelem_of_to_list in Hj. destruct Hj as [(i&Hi&?)|Hj].
-      { apply (f_equal Plength) in Hi.
-        rewrite Preverse_xI, !Papp_length in Hi; simpl in *; lia. }
-      specialize (Hin 1 y). rewrite (left_id_L 1 (++))%positive in Hin.
-      discriminate (Hin Hj). }
-    apply IHl.
-    { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
-      + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
-        by apply (inj (.++ _)) in Hi.
-      + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
-    apply IHr; auto. intros i x Hi.
-    apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
-  - apply IHl.
-    { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
-      + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
-        by apply (inj (.++ _)) in Hi.
-      + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
-    apply IHr; auto. intros i x Hi.
-    apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
-Qed.
-Lemma Pomap_lookup {A B} (f : A → option B) t i :
-  Pomap_raw f t !! i = t !! i ≫= f.
-Proof.
-  revert i. induction t as [|o l IHl r IHr]; intros [i|i|]; simpl;
-    rewrite ?PNode_lookup; simpl; auto.
-Qed.
-Lemma Pmerge_lookup {A B C} (f : option A → option B → option C)
-    (Hf : f None None = None) t1 t2 i :
-  Pmerge_raw f t1 t2 !! i = f (t1 !! i) (t2 !! i).
-Proof.
-  revert t2 i; induction t1 as [|o1 l1 IHl1 r1 IHr1]; intros t2 i; simpl.
-  { rewrite Pomap_lookup. by destruct (t2 !! i). }
-  unfold compose, flip.
-  destruct t2 as [|l2 o2 r2]; rewrite PNode_lookup.
-  - by destruct i; rewrite ?Pomap_lookup; simpl; rewrite ?Pomap_lookup;
-      match goal with |- ?o ≫= _ = _ => destruct o end.
-  - destruct i; rewrite ?Pomap_lookup; simpl; auto.
-Qed.
-
-(** Packed version and instance of the finite map type class *)
-Inductive Pmap (A : Type) : Type :=
-  PMap { pmap_car : Pmap_raw A; pmap_prf : Pmap_wf pmap_car }.
-Arguments PMap {_} _ _ : assert.
-Arguments pmap_car {_} _ : assert.
-Arguments pmap_prf {_} _ : assert.
-Lemma Pmap_eq {A} (m1 m2 : Pmap A) : m1 = m2 ↔ pmap_car m1 = pmap_car m2.
-Proof.
-  split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
-  simplify_eq/=; f_equal; apply proof_irrel.
-Qed.
-Instance Pmap_eq_dec `{EqDecision A} : EqDecision (Pmap A) := λ m1 m2,
-  match Pmap_raw_eq_dec (pmap_car m1) (pmap_car m2) with
-  | left H => left (proj2 (Pmap_eq m1 m2) H)
-  | right H => right (H ∘ proj1 (Pmap_eq m1 m2))
-  end.
-Instance Pempty {A} : Empty (Pmap A) := PMap ∅ I.
-Instance Plookup {A} : Lookup positive A (Pmap A) := λ i m, pmap_car m !! i.
-Instance Ppartial_alter {A} : PartialAlter positive A (Pmap A) := λ f i m,
-  let (t,Ht) := m in PMap (partial_alter f i t) (Ppartial_alter_wf f i _ Ht).
-Instance Pfmap : FMap Pmap := λ A B f m,
-  let (t,Ht) := m in PMap (f <$> t) (Pfmap_wf f _ Ht).
-Instance Pto_list {A} : FinMapToList positive A (Pmap A) := λ m,
-  let (t,Ht) := m in Pto_list_raw 1 t [].
-Instance Pomap : OMap Pmap := λ A B f m,
-  let (t,Ht) := m in PMap (omap f t) (Pomap_wf f _ Ht).
-Instance Pmerge : Merge Pmap := λ A B C f m1 m2,
-  let (t1,Ht1) := m1 in let (t2,Ht2) := m2 in PMap _ (Pmerge_wf f _ _ Ht1 Ht2).
-
-Instance Pmap_finmap : FinMap positive Pmap.
-Proof.
-  split.
-  - by intros ? [t1 ?] [t2 ?] ?; apply Pmap_eq, Pmap_wf_eq.
-  - by intros ? [].
-  - intros ?? [??] ?. by apply Plookup_alter.
-  - intros ?? [??] ??. by apply Plookup_alter_ne.
-  - intros ??? [??]. by apply Plookup_fmap.
-  - intros ? [??]. apply Pto_list_nodup; [|constructor].
-    intros ??. by rewrite elem_of_nil.
-  - intros ? [??] i x; unfold map_to_list, Pto_list.
-    rewrite Pelem_of_to_list, elem_of_nil.
-    split. by intros [(?&->&?)|]. by left; exists i.
-  - intros ?? ? [??] ?. by apply Pomap_lookup.
-  - intros ??? ?? [??] [??] ?. by apply Pmerge_lookup.
-Qed.
-
-Program Instance Pmap_countable `{Countable A} : Countable (Pmap A) := {
-  encode m := encode (map_to_list m : list (positive * A));
-  decode p := list_to_map <$> decode p
-}.
-Next Obligation.
-  intros A ?? m; simpl. rewrite decode_encode; simpl. by rewrite list_to_map_to_list.
-Qed.
-
-(** * Finite sets *)
-(** We construct sets of [positives]s satisfying extensional equality. *)
-Notation Pset := (mapset Pmap).
-Instance Pmap_dom {A} : Dom (Pmap A) Pset := mapset_dom.
-Instance Pmap_dom_spec : FinMapDom positive Pmap Pset := mapset_dom_spec.

theories/strings.v

-From Coq Require Import Ascii.
-From Coq Require Export String.
-From stdpp Require Export list.
-From stdpp Require Import countable.
-Set Default Proof Using "Type".
-
-(* To avoid randomly ending up with String.length because this module is
-imported hereditarily somewhere. *)
-Notation length := List.length.
-
-(** * Fix scopes *)
-Open Scope string_scope.
-(* Make sure [list_scope] has priority over [string_scope], so that
-   the "++" notation designates list concatenation. *)
-Open Scope list_scope.
-Infix "+:+" := String.append (at level 60, right associativity) : stdpp_scope.
-Arguments String.append : simpl never.
-
-(** * Decision of equality *)
-Instance ascii_eq_dec : EqDecision ascii := ascii_dec.
-Instance string_eq_dec : EqDecision string.
-Proof. solve_decision. Defined.
-Instance string_app_inj : Inj (=) (=) (String.append s1).
-Proof. intros s1 ???. induction s1; simplify_eq/=; f_equal/=; auto. Qed.
-
-Instance string_inhabited : Inhabited string := populate "".
-
-(* Reverse *)
-Fixpoint string_rev_app (s1 s2 : string) : string :=
-  match s1 with
-  | "" => s2
-  | String a s1 => string_rev_app s1 (String a s2)
-  end.
-Definition string_rev (s : string) : string := string_rev_app s "".
-
-Definition is_nat (x : ascii) : option nat :=
-  match x with
-  | "0" => Some 0
-  | "1" => Some 1
-  | "2" => Some 2
-  | "3" => Some 3
-  | "4" => Some 4
-  | "5" => Some 5
-  | "6" => Some 6
-  | "7" => Some 7
-  | "8" => Some 8
-  | "9" => Some 9
-  | _ => None
-  end%char.
-
-(* Break a string up into lists of words, delimited by white space *)
-Definition is_space (x : Ascii.ascii) : bool :=
-  match x with
-  | "009" | "010" | "011" | "012" | "013" | " " => true | _ => false
-  end%char.
-
-Fixpoint words_go (cur : option string) (s : string) : list string :=
-  match s with
-  | "" => option_list (string_rev <$> cur)
-  | String a s =>
-     if is_space a then option_list (string_rev <$> cur) ++ words_go None s
-     else words_go (Some (from_option (String a) (String a "") cur)) s
-  end.
-Definition words : string → list string := words_go None.
-
-Ltac words s :=
-  match type of s with
-  | list string => s
-  | string => eval vm_compute in (words s)
-  end.
-
-(** * Encoding and decoding *)
-(** In order to reuse or existing implementation of radix-2 search trees over
-positive binary naturals [positive], we define an injection [string_to_pos]
-from [string] into [positive]. *)
-Fixpoint digits_to_pos (βs : list bool) : positive :=
-  match βs with
-  | [] => xH
-  | false :: βs => (digits_to_pos βs)~0
-  | true :: βs => (digits_to_pos βs)~1
-  end%positive.
-Definition ascii_to_digits (a : Ascii.ascii) : list bool :=
-  match a with
-  | Ascii.Ascii β1 β2 β3 β4 β5 β6 β7 β8 => [β1;β2;β3;β4;β5;β6;β7;β8]
-  end.
-Fixpoint string_to_pos (s : string) : positive :=
-  match s with
-  | EmptyString => xH
-  | String a s => string_to_pos s ++ digits_to_pos (ascii_to_digits a)
-  end%positive.
-Fixpoint digits_of_pos (p : positive) : list bool :=
-  match p with
-  | xH => []
-  | p~0 => false :: digits_of_pos p
-  | p~1 => true :: digits_of_pos p
-  end%positive.
-Fixpoint ascii_of_digits (βs : list bool) : ascii :=
-  match βs with
-  | [] => zero
-  | β :: βs => Ascii.shift β (ascii_of_digits βs)
-  end.
-Fixpoint string_of_digits (βs : list bool) : string :=
-  match βs with
-  | β1 :: β2 :: β3 :: β4 :: β5 :: β6 :: β7 :: β8 :: βs =>
-     String (ascii_of_digits [β1;β2;β3;β4;β5;β6;β7;β8]) (string_of_digits βs)
-  | _ => EmptyString
-  end.
-Definition string_of_pos (p : positive) : string :=
-  string_of_digits (digits_of_pos p).
-Lemma string_of_to_pos s : string_of_pos (string_to_pos s) = s.
-Proof.
-  unfold string_of_pos. by induction s as [|[[][][][][][][][]]]; f_equal/=.
-Qed.
-Program Instance string_countable : Countable string := {|
-  encode := string_to_pos; decode p := Some (string_of_pos p)
-|}.
-Solve Obligations with naive_solver eauto using string_of_to_pos with f_equal.
-Lemma ascii_of_to_digits a : ascii_of_digits (ascii_to_digits a) = a.
-Proof. by destruct a as [[][][][][][][][]]. Qed.
-Instance ascii_countable : Countable ascii :=
-  inj_countable' ascii_to_digits ascii_of_digits ascii_of_to_digits.