Compare revisions

39860d00 · 39860d00 · 39860d00 · 39860d00 · 39860d00 · 39860d00
--- a/theories/relations.v
+++ b/theories/relations.v
 (** This file collects definitions and theorems on abstract rewriting systems.
 These are particularly useful as we define the operational semantics as a
 small step semantics. *)
-From Coq Require Import Wf_nat.
+From stdpp Require Export sets well_founded.
-From stdpp Require Export sets.
 From stdpp Require Import options.
 (** * Definitions *)
@@ -75,14 +74,15 @@ Definition confluent {A} (R : relation A) :=
 Definition locally_confluent {A} (R : relation A) :=
  ∀ x y1 y2, R x y1 → R x y2 → ∃ z, rtc R y1 z ∧ rtc R y2 z.
-Hint Unfold nf red : core.
+Global Hint Unfold nf red : core.
 (** * General theorems *)
-Section closure.
+Section general.
  Context `{R : relation A}.
-  Hint Constructors rtc nsteps bsteps tc : core.
+  Local Hint Constructors rtc nsteps bsteps tc : core.
+  (** ** Results about the reflexive-transitive closure [rtc] *)
  Lemma rtc_transitive x y z : rtc R x y → rtc R y z → rtc R x z.
  Proof. induction 1; eauto. Qed.
@@ -110,7 +110,7 @@ Section closure.
  Lemma rtc_r x y z : rtc R x y → R y z → rtc R x z.
  Proof. intros. etrans; eauto. Qed.
  Lemma rtc_inv x z : rtc R x z → x = z ∨ ∃ y, R x y ∧ rtc R y z.
-  Proof. inversion_clear 1; eauto. Qed.
+  Proof. inv 1; eauto. Qed.
  Lemma rtc_ind_l (P : A → Prop) (z : A)
    (Prefl : P z) (Pstep : ∀ x y, R x y → rtc R y z → P y → P x) :
    ∀ x, rtc R x z → P x.
@@ -139,62 +139,56 @@ Section closure.
    (∀ x y, R x y → R' (f x) (f y)) → rtc R x y → rtc R' (f x) (f y).
  Proof. induction 2; econstructor; eauto. Qed.
+  (** ** Results about [nsteps] *)
  Lemma nsteps_once x y : R x y → nsteps R 1 x y.
  Proof. eauto. Qed.
  Lemma nsteps_once_inv x y : nsteps R 1 x y → R x y.
-  Proof. inversion 1 as [|???? Hhead Htail]; inversion Htail; by subst. Qed.
+  Proof. inv 1 as [|???? Hhead Htail]; by inv Htail. Qed.
  Lemma nsteps_trans n m x y z :
    nsteps R n x y → nsteps R m y z → nsteps R (n + m) x z.
  Proof. induction 1; simpl; eauto. Qed.
  Lemma nsteps_r n x y z : nsteps R n x y → R y z → nsteps R (S n) x z.
  Proof. induction 1; eauto. Qed.
-  Lemma nsteps_rtc n x y : nsteps R n x y → rtc R x y.
-  Proof. induction 1; eauto. Qed.
-  Lemma rtc_nsteps x y : rtc R x y → ∃ n, nsteps R n x y.
-  Proof. induction 1; firstorder eauto. Qed.
-  Lemma nsteps_plus_inv n m x z :
+  Lemma nsteps_add_inv n m x z :
    nsteps R (n + m) x z → ∃ y, nsteps R n x y ∧ nsteps R m y z.
  Proof.
    revert x.
    induction n as [|n IH]; intros x Hx; simpl; [by eauto|].
-    inversion Hx; naive_solver.
+    inv Hx; naive_solver.
  Qed.
  Lemma nsteps_inv_r n x z : nsteps R (S n) x z → ∃ y, nsteps R n x y ∧ R y z.
  Proof.
    rewrite <- PeanoNat.Nat.add_1_r.
-    intros (?&?&?%nsteps_once_inv)%nsteps_plus_inv; eauto.
+    intros (?&?&?%nsteps_once_inv)%nsteps_add_inv; eauto.
  Qed.
  Lemma nsteps_congruence {B} (f : A → B) (R' : relation B) n x y :
    (∀ x y, R x y → R' (f x) (f y)) → nsteps R n x y → nsteps R' n (f x) (f y).
  Proof. induction 2; econstructor; eauto. Qed.
+  (** ** Results about [bsteps] *)
  Lemma bsteps_once n x y : R x y → bsteps R (S n) x y.
  Proof. eauto. Qed.
-  Lemma bsteps_plus_r n m x y :
+  Lemma bsteps_add_r n m x y :
    bsteps R n x y → bsteps R (n + m) x y.
  Proof. induction 1; simpl; eauto. Qed.
  Lemma bsteps_weaken n m x y :
    n ≤ m → bsteps R n x y → bsteps R m x y.
  Proof.
-    intros. rewrite (Minus.le_plus_minus n m); auto using bsteps_plus_r.
+    intros. rewrite (Nat.le_add_sub n m); auto using bsteps_add_r.
  Qed.
-  Lemma bsteps_plus_l n m x y :
+  Lemma bsteps_add_l n m x y :
    bsteps R n x y → bsteps R (m + n) x y.
  Proof. apply bsteps_weaken. auto with arith. Qed.
  Lemma bsteps_S n x y :  bsteps R n x y → bsteps R (S n) x y.
  Proof. apply bsteps_weaken. lia. Qed.
  Lemma bsteps_trans n m x y z :
    bsteps R n x y → bsteps R m y z → bsteps R (n + m) x z.
-  Proof. induction 1; simpl; eauto using bsteps_plus_l. Qed.
+  Proof. induction 1; simpl; eauto using bsteps_add_l. Qed.
  Lemma bsteps_r n x y z : bsteps R n x y → R y z → bsteps R (S n) x z.
  Proof. induction 1; eauto. Qed.
-  Lemma bsteps_rtc n x y : bsteps R n x y → rtc R x y.
-  Proof. induction 1; eauto. Qed.
-  Lemma rtc_bsteps x y : rtc R x y → ∃ n, bsteps R n x y.
-  Proof. induction 1; [exists 0; constructor|]. naive_solver eauto. Qed.
  Lemma bsteps_ind_r (P : nat → A → Prop) (x : A)
    (Prefl : ∀ n, P n x)
    (Pstep : ∀ n y z, bsteps R n x y → R y z → P n y → P (S n) z) :
@@ -216,6 +210,7 @@ Section closure.
    (∀ x y, R x y → R' (f x) (f y)) → bsteps R n x y → bsteps R' n (f x) (f y).
  Proof. induction 2; econstructor; eauto. Qed.
+  (** ** Results about the transitive closure [tc] *)
  Lemma tc_transitive x y z : tc R x y → tc R y z → tc R x z.
  Proof. induction 1; eauto. Qed.
  Global Instance tc_transitive' : Transitive (tc R).
@@ -229,10 +224,18 @@ Section closure.
  Lemma tc_rtc x y : tc R x y → rtc R x y.
  Proof. induction 1; eauto. Qed.
+  Lemma red_tc x : red (tc R) x ↔ red R x.
+  Proof.
+    split.
+    - intros [y []]; eexists; eauto.
+    - intros [y HR]. exists y. by apply tc_once.
+  Qed.
  Lemma tc_congruence {B} (f : A → B) (R' : relation B) x y :
    (∀ x y, R x y → R' (f x) (f y)) → tc R x y → tc R' (f x) (f y).
  Proof. induction 2; econstructor; by eauto. Qed.
+  (** ** Results about the symmetric closure [sc] *)
  Global Instance sc_symmetric : Symmetric (sc R).
  Proof. unfold Symmetric, sc. naive_solver. Qed.
@@ -245,11 +248,120 @@ Section closure.
    (∀ x y, R x y → R' (f x) (f y)) → sc R x y → sc R' (f x) (f y).
  Proof. induction 2; econstructor; by eauto. Qed.
-End closure.
+  (** ** Equivalences between closure operators *)
+  Lemma bsteps_nsteps n x y : bsteps R n x y ↔ ∃ n', n' ≤ n ∧ nsteps R n' x y.
+  Proof.
+    split.
+    - induction 1 as [|n x1 x2 y ?? (n'&?&?)].
+      + exists 0; naive_solver eauto with lia.
+      + exists (S n'); naive_solver eauto with lia.
+    - intros (n'&Hn'&Hsteps). apply bsteps_weaken with n'; [done|].
+      clear Hn'. induction Hsteps; eauto.
+  Qed.
+  Lemma tc_nsteps x y : tc R x y ↔ ∃ n, 0 < n ∧ nsteps R n x y.
+  Proof.
+    split.
+    - induction 1 as [|x1 x2 y ?? (n&?&?)].
+      { exists 1. eauto using nsteps_once with lia. }
+      exists (S n); eauto using nsteps_l.
+    - intros (n & ? & Hstep). induction Hstep as [|n x1 x2 y ? Hstep]; [lia|].
+      destruct Hstep; eauto with lia.
+  Qed.
+  Lemma rtc_tc x y : rtc R x y ↔ x = y ∨ tc R x y.
+  Proof.
+    split; [|naive_solver eauto using tc_rtc].
+    induction 1; naive_solver.
+  Qed.
+  Lemma rtc_nsteps x y : rtc R x y ↔ ∃ n, nsteps R n x y.
+  Proof.
+    split.
+    - induction 1; naive_solver.
+    - intros [n Hsteps]. induction Hsteps; naive_solver.
+  Qed.
+  Lemma rtc_nsteps_1 x y : rtc R x y → ∃ n, nsteps R n x y.
+  Proof. rewrite rtc_nsteps. naive_solver. Qed.
+  Lemma rtc_nsteps_2 n x y : nsteps R n x y → rtc R x y.
+  Proof. rewrite rtc_nsteps. naive_solver. Qed.
+  Lemma rtc_bsteps x y : rtc R x y ↔ ∃ n, bsteps R n x y.
+  Proof. rewrite rtc_nsteps. setoid_rewrite bsteps_nsteps. naive_solver. Qed.
+  Lemma rtc_bsteps_1 x y : rtc R x y → ∃ n, bsteps R n x y.
+  Proof. rewrite rtc_bsteps. naive_solver. Qed.
+  Lemma rtc_bsteps_2 n x y : bsteps R n x y → rtc R x y.
+  Proof. rewrite rtc_bsteps. naive_solver. Qed.
+  Lemma nsteps_list n x y :
+    nsteps R n x y ↔ ∃ l,
+      length l = S n ∧
+      head l = Some x ∧
+      last l = Some y ∧
+      ∀ i a b, l !! i = Some a → l !! S i = Some b → R a b.
+  Proof.
+    setoid_rewrite head_lookup. split.
+    - induction 1 as [x|n' x x' y ?? IH].
+      { exists [x]; naive_solver. }
+      destruct IH as (l & Hlen & Hfirst & Hlast & Hcons).
+      exists (x :: l). simpl. rewrite Hlen, last_cons, Hlast.
+      split_and!; [done..|]. intros [|i]; naive_solver.
+    - intros ([|x' l]&?&Hfirst&Hlast&Hcons); simplify_eq/=.
+      revert x Hlast Hcons.
+      induction l as [|x1 l IH]; intros x2 Hlast Hcons; simplify_eq/=; [constructor|].
+      econstructor; [by apply (Hcons 0)|].
+      apply IH; [done|]. intros i. apply (Hcons (S i)).
+  Qed.
+  Lemma bsteps_list n x y :
+    bsteps R n x y ↔ ∃ l,
+      length l ≤ S n ∧
+      head l = Some x ∧
+      last l = Some y ∧
+      ∀ i a b, l !! i = Some a → l !! S i = Some b → R a b.
+  Proof.
+    rewrite bsteps_nsteps. split.
+    - intros (n'&?&(l&?&?&?&?)%nsteps_list). exists l; eauto with lia.
+    - intros (l&?&?&?&?). exists (pred (length l)). split; [lia|].
+      apply nsteps_list. exists l. split; [|by eauto]. by destruct l.
+  Qed.
+  Lemma rtc_list x y :
+    rtc R x y ↔ ∃ l,
+      head l = Some x ∧
+      last l = Some y ∧
+      ∀ i a b, l !! i = Some a → l !! S i = Some b → R a b.
+  Proof.
+    rewrite rtc_bsteps. split.
+    - intros (n'&(l&?&?&?&?)%bsteps_list). exists l; eauto with lia.
+    - intros (l&?&?&?). exists (pred (length l)).
+      apply bsteps_list. exists l. eauto with lia.
+  Qed.
-Section more_closure.
+  Lemma tc_list x y :
+    tc R x y ↔ ∃ l,
+      1 < length l ∧
+      head l = Some x ∧
+      last l = Some y ∧
+      ∀ i a b, l !! i = Some a → l !! S i = Some b → R a b.
+  Proof.
+    rewrite tc_nsteps. split.
+    - intros (n'&?&(l&?&?&?&?)%nsteps_list). exists l; eauto with lia.
+    - intros (l&?&?&?&?). exists (pred (length l)).
+      split; [lia|]. apply nsteps_list. exists l. eauto with lia.
+  Qed.
+  Lemma ex_loop_inv x :
+    ex_loop R x →
+    ∃ x', R x x' ∧ ex_loop R x'.
+  Proof. inv 1; eauto. Qed.
+End general.
+Section more_general.
  Context `{R : relation A}.
+  (** ** Results about the reflexive-transitive-symmetric closure [rtsc] *)
  Global Instance rtsc_equivalence : Equivalence (rtsc R) | 10.
  Proof. apply rtc_equivalence, _. Qed.
@@ -266,12 +378,27 @@ Section more_closure.
    (∀ x y, R x y → R' (f x) (f y)) → rtsc R x y → rtsc R' (f x) (f y).
  Proof. unfold rtsc; eauto using rtc_congruence, sc_congruence. Qed.
-End more_closure.
+  Lemma ex_loop_tc x :
+    ex_loop (tc R) x ↔ ex_loop R x.
+  Proof.
+    split.
+    - revert x; cofix IH.
+      intros x (y & Hstep & Hloop')%ex_loop_inv.
+      destruct Hstep as [x y Hstep|x y z Hstep Hsteps].
+      + econstructor; eauto.
+      + econstructor; [by eauto|].
+        eapply IH. econstructor; eauto.
+    - revert x; cofix IH.
+      intros x (y & Hstep & Hloop')%ex_loop_inv.
+      econstructor; eauto using tc_once.
+  Qed.
+End more_general.
 Section properties.
  Context `{R : relation A}.
-  Hint Constructors rtc nsteps bsteps tc : core.
+  Local Hint Constructors rtc nsteps bsteps tc : core.
  Lemma nf_wn x : nf R x → wn R x.
  Proof. intros. exists x; eauto. Qed.
@@ -297,8 +424,8 @@ Section properties.
    constructor; simpl; intros x' Hxx'.
    assert (x' ∈ xs) as (xs1&xs2&->)%elem_of_list_split by eauto using tc_once.
    refine (IH (length xs1 + length xs2) _ _ (xs1 ++ xs2) _ _);
-      [rewrite app_length; simpl; lia..|].
+      [rewrite length_app; simpl; lia..|].
-    intros x'' Hx'x''. feed pose proof (Hfin x'') as Hx''; [by econstructor|].
+    intros x'' Hx'x''. opose proof* (Hfin x'') as Hx''; [by econstructor|].
    cut (x' ≠ x''); [set_solver|].
    intros ->. by apply (Hirr x'').
  Qed.
@@ -398,50 +525,3 @@ Section subrel.
  Lemma rtc_subrel x y : subrel → rtc R1 x y → rtc R2 x y.
  Proof. induction 2; [by apply rtc_refl|]. eapply rtc_l; eauto. Qed.
 End subrel.
-(** * Theorems on well founded relations *)
-Lemma Acc_impl {A} (R1 R2 : relation A) x :
-  Acc R1 x → (∀ y1 y2, R2 y1 y2 → R1 y1 y2) → Acc R2 x.
-Proof. induction 1; constructor; naive_solver. Qed.
-Notation wf := well_founded.
-Definition wf_guard `{R : relation A} (n : nat) (wfR : wf R) : wf R :=
-  Acc_intro_generator n wfR.
-(* Generally we do not want [wf_guard] to be expanded (neither by tactics,
-nor by conversion tests in the kernel), but in some cases we do need it for
-computation (that is, we cannot make it opaque). We use the [Strategy]
-command to make its expanding behavior less eager. *)
-Strategy 100 [wf_guard].
-Lemma wf_projected `{R1 : relation A} `(R2 : relation B) (f : A → B) :
-  (∀ x y, R1 x y → R2 (f x) (f y)) →
-  wf R2 → wf R1.
-Proof.
-  intros Hf Hwf.
-  cut (∀ y, Acc R2 y → ∀ x, y = f x → Acc R1 x).
-  { intros aux x. apply (aux (f x)); auto. }
-  induction 1 as [y _ IH]. intros x ?. subst.
-  constructor. intros y ?. apply (IH (f y)); auto.
-Qed.
-Lemma Fix_F_proper `{R : relation A} (B : A → Type) (E : ∀ x, relation (B x))
-    (F : ∀ x, (∀ y, R y x → B y) → B x)
-    (HF : ∀ (x : A) (f g : ∀ y, R y x → B y),
-      (∀ y Hy Hy', E _ (f y Hy) (g y Hy')) → E _ (F x f) (F x g))
-    (x : A) (acc1 acc2 : Acc R x) :
-  E _ (Fix_F B F acc1) (Fix_F B F acc2).
-Proof. revert x acc1 acc2. fix FIX 2. intros x [acc1] [acc2]; simpl; auto. Qed.
-Lemma Fix_unfold_rel `{R : relation A} (wfR : wf R) (B : A → Type) (E : ∀ x, relation (B x))
-    (F: ∀ x, (∀ y, R y x → B y) → B x)
-    (HF: ∀ (x: A) (f g: ∀ y, R y x → B y),
-           (∀ y Hy Hy', E _ (f y Hy) (g y Hy')) → E _ (F x f) (F x g))
-    (x: A) :
-  E _ (Fix wfR B F x) (F x (λ y _, Fix wfR B F y)).
-Proof.
-  unfold Fix.
-  destruct (wfR x); simpl.
-  apply HF; intros.
-  apply Fix_F_proper; auto.
-Qed.
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -2,6 +2,7 @@
 importantly, it implements some tactics to automatically solve goals involving
 sets. *)
 From stdpp Require Export orders list list_numbers.
+From stdpp Require Import finite.
 From stdpp Require Import options.
 (* FIXME: This file needs a 'Proof Using' hint, but they need to be set
@@ -10,13 +11,13 @@ Unset Default Proof Using.
 (* Higher precedence to make sure these instances are not used for other types
 with an [ElemOf] instance, such as lists. *)
-Instance set_equiv `{ElemOf A C} : Equiv C | 20 := λ X Y,
+Global Instance set_equiv_instance `{ElemOf A C} : Equiv C | 20 := λ X Y,
  ∀ x, x ∈ X ↔ x ∈ Y.
-Instance set_subseteq `{ElemOf A C} : SubsetEq C | 20 := λ X Y,
+Global Instance set_subseteq_instance `{ElemOf A C} : SubsetEq C | 20 := λ X Y,
  ∀ x, x ∈ X → x ∈ Y.
-Instance set_disjoint `{ElemOf A C} : Disjoint C | 20 := λ X Y,
+Global Instance set_disjoint_instance `{ElemOf A C} : Disjoint C | 20 := λ X Y,
  ∀ x, x ∈ X → x ∈ Y → False.
-Typeclasses Opaque set_equiv set_subseteq set_disjoint.
+Global Typeclasses Opaque set_equiv_instance set_subseteq_instance set_disjoint_instance.
 (** * Setoids *)
 Section setoids_simple.
@@ -45,6 +46,8 @@ Section setoids_simple.
  Proof.
    intros X1 X2 HX Y1 Y2 HY. apply forall_proper; intros x. by rewrite HX, HY.
  Qed.
+  Global Instance subset_proper : Proper ((≡@{C}) ==> (≡@{C}) ==> iff) (⊂).
+  Proof. solve_proper. Qed.
 End setoids_simple.
 Section setoids.
@@ -92,29 +95,29 @@ involving just [∈]. For example, [A → x ∈ X ∪ ∅] becomes [A → x ∈
 This transformation is implemented using type classes instead of setoid
 rewriting to ensure that we traverse each term at most once and to be able to
-deal with occurences of the set operations under binders. *)
+deal with occurrences of the set operations under binders. *)
 Class SetUnfold (P Q : Prop) := { set_unfold : P ↔ Q }.
-Arguments set_unfold _ _ {_} : assert.
+Global Arguments set_unfold _ _ {_} : assert.
-Hint Mode SetUnfold + - : typeclass_instances.
+Global Hint Mode SetUnfold + - : typeclass_instances.
 (** The class [SetUnfoldElemOf] is a more specialized version of [SetUnfold]
 for propositions of the shape [x ∈ X] to improve performance. *)
 Class SetUnfoldElemOf `{ElemOf A C} (x : A) (X : C) (Q : Prop) :=
  { set_unfold_elem_of : x ∈ X ↔ Q }.
-Arguments set_unfold_elem_of {_ _ _} _ _ _ {_} : assert.
+Global Arguments set_unfold_elem_of {_ _ _} _ _ _ {_} : assert.
-Hint Mode SetUnfoldElemOf + + + - + - : typeclass_instances.
+Global Hint Mode SetUnfoldElemOf + + + - + - : typeclass_instances.
-Instance set_unfold_elem_of_default `{ElemOf A C} (x : A) (X : C) :
+Global Instance set_unfold_elem_of_default `{ElemOf A C} (x : A) (X : C) :
  SetUnfoldElemOf x X (x ∈ X) | 1000.
 Proof. done. Qed.
-Instance set_unfold_elem_of_set_unfold `{ElemOf A C} (x : A) (X : C) Q :
+Global Instance set_unfold_elem_of_set_unfold `{ElemOf A C} (x : A) (X : C) Q :
  SetUnfoldElemOf x X Q → SetUnfold (x ∈ X) Q.
 Proof. by destruct 1; constructor. Qed.
 Class SetUnfoldSimpl (P Q : Prop) := { set_unfold_simpl : SetUnfold P Q }.
-Hint Extern 0 (SetUnfoldSimpl _ _) => csimpl; constructor : typeclass_instances.
+Global Hint Extern 0 (SetUnfoldSimpl _ _) => csimpl; constructor : typeclass_instances.
-Instance set_unfold_default P : SetUnfold P P | 1000. done. Qed.
+Global Instance set_unfold_default P : SetUnfold P P | 1000. done. Qed.
 Definition set_unfold_1 `{SetUnfold P Q} : P → Q := proj1 (set_unfold P Q).
 Definition set_unfold_2 `{SetUnfold P Q} : Q → P := proj2 (set_unfold P Q).
@@ -141,19 +144,19 @@ Proof. constructor. naive_solver. Qed.
 (* Avoid too eager application of the above instances (and thus too eager
 unfolding of type class transparent definitions). *)
-Hint Extern 0 (SetUnfold (_ → _) _) =>
+Global Hint Extern 0 (SetUnfold (_ → _) _) =>
  class_apply set_unfold_impl : typeclass_instances.
-Hint Extern 0 (SetUnfold (_ ∧ _) _) =>
+Global Hint Extern 0 (SetUnfold (_ ∧ _) _) =>
  class_apply set_unfold_and : typeclass_instances.
-Hint Extern 0 (SetUnfold (_ ∨ _) _) =>
+Global Hint Extern 0 (SetUnfold (_ ∨ _) _) =>
  class_apply set_unfold_or : typeclass_instances.
-Hint Extern 0 (SetUnfold (_ ↔ _) _) =>
+Global Hint Extern 0 (SetUnfold (_ ↔ _) _) =>
  class_apply set_unfold_iff : typeclass_instances.
-Hint Extern 0 (SetUnfold (¬ _) _) =>
+Global Hint Extern 0 (SetUnfold (¬ _) _) =>
  class_apply set_unfold_not : typeclass_instances.
-Hint Extern 1 (SetUnfold (∀ _, _) _) =>
+Global Hint Extern 1 (SetUnfold (∀ _, _) _) =>
  class_apply set_unfold_forall : typeclass_instances.
-Hint Extern 0 (SetUnfold (∃ _, _) _) =>
+Global Hint Extern 0 (SetUnfold (∃ _, _) _) =>
  class_apply set_unfold_exist : typeclass_instances.
 Section set_unfold_simple.
@@ -178,16 +181,16 @@ Section set_unfold_simple.
  Global Instance set_unfold_equiv_empty_l X (P : A → Prop) :
    (∀ x, SetUnfoldElemOf x X (P x)) → SetUnfold (∅ ≡ X) (∀ x, ¬P x) | 5.
  Proof.
-    intros ?; constructor. unfold equiv, set_equiv.
+    intros ?; constructor. unfold equiv, set_equiv_instance.
    pose proof (not_elem_of_empty (C:=C)); naive_solver.
  Qed.
  Global Instance set_unfold_equiv_empty_r (P : A → Prop) X :
    (∀ x, SetUnfoldElemOf x X (P x)) → SetUnfold (X ≡ ∅) (∀ x, ¬P x) | 5.
  Proof.
-    intros ?; constructor. unfold equiv, set_equiv.
+    intros ?; constructor. unfold equiv, set_equiv_instance.
    pose proof (not_elem_of_empty (C:=C)); naive_solver.
  Qed.
-  Global Instance set_unfold_equiv (P Q : A → Prop) X :
+  Global Instance set_unfold_equiv (P Q : A → Prop) X Y :
    (∀ x, SetUnfoldElemOf x X (P x)) → (∀ x, SetUnfoldElemOf x Y (Q x)) →
    SetUnfold (X ≡ Y) (∀ x, P x ↔ Q x) | 10.
  Proof. constructor. apply forall_proper; naive_solver. Qed.
@@ -195,7 +198,7 @@ Section set_unfold_simple.
    (∀ x, SetUnfoldElemOf x X (P x)) → (∀ x, SetUnfoldElemOf x Y (Q x)) →
    SetUnfold (X ⊆ Y) (∀ x, P x → Q x).
  Proof. constructor. apply forall_proper; naive_solver. Qed.
-  Global Instance set_unfold_subset (P Q : A → Prop) X :
+  Global Instance set_unfold_subset (P Q : A → Prop) X Y :
    (∀ x, SetUnfoldElemOf x X (P x)) → (∀ x, SetUnfoldElemOf x Y (Q x)) →
    SetUnfold (X ⊂ Y) ((∀ x, P x → Q x) ∧ ¬∀ x, Q x → P x).
  Proof.
@@ -205,7 +208,7 @@ Section set_unfold_simple.
  Global Instance set_unfold_disjoint (P Q : A → Prop) X Y :
    (∀ x, SetUnfoldElemOf x X (P x)) → (∀ x, SetUnfoldElemOf x Y (Q x)) →
    SetUnfold (X ## Y) (∀ x, P x → Q x → False).
-  Proof. constructor. unfold disjoint, set_disjoint. naive_solver. Qed.
+  Proof. constructor. unfold disjoint, set_disjoint_instance. naive_solver. Qed.
  Context `{!LeibnizEquiv C}.
  Global Instance set_unfold_equiv_same_L X : SetUnfold (X = X) True | 1.
@@ -243,7 +246,7 @@ Section set_unfold.
  Qed.
 End set_unfold.
-Instance set_unfold_top `{TopSet A C} (x : A) :
+Global Instance set_unfold_top `{TopSet A C} (x : A) :
  SetUnfoldElemOf x (⊤ : C) True.
 Proof. constructor. split; [done|intros; apply elem_of_top']. Qed.
@@ -253,15 +256,15 @@ Section set_unfold_monad.
  Global Instance set_unfold_ret {A} (x y : A) :
    SetUnfoldElemOf x (mret (M:=M) y) (x = y).
  Proof. constructor; apply elem_of_ret. Qed.
-  Global Instance set_unfold_bind {A B} (f : A → M B) X (P Q : A → Prop) :
+  Global Instance set_unfold_bind {A B} (f : A → M B) X (P Q : A → Prop) x :
    (∀ y, SetUnfoldElemOf y X (P y)) → (∀ y, SetUnfoldElemOf x (f y) (Q y)) →
    SetUnfoldElemOf x (X ≫= f) (∃ y, Q y ∧ P y).
  Proof. constructor. rewrite elem_of_bind; naive_solver. Qed.
-  Global Instance set_unfold_fmap {A B} (f : A → B) (X : M A) (P : A → Prop) :
+  Global Instance set_unfold_fmap {A B} (f : A → B) (X : M A) (P : A → Prop) x :
    (∀ y, SetUnfoldElemOf y X (P y)) →
    SetUnfoldElemOf x (f <$> X) (∃ y, x = f y ∧ P y).
  Proof. constructor. rewrite elem_of_fmap; naive_solver. Qed.
-  Global Instance set_unfold_join {A} (X : M (M A)) (P : M A → Prop) :
+  Global Instance set_unfold_join {A} (X : M (M A)) (P : M A → Prop) x :
    (∀ Y, SetUnfoldElemOf Y X (P Y)) →
    SetUnfoldElemOf x (mjoin X) (∃ Y, x ∈ Y ∧ P Y).
  Proof. constructor. rewrite elem_of_join; naive_solver. Qed.
@@ -284,6 +287,15 @@ Section set_unfold_list.
    intros ??; constructor.
    by rewrite elem_of_app, (set_unfold_elem_of x l P), (set_unfold_elem_of x k Q).
  Qed.
+  Global Instance set_unfold_list_cprod {B} (x : A * B) l (k : list B) P Q :
+    SetUnfoldElemOf x.1 l P → SetUnfoldElemOf x.2 k Q →
+    SetUnfoldElemOf x (cprod l k) (P ∧ Q).
+  Proof.
+    intros ??; constructor.
+    by rewrite elem_of_list_cprod, (set_unfold_elem_of x.1 l P),
+      (set_unfold_elem_of x.2 k Q).
+  Qed.
  Global Instance set_unfold_included l k (P Q : A → Prop) :
    (∀ x, SetUnfoldElemOf x l (P x)) → (∀ x, SetUnfoldElemOf x k (Q x)) →
    SetUnfold (l ⊆ k) (∀ x, P x → Q x).
@@ -296,17 +308,21 @@ Section set_unfold_list.
    SetUnfoldElemOf x l P → SetUnfoldElemOf x (reverse l) P.
  Proof. constructor. by rewrite elem_of_reverse, (set_unfold_elem_of x l P). Qed.
-  Global Instance set_unfold_list_fmap {B} (f : A → B) l P :
+  Global Instance set_unfold_list_fmap {B} (f : A → B) l P y :
-    (∀ y, SetUnfoldElemOf y l (P y)) →
+    (∀ x, SetUnfoldElemOf x l (P x)) →
-    SetUnfoldElemOf x (f <$> l) (∃ y, x = f y ∧ P y).
+    SetUnfoldElemOf y (f <$> l) (∃ x, y = f x ∧ P x).
  Proof.
-    constructor. rewrite elem_of_list_fmap. f_equiv; intros y.
+    constructor. rewrite elem_of_list_fmap. f_equiv; intros x.
-    by rewrite (set_unfold_elem_of y l (P y)).
+    by rewrite (set_unfold_elem_of x l (P x)).
  Qed.
  Global Instance set_unfold_rotate x l P n:
    SetUnfoldElemOf x l P → SetUnfoldElemOf x (rotate n l) P.
  Proof. constructor. by rewrite elem_of_rotate, (set_unfold_elem_of x l P). Qed.
+  Global Instance set_unfold_list_bind {B} (f : A → list B) l P Q y :
+    (∀ x, SetUnfoldElemOf x l (P x)) → (∀ x, SetUnfoldElemOf y (f x) (Q x)) →
+    SetUnfoldElemOf y (l ≫= f) (∃ x, Q x ∧ P x).
+  Proof. constructor. rewrite elem_of_list_bind. naive_solver. Qed.
 End set_unfold_list.
 Tactic Notation "set_unfold" :=
@@ -342,13 +358,13 @@ Tactic Notation "set_solver" "-" hyp_list(Hs) "by" tactic3(tac) :=
  clear Hs; set_solver by tac.
 Tactic Notation "set_solver" "+" hyp_list(Hs) "by" tactic3(tac) :=
  clear -Hs; set_solver by tac.
-Tactic Notation "set_solver" := set_solver by idtac.
+Tactic Notation "set_solver" := set_solver by eauto.
 Tactic Notation "set_solver" "-" hyp_list(Hs) := clear Hs; set_solver.
 Tactic Notation "set_solver" "+" hyp_list(Hs) := clear -Hs; set_solver.
-Hint Extern 1000 (_ ∉ _) => set_solver : set_solver.
+Global Hint Extern 1000 (_ ∉ _) => set_solver : set_solver.
-Hint Extern 1000 (_ ∈ _) => set_solver : set_solver.
+Global Hint Extern 1000 (_ ∈ _) => set_solver : set_solver.
-Hint Extern 1000 (_ ⊆ _) => set_solver : set_solver.
+Global Hint Extern 1000 (_ ⊆ _) => set_solver : set_solver.
 (** * Sets with [∪], [∅] and [{[_]}] *)
@@ -359,10 +375,14 @@ Section semi_set.
  Implicit Types Xs Ys : list C.
  (** Equality *)
-  Lemma elem_of_equiv X Y : X ≡ Y ↔ ∀ x, x ∈ X ↔ x ∈ Y.
+  Lemma set_equiv X Y : X ≡ Y ↔ ∀ x, x ∈ X ↔ x ∈ Y.
  Proof. set_solver. Qed.
-  Lemma set_equiv_spec X Y : X ≡ Y ↔ X ⊆ Y ∧ Y ⊆ X.
+  Lemma set_equiv_subseteq X Y : X ≡ Y ↔ X ⊆ Y ∧ Y ⊆ X.
  Proof. set_solver. Qed.
+  Global Instance singleton_equiv_inj : Inj (=) (≡@{C}) singleton.
+  Proof. unfold Inj. set_solver. Qed.
+  Global Instance singleton_inj `{!LeibnizEquiv C} : Inj (=) (=@{C}) singleton.
+  Proof. unfold Inj. set_solver. Qed.
  (** Subset relation *)
  Global Instance set_subseteq_antisymm: AntiSymm (≡) (⊆@{C}).
@@ -380,8 +400,12 @@ Section semi_set.
  Lemma union_subseteq_l X Y : X ⊆ X ∪ Y.
  Proof. set_solver. Qed.
+  Lemma union_subseteq_l' X X' Y : X ⊆ X' → X ⊆ X' ∪ Y.
+  Proof. set_solver. Qed.
  Lemma union_subseteq_r X Y : Y ⊆ X ∪ Y.
  Proof. set_solver. Qed.
+  Lemma union_subseteq_r' X Y Y' : Y ⊆ Y' → Y ⊆ X ∪ Y'.
+  Proof. set_solver. Qed.
  Lemma union_least X Y Z : X ⊆ Z → Y ⊆ Z → X ∪ Y ⊆ Z.
  Proof. set_solver. Qed.
@@ -389,6 +413,11 @@ Section semi_set.
  Proof. done. Qed.
  Lemma elem_of_subset X Y : X ⊂ Y ↔ (∀ x, x ∈ X → x ∈ Y) ∧ ¬(∀ x, x ∈ Y → x ∈ X).
  Proof. set_solver. Qed.
+  Lemma elem_of_weaken x X Y : x ∈ X → X ⊆ Y → x ∈ Y.
+  Proof. set_solver. Qed.
+  Lemma not_elem_of_weaken x X Y : x ∉ Y → X ⊆ Y → x ∉ X.
+  Proof. set_solver. Qed.
  (** Union *)
  Lemma union_subseteq X Y Z : X ∪ Y ⊆ Z ↔ X ⊆ Z ∧ Y ⊆ Z.
@@ -430,7 +459,7 @@ Section semi_set.
  Proof. set_solver. Qed.
  Lemma elem_of_equiv_empty X : X ≡ ∅ ↔ ∀ x, x ∉ X.
  Proof. set_solver. Qed.
-  Lemma elem_of_empty x : x ∈ (∅ : C) ↔ False.
+  Lemma elem_of_empty x : x ∈@{C} ∅ ↔ False.
  Proof. set_solver. Qed.
  Lemma equiv_empty X : X ⊆ ∅ → X ≡ ∅.
  Proof. set_solver. Qed.
@@ -442,21 +471,26 @@ Section semi_set.
  Proof. set_solver. Qed.
  (** Singleton *)
-  Lemma elem_of_singleton_1 x y : x ∈ ({[y]} : C) → x = y.
+  Lemma elem_of_singleton_1 x y : x ∈@{C} {[y]} → x = y.
  Proof. by rewrite elem_of_singleton. Qed.
-  Lemma elem_of_singleton_2 x y : x = y → x ∈ ({[y]} : C).
+  Lemma elem_of_singleton_2 x y : x = y → x ∈@{C} {[y]}.
  Proof. by rewrite elem_of_singleton. Qed.
  Lemma elem_of_subseteq_singleton x X : x ∈ X ↔ {[ x ]} ⊆ X.
  Proof. set_solver. Qed.
-  Lemma non_empty_singleton x : ({[ x ]} : C) ≢ ∅.
+  Lemma non_empty_singleton x : {[ x ]} ≢@{C} ∅.
  Proof. set_solver. Qed.
-  Lemma not_elem_of_singleton x y : x ∉ ({[ y ]} : C) ↔ x ≠ y.
+  Lemma not_elem_of_singleton x y : x ∉@{C} {[ y ]} ↔ x ≠ y.
  Proof. by rewrite elem_of_singleton. Qed.
-  Lemma not_elem_of_singleton_1 x y : x ∉ ({[ y ]} : C) → x ≠ y.
+  Lemma not_elem_of_singleton_1 x y : x ∉@{C} {[ y ]} → x ≠ y.
  Proof. apply not_elem_of_singleton. Qed.
-  Lemma not_elem_of_singleton_2 x y : x ≠ y → x ∉ ({[ y ]} : C).
+  Lemma not_elem_of_singleton_2 x y : x ≠ y → x ∉@{C} {[ y ]}.
  Proof. apply not_elem_of_singleton. Qed.
+  Lemma singleton_subseteq_l x X : {[ x ]} ⊆ X ↔ x ∈ X.
+  Proof. set_solver. Qed.
+  Lemma singleton_subseteq x y : {[ x ]} ⊆@{C} {[ y ]} ↔ x = y.
+  Proof. set_solver. Qed.
  (** Disjointness *)
  Lemma elem_of_disjoint X Y : X ## Y ↔ ∀ x, x ∈ X → x ∈ Y → False.
  Proof. done. Qed.
@@ -505,6 +539,7 @@ Section semi_set.
  Qed.
  Lemma union_list_mono Xs Ys : Xs ⊆* Ys → ⋃ Xs ⊆ ⋃ Ys.
  Proof. induction 1; simpl; auto using union_mono. Qed.
  Lemma empty_union_list Xs : ⋃ Xs ≡ ∅ ↔ Forall (.≡ ∅) Xs.
  Proof.
    split.
@@ -515,10 +550,10 @@ Section semi_set.
  Section leibniz.
    Context `{!LeibnizEquiv C}.
-    Lemma elem_of_equiv_L X Y : X = Y ↔ ∀ x, x ∈ X ↔ x ∈ Y.
+    Lemma set_eq X Y : X = Y ↔ ∀ x, x ∈ X ↔ x ∈ Y.
-    Proof. unfold_leibniz. apply elem_of_equiv. Qed.
+    Proof. unfold_leibniz. apply set_equiv. Qed.
-    Lemma set_equiv_spec_L X Y : X = Y ↔ X ⊆ Y ∧ Y ⊆ X.
+    Lemma set_eq_subseteq X Y : X = Y ↔ X ⊆ Y ∧ Y ⊆ X.
-    Proof. unfold_leibniz. apply set_equiv_spec. Qed.
+    Proof. unfold_leibniz. apply set_equiv_subseteq. Qed.
    (** Subset relation *)
    Global Instance set_subseteq_partialorder : PartialOrder (⊆@{C}).
@@ -564,7 +599,7 @@ Section semi_set.
    Proof. unfold_leibniz. apply non_empty_inhabited. Qed.
    (** Singleton *)
-    Lemma non_empty_singleton_L x : {[ x ]} ≠ (∅ : C).
+    Lemma non_empty_singleton_L x : {[ x ]} ≠@{C} ∅.
    Proof. unfold_leibniz. apply non_empty_singleton. Qed.
    (** Big unions *)
@@ -574,8 +609,9 @@ Section semi_set.
    Proof. unfold_leibniz. apply union_list_app. Qed.
    Lemma union_list_reverse_L Xs : ⋃ (reverse Xs) = ⋃ Xs.
    Proof. unfold_leibniz. apply union_list_reverse. Qed.
    Lemma empty_union_list_L Xs : ⋃ Xs = ∅ ↔ Forall (.= ∅) Xs.
-    Proof. unfold_leibniz. by rewrite empty_union_list. Qed.
+    Proof. unfold_leibniz. apply empty_union_list. Qed.
  End leibniz.
  Lemma not_elem_of_iff `{!RelDecision (∈@{C})} X Y x :
@@ -584,26 +620,31 @@ Section semi_set.
  Section dec.
    Context `{!RelDecision (≡@{C})}.
    Lemma set_subseteq_inv X Y : X ⊆ Y → X ⊂ Y ∨ X ≡ Y.
    Proof. destruct (decide (X ≡ Y)); [by right|left;set_solver]. Qed.
    Lemma set_not_subset_inv X Y : X ⊄ Y → X ⊈ Y ∨ X ≡ Y.
    Proof. destruct (decide (X ≡ Y)); [by right|left;set_solver]. Qed.
    Lemma non_empty_union X Y : X ∪ Y ≢ ∅ ↔ X ≢ ∅ ∨ Y ≢ ∅.
-    Proof. rewrite empty_union. destruct (decide (X ≡ ∅)); intuition. Qed.
+    Proof. destruct (decide (X ≡ ∅)); set_solver. Qed.
    Lemma non_empty_union_list Xs : ⋃ Xs ≢ ∅ → Exists (.≢ ∅) Xs.
    Proof. rewrite empty_union_list. apply (not_Forall_Exists _). Qed.
+  End dec.
+  Section dec_leibniz.
+    Context `{!RelDecision (≡@{C}), !LeibnizEquiv C}.
-    Context `{!LeibnizEquiv C}.
    Lemma set_subseteq_inv_L X Y : X ⊆ Y → X ⊂ Y ∨ X = Y.
    Proof. unfold_leibniz. apply set_subseteq_inv. Qed.
    Lemma set_not_subset_inv_L X Y : X ⊄ Y → X ⊈ Y ∨ X = Y.
    Proof. unfold_leibniz. apply set_not_subset_inv. Qed.
    Lemma non_empty_union_L X Y : X ∪ Y ≠ ∅ ↔ X ≠ ∅ ∨ Y ≠ ∅.
    Proof. unfold_leibniz. apply non_empty_union. Qed.
    Lemma non_empty_union_list_L Xs : ⋃ Xs ≠ ∅ → Exists (.≠ ∅) Xs.
    Proof. unfold_leibniz. apply non_empty_union_list. Qed.
-  End dec.
+  End dec_leibniz.
 End semi_set.
@@ -647,7 +688,7 @@ Section set.
  Global Instance intersection_empty_r: RightAbsorb (≡@{C}) ∅ (∩).
  Proof. intros X; set_solver. Qed.
-  Lemma intersection_singletons x : ({[x]} : C) ∩ {[x]} ≡ {[x]}.
+  Lemma intersection_singletons x : {[x]} ∩ {[x]} ≡@{C} {[x]}.
  Proof. set_solver. Qed.
  Lemma union_intersection_l X Y Z : X ∪ (Y ∩ Z) ≡ (X ∪ Y) ∩ (X ∪ Z).
@@ -676,9 +717,9 @@ Section set.
  Proof. set_solver. Qed.
  Lemma difference_disjoint X Y : X ## Y → X ∖ Y ≡ X.
  Proof. set_solver. Qed.
-  Lemma subset_difference_elem_of {x: A} {s: C} (inx: x ∈ s): s ∖ {[ x ]} ⊂ s.
+  Lemma subset_difference_elem_of x X : x ∈ X → X ∖ {[ x ]} ⊂ X.
  Proof. set_solver. Qed.
-  Lemma difference_difference X Y Z : (X ∖ Y) ∖ Z ≡ X ∖ (Y ∪ Z).
+  Lemma difference_difference_l X Y Z : (X ∖ Y) ∖ Z ≡ X ∖ (Y ∪ Z).
  Proof. set_solver. Qed.
  Lemma difference_mono X1 X2 Y1 Y2 :
@@ -729,7 +770,7 @@ Section set.
    Global Instance intersection_empty_r_L: RightAbsorb (=@{C}) ∅ (∩).
    Proof. intros ?. unfold_leibniz. apply (right_absorb _ _). Qed.
-    Lemma intersection_singletons_L x : {[x]} ∩ {[x]} = ({[x]} : C).
+    Lemma intersection_singletons_L x : {[x]} ∩ {[x]} =@{C} {[x]}.
    Proof. unfold_leibniz. apply intersection_singletons. Qed.
    Lemma union_intersection_l_L X Y Z : X ∪ (Y ∩ Z) = (X ∪ Y) ∩ (X ∪ Z).
@@ -759,8 +800,8 @@ Section set.
    Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed.
    Lemma difference_disjoint_L X Y : X ## Y → X ∖ Y = X.
    Proof. unfold_leibniz. apply difference_disjoint. Qed.
-    Lemma difference_difference_L X Y Z : (X ∖ Y) ∖ Z = X ∖ (Y ∪ Z).
+    Lemma difference_difference_l_L X Y Z : (X ∖ Y) ∖ Z = X ∖ (Y ∪ Z).
-    Proof. unfold_leibniz. apply difference_difference. Qed.
+    Proof. unfold_leibniz. apply difference_difference_l. Qed.
    (** Disjointness *)
    Lemma disjoint_intersection_L X Y : X ## Y ↔ X ∩ Y = ∅.
@@ -769,6 +810,7 @@ Section set.
  Section dec.
    Context `{!RelDecision (∈@{C})}.
    Lemma not_elem_of_intersection x X Y : x ∉ X ∩ Y ↔ x ∉ X ∨ x ∉ Y.
    Proof. rewrite elem_of_intersection. destruct (decide (x ∈ X)); tauto. Qed.
    Lemma not_elem_of_difference x X Y : x ∉ X ∖ Y ↔ x ∉ X ∨ x ∈ Y.
@@ -778,11 +820,18 @@ Section set.
      intros ? x; split; rewrite !elem_of_union, elem_of_difference; [|intuition].
      destruct (decide (x ∈ X)); intuition.
    Qed.
+    Lemma union_difference_singleton x Y : x ∈ Y → Y ≡ {[x]} ∪ Y ∖ {[x]}.
+    Proof. intros ?. apply union_difference. set_solver. Qed.
    Lemma difference_union X Y : X ∖ Y ∪ Y ≡ X ∪ Y.
    Proof.
      intros x. rewrite !elem_of_union; rewrite elem_of_difference.
      split; [ | destruct (decide (x ∈ Y)) ]; intuition.
    Qed.
+    Lemma difference_difference_r X Y Z : X ∖ (Y ∖ Z) ≡ (X ∖ Y) ∪ (X ∩ Z).
+    Proof. intros x. destruct (decide (x ∈ Z)); set_solver. Qed.
+    Lemma difference_union_intersection X Y : (X ∖ Y) ∪ (X ∩ Y) ≡ X.
+    Proof. rewrite union_intersection_l, difference_union. set_solver. Qed.
    Lemma subseteq_disjoint_union X Y : X ⊆ Y ↔ ∃ Z, Y ≡ X ∪ Z ∧ X ## Z.
    Proof.
      split; [|set_solver].
@@ -794,14 +843,16 @@ Section set.
    Proof. set_solver. Qed.
    Lemma singleton_union_difference X Y x :
      {[x]} ∪ (X ∖ Y) ≡ ({[x]} ∪ X) ∖ (Y ∖ {[x]}).
-    Proof.
+    Proof. intro y; destruct (decide (y ∈@{C} {[x]})); set_solver. Qed.
-      intro y; split; intros Hy; [ set_solver | ].
+  End dec.
-      destruct (decide (y ∈ ({[x]} : C))); set_solver.
-    Qed.
+  Section dec_leibniz.
+    Context `{!RelDecision (∈@{C}), !LeibnizEquiv C}.
-    Context `{!LeibnizEquiv C}.
    Lemma union_difference_L X Y : X ⊆ Y → Y = X ∪ Y ∖ X.
    Proof. unfold_leibniz. apply union_difference. Qed.
+    Lemma union_difference_singleton_L x Y : x ∈ Y → Y = {[x]} ∪ Y ∖ {[x]}.
+    Proof. unfold_leibniz. apply union_difference_singleton. Qed.
    Lemma difference_union_L X Y : X ∖ Y ∪ Y = X ∪ Y.
    Proof. unfold_leibniz. apply difference_union. Qed.
    Lemma non_empty_difference_L X Y : X ⊂ Y → Y ∖ X ≠ ∅.
@@ -813,7 +864,12 @@ Section set.
    Lemma singleton_union_difference_L X Y x :
      {[x]} ∪ (X ∖ Y) = ({[x]} ∪ X) ∖ (Y ∖ {[x]}).
    Proof. unfold_leibniz. apply singleton_union_difference. Qed.
-  End dec.
+    Lemma difference_difference_r_L X Y Z : X ∖ (Y ∖ Z) = (X ∖ Y) ∪ (X ∩ Z).
+    Proof. unfold_leibniz. apply difference_difference_r. Qed.
+    Lemma difference_union_intersection_L X Y : (X ∖ Y) ∪ (X ∩ Y) = X.
+    Proof. unfold_leibniz. apply difference_union_intersection. Qed.
+  End dec_leibniz.
 End set.
@@ -863,39 +919,74 @@ Section option_and_list_to_set.
  Proof. done. Qed.
  Lemma list_to_set_app l1 l2 : list_to_set (l1 ++ l2) ≡@{C} list_to_set l1 ∪ list_to_set l2.
  Proof. set_solver. Qed.
+  Lemma list_to_set_singleton x : list_to_set [x] ≡@{C} {[ x ]}.
+  Proof. set_solver. Qed.
+  Lemma list_to_set_snoc l x : list_to_set (l ++ [x]) ≡@{C} list_to_set l ∪ {[ x ]}.
+  Proof. set_solver. Qed.
  Global Instance list_to_set_perm : Proper ((≡ₚ) ==> (≡)) (list_to_set (C:=C)).
  Proof. induction 1; set_solver. Qed.
-  Context `{!LeibnizEquiv C}.
+  Section leibniz.
-  Lemma list_to_set_app_L l1 l2 : list_to_set (l1 ++ l2) =@{C} list_to_set l1 ∪ list_to_set l2.
+    Context `{!LeibnizEquiv C}.
-  Proof. set_solver. Qed.
-  Global Instance list_to_set_perm_L : Proper ((≡ₚ) ==> (=)) (list_to_set (C:=C)).
+    Lemma list_to_set_app_L l1 l2 :
-  Proof. induction 1; set_solver. Qed.
+      list_to_set (l1 ++ l2) =@{C} list_to_set l1 ∪ list_to_set l2.
+    Proof. set_solver. Qed.
+    Global Instance list_to_set_perm_L : Proper ((≡ₚ) ==> (=)) (list_to_set (C:=C)).
+    Proof. induction 1; set_solver. Qed.
+  End leibniz.
 End option_and_list_to_set.
+(** * Finite types to sets. *)
+Definition fin_to_set (A : Type) `{Singleton A C, Empty C, Union C, Finite A} : C :=
+  list_to_set (enum A).
+Section fin_to_set.
+  Context `{SemiSet A C, Finite A}.
+  Implicit Types a : A.
+  Lemma elem_of_fin_to_set a : a ∈@{C} fin_to_set A.
+  Proof. apply elem_of_list_to_set, elem_of_enum. Qed.
+  Global Instance set_unfold_fin_to_set a :
+    SetUnfoldElemOf (C:=C) a (fin_to_set A) True.
+  Proof. constructor. split; auto using elem_of_fin_to_set. Qed.
+End fin_to_set.
 (** * Guard *)
-Global Instance set_guard `{MonadSet M} : MGuard M :=
+Global Instance set_mfail `{MonadSet M} : MFail M := λ _ _, ∅.
-  λ P dec A x, match dec with left H => x H | _ => ∅ end.
+Global Typeclasses Opaque set_mfail.
 Section set_monad_base.
  Context `{MonadSet M}.
+  Lemma elem_of_mfail {A} x : x ∈@{M A} mfail ↔ False.
+  Proof. unfold mfail, set_mfail. by rewrite elem_of_empty. Qed.
+  Global Instance set_unfold_elem_of_mfail {A} (x : A) :
+    SetUnfoldElemOf x (mfail : M A) False.
+  Proof. constructor. by apply elem_of_mfail. Qed.
+  (** This lemma includes a bind, to avoid equalities of proofs. We cannot have
+  [p ∈ guard P ↔ P] unless [P] is proof irrelant. The best (but less usable)
+  self-contained alternative would be [p ∈ guard P ↔ decide P = left p]. *)
  Lemma elem_of_guard `{Decision P} {A} (x : A) (X : M A) :
-    (x ∈ guard P; X) ↔ P ∧ x ∈ X.
+    x ∈ (guard P;; X) ↔ P ∧ x ∈ X.
  Proof.
-    unfold mguard, set_guard; simpl; case_match;
+    case_guard; rewrite elem_of_bind;
-      rewrite ?elem_of_empty; naive_solver.
+      [setoid_rewrite elem_of_ret | setoid_rewrite elem_of_mfail];
+      naive_solver.
  Qed.
  Lemma elem_of_guard_2 `{Decision P} {A} (x : A) (X : M A) :
-    P → x ∈ X → x ∈ guard P; X.
+    P → x ∈ X → x ∈ (guard P;; X).
  Proof. by rewrite elem_of_guard. Qed.
-  Lemma guard_empty `{Decision P} {A} (X : M A) : (guard P; X) ≡ ∅ ↔ ¬P ∨ X ≡ ∅.
+  Lemma guard_empty `{Decision P} {A} (X : M A) : (guard P;; X) ≡ ∅ ↔ ¬P ∨ X ≡ ∅.
  Proof.
    rewrite !elem_of_equiv_empty; setoid_rewrite elem_of_guard.
    destruct (decide P); naive_solver.
  Qed.
  Global Instance set_unfold_guard `{Decision P} {A} (x : A) (X : M A) Q :
-    SetUnfoldElemOf x X Q → SetUnfoldElemOf x (guard P; X) (P ∧ Q).
+    SetUnfoldElemOf x X Q → SetUnfoldElemOf x (guard P;; X) (P ∧ Q).
  Proof. constructor. by rewrite elem_of_guard, (set_unfold (x ∈ X) Q). Qed.
  Lemma bind_empty {A B} (f : A → M B) X :
    X ≫= f ≡ ∅ ↔ X ≡ ∅ ∨ ∀ x, x ∈ X → f x ≡ ∅.
@@ -911,33 +1002,50 @@ Section quantifiers.
  Context `{SemiSet A C} (P : A → Prop).
  Implicit Types X Y : C.
+  Global Instance set_unfold_set_Forall X (QX QP : A → Prop) :
+    (∀ x, SetUnfoldElemOf x X (QX x)) →
+    (∀ x, SetUnfold (P x) (QP x)) →
+    SetUnfold (set_Forall P X) (∀ x, QX x → QP x).
+  Proof.
+    intros HX HP; constructor. unfold set_Forall. apply forall_proper; intros x.
+    by rewrite (set_unfold (x ∈ X) _), (set_unfold (P x) _).
+  Qed.
+  Global Instance set_unfold_set_Exists X (QX QP : A → Prop) :
+    (∀ x, SetUnfoldElemOf x X (QX x)) →
+    (∀ x, SetUnfold (P x) (QP x)) →
+    SetUnfold (set_Exists P X) (∃ x, QX x ∧ QP x).
+  Proof.
+    intros HX HP; constructor. unfold set_Exists. f_equiv; intros x.
+    by rewrite (set_unfold (x ∈ X) _), (set_unfold (P x) _).
+  Qed.
  Lemma set_Forall_empty : set_Forall P (∅ : C).
-  Proof. unfold set_Forall. set_solver. Qed.
+  Proof. set_solver. Qed.
  Lemma set_Forall_singleton x : set_Forall P ({[ x ]} : C) ↔ P x.
-  Proof. unfold set_Forall. set_solver. Qed.
+  Proof. set_solver. Qed.
  Lemma set_Forall_union X Y :
    set_Forall P X → set_Forall P Y → set_Forall P (X ∪ Y).
-  Proof. unfold set_Forall. set_solver. Qed.
+  Proof. set_solver. Qed.
  Lemma set_Forall_union_inv_1 X Y : set_Forall P (X ∪ Y) → set_Forall P X.
-  Proof. unfold set_Forall. set_solver. Qed.
+  Proof. set_solver. Qed.
  Lemma set_Forall_union_inv_2 X Y : set_Forall P (X ∪ Y) → set_Forall P Y.
-  Proof. unfold set_Forall. set_solver. Qed.
+  Proof. set_solver. Qed.
  Lemma set_Forall_list_to_set l : set_Forall P (list_to_set (C:=C) l) ↔ Forall P l.
-  Proof. rewrite Forall_forall. unfold set_Forall. set_solver. Qed.
+  Proof. rewrite Forall_forall. set_solver. Qed.
  Lemma set_Exists_empty : ¬set_Exists P (∅ : C).
-  Proof. unfold set_Exists. set_solver. Qed.
+  Proof. set_solver. Qed.
  Lemma set_Exists_singleton x : set_Exists P ({[ x ]} : C) ↔ P x.
-  Proof. unfold set_Exists. set_solver. Qed.
+  Proof. set_solver. Qed.
  Lemma set_Exists_union_1 X Y : set_Exists P X → set_Exists P (X ∪ Y).
-  Proof. unfold set_Exists. set_solver. Qed.
+  Proof. set_solver. Qed.
  Lemma set_Exists_union_2 X Y : set_Exists P Y → set_Exists P (X ∪ Y).
-  Proof. unfold set_Exists. set_solver. Qed.
+  Proof. set_solver. Qed.
  Lemma set_Exists_union_inv X Y :
    set_Exists P (X ∪ Y) → set_Exists P X ∨ set_Exists P Y.
-  Proof. unfold set_Exists. set_solver. Qed.
+  Proof. set_solver. Qed.
  Lemma set_Exists_list_to_set l : set_Exists P (list_to_set (C:=C) l) ↔ Exists P l.
-  Proof. rewrite Exists_exists. unfold set_Exists. set_solver. Qed.
+  Proof. rewrite Exists_exists. set_solver. Qed.
 End quantifiers.
 Section more_quantifiers.
@@ -946,10 +1054,10 @@ Section more_quantifiers.
  Lemma set_Forall_impl (P Q : A → Prop) X :
    set_Forall P X → (∀ x, P x → Q x) → set_Forall Q X.
-  Proof. unfold set_Forall. naive_solver. Qed.
+  Proof. set_solver. Qed.
  Lemma set_Exists_impl (P Q : A → Prop) X :
    set_Exists P X → (∀ x, P x → Q x) → set_Exists Q X.
-  Proof. unfold set_Exists. naive_solver. Qed.
+  Proof. set_solver. Qed.
 End more_quantifiers.
 (** * Properties of implementations of sets that form a monad *)
@@ -968,7 +1076,7 @@ Section set_monad.
  Lemma set_bind_singleton {A B} (f : A → M B) x : {[ x ]} ≫= f ≡ f x.
  Proof. set_solver. Qed.
-  Lemma set_guard_True {A} `{Decision P} (X : M A) : P → (guard P; X) ≡ X.
+  Lemma set_guard_True {A} `{Decision P} (X : M A) : P → (guard P;; X) ≡ X.
  Proof. set_solver. Qed.
  Lemma set_fmap_compose {A B C} (f : A → B) (g : B → C) (X : M A) :
    g ∘ f <$> X ≡ g <$> (f <$> X).
@@ -990,7 +1098,7 @@ Section set_monad.
    - revert l. induction k; set_solver by eauto.
    - induction 1; set_solver.
  Qed.
-  Lemma set_mapM_length {A B} (f : A → M B) l k :
+  Lemma length_set_mapM {A B} (f : A → M B) l k :
    l ∈ mapM f k → length l = length k.
  Proof. revert l; induction k; set_solver by eauto. Qed.
  Lemma elem_of_mapM_fmap {A B} (f : A → B) (g : B → M A) l k :
@@ -1004,8 +1112,26 @@ Section set_monad.
    Forall2 P l1 l2.
  Proof.
    rewrite elem_of_mapM. intros Hl1. revert l2.
-    induction Hl1; inversion_clear 1; constructor; auto.
+    induction Hl1; inv 1; constructor; auto.
+  Qed.
+  Global Instance monadset_cprod {A B} : CProd (M A) (M B) (M (A * B)) := λ X Y,
+    x ← X; fmap (x,.) Y.
+  Lemma elem_of_monadset_cprod {A B} (X : M A) (Y : M B) (x : A * B) :
+    x ∈ cprod X Y ↔ x.1 ∈ X ∧ x.2 ∈ Y.
+  Proof. unfold cprod, monadset_cprod. destruct x; set_solver. Qed.
+  Global Instance set_unfold_monadset_cprod {A B} (X : M A) (Y : M B) P Q x :
+    SetUnfoldElemOf x.1 X P →
+    SetUnfoldElemOf x.2 Y Q →
+    SetUnfoldElemOf x (cprod X Y) (P ∧ Q).
+  Proof.
+    constructor.
+    by rewrite elem_of_monadset_cprod, (set_unfold_elem_of x.1 X P),
+      (set_unfold_elem_of x.2 Y Q).
  Qed.
 End set_monad.
 (** Finite sets *)
@@ -1024,6 +1150,18 @@ Section pred_finite_infinite.
    pred_infinite P → (∀ x, P x → Q x) → pred_infinite Q.
  Proof. unfold pred_infinite. set_solver. Qed.
+  (** If [f] is surjective onto [P], then pre-composing with [f] preserves
+  infinity. *)
+  Lemma pred_infinite_surj {A B} (P : B → Prop) (f : A → B) :
+    (∀ x, P x → ∃ y, f y = x) →
+    pred_infinite P → pred_infinite (P ∘ f).
+  Proof.
+    intros Hf HP xs. destruct (HP (f <$> xs)) as [x [HPx Hx]].
+    destruct (Hf _ HPx) as [y Hf']. exists y. split.
+    - simpl. rewrite Hf'. done.
+    - intros Hy. apply Hx. apply elem_of_list_fmap. eauto.
+  Qed.
  Lemma pred_not_infinite_finite {A} (P : A → Prop) :
    pred_infinite P → pred_finite P → False.
  Proof. intros Hinf [xs ?]. destruct (Hinf xs). set_solver. Qed.
@@ -1076,6 +1214,8 @@ Section set_finite_infinite.
  Proof. intros [l ?]; exists l; set_solver. Qed.
  Lemma union_finite_inv_r X Y : set_finite (X ∪ Y) → set_finite Y.
  Proof. intros [l ?]; exists l; set_solver. Qed.
+  Lemma list_to_set_finite l : set_finite (list_to_set (C:=C) l).
+  Proof. exists l. intros x. by rewrite elem_of_list_to_set. Qed.
  Global Instance set_infinite_subseteq :
    Proper ((⊆) ==> impl) (@set_infinite A C _).
@@ -1111,6 +1251,42 @@ Section more_finite.
  Proof. intros Hinf [xs ?] xs'. destruct (Hinf (xs ++ xs')). set_solver. Qed.
 End more_finite.
+Lemma top_infinite `{TopSet A C, Infinite A} : set_infinite (⊤ : C).
+Proof.
+  intros xs. exists (fresh xs). split; [set_solver|]. apply infinite_is_fresh.
+Qed.
+(** This formulation of finiteness is stronger than [pred_finite]: when equality
+    is decidable, it is equivalent to the predicate being finite AND decidable. *)
+Lemma dec_pred_finite_alt {A} (P : A → Prop) `{!∀ x, Decision (P x)} :
+  pred_finite P ↔ ∃ xs : list A, ∀ x, P x ↔ x ∈ xs.
+Proof.
+  split; intros [xs ?].
+  - exists (filter P xs). intros x. rewrite elem_of_list_filter. naive_solver.
+  - exists xs. naive_solver.
+Qed.
+Lemma finite_sig_pred_finite {A} (P : A → Prop) `{Finite (sig P)} :
+  pred_finite P.
+Proof.
+  exists (proj1_sig <$> enum _). intros x px.
+  apply elem_of_list_fmap_1_alt with (x ↾ px); [apply elem_of_enum|]; done.
+Qed.
+Lemma pred_finite_arg2 {A B} (P : A → B → Prop) x :
+  pred_finite (uncurry P) → pred_finite (P x).
+Proof.
+  intros [xys ?]. exists (xys.*2). intros y ?.
+  apply elem_of_list_fmap_1_alt with (x, y); by auto.
+Qed.
+Lemma pred_finite_arg1 {A B} (P : A → B → Prop) y :
+  pred_finite (uncurry P) → pred_finite (flip P y).
+Proof.
+  intros [xys ?]. exists (xys.*1). intros x ?.
+  apply elem_of_list_fmap_1_alt with (x, y); by auto.
+Qed.
 (** Sets of sequences of natural numbers *)
 (* The set [seq_seq start len] of natural numbers contains the sequence
 [start, start + 1, ..., start + (len-1)]. *)
@@ -1131,7 +1307,7 @@ Section set_seq.
    - rewrite elem_of_empty. lia.
    - rewrite elem_of_union, elem_of_singleton, IH. lia.
  Qed.
-  Global Instance set_unfold_seq start len :
+  Global Instance set_unfold_seq start len x :
    SetUnfoldElemOf x (set_seq (C:=C) start len) (start ≤ x < start + len).
  Proof. constructor; apply elem_of_set_seq. Qed.
@@ -1156,17 +1332,17 @@ Section set_seq.
    - rewrite set_seq_subseteq; lia.
  Qed.
-  Lemma set_seq_plus_disjoint start len1 len2 :
+  Lemma set_seq_add_disjoint start len1 len2 :
    set_seq (C:=C) start len1 ## set_seq (start + len1) len2.
  Proof. set_solver by lia. Qed.
-  Lemma set_seq_plus start len1 len2 :
+  Lemma set_seq_add start len1 len2 :
    set_seq (C:=C) start (len1 + len2)
    ≡ set_seq start len1 ∪ set_seq (start + len1) len2.
  Proof. set_solver by lia. Qed.
-  Lemma set_seq_plus_L `{!LeibnizEquiv C} start len1 len2 :
+  Lemma set_seq_add_L `{!LeibnizEquiv C} start len1 len2 :
    set_seq (C:=C) start (len1 + len2)
    = set_seq start len1 ∪ set_seq (start + len1) len2.
-  Proof. unfold_leibniz. apply set_seq_plus. Qed.
+  Proof. unfold_leibniz. apply set_seq_add. Qed.
  Lemma set_seq_S_start_disjoint start len :
    {[ start ]} ## set_seq (C:=C) (S start) len.
@@ -1198,8 +1374,8 @@ End set_seq.
 (** Mimimal elements *)
 Definition minimal `{ElemOf A C} (R : relation A) (x : A) (X : C) : Prop :=
  ∀ y, y ∈ X → R y x → R x y.
-Instance: Params (@minimal) 5 := {}.
+Global Instance: Params (@minimal) 5 := {}.
-Typeclasses Opaque minimal.
+Global Typeclasses Opaque minimal.
 Section minimal.
  Context `{SemiSet A C} {R : relation A}.

--- a/theories/sorting.v
+++ b/theories/sorting.v
@@ -2,6 +2,7 @@
 standard library, but without using the module system. *)
 From Coq Require Export Sorted.
 From stdpp Require Export orders list.
+From stdpp Require Import sets.
 From stdpp Require Import options.
 Section merge_sort.
@@ -48,43 +49,67 @@ Inductive TlRel {A} (R : relation A) (a : A) : list A → Prop :=
 Section sorted.
  Context {A} (R : relation A).
-  Lemma elem_of_StronglySorted_app l1 l2 x1 x2 :
+  Lemma StronglySorted_cons l x :
-    StronglySorted R (l1 ++ l2) → x1 ∈ l1 → x2 ∈ l2 → R x1 x2.
+    StronglySorted R (x :: l) ↔
+      Forall (R x) l ∧ StronglySorted R l.
+  Proof. split; [inv 1|constructor]; naive_solver. Qed.
+  Lemma StronglySorted_app l1 l2 :
+    StronglySorted R (l1 ++ l2) ↔
+      (∀ x1 x2, x1 ∈ l1 → x2 ∈ l2 → R x1 x2) ∧
+      StronglySorted R l1 ∧
+      StronglySorted R l2.
  Proof.
-    induction l1 as [|x1' l1 IH]; simpl; [by rewrite elem_of_nil|].
+    induction l1 as [|x1' l1 IH]; simpl.
-    intros [? Hall]%StronglySorted_inv [->|?]%elem_of_cons ?; [|by auto].
+    - set_solver by eauto using SSorted_nil.
-    rewrite Forall_app, !Forall_forall in Hall. naive_solver.
+    - rewrite !StronglySorted_cons, IH, !Forall_forall. set_solver.
  Qed.
-  Lemma StronglySorted_app_inv_l l1 l2 :
+  Lemma StronglySorted_app_2 l1 l2 :
+    (∀ x1 x2, x1 ∈ l1 → x2 ∈ l2 → R x1 x2) →
+    StronglySorted R l1 →
+    StronglySorted R l2 →
+    StronglySorted R (l1 ++ l2).
+  Proof. by rewrite StronglySorted_app. Qed.
+  Lemma StronglySorted_app_1_elem_of l1 l2 x1 x2 :
+    StronglySorted R (l1 ++ l2) → x1 ∈ l1 → x2 ∈ l2 → R x1 x2.
+  Proof. rewrite StronglySorted_app. naive_solver. Qed.
+  Lemma StronglySorted_app_1_l l1 l2 :
    StronglySorted R (l1 ++ l2) → StronglySorted R l1.
-  Proof.
+  Proof. rewrite StronglySorted_app. naive_solver. Qed.
-    induction l1 as [|x1' l1 IH]; simpl;
+  Lemma StronglySorted_app_1_r l1 l2 :
-      [|inversion_clear 1]; decompose_Forall; constructor; auto.
-  Qed.
-  Lemma StronglySorted_app_inv_r l1 l2 :
    StronglySorted R (l1 ++ l2) → StronglySorted R l2.
-  Proof.
+  Proof. rewrite StronglySorted_app. naive_solver. Qed.
-    induction l1 as [|x1' l1 IH]; simpl;
-      [|inversion_clear 1]; decompose_Forall; auto.
-  Qed.
  Lemma Sorted_StronglySorted `{!Transitive R} l :
    Sorted R l → StronglySorted R l.
  Proof. by apply Sorted.Sorted_StronglySorted. Qed.
-  Lemma StronglySorted_unique `{!AntiSymm (=) R} l1 l2 :
+  Lemma StronglySorted_unique_strong l1 l2 :
+    (∀ x1 x2, x1 ∈ l1 → x2 ∈ l2 → R x1 x2 → R x2 x1 → x1 = x2) →
    StronglySorted R l1 → StronglySorted R l2 → l1 ≡ₚ l2 → l1 = l2.
  Proof.
-    intros Hl1; revert l2. induction Hl1 as [|x1 l1 ? IH Hx1]; intros l2 Hl2 E.
+    intros Hasym Hl1. revert l2 Hasym.
+    induction Hl1 as [|x1 l1 ? IH Hx1]; intros l2 Hasym Hl2 E.
    { symmetry. by apply Permutation_nil. }
    destruct Hl2 as [|x2 l2 ? Hx2].
-    { by apply Permutation_nil in E. }
+    { by apply Permutation_nil_r in E. }
    assert (x1 = x2); subst.
    { rewrite Forall_forall in Hx1, Hx2.
      assert (x2 ∈ x1 :: l1) as Hx2' by (by rewrite E; left).
      assert (x1 ∈ x2 :: l2) as Hx1' by (by rewrite <-E; left).
-      inversion Hx1'; inversion Hx2'; simplify_eq; auto. }
+      inv Hx1'; inv Hx2'; simplify_eq; [eauto..|].
-    f_equal. by apply IH, (inj (x2 ::.)).
+      apply Hasym; [by constructor..| |]; by eauto. }
+    f_equal. apply IH, (inj (x2 ::.)); [|done..].
+    intros ????. apply Hasym; by constructor.
  Qed.
+  Lemma StronglySorted_unique `{!AntiSymm (=) R} l1 l2 :
+    StronglySorted R l1 → StronglySorted R l2 → l1 ≡ₚ l2 → l1 = l2.
+  Proof. apply StronglySorted_unique_strong; eauto. Qed.
+  Lemma Sorted_unique_strong `{!Transitive R} l1 l2 :
+    (∀ x1 x2, x1 ∈ l1 → x2 ∈ l2 → R x1 x2 → R x2 x1 → x1 = x2) →
+    Sorted R l1 → Sorted R l2 → l1 ≡ₚ l2 → l1 = l2.
+  Proof. auto using StronglySorted_unique_strong, Sorted_StronglySorted. Qed.
  Lemma Sorted_unique `{!Transitive R, !AntiSymm (=) R} l1 l2 :
    Sorted R l1 → Sorted R l2 → l1 ≡ₚ l2 → l1 = l2.
  Proof. auto using StronglySorted_unique, Sorted_StronglySorted. Qed.
@@ -96,7 +121,7 @@ Section sorted.
    match l with
    | [] => left _
    | y :: l => cast_if (decide (R x y))
-    end; abstract first [by constructor | by inversion 1].
+    end; abstract first [by constructor | by inv 1].
  Defined.
  Global Instance Sorted_dec `{∀ x y, Decision (R x y)} : ∀ l,
    Decision (Sorted R l).
@@ -106,7 +131,7 @@ Section sorted.
    match l return Decision (Sorted R l) with
    | [] => left _
    | x :: l => cast_if_and (decide (HdRel R x l)) (go l)
-    end); clear go; abstract first [by constructor | by inversion 1].
+    end); clear go; abstract first [by constructor | by inv 1].
  Defined.
  Global Instance StronglySorted_dec `{∀ x y, Decision (R x y)} : ∀ l,
    Decision (StronglySorted R l).
@@ -116,7 +141,7 @@ Section sorted.
    match l return Decision (StronglySorted R l) with
    | [] => left _
    | x :: l => cast_if_and (decide (Forall (R x) l)) (go l)
-    end); clear go; abstract first [by constructor | by inversion 1].
+    end); clear go; abstract first [by constructor | by inv 1].
  Defined.
  Section fmap.
@@ -144,9 +169,9 @@ Section sorted.
    induction 1 as [|y l Hsort IH Hhd]; intros Htl; simpl.
    { repeat constructor. }
    constructor.
-    - apply IH. inversion Htl as [|? [|??]]; simplify_list_eq; by constructor.
+    - apply IH. inv Htl as [|? [|??]]; simplify_list_eq; by constructor.
    - destruct Hhd; constructor; [|done].
-      inversion Htl as [|? [|??]]; by try discriminate_list.
+      inv Htl as [|? [|??]]; by try discriminate_list.
  Qed.
 End sorted.

--- a/stdpp/ssreflect.v
+++ b/stdpp/ssreflect.v
+(** This file provides support for using std++ in combination with the ssreflect
+tactics. It patches up some global options of ssreflect. *)
+From Coq.ssr Require Export ssreflect.
+From stdpp Require Export prelude.
+From stdpp Require Import options.
+(** Restore Coq's normal "if" scope, ssr redefines it. *)
+Global Open Scope general_if_scope.
+(** See Coq issue #5706 *)
+Global Set SsrOldRewriteGoalsOrder.
+(** Overwrite ssr's [done] tactic with ours *)
+Ltac done := stdpp.tactics.done.
--- a/theories/streams.v
+++ b/theories/streams.v
 From stdpp Require Export tactics.
 From stdpp Require Import options.
-CoInductive stream (A : Type) : Type := scons : A → stream A → stream A.
+Declare Scope stream_scope.
-Arguments scons {_} _ _ : assert.
 Delimit Scope stream_scope with stream.
-Bind Scope stream_scope with stream.
+Global Open Scope stream_scope.
-Open Scope stream_scope.
+CoInductive stream (A : Type) : Type := scons : A → stream A → stream A.
+Global Arguments scons {_} _ _ : assert.
 Infix ":.:" := scons (at level 60, right associativity) : stream_scope.
+Bind Scope stream_scope with stream.
 Definition shead {A} (s : stream A) : A := match s with x :.: _ => x end.
 Definition stail {A} (s : stream A) : stream A := match s with _ :.: s => s end.
@@ -15,7 +17,7 @@ CoInductive stream_equiv' {A} (s1 s2 : stream A) : Prop :=
  scons_equiv' :
    shead s1 = shead s2 → stream_equiv' (stail s1) (stail s2) →
    stream_equiv' s1 s2.
-Instance stream_equiv {A} : Equiv (stream A) := stream_equiv'.
+Global Instance stream_equiv {A} : Equiv (stream A) := stream_equiv'.
 Reserved Infix "!.!" (at level 20).
 Fixpoint slookup {A} (i : nat) (s : stream A) : A :=

--- a/theories/stringmap.v
+++ b/theories/stringmap.v
@@ -17,7 +17,7 @@ Let R {A} (s : string) (m : stringmap A) (n1 n2 : N) :=
 Lemma fresh_string_step {A} s (m : stringmap A) n x :
  m !! (s +:+ pretty n) = Some x → R s m (1 + n) n.
 Proof. split; [lia|]. replace (1 + n - 1) with n by lia; eauto. Qed.
-Lemma fresh_string_R_wf {A} s (m : stringmap A) : wf (R s m).
+Lemma fresh_string_R_wf {A} s (m : stringmap A) : well_founded (R s m).
 Proof.
  induction (map_wf m) as [m _ IH]. intros n1; constructor; intros n2 [Hn Hs].
  specialize (IH _ (delete_subset m (s +:+ pretty (n2 - 1)) Hs) n2).

--- a/stdpp/strings.v
+++ b/stdpp/strings.v
+From Coq Require Import Ascii.
+From Coq Require String.
+From stdpp Require Export list.
+From stdpp Require Import countable.
+From stdpp Require Import options.
+(** We define the ascii/string methods in corresponding modules, similar to what
+is done for numbers. These modules should generally not be imported, e.g., use
+[Ascii.is_nat] instead. *)
+(** To avoid poluting the global namespace, we export only the [string] data
+type (with its constructors and eliminators) and notations. *)
+Export String (string(..)).
+Export (notations) String.
+(** Enable the string literal and append notation in [stdpp_scope], making
+it possible to write string literals as "foo" instead of "foo"%string.
+One could also enable the string literal notation via [Open Scope string_scope]
+but that overrides various notations (e.g, [=?] on [nat]) with the version for
+strings. *)
+String Notation string
+  String.string_of_list_byte String.list_byte_of_string : stdpp_scope.
+Infix "+:+" := String.append (at level 60, right associativity) : stdpp_scope.
+(** * Encoding and decoding *)
+(** The [Countable] instance of [string] is particularly useful to allow strings
+to be used as keys in [gmap].
+The encoding of [string] to [positive] is taken from
+https://github.com/xavierleroy/canonical-binary-tries/blob/v2/lib/String2pos.v.
+It avoids creating auxiliary data structures such as [list bool], thereby
+improving efficiency.
+We first provide some [Local] helper functions and then define the [Countable]
+instances for encoding/decoding in the modules [Ascii] and [String]. End-users
+should always use these instances. *)
+Local Definition bool_cons_pos (b : bool) (p : positive) : positive :=
+  if b then p~1 else p~0.
+Local Definition ascii_cons_pos (c : ascii) (p : positive) : positive :=
+  match c with
+  | Ascii b0 b1 b2 b3 b4 b5 b6 b7 =>
+     bool_cons_pos b0 $ bool_cons_pos b1 $ bool_cons_pos b2 $
+       bool_cons_pos b3 $ bool_cons_pos b4 $ bool_cons_pos b5 $
+       bool_cons_pos b6 $ bool_cons_pos b7 p
+  end.
+Local Fixpoint string_to_pos (s : string) : positive :=
+  match s with
+  | EmptyString => 1
+  | String c s => ascii_cons_pos c (string_to_pos s)
+  end.
+(* The decoder that turns [positive] into string results in 256 cases (we need
+to peel off 8 times a [~0]/[~1] constructor) and a number of fall through cases.
+We avoid writing these cases explicitly by generating the definition using Ltac.
+The lemma [string_of_to_pos] ensures the generated definition is correct.
+Alternatively, we could implement it in two steps. Convert the [positive] to
+[list bool], and convert the list to [string]. This definition will be slower
+since auxiliary data structures are created. *)
+Local Fixpoint pos_to_string (p : positive) : string.
+Proof.
+  (** The argument [p] is the [positive] that we are peeling off.
+  The argument [a] is the constructor [Ascii] partially applied to some number
+  of Booleans (so its Coq type changes during the iteration).
+  The argument [n] says how many more Booleans are needed to make this fully
+  applied so that the [constr] has type ascii. *)
+  let rec gen p a n :=
+    lazymatch n with
+    (* This character is done. Stop the ltac recursion; recursively invoke
+    [pos_to_string] on the Gallina level for the remaining bits. *)
+    | 0 => exact (String a (pos_to_string p))
+    (* There are more bits to consume for this character, generate an
+    appropriate [match] with ltac. *)
+    | S ?n =>
+       exact (match p with
+              | 1 => EmptyString
+              | p~0 => ltac:(gen p (a false) n)
+              | p~1 => ltac:(gen p (a true) n)
+              end%positive)
+    end in
+  gen p Ascii 8.
+Defined.
+Local Lemma pos_to_string_string_to_pos s : pos_to_string (string_to_pos s) = s.
+Proof. induction s as [|[[][][][][][][][]]]; by f_equal/=. Qed.
+Module Ascii.
+  Global Instance eq_dec : EqDecision ascii := ascii_dec.
+  Global Program Instance countable : Countable ascii := {|
+    encode a := string_to_pos (String a EmptyString);
+    decode p := match pos_to_string p return _ with String a _ => Some a | _ => None end
+  |}.
+  Next Obligation. by intros [[] [] [] [] [] [] [] []]. Qed.
+  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.
+  Definition is_space (x : ascii) : bool :=
+    match x with
+    | "009" | "010" | "011" | "012" | "013" | " " => true | _ => false
+    end%char.
+End Ascii.
+Module String.
+  (** Use a name that is consistent with [list]. *)
+  Notation app := String.append.
+  (** And obtain a proper behavior for [simpl]. *)
+  Global Arguments app : simpl never.
+  Global Instance eq_dec : EqDecision string.
+  Proof. solve_decision. Defined.
+  Global Instance inhabited : Inhabited string := populate "".
+  Global Program Instance countable : Countable string := {|
+    encode := string_to_pos;
+    decode p := Some (pos_to_string p)
+  |}.
+  Solve Obligations with
+    naive_solver eauto using pos_to_string_string_to_pos with f_equal.
+  Definition le (s1 s2 : string) : Prop := String.leb s1 s2.
+  Global Instance le_dec : RelDecision le.
+  Proof. intros s1 s2. apply _. Defined.
+  Global Instance le_pi s1 s2 : ProofIrrel (le s1 s2).
+  Proof. apply _. Qed.
+  Global Instance le_po : PartialOrder le.
+  Proof.
+    unfold le. split; [split|].
+    - intros s. unfold String.leb. assert ((s ?= s)%string = Eq) as ->; [|done].
+      induction s; simpl; [done|].
+      unfold Ascii.compare. by rewrite N.compare_refl.
+    - intros s1 s2 s3. unfold String.leb.
+      destruct (s1 ?= s2)%string eqn:Hs12; [..|done].
+      { by apply String.compare_eq_iff in Hs12 as ->. }
+      destruct (s2 ?= s3)%string eqn:Hs23; [..|done].
+      { apply String.compare_eq_iff in Hs23 as ->. by rewrite Hs12. }
+      assert ((s1 ?= s3)%string = Lt) as ->; [|done].
+      revert s2 s3 Hs12 Hs23.
+      induction s1 as [|a1 s1]; intros [|a2 s2] [|a3 s3] ??;
+        simplify_eq/=; [done..|].
+      destruct (Ascii.compare a1 a2) eqn:Ha12; simplify_eq/=.
+      { apply Ascii.compare_eq_iff in Ha12 as ->.
+        destruct (Ascii.compare a2 a3); simpl; eauto. }
+      destruct (Ascii.compare a2 a3) eqn:Ha23; simplify_eq/=.
+      { apply Ascii.compare_eq_iff in Ha23 as ->. by rewrite Ha12. }
+      assert (Ascii.compare a1 a3 = Lt) as ->; [|done].
+      apply N.compare_lt_iff. by etrans; apply N.compare_lt_iff.
+    - intros s1 s2 ?%Is_true_true ?%Is_true_true. by apply String.leb_antisym.
+  Qed.
+  Global Instance le_total : Total le.
+  Proof.
+    intros s1 s2. unfold le. destruct (String.leb_total s1 s2) as [->| ->]; auto.
+  Qed.
+  Global Instance app_inj s1 : Inj (=) (=) (app s1).
+  Proof. intros ???. induction s1; simplify_eq/=; f_equal/=; auto. Qed.
+  Fixpoint rev_app (s1 s2 : string) : string :=
+    match s1 with
+    | "" => s2
+    | String a s1 => rev_app s1 (String a s2)
+    end.
+  Definition rev (s : string) : string := rev_app s "".
+  (* Break a string up into lists of words, delimited by white space *)
+  Fixpoint words_go (cur : option string) (s : string) : list string :=
+    match s with
+    | "" => option_list (rev <$> cur)
+    | String a s =>
+       if Ascii.is_space a
+       then option_list (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.
+End String.
+Infix "≤" := String.le : string_scope.
+Notation "(≤)" := String.le (only parsing) : string_scope.
+Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%string : string_scope.
+Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%string : string_scope.
+Global Hint Extern 0 (_ ≤ _)%string => reflexivity : core.
--- a/theories/tactics.v
+++ b/theories/tactics.v
 (** This file collects general purpose tactics that are used throughout
 the development. *)
-From Coq Require Import Omega.
 From Coq Require Export Lia.
 From stdpp Require Export decidable.
 From stdpp Require Import options.
@@ -21,17 +20,23 @@ Ltac f_equal :=
 (** We declare hint databases [f_equal], [congruence] and [lia] and containing
 solely the tactic corresponding to its name. These hint database are useful in
 to be combined in combination with other hint database. *)
-Hint Extern 998 (_ = _) => f_equal : f_equal.
+Global Hint Extern 998 (_ = _) => f_equal : f_equal.
-Hint Extern 999 => congruence : congruence.
+Global Hint Extern 999 => congruence : congruence.
-Hint Extern 1000 => lia : lia.
+Global Hint Extern 1000 => lia : lia.
-Hint Extern 1000 => omega : omega.
+Global Hint Extern 1001 => progress subst : subst. (** backtracking on this one will
-Hint Extern 1001 => progress subst : subst. (** backtracking on this one will
 be very bad, so use with care! *)
 (** The tactic [intuition] expands to [intuition auto with *] by default. This
-is rather efficient when having big hint databases, or expensive [Hint Extern]
+is rather inefficient when having big hint databases, or expensive [Hint Extern]
 declarations as the ones above. *)
-Tactic Notation "intuition" := intuition auto.
+Ltac intuition_solver ::= auto.
+(** The [fast_reflexivity] tactic only works on syntactically equal terms. It
+can be used to avoid expensive failing unification. *)
+Ltac fast_reflexivity :=
+  match goal with
+  | |- _ ?x ?x => solve [simple apply reflexivity]
+  end.
 (** [done] can get slow as it calls "trivial". [fast_done] can solve way less
 goals, but it will also always finish quickly.  We do 'reflexivity' last because
@@ -46,6 +51,9 @@ Ltac fast_done :=
 Tactic Notation "fast_by" tactic(tac) :=
  tac; fast_done.
+Class TCFastDone (P : Prop) : Prop := tc_fast_done : P.
+Global Hint Extern 1 (TCFastDone ?P) => (change P; fast_done) : typeclass_instances.
 (** A slightly modified version of Ssreflect's finishing tactic [done]. It
 also performs [reflexivity] and uses symmetry of negated equalities. Compared
 to Ssreflect's [done], it does not compute the goal's [hnf] so as to avoid
@@ -75,7 +83,7 @@ Ltac done_if b :=
  | false => idtac
  end.
-(** Aliases for trans and etrans that are easier to type *)
+(** Aliases for transitivity and etransitivity that are easier to type *)
 Tactic Notation "trans" constr(A) := transitivity A.
 Tactic Notation "etrans" := etransitivity.
@@ -162,11 +170,27 @@ Tactic Notation "destruct_or" "!" :=
 (** The tactic [case_match] destructs an arbitrary match in the conclusion or
 assumptions, and generates a corresponding equality. This tactic is best used
 together with the [repeat] tactical. *)
+Tactic Notation "case_match" "eqn" ":" ident(Hd) :=
+  match goal with
+  | H : context [ match ?x with _ => _ end ] |- _ => destruct x eqn:Hd
+  | |- context [ match ?x with _ => _ end ] => destruct x eqn:Hd
+  end.
 Ltac case_match :=
+  let H := fresh in case_match eqn:H.
+Tactic Notation "case_guard" "as" ident(Hx) :=
  match goal with
-  | H : context [ match ?x with _ => _ end ] |- _ => destruct x eqn:?
+  | H : context C [@guard_or ?E ?e ?M ?T ?R ?P ?dec] |- _ =>
-  | |- context [ match ?x with _ => _ end ] => destruct x eqn:?
+      change (@guard_or E e M T R P dec) with (
+        match @decide P dec with left H' => @mret M R P H' | _ => @mthrow E M T P e end) in *;
+      destruct_decide (@decide P dec) as Hx
+  | |- context C [@guard_or ?E ?e ?M ?T ?R ?P ?dec] =>
+      change (@guard_or E e M T R P dec) with (
+        match @decide P dec with left H' => @mret M R P H' | _ => @mthrow E M T P e end) in *;
+      destruct_decide (@decide P dec) as Hx
  end.
+Tactic Notation "case_guard" :=
+  let H := fresh in case_guard as H.
 (** The tactic [unless T by tac_fail] succeeds if [T] is not provable by
 the tactic [tac_fail]. *)
@@ -179,7 +203,8 @@ Tactic Notation "repeat_on_hyps" tactic3(tac) :=
  repeat match goal with H : _ |- _ => progress tac H end.
 (** The tactic [clear dependent H1 ... Hn] clears the hypotheses [Hi] and
-their dependencies. *)
+their dependencies. This provides an n-ary variant of Coq's standard
+[clear dependent]. *)
 Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) :=
  clear dependent H1; clear dependent H2.
 Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) hyp(H3) :=
@@ -216,6 +241,49 @@ does the converse. *)
 Ltac var_eq x1 x2 := match x1 with x2 => idtac | _ => fail 1 end.
 Ltac var_neq x1 x2 := match x1 with x2 => fail 1 | _ => idtac end.
+(** The tactic [mk_evar T] returns a new evar of type [T], without affecting the
+current context.
+This is usually a more useful behavior than Coq's [evar], which is a
+side-effecting tactic (not returning anything) that introduces a local
+definition into the context that holds the evar.
+Note that the obvious alternative [open_constr (_:T)] has subtly different
+behavior, see std++ issue 115.
+Usually, Ltacs cannot return a value and have a side-effect, but we use the
+trick described at
+<https://stackoverflow.com/questions/45949064/check-for-evars-in-a-tactic-that-returns-a-value/46178884#46178884>
+to work around that: wrap the side-effect in a [match goal]. *)
+Ltac mk_evar T :=
+  let T := constr:(T : Type) in
+  let e := fresh in
+  let _ := match goal with _ => evar (e:T) end in
+  let e' := eval unfold e in e in
+  let _ := match goal with _ => clear e end in
+  e'.
+(** The tactic [get_head t] returns the head function [f] when [t] is of the
+shape [f a1 ... aN]. This is purely syntactic, no unification is performed. *)
+Ltac get_head e :=
+  lazymatch e with
+  | ?h _ => get_head h
+  | _    => e
+  end.
+(** The tactic [eunify x y] succeeds if [x] and [y] can be unified, and fails
+otherwise. If it succeeds, it will instantiate necessary evars in [x] and [y].
+Contrary to Coq's standard [unify] tactic, which uses [constr] for the arguments
+[x] and [y], [eunify] uses [open_constr] so that one can use holes (i.e., [_]s).
+For example, it allows one to write [eunify x (S _)], which will test if [x]
+unifies a successor. *)
+Tactic Notation "eunify" open_constr(x) open_constr(y) :=
+  unify x y.
+(** The tactic [no_new_unsolved_evars tac] executes [tac] and fails if it
+creates any new evars or leaves behind any subgoals. *)
+Ltac no_new_unsolved_evars tac := solve [unshelve tac].
 (** Operational type class projections in recursive calls are not folded back
 appropriately by [simpl]. The tactic [csimpl] uses the [fold_classes] tactics
 to refold recursive calls of [fmap], [mbind], [omap] and [alter]. A
@@ -317,6 +385,14 @@ Ltac setoid_subst :=
  | H : @equiv ?A ?e _ ?x |- _ => symmetry in H; setoid_subst_aux (@equiv A e) x
  end.
+(** A little helper for [f_equiv] and [solve_proper] that simplifies away [flip]
+relations. *)
+Ltac clean_flip :=
+  repeat match goal with
+  | |- (flip ?R) ?x ?y => change (R y x)
+  | H : (flip ?R) ?x ?y |- _ => change (R y x) in H
+  end.
 (** f_equiv works on goals of the form [f _ = f _], for any relation and any
 number of arguments. It looks for an appropriate [Proper] instance, and applies
 it. The tactic is somewhat limited, since it cannot be used to backtrack on
@@ -326,66 +402,102 @@ we try to "maintain" the relation of the current goal. For example,
 when having [Proper (equiv ==> dist) f] and [Proper (dist ==> dist) f], it will
 favor the second because the relation (dist) stays the same. *)
 Ltac f_equiv :=
+  (* Simplify away [flip], they would get in the way later. *)
+  clean_flip;
+  (* Find out what kind of goal we have, and try to make progress. *)
  match goal with
+  (* Similar to [f_equal] also handle the reflexivity case. *)
+  | |- _ ?x ?x => fast_reflexivity
+  (* Making progress on [pointwise_relation] is as simple as introducing the variable. *)
  | |- pointwise_relation _ _ _ _ => intros ?
  (* We support matches on both sides, *if* they concern the same variable, or
-     variables in some relation. *)
+     terms in some relation. *)
  | |- ?R (match ?x with _ => _ end) (match ?x with _ => _ end) =>
    destruct x
  | H : ?R ?x ?y |- ?R2 (match ?x with _ => _ end) (match ?y with _ => _ end) =>
     destruct H
-  (* First assume that the arguments need the same relation as the result *)
+  (* First assume that the arguments need the same relation as the result. We
-  | |- ?R (?f _) _ => simple apply (_ : Proper (R ==> R) f)
+  check the most restrictive pattern first: [(?f _) (?f _)] requires all but the
-  | |- ?R (?f _ _) _ => simple apply (_ : Proper (R ==> R ==> R) f)
+  last argument to be syntactically equal. *)
-  | |- ?R (?f _ _ _) _ => simple apply (_ : Proper (R ==> R ==> R ==> R) f)
+  | |- ?R (?f _) (?f _) => simple apply (_ : Proper (R ==> R) f)
-  | |- ?R (?f _ _ _ _) _ => simple apply (_ : Proper (R ==> R ==> R ==> R ==> R) f)
+  | |- ?R (?f _ _) (?f _ _) => simple apply (_ : Proper (R ==> R ==> R) f)
+  | |- ?R (?f _ _ _) (?f _ _ _) => simple apply (_ : Proper (R ==> R ==> R ==> R) f)
+  | |- ?R (?f _ _ _ _) (?f _ _ _ _) => simple apply (_ : Proper (R ==> R ==> R ==> R ==> R) f)
+  | |- ?R (?f _ _ _ _ _) (?f _ _ _ _ _) => simple apply (_ : Proper (R ==> R ==> R ==> R ==> R ==> R) f)
  (* For the case in which R is polymorphic, or an operational type class,
  like equiv. *)
-  | |- (?R _) (?f _) _ => simple apply (_ : Proper (R _ ==> _) f)
+  | |- (?R _) (?f _) (?f _) => simple apply (_ : Proper (R _ ==> R _) f)
-  | |- (?R _ _) (?f _) _ => simple apply (_ : Proper (R _ _ ==> _) f)
+  | |- (?R _ _) (?f _) (?f _) => simple apply (_ : Proper (R _ _ ==> R _ _) f)
-  | |- (?R _ _ _) (?f _) _ => simple apply (_ : Proper (R _ _ _ ==> _) f)
+  | |- (?R _ _ _) (?f _) (?f _) => simple apply (_ : Proper (R _ _ _ ==> R _ _ _) f)
-  | |- (?R _) (?f _ _) _ => simple apply (_ : Proper (R _ ==> R _ ==> _) f)
-  | |- (?R _ _) (?f _ _) _ => simple apply (_ : Proper (R _ _ ==> R _ _ ==> _) f)
+  | |- (?R _) (?f _ _) (?f _ _) => simple apply (_ : Proper (R _ ==> R _ ==> R _) f)
-  | |- (?R _ _ _) (?f _ _) _ => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> _) f)
+  | |- (?R _ _) (?f _ _) (?f _ _) => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _) f)
-  | |- (?R _) (?f _ _ _) _ => simple apply (_ : Proper (R _ ==> R _ ==> R _ ==> _) f)
+  | |- (?R _ _ _) (?f _ _) (?f _ _) => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> R _ _ _) f)
-  | |- (?R _ _) (?f _ _ _) _ => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _ ==> _) f)
-  | |- (?R _ _ _) (?f _ _ _) _ => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ R _ _ _ ==> _) f)
+  | |- (?R _) (?f _ _ _) (?f _ _ _) => simple apply (_ : Proper (R _ ==> R _ ==> R _ ==> R _) f)
-  | |- (?R _) (?f _ _ _ _) _ => simple apply (_ : Proper (R _ ==> R _ ==> R _ ==> R _ ==> _) f)
+  | |- (?R _ _) (?f _ _ _) (?f _ _ _) => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _ ==> R _ _) f)
-  | |- (?R _ _) (?f _ _ _ _) _ => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _ ==> R _ _ ==> _) f)
+  | |- (?R _ _ _) (?f _ _ _) (?f _ _ _) => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _) f)
-  | |- (?R _ _ _) (?f _ _ _ _) _ => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ R _ _ _ ==> R _ _ _ ==> _) f)
-  (* Next, try to infer the relation. Unfortunately, very often, it will turn
+  | |- (?R _) (?f _ _ _ _) (?f _ _ _ _) => simple apply (_ : Proper (R _ ==> R _ ==> R _ ==> R _ ==> R _) f)
-     the goal into a Leibniz equality so we get stuck. *)
+  | |- (?R _ _) (?f _ _ _ _) (?f _ _ _ _) => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _ ==> R _ _ ==> R _ _) f)
-  (* TODO: Can we exclude that instance? *)
+  | |- (?R _ _ _) (?f _ _ _ _) (?f _ _ _ _) => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _) f)
+  | |- (?R _) (?f _ _ _ _ _) (?f _ _ _ _ _) => simple apply (_ : Proper (R _ ==> R _ ==> R _ ==> R _ ==> R _ ==> R _) f)
+  | |- (?R _ _) (?f _ _ _ _ _) (?f _ _ _ _ _) => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _ ==> R _ _ ==> R _ _ ==> R _ _) f)
+  | |- (?R _ _ _) (?f _ _ _ _ _) (?f _ _ _ _ _) => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _) f)
+  (* In case the function symbol differs, but the arguments are the same, maybe
+     we have a relation about those functions in our context that we can simply
+     apply. (The case where the arguments differ is a lot more complicated; with
+     the way we typically define the relations on function spaces it further
+     requires [Proper]ness of [f] or [g]). *)
+  | H : _ ?f ?g |- ?R (?f ?x) (?g ?x) => solve [simple apply H]
+  | H : _ ?f ?g |- ?R (?f ?x ?y) (?g ?x ?y) => solve [simple apply H]
+  (* Fallback case: try to infer the relation, and allow the function to not be
+     syntactically the same on both sides. Unfortunately, very often, it will
+     turn the goal into a Leibniz equality so we get stuck. Furthermore, looking
+     for instances in this order will mean that Coq will try to unify the
+     remaining arguments that we have not explicitly generalized, which can be
+     very slow -- but if we go for the opposite order, we will hit the Leibniz
+     equality fallback instance even more often. *)
+  (* TODO: Can we exclude that Leibniz equality instance? *)
  | |- ?R (?f _) _ => simple apply (_ : Proper (_ ==> R) f)
  | |- ?R (?f _ _) _ => simple apply (_ : Proper (_ ==> _ ==> R) f)
  | |- ?R (?f _ _ _) _ => simple apply (_ : Proper (_ ==> _ ==> _ ==> R) f)
  | |- ?R (?f _ _ _ _) _ => simple apply (_ : Proper (_ ==> _ ==> _ ==> _ ==> R) f)
-  (* In case the function symbol differs, but the arguments are the same,
+  | |- ?R (?f _ _ _ _ _) _ => simple apply (_ : Proper (_ ==> _ ==> _ ==> _ ==> _ ==> R) f)
-     maybe we have a pointwise_relation in our context. *)
-  (* TODO: If only some of the arguments are the same, we could also
-     query for "pointwise_relation"'s. But that leads to a combinatorial
-     explosion about which arguments are and which are not the same. *)
-  | H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) => simple apply H
-  | H : pointwise_relation _ (pointwise_relation _ ?R) ?f ?g |- ?R (?f ?x ?y) (?g ?x ?y) => simple apply H
  end;
-  try simple apply reflexivity.
+  (* Similar to [f_equal] immediately solve trivial goals *)
+  try fast_reflexivity.
 Tactic Notation "f_equiv" "/=" := csimpl in *; f_equiv.
+(** The typeclass [SolveProperSubrelation] is used by the [solve_proper] tactic
+when the goal is of the form [R1 x y] and there are assumptions of the form [R2
+x y]. We cannot use Coq's [subrelation] class here as adding the [subrelation]
+instances causes lots of backtracking in the [Proper] hint search, resulting in
+very slow/diverging [rewrite]s due to exponential instance search. *)
+Class SolveProperSubrelation {A} (R R' : relation A) :=
+  is_solve_proper_subrelation x y : R x y → R' x y.
+(** We use [!] to handle indexed relations such as [dist], where we
+can have an [R n] assumption and a [R ?m] goal. *)
+Global Hint Mode SolveProperSubrelation + ! ! : typeclass_instances.
+Global Arguments is_solve_proper_subrelation {A R R' _ x y}.
+Global Instance subrelation_solve_proper_subrelation {A} (R R' : relation A) :
+  subrelation R R' →
+  SolveProperSubrelation R R'.
+Proof. intros ???. apply is_subrelation. Qed.
 (** The tactic [solve_proper_unfold] unfolds the first head symbol, so that
 we proceed by repeatedly using [f_equiv]. *)
 Ltac solve_proper_unfold :=
  (* Try unfolding the head symbol, which is the one we are proving a new property about *)
-  lazymatch goal with
+  try lazymatch goal with
-  | |- ?R (?f _ _ _ _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _ _ _ _) => unfold f
+  | |- ?R ?t1 ?t2 =>
-  | |- ?R (?f _ _ _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _ _ _) => unfold f
+    let h1 := get_head t1 in
-  | |- ?R (?f _ _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _ _) => unfold f
+    let h2 := get_head t2 in
-  | |- ?R (?f _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _) => unfold f
+    unify h1 h2;
-  | |- ?R (?f _ _ _ _ _ _) (?f _ _ _ _ _ _) => unfold f
+    unfold h1
-  | |- ?R (?f _ _ _ _ _) (?f _ _ _ _ _) => unfold f
-  | |- ?R (?f _ _ _ _) (?f _ _ _ _) => unfold f
-  | |- ?R (?f _ _ _) (?f _ _ _) => unfold f
-  | |- ?R (?f _ _) (?f _ _) => unfold f
-  | |- ?R (?f _) (?f _) => unfold f
  end.
 (** [solve_proper_prepare] does some preparation work before the main
 [solve_proper] loop.  Having this as a separate tactic is useful for debugging
@@ -409,17 +521,30 @@ Ltac solve_proper_prepare :=
     (* Now forcefully introduce the first ∀ and other ∀s that show up in the
     goal afterwards. *)
     intros ?; intros
-  end; simplify_eq;
+  end;
+  (* Simplify things, if we can. *)
+  simplify_eq;
  (* We try with and without unfolding. We have to backtrack on
     that because unfolding may succeed, but then the proof may fail. *)
  (solve_proper_unfold + idtac); simpl.
+(** [solve_proper_finish] is basically a version of [eassumption]
+that can also take into account [subrelation]. *)
+Ltac solve_proper_finish :=
+  (* We always try this first, since the syntactic match below is not always
+  able to find the assumptions we are looking for (e.g. when [Some x ⊑ Some y]
+  is convertible to [x ⊑ y]). *)
+  eassumption ||
+  match goal with
+  | H : ?R1 ?x ?y |- ?R2 ?x ?y =>
+    no_new_unsolved_evars ltac:(eapply (is_solve_proper_subrelation H))
+  end.
 (** The tactic [solve_proper_core tac] solves goals of the form "Proper (R1 ==> R2)", for
 any number of relations. The actual work is done by repeatedly applying
 [tac]. *)
 Ltac solve_proper_core tac :=
  solve_proper_prepare;
-  (* Now do the job. *)
+  (* Now do the job. The inner tactics can rely on [flip] having been cleaned. *)
-  solve [repeat first [eassumption | tac ()] ].
+  solve [repeat (clean_flip; first [solve_proper_finish | tac ()]) ].
 (** Finally, [solve_proper] tries to apply [f_equiv] in a loop. *)
 Ltac solve_proper := solve_proper_core ltac:(fun _ => f_equiv).
@@ -433,74 +558,185 @@ Ltac intros_revert tac :=
  end.
 (** The tactic [iter tac l] runs [tac x] for each element [x ∈ l] until [tac x]
-succeeds. If it does not suceed for any element of the generated list, the whole
+succeeds. If it does not succeed for any element of the generated list, the whole
 tactic wil fail. *)
 Tactic Notation "iter" tactic(tac) tactic(l) :=
  let rec go l :=
  match l with ?x :: ?l => tac x || go l end in go l.
-(** Given [H : A_1 → ... → A_n → B] (where each [A_i] is non-dependent), the
+(** Runs [tac] on the n-th hypothesis that can be introduced from the goal. *)
-tactic [feed tac H tac_by] creates a subgoal for each [A_i] and calls [tac p]
+Ltac num_tac n tac :=
-with the generated proof [p] of [B]. *)
+  intros until n;
-Tactic Notation "feed" tactic(tac) constr(H) :=
+  lazymatch goal with
-  let rec go H :=
+  (* matches the last hypothesis, which is what we want *)
-  let T := type of H in
+  | H : _ |- _ => tac H
-  lazymatch eval hnf in T with
+  end.
-  | ?T1 → ?T2 =>
-    (* Use a separate counter for fresh names to make it more likely that
+(** The tactic [inv] is a fixed version of [inversion_clear] from the standard
-    the generated name is "fresh" with respect to those generated before
+library that works around <https://github.com/coq/coq/issues/2465>. It also
-    calling the [feed] tactic. In particular, this hack makes sure that
+has a shorter name since clearing is the default for [destruct], why wouldn't
-    tactics like [let H' := fresh in feed (fun p => pose proof p as H') H] do
+it also be the default for inversion?
-    not break. *)
+This is inspired by CompCert's [inv] tactic
-    let HT1 := fresh "feed" in assert T1 as HT1;
+<https://github.com/AbsInt/CompCert/blob/5f761eb8456609d102acd8bc780b6fd3481131ef/lib/Coqlib.v#L30>. *)
-      [| go (H HT1); clear HT1 ]
+Tactic Notation "inv" ident(H) "as" simple_intropattern(ipat) :=
-  | ?T1 => tac H
+  inversion H as ipat; clear H; simplify_eq.
-  end in go H.
+Tactic Notation "inv" ident(H) :=
+  inversion H; clear H; simplify_eq.
-(** The tactic [efeed tac H] is similar to [feed], but it also instantiates
-dependent premises of [H] with evars. *)
+(* We overload the notation with [integer] and [ident] to support
-Tactic Notation "efeed" constr(H) "using" tactic3(tac) "by" tactic3 (bytac) :=
+[inv H] and [inv 1], like the regular [inversion] tactic. *)
-  let rec go H :=
+Tactic Notation "inv" integer(n) "as" simple_intropattern(ipat) :=
-  let T := type of H in
+  num_tac n ltac:(fun H => inv H as ipat).
-  lazymatch eval hnf in T with
+Tactic Notation "inv" integer(n) :=
+  num_tac n ltac:(fun H => inv H).
+(** * The "o" family of tactics equips [pose proof], [destruct], [inversion],
+[generalize] and [specialize] with support for "o"pen terms. You can leave
+underscores that become evars or subgoals, similar to [refine]. You can suffix
+the tactic with [*] (e.g., [opose proof*]) to eliminate all remaining ∀ and →
+(i.e., add underscores for the remaining arguments). For [odestruct] and
+[oinversion], eliminating all remaining ∀ and → is the default (hence there is
+no [*] version). *)
+(** The helper [opose_core p tac] takes a uconstr [p] and turns it into a constr
+that is passed to [tac]. All underscores inside [p] become evars, and the ones
+that are unifiable (i.e, appear in the type of other evars) are shelved.
+This is similar to creating a [open_constr], except that we have control over
+what does and does not get shelved. Creating a [open_constr] would shelve every
+created evar, which is not what we want, and it is hard to avoid since it
+happens very early (before we can easily wrap things in [unshelve]). *)
+Ltac opose_core p tac :=
+  (* The "opose_internal" here is useful for debugging but not helpful for name
+  collisions since it gets ignored with name mangling. The [clear] below is what
+  ensures we don't get name collisions. *)
+  let i := fresh "opose_internal" in
+  unshelve (epose _ as i);
+    [shelve (*type of [p]*)
+    |refine p (* will create the subgoals, and shelve some of them *)
+    |(* Now we have [i := t] in the context, let's get the [t] and remove [i]. *)
+     let t := eval unfold i in i in
+     (* We want to leave the context exactly as we found it, to avoid
+     any issues with fresh name generation. So clear [i] before calling
+     the user-visible tactic. *)
+     clear i;
+     tac t];
+  (* [tac] might have added more subgoals, making some existing ones
+  unifiable, so we need to shelve again. *)
+  shelve_unifiable.
+(** Turn all leading ∀ and → of [p] into evars (∀-evars will be shelved), and
+call [tac] with the term applied with those evars. This fill unfold definitions
+to find leading ∀/→.
+The type of [p] will be normalized by calling the [normalizer] function.
+[_name_guard] is an unused argument where you can pass anything you want. If the
+argument is an intro pattern, those will be taken into account by the [fresh]
+that is inside this tactic, avoiding name collisions that can otherwise arise.
+This is a work-around for https://github.com/coq/coq/issues/18109. *)
+Ltac evar_foralls p _name_guard normalizer tac :=
+  let T := type of p in
+  lazymatch normalizer T with
  | ?T1 → ?T2 =>
-    let HT1 := fresh "feed" in assert T1 as HT1;
+    (* This is the [fresh] where the presence of [_name_guard] matters.
-      [bytac | go (H HT1); clear HT1 ]
+    Note that the "opose_internal" is nice but not sufficient because
-  | ?T1 → _ =>
+    it gets ignored when name mangling is enabled. *)
-    let e := fresh "feed" in evar (e:T1);
+    let pT1 := fresh "__evar_foralls_internal" in
-    let e' := eval unfold e in e in
+    assert T1 as pT1; [| evar_foralls (p pT1) _name_guard normalizer tac; clear pT1]
-    clear e; go (H e')
+  | ∀ x : ?T1, _ =>
-  | ?T1 => tac H
+    let e := mk_evar T1 in
-  end in go H.
+    evar_foralls (p e) _name_guard normalizer tac
-Tactic Notation "efeed" constr(H) "using" tactic3(tac) :=
+  | ?T1 => tac p
-  efeed H using tac by idtac.
+  end.
-(** The following variants of [pose proof], [specialize], [inversion], and
+Ltac opose_specialize_foralls_core p _name_guard tac :=
-[destruct], use the [feed] tactic before invoking the actual tactic. *)
+  opose_core p ltac:(fun p =>
-Tactic Notation "feed" "pose" "proof" constr(H) "as" ident(H') :=
+    evar_foralls p _name_guard ltac:(fun t => eval hnf in t) tac).
-  feed (fun p => pose proof p as H') H.
-Tactic Notation "feed" "pose" "proof" constr(H) :=
+Tactic Notation "opose" "proof" uconstr(p) "as" simple_intropattern(pat) :=
-  feed (fun p => pose proof p) H.
+  opose_core p ltac:(fun p => pose proof p as pat).
+Tactic Notation "opose" "proof" "*" uconstr(p) "as" simple_intropattern(pat) :=
-Tactic Notation "efeed" "pose" "proof" constr(H) "as" ident(H') :=
+  opose_specialize_foralls_core p pat ltac:(fun p => pose proof p as pat).
-  efeed H using (fun p => pose proof p as H').
-Tactic Notation "efeed" "pose" "proof" constr(H) :=
+Tactic Notation "opose" "proof" uconstr(p) := opose proof p as ?.
-  efeed H using (fun p => pose proof p).
+Tactic Notation "opose" "proof" "*" uconstr(p) := opose proof* p as ?.
-Tactic Notation "feed" "specialize" hyp(H) :=
+Tactic Notation "ogeneralize" uconstr(p) :=
-  feed (fun p => specialize p) H.
+  opose_core p ltac:(fun p => generalize p).
-Tactic Notation "efeed" "specialize" hyp(H) :=
+Tactic Notation "ogeneralize" "*" uconstr(p) :=
-  efeed H using (fun p => specialize p).
+  opose_specialize_foralls_core p () ltac:(fun p => generalize p).
-Tactic Notation "feed" "inversion" constr(H) :=
+(** Similar to [edestruct], [odestruct] will never clear the destructed
-  feed (fun p => let H':=fresh in pose proof p as H'; inversion H') H.
+variable. *)
-Tactic Notation "feed" "inversion" constr(H) "as" simple_intropattern(IP) :=
+(** No [*] versions for [odestruct] and [oinversion]: we always specialize all
-  feed (fun p => let H':=fresh in pose proof p as H'; inversion H' as IP) H.
+foralls and implications; otherwise it does not make sense to destruct/invert.
+We also do not support [eqn:EQ]; this would not make sense for most users of
-Tactic Notation "feed" "destruct" constr(H) :=
+this tactic since the term being destructed is [some_lemma ?evar ?proofterm]. *)
-  feed (fun p => let H':=fresh in pose proof p as H'; destruct H') H.
+Tactic Notation "odestruct" uconstr(p) :=
-Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
+  opose_specialize_foralls_core p () ltac:(fun p => destruct p).
-  feed (fun p => let H':=fresh in pose proof p as H'; destruct H' as IP) H.
+Tactic Notation "odestruct" uconstr(p) "as" simple_intropattern(pat) :=
+  opose_specialize_foralls_core p pat ltac:(fun p => destruct p as pat).
+Tactic Notation "oinversion" uconstr(p) "as" simple_intropattern(pat) :=
+  opose_specialize_foralls_core p pat ltac:(fun p =>
+    (* We have to create a temporary as [inversion] does not support
+    general terms; then we clear the temporary. *)
+    let Hp := fresh in pose proof p as Hp; inversion Hp as pat; clear Hp).
+Tactic Notation "oinversion" uconstr(p) :=
+  opose_specialize_foralls_core p () ltac:(fun p =>
+    let Hp := fresh in pose proof p as Hp; inversion Hp; clear Hp).
+Tactic Notation "oinv" uconstr(p) "as" simple_intropattern(pat) :=
+  opose_specialize_foralls_core p pat ltac:(fun p =>
+    (* If it is a variable we want to call [inv] on it directly
+    so that it gets cleared. *)
+    tryif is_var p then
+      inv p as pat
+    else
+      (* No need to [clear Hp]; [inv] does that. *)
+      let Hp := fresh in pose proof p as Hp; inv Hp as pat).
+Tactic Notation "oinv" uconstr(p) :=
+  opose_specialize_foralls_core p () ltac:(fun p =>
+    tryif is_var p then
+      inv p
+    else
+      let Hp := fresh in pose proof p as Hp; inv Hp).
+(* As above, we overload the notation with [integer] and [ident] to support
+[oinv 1], like the regular [inversion] tactic. *)
+Tactic Notation "oinv" integer(n) "as" simple_intropattern(ipat) :=
+  num_tac n ltac:(fun H => oinv H as ipat).
+Tactic Notation "oinv" integer(n) :=
+  num_tac n ltac:(fun H => oinv H).
+(** Helper for [ospecialize]: call [tac] with the name of the head term *if*
+that term is a variable.
+Written in CPS to get around weird thunking limitations. *)
+Ltac ospecialize_ident_head_of t tac :=
+  let h := get_head t in
+  tryif is_var h then tac h else
+    fail "ospecialize can only specialize a local hypothesis;"
+         "use opose proof instead".
+Tactic Notation "ospecialize" uconstr(p) :=
+  (* Unfortunately there does not seem to be a way to reuse [specialize] here,
+  so we need to re-implement the logic for reusing the name. *)
+  opose_core p ltac:(fun p =>
+    ospecialize_ident_head_of p ltac:(fun H =>
+      (* The term of [p] (but not its type) can refer to [H], so we need to use
+      a temporary [H'] here to hold the type of [p] before we can clear [H]. *)
+      let H' := fresh in
+      pose proof p as H'; clear H; rename H' into H
+  )).
+Tactic Notation "ospecialize" "*" uconstr(p) :=
+  opose_specialize_foralls_core p () ltac:(fun p =>
+    ospecialize_ident_head_of p ltac:(fun H =>
+      (* The term of [p] (but not its type) can refer to [H], so we need to use
+      a temporary [H'] here to hold the type of [p] before we can clear [H]. *)
+      let H' := fresh in
+      pose proof p as H'; clear H; rename H' into H
+  )).
 (** The block definitions are taken from [Coq.Program.Equality] and can be used
 by tactics to separate their goal from hypotheses they generalize over. *)
@@ -509,36 +745,89 @@ Definition block {A : Type} (a : A) := a.
 Ltac block_goal := match goal with [ |- ?T ] => change (block T) end.
 Ltac unblock_goal := unfold block in *.
+(** [learn_hyp p as H] and [learn_hyp p], where [p] is a proof of [P],
-(** The following tactic can be used to add support for patterns to tactic notation:
+add [P] to the context and fail if [P] already exists in the context.
-It will search for the first subterm of the goal matching [pat], and then call [tac]
+This is a simple form of the learning pattern. These tactics are
-with that subterm. *)
+inspired by [Program.Tactics.add_hypothesis]. *)
-Ltac find_pat pat tac :=
+Tactic Notation "learn_hyp" constr(p) "as" ident(H') :=
+  let P := type of p in
  match goal with
-  |- context [?x] =>
+  | H : P |- _ => fail 1
-      unify pat x with typeclass_instances;
+  | _ => pose proof p as H'
-      tryif tac x then idtac else fail 2
  end.
+Tactic Notation "learn_hyp" constr(p) :=
+  let H := fresh in learn_hyp p as H.
+(** The tactic [select pat tac] finds the last (i.e., bottommost) hypothesis
+matching [pat] and passes it to the continuation [tac]. Its main advantage over
+using [match goal with ] directly is that it is shorter. If [pat] matches
+multiple hypotheses and [tac] fails, then [select tac] will not backtrack on
+subsequent matching hypotheses.
-(** [select] finds the first hypothesis matching [pat] and passes it
+The tactic [select] is written in CPS and does not return the name of the
-to the continuation [tac]. Its main advantage over using [match goal
-with ] directly is that it is shorter. If [pat] matches multiple
-hypotheses, then [tac] will only be called on the first matching
-hypothesis. If [tac] fails, [select] will not backtrack on subsequent
-matching hypotheses.
-[select] is written in CPS and does not return the name of the
 hypothesis due to limitations in the Ltac1 tactic runtime (see
 https://gitter.im/coq/coq?at=5e96c82f85b01628f04bbb89). *)
 Tactic Notation "select" open_constr(pat) tactic3(tac) :=
  lazymatch goal with
-  (* The [unify] is necessary, otherwise holes in [pat] stay as side-conditions *)
+  (** Before running [tac] on the hypothesis [H] we must first unify the
+      pattern [pat] with the term it matched against. This forces every evar
+      coming from [pat] (and in particular from the holes [_] it contains and
+      from the implicit arguments it uses) to be instantiated. If we do not do
+      so then shelved goals are produced for every such evar. *)
  | H : pat |- _ => let T := (type of H) in unify T pat; tac H
  end.
+(** We provide [select] variants of some widely used tactics. *)
 (** [select_revert] reverts the first hypothesis matching [pat]. *)
 Tactic Notation "revert" "select" open_constr(pat) := select pat (fun H => revert H).
+Tactic Notation "rename" "select" open_constr(pat) "into" ident(name) :=
+  select pat (fun H => rename H into name).
+Tactic Notation "destruct" "select" open_constr(pat) :=
+  select pat (fun H => destruct H).
+Tactic Notation "destruct" "select" open_constr(pat) "as" simple_intropattern(ipat) :=
+  select pat (fun H => destruct H as ipat).
+Tactic Notation "inversion" "select" open_constr(pat) :=
+  select pat (fun H => inversion H).
+Tactic Notation "inversion" "select" open_constr(pat) "as" simple_intropattern(ipat) :=
+  select pat (fun H => inversion H as ipat).
+Tactic Notation "inv" "select" open_constr(pat) :=
+  select pat (fun H => inv H).
+Tactic Notation "inv" "select" open_constr(pat) "as" simple_intropattern(ipat) :=
+  select pat (fun H => inv H as ipat).
+(** The tactic [is_closed_term t] succeeds if [t] is a closed term and fails otherwise.
+By closed we mean that [t] does not depend on any variable bound in the context.
+axioms are considered closed terms by this tactic (but Section
+variables are not). A function application is considered closed if the
+function and the argument are closed, without considering the body of
+the function (or whether it is opaque or not). This tactic is useful
+for example to decide whether to call [vm_compute] on [t].
+This trick was originally suggested by Jason Gross:
+https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Check.20that.20a.20term.20is.20closed.20in.20Ltac/near/240885618
+*)
+Ltac is_closed_term t :=
+  first [
+      (** We use the [assert_succeeds] sandbox to be able to freely
+      change the context. *)
+      assert_succeeds (
+          (** Make sure that the goal only contains [t]. (We use
+          [const False t] instead of [let x := t in False] as the
+          let-binding in the latter would be unfolded by the [unfold]
+          later.) *)
+          exfalso; change_no_check (const False t);
+          (** Clear all hypotheses. *)
+          repeat match goal with H : _ |- _ => try unfold H in *; clear H end;
+          (** If there are still hypotheses left, [t] is not closed. *)
+          lazymatch goal with H : _ |- _ => fail | _ => idtac end
+        ) |
+      fail 1 "The term" t "is not closed"
+    ].
 (** Coq's [firstorder] tactic fails or loops on rather small goals already. In
 particular, on those generated by the tactic [unfold_elem_ofs] which is used
 to solve propositions on sets. The [naive_solver] tactic implements an
@@ -561,12 +850,6 @@ Lemma forall_and_distr (A : Type) (P Q : A → Prop) :
  (∀ x, P x ∧ Q x) ↔ (∀ x, P x) ∧ (∀ x, Q x).
 Proof. firstorder. Qed.
-(** The tactic [no_new_unsolved_evars tac] executes [tac] and fails if it
-creates any new evars. This trick is by Jonathan Leivent, see:
-https://coq.inria.fr/bugs/show_bug.cgi?id=3872 *)
-Ltac no_new_unsolved_evars tac := exact ltac:(tac).
 Tactic Notation "naive_solver" tactic(tac) :=
  unfold iff, not in *;
  repeat match goal with
@@ -602,7 +885,7 @@ Tactic Notation "naive_solver" tactic(tac) :=
  | H : Is_true (_ || _) |- _ =>
     apply orb_True in H; let H1 := fresh in destruct H as [H1|H1]; try clear H
  (**i solve the goal using the user supplied tactic *)
-  | |- _ => solve [tac]
+  | |- _ => no_new_unsolved_evars (tac)
  end;
  (**i use recursion to enable backtracking on the following clauses. *)
  match goal with
@@ -619,7 +902,7 @@ Tactic Notation "naive_solver" tactic(tac) :=
      | H : _ → _ |- _ =>
        is_non_dependent H;
        no_new_unsolved_evars
-          ltac:(first [eapply H | efeed pose proof H]; clear H; go n')
+          ltac:(first [eapply H | opose proof* H]; clear H; go n')
      end
    end
  end

--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -2,13 +2,19 @@ From stdpp Require Import base tactics.
 From stdpp Require Import options.
 Local Set Universe Polymorphism.
+Local Set Polymorphic Inductive Cumulativity.
+(** Without this flag, Coq minimizes some universes to [Set] when they
+    should not be, e.g. in [texist_exist].
+    See the [texist_exist_universes] test. *)
+Local Unset Universe Minimization ToSet.
 (** Telescopes *)
 Inductive tele : Type :=
  | TeleO : tele
  | TeleS {X} (binder : X → tele) : tele.
-Arguments TeleS {_} _.
+Global Arguments TeleS {_} _.
 (** The telescope version of Coq's function type *)
 Fixpoint tele_fun (TT : tele) (T : Type) : Type :=
@@ -30,34 +36,69 @@ Definition tele_fold {X Y} {TT : tele} (step : ∀ {A : Type}, (A → Y) → Y)
     | TeleO => λ x : X, base x
     | TeleS b => λ f, step (λ x, rec (f x))
     end) TT.
-Arguments tele_fold {_ _ !_} _ _ _ /.
+Global Arguments tele_fold {_ _ !_} _ _ _ /.
+(** A duplication of the type [sigT] to avoid any connection to other universes
+ *)
+Record tele_arg_cons {X : Type} (f : X → Type) : Type := TeleArgCons
+  { tele_arg_head : X;
+    tele_arg_tail : f tele_arg_head }.
+Global Arguments TeleArgCons {_ _} _ _.
 (** A sigma-like type for an "element" of a telescope, i.e. the data it
  takes to get a [T] from a [TT -t> T]. *)
-Inductive tele_arg : tele → Type :=
+Fixpoint tele_arg@{u} (t : tele@{u}) : Type@{u} :=
-| TargO : tele_arg TeleO
+  match t with
-(* the [x] is the only relevant data here *)
+  | TeleO => unit
-| TargS {X} {binder} (x : X) : tele_arg (binder x) → tele_arg (TeleS binder).
+  | TeleS f => tele_arg_cons (λ x, tele_arg (f x))
+  end.
-Definition tele_app {TT : tele} {T} (f : TT -t> T) : tele_arg TT → T :=
+Global Arguments tele_arg _ : simpl never.
-  λ a, (fix rec {TT} (a : tele_arg TT) : (TT -t> T) → T :=
-     match a in tele_arg TT return (TT -t> T) → T with
+(* Coq has no idea that [unit] and [tele_arg_cons] have anything to do with
-     | TargO => λ t : T, t
+   telescopes. This only becomes a problem when concrete telescope arguments
-     | TargS x a => λ f, rec a (f x)
+   (of concrete telescopes) need to be typechecked. To work around this, we
-     end) TT a f.
+   annotate the notations below with extra information to guide unification.
-Arguments tele_app {!_ _} _ !_ /.
+ *)
+(* The cast in the notation below is necessary to make Coq understand that
+   [TargO] can be unified with [tele_arg TeleO]. *)
+Notation TargO := (tt : tele_arg TeleO) (only parsing).
+(* The casts and annotations are necessary for Coq to typecheck nested [TargS]
+   as well as the final [TargO] in a chain of [TargS]. *)
+Notation TargS a b :=
+  ((@TeleArgCons _ (λ x, tele_arg (_ x)) a b) : (tele_arg (TeleS _))) (only parsing).
 Coercion tele_arg : tele >-> Sortclass.
+Lemma tele_arg_ind (P : ∀ TT, tele_arg TT → Prop) :
+  P TeleO TargO →
+  (∀ T (b : T → tele) x xs, P (b x) xs → P (TeleS b) (TargS x xs)) →
+  ∀ TT (xs : tele_arg TT), P TT xs.
+Proof.
+  intros H0 HS TT. induction TT as [|T b IH]; simpl.
+  - by intros [].
+  - intros [x xs]. by apply HS.
+Qed.
+Fixpoint tele_app {TT : tele} {U} : (TT -t> U) -> TT → U :=
+  match TT as TT return (TT -t> U) -> TT → U with
+  | TeleO => λ F _, F
+  | TeleS r => λ (F : TeleS r -t> U) '(TeleArgCons x b),
+      tele_app (F x) b
+  end.
+(* The bidirectionality hint [&] simplifies defining tele_app-based notation
+such as the atomic updates and atomic triples in Iris. *)
+Global Arguments tele_app {!_ _} & _ !_ /.
 (* This is a local coercion because otherwise, the "λ.." notation stops working. *)
 Local Coercion tele_app : tele_fun >-> Funclass.
 (** Inversion lemma for [tele_arg] *)
-Lemma tele_arg_inv {TT : tele} (a : TT) :
+Lemma tele_arg_inv {TT : tele} (a : tele_arg TT) :
-  match TT as TT return TT → Prop with
+  match TT as TT return tele_arg TT → Prop with
  | TeleO => λ a, a = TargO
  | TeleS f => λ a, ∃ x a', a = TargS x a'
  end a.
-Proof. induction a; eauto. Qed.
+Proof. destruct TT; destruct a; eauto. Qed.
 Lemma tele_arg_O_inv (a : TeleO) : a = TargO.
 Proof. exact (tele_arg_inv a). Qed.
 Lemma tele_arg_S_inv {X} {f : X → tele} (a : TeleS f) :
@@ -71,7 +112,7 @@ Fixpoint tele_map {T U} {TT : tele} : (T → U) → (TT -t> T) → TT -t> U :=
  | @TeleS X b => λ (F : T → U) (f : TeleS b -t> T) (x : X),
                  tele_map F (f x)
  end.
-Arguments tele_map {_ _ !_} _ _ /.
+Global Arguments tele_map {_ _ !_} _ _ /.
 Lemma tele_map_app {T U} {TT : tele} (F : T → U) (t : TT -t> T) (x : TT) :
  (tele_map F t) x = F (t x).
@@ -91,15 +132,15 @@ Proof. apply tele_map_app. Qed.
 (** Operate below [tele_fun]s with argument telescope [TT]. *)
 Fixpoint tele_bind {U} {TT : tele} : (TT → U) → TT -t> U :=
  match TT as TT return (TT → U) → TT -t> U with
-  | TeleO => λ F, F TargO
+  | TeleO => λ F, F tt
  | @TeleS X b => λ (F : TeleS b → U) (x : X), (* b x -t> U *)
-                  tele_bind (λ a, F (TargS x a))
+      tele_bind (λ a, F (TargS x a))
  end.
-Arguments tele_bind {_ !_} _ /.
+Global Arguments tele_bind {_ !_} _ /.
 (* Show that tele_app ∘ tele_bind is the identity. *)
 Lemma tele_app_bind {U} {TT : tele} (f : TT → U) x :
-  (tele_app $ tele_bind f) x = f x.
+  (tele_bind f) x = f x.
 Proof.
  induction TT as [|X b IH]; simpl in *.
  - rewrite (tele_arg_O_inv x). done.
@@ -148,10 +189,10 @@ Notation "'λ..' x .. y , e" :=
 (** Telescopic quantifiers *)
 Definition tforall {TT : tele} (Ψ : TT → Prop) : Prop :=
  tele_fold (λ (T : Type) (b : T → Prop), ∀ x : T, b x) (λ x, x) (tele_bind Ψ).
-Arguments tforall {!_} _ /.
+Global Arguments tforall {!_} _ /.
 Definition texist {TT : tele} (Ψ : TT → Prop) : Prop :=
  tele_fold ex (λ x, x) (tele_bind Ψ).
-Arguments texist {!_} _ /.
+Global Arguments texist {!_} _ /.
 Notation "'∀..' x .. y , P" := (tforall (λ x, .. (tforall (λ y, P)) .. ))
  (at level 200, x binder, y binder, right associativity,
@@ -188,8 +229,8 @@ Proof.
 Qed.
 (* Teach typeclass resolution how to make progress on these binders *)
-Typeclasses Opaque tforall texist.
+Global Typeclasses Opaque tforall texist.
-Hint Extern 1 (tforall _) =>
+Global Hint Extern 1 (tforall _) =>
  progress cbn [tforall tele_fold tele_bind tele_app] : typeclass_instances.
-Hint Extern 1 (texist _) =>
+Global Hint Extern 1 (texist _) =>
  progress cbn [texist tele_fold tele_bind tele_app] : typeclass_instances.
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -2,10 +2,15 @@
 (lists of fixed length). It uses the definitions from the standard library, but
 renames or changes their notations, so that it becomes more consistent with the
 naming conventions in this development. *)
+(* Coq warns about using vector, but it is not deprecated. Instead somehow they seem concerned
+about people having too much fun with type indices. See
+<https://github.com/coq/coq/pull/18032> for discussion. Let's just silence that. *)
+Local Set Warnings "-stdlib-vector".
+From Coq Require Vector.
 From stdpp Require Import countable.
 From stdpp Require Export fin list.
 From stdpp Require Import options.
-Open Scope vector_scope.
+Global Open Scope vector_scope.
 (** The type [vec n] represents lists of consisting of exactly [n] elements.
 Whereas the standard library declares exactly the same notations for vectors as
@@ -13,10 +18,10 @@ used for lists, we use slightly different notations so it becomes easier to use
 lists and vectors together. *)
 Notation vec := Vector.t.
 Notation vnil := Vector.nil.
-Arguments vnil {_}.
+Global Arguments vnil {_}.
 Notation vcons := Vector.cons.
 Notation vapp := Vector.append.
-Arguments vcons {_} _ {_} _.
+Global Arguments vcons {_} _ {_} _.
 Infix ":::" := vcons (at level 60, right associativity) : vector_scope.
 Notation "(:::)" := vcons (only parsing) : vector_scope.
@@ -41,7 +46,7 @@ Proof.
  refine match v with [#] => tt | x ::: v => λ P Hcons, Hcons x v end.
 Defined.
-Instance vector_lookup_total A : ∀ m, LookupTotal (fin m) A (vec A m) :=
+Global Instance vector_lookup_total A : ∀ m, LookupTotal (fin m) A (vec A m) :=
  fix go m i {struct i} := let _ : ∀ m, LookupTotal _ _ _ := @go in
  match i in fin m return vec A m → A with
  | 0%fin => vec_S_inv (λ _, A) (λ x _, x)
@@ -74,7 +79,7 @@ Proof.
  - apply IH. intros i. apply (Hi (FS i)).
 Qed.
-Instance vec_dec {A} {dec : EqDecision A} {n} : EqDecision (vec A n).
+Global Instance vec_dec {A} {dec : EqDecision A} {n} : EqDecision (vec A n).
 Proof.
 refine (vec_rect2
  (λ n (v w : vec A n), { v = w } + { v ≠ w })
@@ -88,9 +93,12 @@ Ltac inv_vec v :=
  match eval hnf in T with
  | vec _ ?n =>
    match eval hnf in n with
-    | 0 => revert dependent v; match goal with |- ∀ v, @?P v => apply (vec_0_inv P) end
+    | 0 =>
+      generalize dependent v;
+      match goal with |- ∀ v, @?P v => apply (vec_0_inv P) end
    | S ?n =>
-      revert dependent v; match goal with |- ∀ v, @?P v => apply (vec_S_inv P) end;
+      generalize dependent v;
+      match goal with |- ∀ v, @?P v => apply (vec_S_inv P) end;
      (* Try going on recursively. *)
      try (let x := fresh "x" in intros x v; inv_vec v; revert x)
    end
@@ -121,11 +129,11 @@ Lemma vec_to_list_app {A n m} (v : vec A n) (w : vec A m) :
 Proof. by induction v; f_equal/=. Qed.
 Lemma vec_to_list_to_vec {A} (l : list A): vec_to_list (list_to_vec l) = l.
 Proof. by induction l; f_equal/=. Qed.
-Lemma vec_to_list_length {A n} (v : vec A n) : length (vec_to_list v) = n.
+Lemma length_vec_to_list {A n} (v : vec A n) : length (vec_to_list v) = n.
 Proof. induction v; simpl; by f_equal. Qed.
 Lemma vec_to_list_same_length {A B n} (v : vec A n) (w : vec B n) :
  length v = length w.
-Proof. by rewrite !vec_to_list_length. Qed.
+Proof. by rewrite !length_vec_to_list. Qed.
 Lemma vec_to_list_inj1 {A n m} (v : vec A n) (w : vec A m) :
  vec_to_list v = vec_to_list w → n = m.
 Proof.
@@ -139,10 +147,10 @@ Proof.
    simplify_eq/=; f_equal; eauto.
 Qed.
 Lemma list_to_vec_to_list {A n} (v : vec A n) :
-  list_to_vec (vec_to_list v) = eq_rect _ _ v _ (eq_sym (vec_to_list_length v)).
+  list_to_vec (vec_to_list v) = eq_rect _ _ v _ (eq_sym (length_vec_to_list v)).
 Proof.
  apply vec_to_list_inj2. rewrite vec_to_list_to_vec.
-  by destruct (eq_sym (vec_to_list_length v)).
+  by destruct (eq_sym (length_vec_to_list v)).
 Qed.
 Lemma vlookup_middle {A n m} (v : vec A n) (w : vec A m) x :
@@ -183,7 +191,7 @@ Proof.
  split.
  - intros [Hlt ?]. rewrite <-(fin_to_nat_to_fin i n Hlt). by apply vlookup_lookup.
  - intros Hvix. assert (Hlt:=lookup_lt_Some _ _ _ Hvix).
-    rewrite vec_to_list_length in Hlt. exists Hlt.
+    rewrite length_vec_to_list in Hlt. exists Hlt.
    apply vlookup_lookup. by rewrite fin_to_nat_to_fin.
 Qed.
 Lemma elem_of_vlookup {A n} (v : vec A n) x :
@@ -212,7 +220,7 @@ Lemma Forall2_vlookup {A B} (P : A → B → Prop) {n}
 Proof.
  split.
  - vec_double_ind v1 v2; [intros _ i; inv_fin i |].
-    intros n v1 v2 IH a b; simpl. inversion_clear 1.
+    intros n v1 v2 IH a b; simpl. inv 1.
    intros i. inv_fin i; simpl; auto.
  - vec_double_ind v1 v2; [constructor|].
    intros ??? IH ?? H. constructor.
@@ -330,12 +338,12 @@ Global Instance vec_0_inhabited T : Inhabited (vec T 0) := populate [#].
 Global Instance vec_inhabited `{Inhabited T} n : Inhabited (vec T n) :=
  populate (vreplicate n inhabitant).
-Instance vec_countable `{Countable A} n : Countable (vec A n).
+Global Instance vec_countable `{Countable A} n : Countable (vec A n).
 Proof.
  apply (inj_countable vec_to_list (λ l,
-    guard (n = length l) as H; Some (eq_rect _ _ (list_to_vec l) _ (eq_sym H)))).
+    H ← guard (n = length l); Some (eq_rect _ _ (list_to_vec l) _ (eq_sym H)))).
-  intros v. case_option_guard as Hn.
+  intros v. case_guard as Hn; simplify_eq/=.
  - rewrite list_to_vec_to_list.
    rewrite (proof_irrel (eq_sym _) Hn). by destruct Hn.
-  - by rewrite vec_to_list_length in Hn.
+  - by rewrite length_vec_to_list in Hn.
 Qed.
--- a/stdpp/well_founded.v
+++ b/stdpp/well_founded.v
+(** * Theorems on well founded relations *)
+From stdpp Require Import base.
+From stdpp Require Import options.
+Lemma Acc_impl {A} (R1 R2 : relation A) x :
+  Acc R1 x → (∀ y1 y2, R2 y1 y2 → R1 y1 y2) → Acc R2 x.
+Proof. induction 1; constructor; auto. Qed.
+(** The function [wf_guard n wfR] adds [2 ^ n - 1] times an [Acc_intro]
+constructor ahead of the [wfR] proof. This definition can be used to make
+opaque [well_founded] proofs "compute". For big enough [n], say [32], computation will
+reach implementation limits before running into the opaque [well_founded] proof.
+This trick is originally due to Georges Gonthier, see
+https://sympa.inria.fr/sympa/arc/coq-club/2007-07/msg00013.html *)
+Definition wf_guard `{R : relation A} (n : nat)
+    (wfR : well_founded R) : well_founded R :=
+  Acc_intro_generator n wfR.
+(* Generally we do not want [wf_guard] to be expanded (neither by tactics,
+nor by conversion tests in the kernel), but in some cases we do need it for
+computation (that is, we cannot make it opaque). We use the [Strategy]
+command to make its expanding behavior less eager. *)
+Strategy 100 [wf_guard].
+Lemma wf_projected `{R1 : relation A} `(R2 : relation B) (f : A → B) :
+  (∀ x y, R1 x y → R2 (f x) (f y)) →
+  well_founded R2 → well_founded R1.
+Proof.
+  intros Hf Hwf.
+  cut (∀ y, Acc R2 y → ∀ x, y = f x → Acc R1 x).
+  { intros aux x. apply (aux (f x)); auto. }
+  induction 1 as [y _ IH]. intros x ?. subst.
+  constructor. intros y ?. apply (IH (f y)); auto.
+Qed.
+Lemma Fix_F_proper `{R : relation A} (B : A → Type) (E : ∀ x, relation (B x))
+    (F : ∀ x, (∀ y, R y x → B y) → B x)
+    (HF : ∀ (x : A) (f g : ∀ y, R y x → B y),
+      (∀ y Hy Hy', E _ (f y Hy) (g y Hy')) → E _ (F x f) (F x g))
+    (x : A) (acc1 acc2 : Acc R x) :
+  E _ (Fix_F B F acc1) (Fix_F B F acc2).
+Proof. revert x acc1 acc2. fix FIX 2. intros x [acc1] [acc2]; simpl; auto. Qed.
+Lemma Fix_unfold_rel `{R : relation A} (wfR : well_founded R)
+    (B : A → Type) (E : ∀ x, relation (B x))
+    (F: ∀ x, (∀ y, R y x → B y) → B x)
+    (HF: ∀ (x: A) (f g: ∀ y, R y x → B y),
+           (∀ y Hy Hy', E _ (f y Hy) (g y Hy')) → E _ (F x f) (F x g))
+    (x: A) :
+  E _ (Fix wfR B F x) (F x (λ y _, Fix wfR B F y)).
+Proof.
+  unfold Fix.
+  destruct (wfR x); simpl.
+  apply HF; intros.
+  apply Fix_F_proper; auto.
+Qed.
+(**
+Generate an induction principle for [Acc] for reasoning about recursion on
+[Acc], such as [countable.choose_proper].
+We need an induction principle to prove predicates of [Acc] values, with
+conclusion [∀ (x : A) (a : Acc R x), P x a]. Instead, [Acc_ind] has conclusion
+[∀ x : A, Acc R x → P x], as if it were generated by
+[Scheme Acc_rect := Minimality for Acc Sort Prop.]
+*)
+Scheme Acc_dep_ind := Induction for Acc Sort Prop.
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -7,12 +7,13 @@ Local Open Scope Z_scope.
 Record Zmap (A : Type) : Type :=
  ZMap { Zmap_0 : option A; Zmap_pos : Pmap A; Zmap_neg : Pmap A }.
-Arguments Zmap_0 {_} _ : assert.
+Add Printing Constructor Zmap.
-Arguments Zmap_pos {_} _ : assert.
+Global Arguments Zmap_0 {_} _ : assert.
-Arguments Zmap_neg {_} _ : assert.
+Global Arguments Zmap_pos {_} _ : assert.
-Arguments ZMap {_} _ _ _ : assert.
+Global Arguments Zmap_neg {_} _ : assert.
+Global Arguments ZMap {_} _ _ _ : assert.
-Instance Zmap_eq_dec `{EqDecision A} : EqDecision (Zmap A).
+Global Instance Zmap_eq_dec `{EqDecision A} : EqDecision (Zmap A).
 Proof.
 refine (λ t1 t2,
  match t1, t2 with
@@ -20,76 +21,61 @@ Proof.
     cast_if_and3 (decide (x = y)) (decide (t1 = t2)) (decide (t1' = t2'))
  end); abstract congruence.
 Defined.
-Instance Zempty {A} : Empty (Zmap A) := ZMap None ∅ ∅.
+Global Instance Zmap_empty {A} : Empty (Zmap A) := ZMap None ∅ ∅.
-Instance Zlookup {A} : Lookup Z A (Zmap A) := λ i t,
+Global Instance Zmap_lookup {A} : Lookup Z A (Zmap A) := λ i t,
  match i with
  | Z0 => Zmap_0 t | Zpos p => Zmap_pos t !! p | Zneg p => Zmap_neg t !! p
  end.
-Instance Zpartial_alter {A} : PartialAlter Z A (Zmap A) := λ f i t,
+Global Instance Zmap_partial_alter {A} : PartialAlter Z A (Zmap A) := λ f i t,
  match i, t with
  | Z0, ZMap o t t' => ZMap (f o) t t'
-  | Zpos p, ZMap o t t' => ZMap o (partial_alter f p t) t'
+  | Z.pos p, ZMap o t t' => ZMap o (partial_alter f p t) t'
-  | Zneg p, ZMap o t t' => ZMap o t (partial_alter f p t')
+  | Z.neg p, ZMap o t t' => ZMap o t (partial_alter f p t')
  end.
-Instance Zto_list {A} : FinMapToList Z A (Zmap A) := λ t,
+Global Instance Zmap_fmap: FMap Zmap := λ A B f t,
-  match t with
+  match t with ZMap o t t' => ZMap (f <$> o) (f <$> t) (f <$> t') end.
-  | ZMap o t t' => from_option (λ x, [(0,x)]) [] o ++
+Global Instance Zmap_omap: OMap Zmap := λ A B f t,
-     (prod_map Zpos id <$> map_to_list t) ++
-     (prod_map Zneg id <$> map_to_list t')
-  end.
-Instance Zomap: OMap Zmap := λ A B f t,
  match t with ZMap o t t' => ZMap (o ≫= f) (omap f t) (omap f t') end.
-Instance Zmerge: Merge Zmap := λ A B C f t1 t2,
+Global Instance Zmap_merge: Merge Zmap := λ A B C f t1 t2,
  match t1, t2 with
  | ZMap o1 t1 t1', ZMap o2 t2 t2' =>
-     ZMap (f o1 o2) (merge f t1 t2) (merge f t1' t2')
+     ZMap (diag_None f o1 o2) (merge f t1 t2) (merge f t1' t2')
+  end.
+Global Instance Zmap_fold {A} : MapFold Z A (Zmap A) := λ B f d t,
+  match t with
+  | ZMap mx t t' => map_fold (f ∘ Z.pos) (map_fold (f ∘ Z.neg)
+     match mx with Some x => f 0 x d | None => d end t') t
  end.
-Instance Nfmap: FMap Zmap := λ A B f t,
-  match t with ZMap o t t' => ZMap (f <$> o) (f <$> t) (f <$> t') end.
-Instance: FinMap Z Zmap.
+Global Instance Zmap_map: FinMap Z Zmap.
 Proof.
  split.
  - intros ? [??] [??] H. f_equal.
    + apply (H 0).
-    + apply map_eq. intros i. apply (H (Zpos i)).
+    + apply map_eq. intros i. apply (H (Z.pos i)).
-    + apply map_eq. intros i. apply (H (Zneg i)).
+    + apply map_eq. intros i. apply (H (Z.neg i)).
  - by intros ? [].
  - intros ? f [] [|?|?]; simpl; [done| |]; apply lookup_partial_alter.
  - intros ? f [] [|?|?] [|?|?]; simpl; intuition congruence ||
      intros; apply lookup_partial_alter_ne; congruence.
  - intros ??? [??] []; simpl; [done| |]; apply lookup_fmap.
-  - intros ? [o t t']; unfold map_to_list; simpl.
-    assert (NoDup ((prod_map Z.pos id <$> map_to_list t) ++
-      (prod_map Z.neg id <$> map_to_list t'))).
-    { apply NoDup_app; split_and?.
-      - apply (NoDup_fmap_2 _), NoDup_map_to_list.
-      - intro. rewrite !elem_of_list_fmap. naive_solver.
-      - apply (NoDup_fmap_2 _), NoDup_map_to_list. }
-    destruct o; simpl; auto. constructor; auto.
-    rewrite elem_of_app, !elem_of_list_fmap. naive_solver.
-  - intros ? t i x. unfold map_to_list. split.
-    + destruct t as [[y|] t t']; simpl.
-      * rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap.
-        intros [?|[[[??][??]]|[[??][??]]]]; simplify_eq/=; [done| |];
-          by apply elem_of_map_to_list.
-      * rewrite elem_of_app, !elem_of_list_fmap. intros [[[??][??]]|[[??][??]]];
-          simplify_eq/=; by apply elem_of_map_to_list.
-    + destruct t as [[y|] t t']; simpl.
-      * rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap.
-        destruct i as [|i|i]; simpl; [intuition congruence| |].
-        { right; left. exists (i, x). by rewrite elem_of_map_to_list. }
-        right; right. exists (i, x). by rewrite elem_of_map_to_list.
-      * rewrite elem_of_app, !elem_of_list_fmap.
-        destruct i as [|i|i]; simpl; [done| |].
-        { left; exists (i, x). by rewrite elem_of_map_to_list. }
-        right; exists (i, x). by rewrite elem_of_map_to_list.
  - intros ?? f [??] [|?|?]; simpl; [done| |]; apply (lookup_omap f).
-  - intros ??? f ? [??] [??] [|?|?]; simpl; [done| |]; apply (lookup_merge f).
+  - intros ??? f [??] [??] [|?|?]; simpl; [done| |]; apply (lookup_merge f).
+  - done.
+  - intros A P Hemp Hins [mx t t'].
+    induction t as [|i x t ? Hfold IH] using map_fold_fmap_ind.
+    { induction t' as [|i x t' ? Hfold IH] using map_fold_fmap_ind.
+      { destruct mx as [x|]; [|done].
+        replace (ZMap (Some x) ∅ ∅) with (<[0:=x]> ∅ : Zmap _) by done.
+        by apply Hins. }
+      apply (Hins (Z.neg i) x (ZMap mx ∅ t')); [done| |done].
+      intros A' B f g b. apply Hfold. }
+    apply (Hins (Z.pos i) x (ZMap mx t t')); [done| |done].
+    intros A' B f g b. apply Hfold.
 Qed.
 (** * Finite sets *)
 (** We construct sets of [Z]s satisfying extensional equality. *)
 Notation Zset := (mapset Zmap).
-Instance Zmap_dom {A} : Dom (Zmap A) Zset := mapset_dom.
+Global Instance Zmap_dom {A} : Dom (Zmap A) Zset := mapset_dom.
-Instance: FinMapDom Z Zmap Zset := mapset_dom_spec.
+Global Instance: FinMapDom Z Zmap Zset := mapset_dom_spec.
--- a/stdpp_bitvector/bitvector.v
+++ b/stdpp_bitvector/bitvector.v
+(** This file is maintained by Michael Sammler. *)
+From stdpp.bitvector Require Export definitions tactics.
+From stdpp Require Import options.
--- a/stdpp_bitvector/definitions.v
+++ b/stdpp_bitvector/definitions.v
+(** This file is maintained by Michael Sammler. *)
+From stdpp Require Export numbers.
+From stdpp Require Import countable finite.
+From stdpp Require Import options.
+(** * bitvector library *)
+(** This file provides the [bv n] type for representing [n]-bit
+integers with the standard operations. It also provides the
+[bv_saturate] tactic for learning facts about the range of bit vector
+variables in context. More extensive automation can be found in
+[bitvector_auto.v].
+Additionally, this file provides the [bvn] type for representing a
+bitvector of arbitrary size. *)
+(** * Settings *)
+Local Open Scope Z_scope.
+(** * Preliminary definitions *)
+Definition bv_modulus (n : N) : Z := 2 ^ (Z.of_N n).
+Definition bv_half_modulus (n : N) : Z := bv_modulus n `div` 2.
+Definition bv_wrap (n : N) (z : Z) : Z := z `mod` bv_modulus n.
+Definition bv_swrap (n : N) (z : Z) : Z := bv_wrap n (z + bv_half_modulus n) - bv_half_modulus n.
+Lemma bv_modulus_pos n :
+  0 < bv_modulus n.
+Proof. apply Z.pow_pos_nonneg; lia. Qed.
+Lemma bv_modulus_gt_1 n :
+  n ≠ 0%N →
+  1 < bv_modulus n.
+Proof. intros ?. apply Z.pow_gt_1; lia. Qed.
+Lemma bv_half_modulus_nonneg n :
+  0 ≤ bv_half_modulus n.
+Proof. apply Z.div_pos; [|done]. pose proof bv_modulus_pos n. lia. Qed.
+Lemma bv_modulus_add n1 n2 :
+  bv_modulus (n1 + n2) = bv_modulus n1 * bv_modulus n2.
+Proof. unfold bv_modulus. rewrite N2Z.inj_add. eapply Z.pow_add_r; lia. Qed.
+Lemma bv_half_modulus_twice n:
+  n ≠ 0%N →
+  bv_half_modulus n + bv_half_modulus n = bv_modulus n.
+Proof.
+  intros. unfold bv_half_modulus, bv_modulus.
+  rewrite Z.add_diag. symmetry. apply Z_div_exact_2; [lia|].
+  rewrite <-Z.pow_pred_r by lia. rewrite Z.mul_comm. by apply Z.mod_mul.
+Qed.
+Lemma bv_half_modulus_lt_modulus n:
+  bv_half_modulus n < bv_modulus n.
+Proof.
+  pose proof bv_modulus_pos n.
+  apply Z_div_lt; [done| lia].
+Qed.
+Lemma bv_modulus_le_mono n m:
+  (n ≤ m)%N →
+  bv_modulus n ≤ bv_modulus m.
+Proof. intros. apply Z.pow_le_mono; [done|lia]. Qed.
+Lemma bv_half_modulus_le_mono n m:
+  (n ≤ m)%N →
+  bv_half_modulus n ≤ bv_half_modulus m.
+Proof. intros. apply Z.div_le_mono; [done|]. by apply bv_modulus_le_mono. Qed.
+Lemma bv_modulus_0:
+  bv_modulus 0 = 1.
+Proof. done. Qed.
+Lemma bv_half_modulus_0:
+  bv_half_modulus 0 = 0.
+Proof. done. Qed.
+Lemma bv_half_modulus_twice_mult n:
+  bv_half_modulus n + bv_half_modulus n = (Z.of_N n `min` 1) * bv_modulus n.
+Proof. destruct (decide (n = 0%N)); subst; [ rewrite bv_half_modulus_0 | rewrite bv_half_modulus_twice]; lia. Qed.
+Lemma bv_wrap_in_range n z:
+  0 ≤ bv_wrap n z < bv_modulus n.
+Proof. apply Z.mod_pos_bound. apply bv_modulus_pos. Qed.
+Lemma bv_swrap_in_range n z:
+  n ≠ 0%N →
+  - bv_half_modulus n ≤ bv_swrap n z < bv_half_modulus n.
+Proof.
+  intros ?. unfold bv_swrap.
+  pose proof bv_half_modulus_twice n.
+  pose proof bv_wrap_in_range n (z + bv_half_modulus n).
+  lia.
+Qed.
+Lemma bv_wrap_small n z :
+  0 ≤ z < bv_modulus n → bv_wrap n z = z.
+Proof. intros. by apply Z.mod_small. Qed.
+Lemma bv_swrap_small n z :
+  - bv_half_modulus n ≤ z < bv_half_modulus n →
+  bv_swrap n z = z.
+Proof.
+  intros Hrange. unfold bv_swrap.
+  destruct (decide (n = 0%N)); subst.
+  { rewrite bv_half_modulus_0 in Hrange. lia. }
+  pose proof bv_half_modulus_twice n.
+  rewrite bv_wrap_small by lia. lia.
+Qed.
+Lemma bv_wrap_0 n :
+  bv_wrap n 0 = 0.
+Proof. done. Qed.
+Lemma bv_swrap_0 n :
+  bv_swrap n 0 = 0.
+Proof.
+  pose proof bv_half_modulus_lt_modulus n.
+  pose proof bv_half_modulus_nonneg n.
+  unfold bv_swrap. rewrite bv_wrap_small; lia.
+Qed.
+Lemma bv_wrap_idemp n b : bv_wrap n (bv_wrap n b) = bv_wrap n b.
+Proof. unfold bv_wrap. by rewrite Zmod_mod. Qed.
+Definition bv_wrap_factor (n : N) (x z : Z) :=
+  x = - z `div` bv_modulus n.
+Lemma bv_wrap_factor_intro n z :
+  ∃ x, bv_wrap_factor n x z ∧ bv_wrap n z = z + x * bv_modulus n.
+Proof.
+  eexists _. split; [done|].
+  pose proof (bv_modulus_pos n). unfold bv_wrap. rewrite Z.mod_eq; lia.
+Qed.
+Lemma bv_wrap_add_modulus c n z:
+  bv_wrap n (z + c * bv_modulus n) = bv_wrap n z.
+Proof. apply Z_mod_plus_full. Qed.
+Lemma bv_wrap_add_modulus_1 n z:
+  bv_wrap n (z + bv_modulus n) = bv_wrap n z.
+Proof. rewrite <-(bv_wrap_add_modulus 1 n z). f_equal. lia. Qed.
+Lemma bv_wrap_sub_modulus c n z:
+  bv_wrap n (z - c * bv_modulus n) = bv_wrap n z.
+Proof. rewrite <-(bv_wrap_add_modulus (-c) n z). f_equal. lia. Qed.
+Lemma bv_wrap_sub_modulus_1 n z:
+  bv_wrap n (z - bv_modulus n) = bv_wrap n z.
+Proof. rewrite <-(bv_wrap_add_modulus (-1) n z). done. Qed.
+Lemma bv_wrap_add_idemp n x y :
+  bv_wrap n (bv_wrap n x + bv_wrap n y) = bv_wrap n (x + y).
+Proof. symmetry. apply Zplus_mod. Qed.
+Lemma bv_wrap_add_idemp_l n x y :
+  bv_wrap n (bv_wrap n x + y) = bv_wrap n (x + y).
+Proof. apply Zplus_mod_idemp_l. Qed.
+Lemma bv_wrap_add_idemp_r n x y :
+  bv_wrap n (x + bv_wrap n y) = bv_wrap n (x + y).
+Proof. apply Zplus_mod_idemp_r. Qed.
+Lemma bv_wrap_opp_idemp n x :
+  bv_wrap n (- bv_wrap n x) = bv_wrap n (- x).
+Proof.
+  unfold bv_wrap. pose proof (bv_modulus_pos n).
+  destruct (decide (x `mod` bv_modulus n = 0)) as [Hx|Hx].
+  - rewrite !Z.mod_opp_l_z; [done |lia|done|lia|by rewrite Hx].
+  - rewrite !Z.mod_opp_l_nz, Z.mod_mod;
+      [done|lia|lia|done|lia|by rewrite Z.mod_mod by lia].
+Qed.
+Lemma bv_wrap_mul_idemp n x y :
+  bv_wrap n (bv_wrap n x * bv_wrap n y) = bv_wrap n (x * y).
+Proof. etrans; [| apply Zmult_mod_idemp_r]. apply Zmult_mod_idemp_l. Qed.
+Lemma bv_wrap_mul_idemp_l n x y :
+  bv_wrap n (bv_wrap n x * y) = bv_wrap n (x * y).
+Proof. apply Zmult_mod_idemp_l. Qed.
+Lemma bv_wrap_mul_idemp_r n x y :
+  bv_wrap n (x * bv_wrap n y) = bv_wrap n (x * y).
+Proof. apply Zmult_mod_idemp_r. Qed.
+Lemma bv_wrap_sub_idemp n x y :
+  bv_wrap n (bv_wrap n x - bv_wrap n y) = bv_wrap n (x - y).
+Proof.
+  by rewrite <-!Z.add_opp_r, <-bv_wrap_add_idemp_r,
+    bv_wrap_opp_idemp, bv_wrap_add_idemp.
+ Qed.
+Lemma bv_wrap_sub_idemp_l n x y :
+  bv_wrap n (bv_wrap n x - y) = bv_wrap n (x - y).
+Proof. by rewrite <-!Z.add_opp_r, bv_wrap_add_idemp_l. Qed.
+Lemma bv_wrap_sub_idemp_r n x y :
+  bv_wrap n (x - bv_wrap n y) = bv_wrap n (x - y).
+Proof.
+  by rewrite <-!Z.add_opp_r, <-bv_wrap_add_idemp_r,
+    bv_wrap_opp_idemp, bv_wrap_add_idemp_r.
+Qed.
+Lemma bv_wrap_succ_idemp n x :
+  bv_wrap n (Z.succ (bv_wrap n x)) = bv_wrap n (Z.succ x).
+Proof. by rewrite <-!Z.add_1_r, bv_wrap_add_idemp_l. Qed.
+Lemma bv_wrap_pred_idemp n x :
+  bv_wrap n (Z.pred (bv_wrap n x)) = bv_wrap n (Z.pred x).
+Proof. by rewrite <-!Z.sub_1_r, bv_wrap_sub_idemp_l. Qed.
+Lemma bv_wrap_add_inj n x1 x2 y :
+  bv_wrap n x1 = bv_wrap n x2 ↔ bv_wrap n (x1 + y) = bv_wrap n (x2 + y).
+Proof.
+  split; intros Heq.
+  - by rewrite <-bv_wrap_add_idemp_l, Heq, bv_wrap_add_idemp_l.
+  - pose proof (bv_wrap_factor_intro n (x1 + y)) as [f1[? Hx1]].
+    pose proof (bv_wrap_factor_intro n (x2 + y)) as [f2[? Hx2]].
+    assert (x1 = x2 + f2 * bv_modulus n - f1 * bv_modulus n) as -> by lia.
+    by rewrite bv_wrap_sub_modulus, bv_wrap_add_modulus.
+Qed.
+Lemma bv_swrap_wrap n z:
+  bv_swrap n (bv_wrap n z) = bv_swrap n z.
+Proof. unfold bv_swrap, bv_wrap. by rewrite Zplus_mod_idemp_l. Qed.
+Lemma bv_wrap_bv_wrap n1 n2 bv :
+  (n1 ≤ n2)%N →
+  bv_wrap n1 (bv_wrap n2 bv) = bv_wrap n1 bv.
+Proof.
+  intros ?. unfold bv_wrap.
+  rewrite <-Znumtheory.Zmod_div_mod; [done| apply bv_modulus_pos.. |].
+  unfold bv_modulus. eexists (2 ^ (Z.of_N n2 - Z.of_N n1)).
+  rewrite <-Z.pow_add_r by lia. f_equal. lia.
+Qed.
+Lemma bv_wrap_land n z :
+  bv_wrap n z = Z.land z (Z.ones (Z.of_N n)).
+Proof. by rewrite Z.land_ones by lia. Qed.
+Lemma bv_wrap_spec n z i:
+  0 ≤ i →
+  Z.testbit (bv_wrap n z) i = bool_decide (i < Z.of_N n) && Z.testbit z i.
+Proof.
+  intros ?. rewrite bv_wrap_land, Z.land_spec, Z.ones_spec by lia.
+  case_bool_decide; simpl; by rewrite ?andb_true_r, ?andb_false_r.
+Qed.
+Lemma bv_wrap_spec_low n z i:
+  0 ≤ i < Z.of_N n →
+  Z.testbit (bv_wrap n z) i = Z.testbit z i.
+Proof. intros ?. rewrite bv_wrap_spec; [|lia]. case_bool_decide; [done|]. lia. Qed.
+Lemma bv_wrap_spec_high n z i:
+  Z.of_N n ≤ i →
+  Z.testbit (bv_wrap n z) i = false.
+Proof. intros ?. rewrite bv_wrap_spec; [|lia]. case_bool_decide; [|done]. lia. Qed.
+(** * [BvWf] *)
+(** The [BvWf] typeclass checks that the integer [z] can be
+interpreted as a [n]-bit integer. [BvWf] is a typeclass such that it
+can be automatically inferred for bitvector constants. *)
+Class BvWf (n : N) (z : Z) : Prop :=
+    bv_wf : (0 <=? z) && (z <? bv_modulus n)
+.
+Global Hint Mode BvWf + + : typeclass_instances.
+Global Instance bv_wf_pi n z : ProofIrrel (BvWf n z).
+Proof. unfold BvWf. apply _. Qed.
+Global Instance bv_wf_dec n z : Decision (BvWf n z).
+Proof. unfold BvWf. apply _. Defined.
+Global Typeclasses Opaque BvWf.
+Ltac solve_BvWf :=
+  lazymatch goal with
+    |- BvWf ?n ?v =>
+      is_closed_term n;
+      is_closed_term v;
+      try (vm_compute; exact I);
+      fail "Bitvector constant" v "does not fit into" n "bits"
+  end.
+Global Hint Extern 10 (BvWf _ _) => solve_BvWf : typeclass_instances.
+Lemma bv_wf_in_range n z:
+  BvWf n z ↔ 0 ≤ z < bv_modulus n.
+Proof. unfold BvWf. by rewrite andb_True, !Is_true_true, Z.leb_le, Z.ltb_lt. Qed.
+Lemma bv_wrap_wf n z :
+  BvWf n (bv_wrap n z).
+Proof. apply bv_wf_in_range. apply bv_wrap_in_range. Qed.
+Lemma bv_wf_bitwise_op {n} op bop n1 n2 :
+  (∀ k, Z.testbit (op n1 n2) k = bop (Z.testbit n1 k) (Z.testbit n2 k)) →
+  (0 ≤ n1 → 0 ≤ n2 → 0 ≤ op n1 n2) →
+  bop false false = false →
+  BvWf n n1 →
+  BvWf n n2 →
+  BvWf n (op n1 n2).
+Proof.
+  intros Hbits Hnonneg Hop [? Hok1]%bv_wf_in_range [? Hok2]%bv_wf_in_range. apply bv_wf_in_range.
+  split; [lia|].
+  apply Z.bounded_iff_bits_nonneg; [lia..|]. intros l ?.
+  eapply Z.bounded_iff_bits_nonneg in Hok1;[|try done; lia..].
+  eapply Z.bounded_iff_bits_nonneg in Hok2;[|try done; lia..].
+  by rewrite Hbits, Hok1, Hok2.
+Qed.
+(** * Definition of [bv n] *)
+Record bv (n : N) := BV {
+  bv_unsigned : Z;
+  bv_is_wf : BvWf n bv_unsigned;
+}.
+Global Arguments bv_unsigned {_}.
+Global Arguments bv_is_wf {_}.
+Global Arguments BV _ _ {_}.
+Add Printing Constructor bv.
+Global Arguments bv_unsigned : simpl never.
+Definition bv_signed {n} (b : bv n) := bv_swrap n (bv_unsigned b).
+Lemma bv_eq n (b1 b2 : bv n) :
+  b1 = b2 ↔ b1.(bv_unsigned) = b2.(bv_unsigned).
+Proof.
+  destruct b1, b2. unfold bv_unsigned. split; [ naive_solver|].
+  intros. subst. f_equal. apply proof_irrel.
+Qed.
+Lemma bv_neq n (b1 b2 : bv n) :
+  b1 ≠ b2 ↔ b1.(bv_unsigned) ≠ b2.(bv_unsigned).
+Proof. unfold not. by rewrite bv_eq. Qed.
+Global Instance bv_unsigned_inj n : Inj (=) (=) (@bv_unsigned n).
+Proof. intros ???. by apply bv_eq. Qed.
+Definition Z_to_bv_checked (n : N) (z : Z) : option (bv n) :=
+  H ← guard (BvWf n z); Some (@BV n z H).
+Program Definition Z_to_bv (n : N) (z : Z) : bv n :=
+  @BV n (bv_wrap n z) _.
+Next Obligation. apply bv_wrap_wf. Qed.
+Lemma Z_to_bv_unsigned n z:
+  bv_unsigned (Z_to_bv n z) = bv_wrap n z.
+Proof. done. Qed.
+Lemma Z_to_bv_signed n z:
+  bv_signed (Z_to_bv n z) = bv_swrap n z.
+Proof. apply bv_swrap_wrap. Qed.
+Lemma Z_to_bv_small n z:
+  0 ≤ z < bv_modulus n →
+  bv_unsigned (Z_to_bv n z) = z.
+Proof. rewrite Z_to_bv_unsigned. apply bv_wrap_small. Qed.
+Lemma bv_unsigned_BV n z Hwf:
+  bv_unsigned (@BV n z Hwf) = z.
+Proof. done. Qed.
+Lemma bv_signed_BV n z Hwf:
+  bv_signed (@BV n z Hwf) = bv_swrap n z.
+Proof. done. Qed.
+Lemma bv_unsigned_in_range n (b : bv n):
+  0 ≤ bv_unsigned b < bv_modulus n.
+Proof. apply bv_wf_in_range. apply bv_is_wf. Qed.
+Lemma bv_wrap_bv_unsigned n (b : bv n):
+  bv_wrap n (bv_unsigned b) = bv_unsigned b.
+Proof. rewrite bv_wrap_small; [done|apply bv_unsigned_in_range]. Qed.
+Lemma Z_to_bv_bv_unsigned n (b : bv n):
+  Z_to_bv n (bv_unsigned b) = b.
+Proof. apply bv_eq. by rewrite Z_to_bv_unsigned, bv_wrap_bv_unsigned. Qed.
+Lemma bv_eq_wrap n (b1 b2 : bv n) :
+  b1 = b2 ↔ bv_wrap n b1.(bv_unsigned) = bv_wrap n b2.(bv_unsigned).
+Proof.
+  rewrite !bv_wrap_small; [apply bv_eq | apply bv_unsigned_in_range..].
+Qed.
+Lemma bv_neq_wrap n (b1 b2 : bv n) :
+  b1 ≠ b2 ↔ bv_wrap n b1.(bv_unsigned) ≠ bv_wrap n b2.(bv_unsigned).
+Proof. unfold not. by rewrite bv_eq_wrap. Qed.
+Lemma bv_eq_signed n (b1 b2 : bv n) :
+  b1 = b2 ↔ bv_signed b1 = bv_signed b2.
+Proof.
+  split; [naive_solver |].
+  unfold bv_signed, bv_swrap. intros ?.
+  assert (bv_wrap n (bv_unsigned b1 + bv_half_modulus n)
+          = bv_wrap n (bv_unsigned b2 + bv_half_modulus n)) as ?%bv_wrap_add_inj by lia.
+  by apply bv_eq_wrap.
+Qed.
+Lemma bv_signed_in_range n (b : bv n):
+  n ≠ 0%N →
+  - bv_half_modulus n ≤ bv_signed b < bv_half_modulus n.
+Proof. apply bv_swrap_in_range. Qed.
+Lemma bv_unsigned_spec_high i n (b : bv n) :
+  Z.of_N n ≤ i →
+  Z.testbit (bv_unsigned b) i = false.
+Proof.
+  intros ?. pose proof (bv_unsigned_in_range _ b). unfold bv_modulus in *.
+  eapply Z.bounded_iff_bits_nonneg; [..|done]; lia.
+Qed.
+Lemma bv_unsigned_N_0 (b : bv 0):
+  bv_unsigned b = 0.
+Proof.
+  pose proof bv_unsigned_in_range 0 b as H.
+  rewrite bv_modulus_0 in H. lia.
+Qed.
+Lemma bv_signed_N_0 (b : bv 0):
+  bv_signed b = 0.
+Proof. unfold bv_signed. by rewrite bv_unsigned_N_0, bv_swrap_0. Qed.
+Lemma bv_swrap_bv_signed n (b : bv n):
+  bv_swrap n (bv_signed b) = bv_signed b.
+Proof.
+  destruct (decide (n = 0%N)); subst.
+  { by rewrite bv_signed_N_0, bv_swrap_0. }
+  apply bv_swrap_small. by apply bv_signed_in_range.
+Qed.
+Lemma Z_to_bv_checked_bv_unsigned n (b : bv n):
+  Z_to_bv_checked n (bv_unsigned b) = Some b.
+Proof.
+  unfold Z_to_bv_checked. case_guard; simplify_option_eq.
+  - f_equal. by apply bv_eq.
+  - by pose proof bv_is_wf b.
+Qed.
+Lemma Z_to_bv_checked_Some n a (b : bv n):
+  Z_to_bv_checked n a = Some b ↔ a = bv_unsigned b.
+Proof.
+  split.
+  - unfold Z_to_bv_checked. case_guard; [|done]. intros ?. by simplify_option_eq.
+  - intros ->. apply Z_to_bv_checked_bv_unsigned.
+Qed.
+(** * Typeclass instances for [bv n] *)
+Global Program Instance bv_eq_dec n : EqDecision (bv n) := λ '(@BV _ v1 p1) '(@BV _ v2 p2),
+   match decide (v1 = v2) with
+   | left eqv => left _
+   | right eqv => right _
+   end.
+Next Obligation.
+  (* TODO: Can we get a better proof term here? *)
+  intros n b1 v1 p1 ? b2 v2 p2 ????. subst.
+  rewrite (proof_irrel p1 p2). exact eq_refl.
+Defined.
+Next Obligation. intros. by injection. Qed.
+Global Instance bv_countable n : Countable (bv n) :=
+  inj_countable bv_unsigned (Z_to_bv_checked n) (Z_to_bv_checked_bv_unsigned n).
+Global Program Instance bv_finite n : Finite (bv n) :=
+  {| enum := Z_to_bv n <$> (seqZ 0 (bv_modulus n)) |}.
+Next Obligation.
+  intros n. apply NoDup_alt. intros i j x.
+  rewrite !list_lookup_fmap.
+  intros [? [[??]%lookup_seqZ ?]]%fmap_Some.
+  intros [? [[??]%lookup_seqZ Hz]]%fmap_Some. subst.
+  apply bv_eq in Hz. rewrite !Z_to_bv_small in Hz; lia.
+Qed.
+Next Obligation.
+  intros n x. apply elem_of_list_lookup. eexists (Z.to_nat (bv_unsigned x)).
+  rewrite list_lookup_fmap. apply fmap_Some. eexists _.
+  pose proof (bv_unsigned_in_range _ x). split.
+  - apply lookup_seqZ. split; [done|]. rewrite Z2Nat.id; lia.
+  - apply bv_eq. rewrite Z_to_bv_small; rewrite Z2Nat.id; lia.
+Qed.
+Lemma bv_1_ind (P : bv 1 → Prop) :
+  P (@BV 1 1 I) → P (@BV 1 0 I) → ∀ b : bv 1, P b.
+Proof.
+  intros ??. apply Forall_finite. repeat constructor.
+  - by assert ((@BV 1 0 I) = (Z_to_bv 1 (Z.of_nat 0 + 0))) as <- by by apply bv_eq.
+  - by assert ((@BV 1 1 I) = (Z_to_bv 1 (Z.of_nat 1 + 0))) as <- by by apply bv_eq.
+Qed.
+(** * [bv_saturate]: Add range facts about bit vectors to the context *)
+Lemma bv_unsigned_in_range_alt n (b : bv n):
+  -1 < bv_unsigned b < bv_modulus n.
+Proof. pose proof (bv_unsigned_in_range _ b). lia. Qed.
+Ltac bv_saturate :=
+  repeat match goal with b : bv _ |- _ => first [
+     clear b | (* Clear if unused *)
+     (* We use [bv_unsigned_in_range_alt] instead of
+     [bv_unsigned_in_range] since hypothesis of the form [0 ≤ ... < ...]
+     can cause significant slowdowns in
+     [Z.euclidean_division_equations_cleanup] due to
+     https://github.com/coq/coq/pull/17984 . *)
+     learn_hyp (bv_unsigned_in_range_alt _ b) |
+     learn_hyp (bv_signed_in_range _ b)
+  ] end.
+Ltac bv_saturate_unsigned :=
+  repeat match goal with b : bv _ |- _ => first [
+     clear b | (* Clear if unused *)
+     (* See comment in [bv_saturate]. *)
+     learn_hyp (bv_unsigned_in_range_alt _ b)
+  ] end.
+(** * Operations on [bv n] *)
+Program Definition bv_0 (n : N) :=
+  @BV n 0 _.
+Next Obligation.
+  intros n. apply bv_wf_in_range. split; [done| apply bv_modulus_pos].
+Qed.
+Global Instance bv_inhabited n : Inhabited (bv n) := populate (bv_0 n).
+Definition bv_succ {n} (x : bv n) : bv n :=
+  Z_to_bv n (Z.succ (bv_unsigned x)).
+Definition bv_pred {n} (x : bv n) : bv n :=
+  Z_to_bv n (Z.pred (bv_unsigned x)).
+Definition bv_add {n} (x y : bv n) : bv n := (* SMT: bvadd *)
+  Z_to_bv n (Z.add (bv_unsigned x) (bv_unsigned y)).
+Definition bv_sub {n} (x y : bv n) : bv n := (* SMT: bvsub *)
+  Z_to_bv n (Z.sub (bv_unsigned x) (bv_unsigned y)).
+Definition bv_opp {n} (x : bv n) : bv n := (* SMT: bvneg *)
+  Z_to_bv n (Z.opp (bv_unsigned x)).
+Definition bv_mul {n} (x y : bv n) : bv n := (* SMT: bvmul *)
+  Z_to_bv n (Z.mul (bv_unsigned x) (bv_unsigned y)).
+Program Definition bv_divu {n} (x y : bv n) : bv n := (* SMT: bvudiv *)
+  @BV n (Z.div (bv_unsigned x) (bv_unsigned y)) _.
+Next Obligation.
+  intros n x y. apply bv_wf_in_range. bv_saturate.
+  destruct (decide (bv_unsigned y = 0)) as [->|?].
+  { rewrite Zdiv_0_r. lia. }
+  split; [ apply Z.div_pos; lia |].
+  apply (Z.le_lt_trans _ (bv_unsigned x)); [|lia].
+  apply Z.div_le_upper_bound; [ lia|]. nia.
+Qed.
+Program Definition bv_modu {n} (x y : bv n) : bv n := (* SMT: bvurem *)
+  @BV n (Z.modulo (bv_unsigned x) (bv_unsigned y)) _.
+Next Obligation.
+  intros n x y. apply bv_wf_in_range. bv_saturate.
+  destruct (decide (bv_unsigned y = 0)) as [->|?].
+  { rewrite Zmod_0_r. lia. }
+  split; [ apply Z.mod_pos; lia |].
+  apply (Z.le_lt_trans _ (bv_unsigned x)); [|lia].
+  apply Z.mod_le; lia.
+Qed.
+Definition bv_divs {n} (x y : bv n) : bv n :=
+  Z_to_bv n (Z.div (bv_signed x) (bv_signed y)).
+Definition bv_quots {n} (x y : bv n) : bv n := (* SMT: bvsdiv *)
+  Z_to_bv n (Z.quot (bv_signed x) (bv_signed y)).
+Definition bv_mods {n} (x y : bv n) : bv n := (* SMT: bvsmod *)
+  Z_to_bv n (Z.modulo (bv_signed x) (bv_signed y)).
+Definition bv_rems {n} (x y : bv n) : bv n := (* SMT: bvsrem *)
+  Z_to_bv n (Z.rem (bv_signed x) (bv_signed y)).
+Definition bv_shiftl {n} (x y : bv n) : bv n := (* SMT: bvshl *)
+  Z_to_bv n (Z.shiftl (bv_unsigned x) (bv_unsigned y)).
+Program Definition bv_shiftr {n} (x y : bv n) : bv n := (* SMT: bvlshr *)
+  @BV n (Z.shiftr (bv_unsigned x) (bv_unsigned y)) _.
+Next Obligation.
+  intros n x y. apply bv_wf_in_range. bv_saturate.
+  split; [ apply Z.shiftr_nonneg; lia|].
+  rewrite Z.shiftr_div_pow2; [|lia].
+  apply (Z.le_lt_trans _ (bv_unsigned x)); [|lia].
+  pose proof (Z.pow_pos_nonneg 2 (bv_unsigned y)).
+  apply Z.div_le_upper_bound; [ lia|]. nia.
+Qed.
+Definition bv_ashiftr {n} (x y : bv n) : bv n := (* SMT: bvashr *)
+  Z_to_bv n (Z.shiftr (bv_signed x) (bv_unsigned y)).
+Program Definition bv_or {n} (x y : bv n) : bv n := (* SMT: bvor *)
+  @BV n (Z.lor (bv_unsigned x) (bv_unsigned y)) _.
+Next Obligation.
+  intros. eapply bv_wf_bitwise_op; [ apply Z.lor_spec |
+    by intros; eapply Z.lor_nonneg | done | apply bv_is_wf..].
+Qed.
+Program Definition bv_and {n} (x y : bv n) : bv n := (* SMT: bvand *)
+  @BV n (Z.land (bv_unsigned x) (bv_unsigned y)) _.
+Next Obligation.
+  intros. eapply bv_wf_bitwise_op; [ apply Z.land_spec |
+    intros; eapply Z.land_nonneg; by left | done | apply bv_is_wf..].
+Qed.
+Program Definition bv_xor {n} (x y : bv n) : bv n := (* SMT: bvxor *)
+  @BV n (Z.lxor (bv_unsigned x) (bv_unsigned y)) _.
+Next Obligation.
+  intros. eapply bv_wf_bitwise_op; [ apply Z.lxor_spec |
+    intros; eapply Z.lxor_nonneg; naive_solver | done | apply bv_is_wf..].
+Qed.
+Program Definition bv_not {n} (x : bv n) : bv n := (* SMT: bvnot *)
+  Z_to_bv n (Z.lnot (bv_unsigned x)).
+(* [bv_zero_extends z b] extends [b] to [z] bits with 0. If [z] is
+smaller than [n], [b] is truncated. Note that [z] gives the resulting
+size instead of the number of bits to add (as SMTLIB does) to avoid a
+type-level [_ + _] *)
+Program Definition bv_zero_extend {n} (z : N) (b : bv n) : bv z := (* SMT: zero_extend *)
+  Z_to_bv z (bv_unsigned b).
+Program Definition bv_sign_extend {n} (z : N) (b : bv n) : bv z := (* SMT: sign_extend *)
+  Z_to_bv z (bv_signed b).
+(* s is start index and l is length. Note that this is different from
+extract in SMTLIB which uses [extract (inclusive upper bound)
+(inclusive lower bound)]. The version here is phrased in a way that
+makes it impossible to use an upper bound that is lower than the lower
+bound. *)
+Definition bv_extract {n} (s l : N) (b : bv n) : bv l :=
+  Z_to_bv l (bv_unsigned b ≫ Z.of_N s).
+(* Note that we should always have n1 + n2 = n, but we use a parameter to avoid a type-level (_ + _) *)
+Program Definition bv_concat n {n1 n2} (b1 : bv n1) (b2 : bv n2) : bv n := (* SMT: concat *)
+  Z_to_bv n (Z.lor (bv_unsigned b1 ≪ Z.of_N n2) (bv_unsigned b2)).
+Definition bv_to_little_endian m n (z : Z) : list (bv n) :=
+  (λ b, Z_to_bv n b) <$> Z_to_little_endian m (Z.of_N n) z.
+Definition little_endian_to_bv n (bs : list (bv n)) : Z :=
+  little_endian_to_Z (Z.of_N n) (bv_unsigned <$> bs).
+(** * Operations on [bv n] and Z *)
+Definition bv_add_Z {n} (x : bv n) (y : Z) : bv n :=
+  Z_to_bv n (Z.add (bv_unsigned x) y).
+Definition bv_sub_Z {n} (x : bv n) (y : Z) : bv n :=
+  Z_to_bv n (Z.sub (bv_unsigned x) y).
+Definition bv_mul_Z {n} (x : bv n) (y : Z) : bv n :=
+  Z_to_bv n (Z.mul (bv_unsigned x) y).
+Definition bv_seq {n} (x : bv n) (len : Z) : list (bv n) :=
+  (bv_add_Z x) <$> seqZ 0 len.
+(** * Operations on [bv n] and bool *)
+Definition bool_to_bv (n : N) (b : bool) : bv n :=
+  Z_to_bv n (bool_to_Z b).
+Definition bv_to_bits {n} (b : bv n) : list bool :=
+  (λ i, Z.testbit (bv_unsigned b) i) <$> seqZ 0 (Z.of_N n).
+(** * Notation for [bv] operations *)
+Declare Scope bv_scope.
+Delimit Scope bv_scope with bv.
+Bind Scope bv_scope with bv.
+Infix "+" := bv_add : bv_scope.
+Infix "-" := bv_sub : bv_scope.
+Notation "- x" := (bv_opp x) : bv_scope.
+Infix "*" := bv_mul : bv_scope.
+Infix "`divu`" := bv_divu (at level 35) : bv_scope.
+Infix "`modu`" := bv_modu (at level 35) : bv_scope.
+Infix "`divs`" := bv_divs (at level 35) : bv_scope.
+Infix "`quots`" := bv_quots (at level 35) : bv_scope.
+Infix "`mods`" := bv_mods (at level 35) : bv_scope.
+Infix "`rems`" := bv_rems (at level 35) : bv_scope.
+Infix "≪" := bv_shiftl : bv_scope.
+Infix "≫" := bv_shiftr : bv_scope.
+Infix "`ashiftr`" := bv_ashiftr (at level 35) : bv_scope.
+Infix "`+Z`" := bv_add_Z (at level 50) : bv_scope.
+Infix "`-Z`" := bv_sub_Z (at level 50) : bv_scope.
+Infix "`*Z`" := bv_mul_Z (at level 40) : bv_scope.
+(** This adds number notations into [bv_scope].
+If the number literal is positive or 0, it gets expanded to [BV _ {num} _].
+If the number literal is negative, it gets expanded as [Z_to_bv _ {num}].
+In the negative case, the notation is parsing only and the [Z_to_bv] call will be
+printed explicitly. *)
+Inductive bv_number_notation := BVNumNonNeg (z : Z) | BVNumNeg (z : Z).
+Definition bv_number_notation_to_Z (n : bv_number_notation) : option Z :=
+  match n with
+  | BVNumNonNeg z => Some z
+  (** Don't use the notation for negative numbers for printing. *)
+  | BVNumNeg z => None
+  end.
+Definition Z_to_bv_number_notation (z : Z) :=
+  match z with
+  | Zneg _ => BVNumNeg z
+  | _ => BVNumNonNeg z
+  end.
+(** We need to temporarily change the implicit arguments of BV and
+Z_to_bv such that we can pass them to [Number Notation]. *)
+Local Arguments Z_to_bv {_} _.
+Local Arguments BV {_} _ {_}.
+Number Notation bv Z_to_bv_number_notation bv_number_notation_to_Z
+  (via bv_number_notation mapping [[BV] => BVNumNonNeg, [Z_to_bv] => BVNumNeg]) : bv_scope.
+Local Arguments BV _ _ {_}.
+Local Arguments Z_to_bv : clear implicits.
+(** * [bv_wrap_simplify]: typeclass-based automation for simplifying [bv_wrap] *)
+(** The [bv_wrap_simplify] tactic removes [bv_wrap] where possible by
+using the fact that [bv_wrap n (bv_warp n z) = bv_wrap n z]. The main
+use case for this tactic is for proving the lemmas about the
+operations of [bv n] below. Users should use the more extensive
+automation provided by [bitvector_auto.v]. *)
+Create HintDb bv_wrap_simplify_db discriminated.
+Global Hint Constants Opaque : bv_wrap_simplify_db.
+Global Hint Variables Opaque : bv_wrap_simplify_db.
+Class BvWrapSimplify (n : N) (z z' : Z) := {
+  bv_wrap_simplify_proof : bv_wrap n z = bv_wrap n z';
+}.
+Global Arguments bv_wrap_simplify_proof _ _ _ {_}.
+Global Hint Mode BvWrapSimplify + + - : bv_wrap_simplify_db.
+(** Default instance to end search. *)
+Lemma bv_wrap_simplify_id n z :
+  BvWrapSimplify n z z.
+Proof. by constructor. Qed.
+Global Hint Resolve bv_wrap_simplify_id | 1000 : bv_wrap_simplify_db.
+(** [bv_wrap_simplify_bv_wrap] performs the actual simplification. *)
+Lemma bv_wrap_simplify_bv_wrap n z z' :
+  BvWrapSimplify n z z' →
+  BvWrapSimplify n (bv_wrap n z) z'.
+Proof. intros [->]. constructor. by rewrite bv_wrap_bv_wrap. Qed.
+Global Hint Resolve bv_wrap_simplify_bv_wrap | 10 : bv_wrap_simplify_db.
+(** The rest of the instances propagate [BvWrapSimplify].  *)
+Lemma bv_wrap_simplify_succ n z z' :
+  BvWrapSimplify n z z' →
+  BvWrapSimplify n (Z.succ z) (Z.succ z').
+Proof.
+  intros [Hz]. constructor. by rewrite <-bv_wrap_succ_idemp, Hz, bv_wrap_succ_idemp.
+Qed.
+Global Hint Resolve bv_wrap_simplify_succ | 10 : bv_wrap_simplify_db.
+Lemma bv_wrap_simplify_pred n z z' :
+  BvWrapSimplify n z z' →
+  BvWrapSimplify n (Z.pred z) (Z.pred z').
+Proof.
+  intros [Hz]. constructor. by rewrite <-bv_wrap_pred_idemp, Hz, bv_wrap_pred_idemp.
+Qed.
+Global Hint Resolve bv_wrap_simplify_pred | 10 : bv_wrap_simplify_db.
+Lemma bv_wrap_simplify_opp n z z' :
+  BvWrapSimplify n z z' →
+  BvWrapSimplify n (- z) (- z').
+Proof.
+  intros [Hz]. constructor. by rewrite <-bv_wrap_opp_idemp, Hz, bv_wrap_opp_idemp.
+Qed.
+Global Hint Resolve bv_wrap_simplify_opp | 10 : bv_wrap_simplify_db.
+Lemma bv_wrap_simplify_add n z1 z1' z2 z2' :
+  BvWrapSimplify n z1 z1' →
+  BvWrapSimplify n z2 z2' →
+  BvWrapSimplify n (z1 + z2) (z1' + z2').
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  by rewrite <-bv_wrap_add_idemp, Hz1, Hz2, bv_wrap_add_idemp.
+Qed.
+Global Hint Resolve bv_wrap_simplify_add | 10 : bv_wrap_simplify_db.
+Lemma bv_wrap_simplify_sub n z1 z1' z2 z2' :
+  BvWrapSimplify n z1 z1' →
+  BvWrapSimplify n z2 z2' →
+  BvWrapSimplify n (z1 - z2) (z1' - z2').
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  by rewrite <-bv_wrap_sub_idemp, Hz1, Hz2, bv_wrap_sub_idemp.
+Qed.
+Global Hint Resolve bv_wrap_simplify_sub | 10 : bv_wrap_simplify_db.
+Lemma bv_wrap_simplify_mul n z1 z1' z2 z2' :
+  BvWrapSimplify n z1 z1' →
+  BvWrapSimplify n z2 z2' →
+  BvWrapSimplify n (z1 * z2) (z1' * z2').
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  by rewrite <-bv_wrap_mul_idemp, Hz1, Hz2, bv_wrap_mul_idemp.
+Qed.
+Global Hint Resolve bv_wrap_simplify_mul | 10 : bv_wrap_simplify_db.
+(** [bv_wrap_simplify_left] applies for goals of the form [bv_wrap n z1 = _] and
+ tries to simplify them by removing any [bv_wrap] inside z1. *)
+Ltac bv_wrap_simplify_left :=
+  lazymatch goal with |- bv_wrap _ _ = _ => idtac end;
+  etrans; [ notypeclasses refine (bv_wrap_simplify_proof _ _ _);
+            typeclasses eauto with bv_wrap_simplify_db | ]
+.
+(** [bv_wrap_simplify] applies for goals of the form [bv_wrap n z1 = bv_wrap n z2] and
+[bv_swrap n z1 = bv_swrap n z2] and tries to simplify them by removing any [bv_wrap]
+and [bv_swrap] inside z1 and z2. *)
+Ltac bv_wrap_simplify :=
+  unfold bv_signed, bv_swrap;
+  try match goal with | |- _ - _ = _ - _ => f_equal end;
+  bv_wrap_simplify_left;
+  symmetry;
+  bv_wrap_simplify_left;
+  symmetry.
+Ltac bv_wrap_simplify_solve :=
+  bv_wrap_simplify; f_equal; lia.
+(** * Lemmas about [bv n] operations *)
+(** ** Unfolding lemmas for the operations. *)
+Section unfolding.
+  Context {n : N}.
+  Implicit Types (b : bv n).
+  Lemma bv_0_unsigned :
+    bv_unsigned (bv_0 n) = 0.
+  Proof. done. Qed.
+  Lemma bv_0_signed :
+    bv_signed (bv_0 n) = 0.
+  Proof. unfold bv_0. by rewrite bv_signed_BV, bv_swrap_0. Qed.
+  Lemma bv_succ_unsigned b :
+    bv_unsigned (bv_succ b) = bv_wrap n (Z.succ (bv_unsigned b)).
+  Proof. done. Qed.
+  Lemma bv_succ_signed b :
+    bv_signed (bv_succ b) = bv_swrap n (Z.succ (bv_signed b)).
+  Proof. unfold bv_succ. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
+  Lemma bv_pred_unsigned b :
+    bv_unsigned (bv_pred b) = bv_wrap n (Z.pred (bv_unsigned b)).
+  Proof. done. Qed.
+  Lemma bv_pred_signed b :
+    bv_signed (bv_pred b) = bv_swrap n (Z.pred (bv_signed b)).
+  Proof. unfold bv_pred. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
+  Lemma bv_add_unsigned b1 b2 :
+    bv_unsigned (b1 + b2) = bv_wrap n (bv_unsigned b1 + bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_add_signed b1 b2 :
+    bv_signed (b1 + b2) = bv_swrap n (bv_signed b1 + bv_signed b2).
+  Proof. unfold bv_add. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
+  Lemma bv_sub_unsigned b1 b2 :
+    bv_unsigned (b1 - b2) = bv_wrap n (bv_unsigned b1 - bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_sub_signed b1 b2 :
+    bv_signed (b1 - b2) = bv_swrap n (bv_signed b1 - bv_signed b2).
+  Proof. unfold bv_sub. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
+  Lemma bv_opp_unsigned b :
+    bv_unsigned (- b) = bv_wrap n (- bv_unsigned b).
+  Proof. done. Qed.
+  Lemma bv_opp_signed b :
+    bv_signed (- b) = bv_swrap n (- bv_signed b).
+  Proof. unfold bv_opp. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
+  Lemma bv_mul_unsigned b1 b2 :
+    bv_unsigned (b1 * b2) = bv_wrap n (bv_unsigned b1 * bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_mul_signed b1 b2 :
+    bv_signed (b1 * b2) = bv_swrap n (bv_signed b1 * bv_signed b2).
+  Proof. unfold bv_mul. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
+  Lemma bv_divu_unsigned b1 b2 :
+    bv_unsigned (b1 `divu` b2) = bv_unsigned b1 `div` bv_unsigned b2.
+  Proof. done. Qed.
+  Lemma bv_divu_signed b1 b2 :
+    bv_signed (b1 `divu` b2) = bv_swrap n (bv_unsigned b1 `div` bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_modu_unsigned b1 b2 :
+    bv_unsigned (b1 `modu` b2) = bv_unsigned b1 `mod` bv_unsigned b2.
+  Proof. done. Qed.
+  Lemma bv_modu_signed b1 b2 :
+    bv_signed (b1 `modu` b2) = bv_swrap n (bv_unsigned b1 `mod` bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_divs_unsigned b1 b2 :
+    bv_unsigned (b1 `divs` b2) = bv_wrap n (bv_signed b1 `div` bv_signed b2).
+  Proof. done. Qed.
+  Lemma bv_divs_signed b1 b2 :
+    bv_signed (b1 `divs` b2) = bv_swrap n (bv_signed b1 `div` bv_signed b2).
+  Proof. unfold bv_divs. rewrite Z_to_bv_signed. done. Qed.
+  Lemma bv_quots_unsigned b1 b2 :
+    bv_unsigned (b1 `quots` b2) = bv_wrap n (bv_signed b1 `quot` bv_signed b2).
+  Proof. done. Qed.
+  Lemma bv_quots_signed b1 b2 :
+    bv_signed (b1 `quots` b2) = bv_swrap n (bv_signed b1 `quot` bv_signed b2).
+  Proof. unfold bv_quots. rewrite Z_to_bv_signed. done. Qed.
+  Lemma bv_mods_unsigned b1 b2 :
+    bv_unsigned (b1 `mods` b2) = bv_wrap n (bv_signed b1 `mod` bv_signed b2).
+  Proof. done. Qed.
+  Lemma bv_mods_signed b1 b2 :
+    bv_signed (b1 `mods` b2) = bv_swrap n (bv_signed b1 `mod` bv_signed b2).
+  Proof. unfold bv_mods. rewrite Z_to_bv_signed. done. Qed.
+  Lemma bv_rems_unsigned b1 b2 :
+    bv_unsigned (b1 `rems` b2) = bv_wrap n (bv_signed b1 `rem` bv_signed b2).
+  Proof. done. Qed.
+  Lemma bv_rems_signed b1 b2 :
+    bv_signed (b1 `rems` b2) = bv_swrap n (bv_signed b1 `rem` bv_signed b2).
+  Proof. unfold bv_rems. rewrite Z_to_bv_signed. done. Qed.
+  Lemma bv_shiftl_unsigned b1 b2 :
+    bv_unsigned (b1 ≪ b2) = bv_wrap n (bv_unsigned b1 ≪ bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_shiftl_signed b1 b2 :
+    bv_signed (b1 ≪ b2) = bv_swrap n (bv_unsigned b1 ≪ bv_unsigned b2).
+  Proof. unfold bv_shiftl. rewrite Z_to_bv_signed. done. Qed.
+  Lemma bv_shiftr_unsigned b1 b2 :
+    bv_unsigned (b1 ≫ b2) = bv_unsigned b1 ≫ bv_unsigned b2.
+  Proof. done. Qed.
+  Lemma bv_shiftr_signed b1 b2 :
+    bv_signed (b1 ≫ b2) = bv_swrap n (bv_unsigned b1 ≫ bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_ashiftr_unsigned b1 b2 :
+    bv_unsigned (b1 `ashiftr` b2) = bv_wrap n (bv_signed b1 ≫ bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_ashiftr_signed b1 b2 :
+    bv_signed (b1 `ashiftr` b2) = bv_swrap n (bv_signed b1 ≫ bv_unsigned b2).
+  Proof. unfold bv_ashiftr. rewrite Z_to_bv_signed. done. Qed.
+  Lemma bv_or_unsigned b1 b2 :
+    bv_unsigned (bv_or b1 b2) = Z.lor (bv_unsigned b1) (bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_or_signed b1 b2 :
+    bv_signed (bv_or b1 b2) = bv_swrap n (Z.lor (bv_unsigned b1) (bv_unsigned b2)).
+  Proof. done. Qed.
+  Lemma bv_and_unsigned b1 b2 :
+    bv_unsigned (bv_and b1 b2) = Z.land (bv_unsigned b1) (bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_and_signed b1 b2 :
+    bv_signed (bv_and b1 b2) = bv_swrap n (Z.land (bv_unsigned b1) (bv_unsigned b2)).
+  Proof. done. Qed.
+  Lemma bv_xor_unsigned b1 b2 :
+    bv_unsigned (bv_xor b1 b2) = Z.lxor (bv_unsigned b1) (bv_unsigned b2).
+  Proof. done. Qed.
+  Lemma bv_xor_signed b1 b2 :
+    bv_signed (bv_xor b1 b2) = bv_swrap n (Z.lxor (bv_unsigned b1) (bv_unsigned b2)).
+  Proof. done. Qed.
+  Lemma bv_not_unsigned b :
+    bv_unsigned (bv_not b) = bv_wrap n (Z.lnot (bv_unsigned b)).
+  Proof. done. Qed.
+  Lemma bv_not_signed b :
+    bv_signed (bv_not b) = bv_swrap n (Z.lnot (bv_unsigned b)).
+  Proof. unfold bv_not. rewrite Z_to_bv_signed. done. Qed.
+  Lemma bv_zero_extend_unsigned' z b :
+    bv_unsigned (bv_zero_extend z b) = bv_wrap z (bv_unsigned b).
+  Proof. done. Qed.
+  (* [bv_zero_extend_unsigned] is the version that we want, but it
+  only holds with a precondition. *)
+  Lemma bv_zero_extend_unsigned z b :
+    (n ≤ z)%N →
+    bv_unsigned (bv_zero_extend z b) = bv_unsigned b.
+  Proof.
+    intros ?. rewrite bv_zero_extend_unsigned', bv_wrap_small; [done|].
+    bv_saturate. pose proof (bv_modulus_le_mono n z). lia.
+  Qed.
+  Lemma bv_zero_extend_signed z b :
+    bv_signed (bv_zero_extend z b) = bv_swrap z (bv_unsigned b).
+  Proof. unfold bv_zero_extend. rewrite Z_to_bv_signed. done. Qed.
+  Lemma bv_sign_extend_unsigned z b :
+    bv_unsigned (bv_sign_extend z b) = bv_wrap z (bv_signed b).
+  Proof. done. Qed.
+  Lemma bv_sign_extend_signed' z b :
+    bv_signed (bv_sign_extend z b) = bv_swrap z (bv_signed b).
+  Proof. unfold bv_sign_extend. rewrite Z_to_bv_signed. done. Qed.
+  (* [bv_sign_extend_signed] is the version that we want, but it
+  only holds with a precondition. *)
+  Lemma bv_sign_extend_signed z b :
+    (n ≤ z)%N →
+    bv_signed (bv_sign_extend z b) = bv_signed b.
+  Proof.
+    intros ?. rewrite bv_sign_extend_signed'.
+    destruct (decide (n = 0%N)); subst.
+    { by rewrite bv_signed_N_0, bv_swrap_0. }
+    apply bv_swrap_small. bv_saturate.
+    pose proof bv_half_modulus_le_mono n z. lia.
+  Qed.
+  Lemma bv_extract_unsigned s l b :
+    bv_unsigned (bv_extract s l b) = bv_wrap l (bv_unsigned b ≫ Z.of_N s).
+  Proof. done. Qed.
+  Lemma bv_extract_signed s l b :
+    bv_signed (bv_extract s l b) = bv_swrap l (bv_unsigned b ≫ Z.of_N s).
+  Proof. unfold bv_extract. rewrite Z_to_bv_signed. done. Qed.
+  Lemma bv_concat_unsigned' m  n2 b1 (b2 : bv n2) :
+    bv_unsigned (bv_concat m b1 b2) = bv_wrap m (Z.lor (bv_unsigned b1 ≪ Z.of_N n2) (bv_unsigned b2)).
+  Proof. done. Qed.
+  (* [bv_concat_unsigned] is the version that we want, but it
+  only holds with a precondition. *)
+  Lemma bv_concat_unsigned m n2 b1 (b2 : bv n2) :
+    (m = n + n2)%N →
+    bv_unsigned (bv_concat m b1 b2) = Z.lor (bv_unsigned b1 ≪ Z.of_N n2) (bv_unsigned b2).
+  Proof.
+    intros ->. rewrite bv_concat_unsigned', bv_wrap_small; [done|].
+    apply Z.bounded_iff_bits_nonneg'; [lia | |].
+    { apply Z.lor_nonneg. bv_saturate. split; [|lia]. apply Z.shiftl_nonneg. lia. }
+    intros k ?. rewrite Z.lor_spec, Z.shiftl_spec; [|lia].
+    apply orb_false_intro; (eapply Z.bounded_iff_bits_nonneg; [..|done]); bv_saturate; try lia.
+    - apply (Z.lt_le_trans _ (bv_modulus n)); [lia|]. apply Z.pow_le_mono_r; lia.
+    - apply (Z.lt_le_trans _ (bv_modulus n2)); [lia|]. apply Z.pow_le_mono_r; lia.
+  Qed.
+  Lemma bv_concat_signed m n2 b1 (b2 : bv n2) :
+    bv_signed (bv_concat m b1 b2) = bv_swrap m (Z.lor (bv_unsigned b1 ≪ Z.of_N n2) (bv_unsigned b2)).
+  Proof. unfold bv_concat. rewrite Z_to_bv_signed. done. Qed.
+  Lemma bv_add_Z_unsigned b z :
+    bv_unsigned (b `+Z` z) = bv_wrap n (bv_unsigned b + z).
+  Proof. done. Qed.
+  Lemma bv_add_Z_signed b z :
+    bv_signed (b `+Z` z) = bv_swrap n (bv_signed b + z).
+  Proof. unfold bv_add_Z. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
+  Lemma bv_sub_Z_unsigned b z :
+    bv_unsigned (b `-Z` z) = bv_wrap n (bv_unsigned b - z).
+  Proof. done. Qed.
+  Lemma bv_sub_Z_signed b z :
+    bv_signed (b `-Z` z) = bv_swrap n (bv_signed b - z).
+  Proof. unfold bv_sub_Z. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
+  Lemma bv_mul_Z_unsigned b z:
+    bv_unsigned (b `*Z` z) = bv_wrap n (bv_unsigned b * z).
+  Proof. done. Qed.
+  Lemma bv_mul_Z_signed b z :
+    bv_signed (b `*Z` z) = bv_swrap n (bv_signed b * z).
+  Proof. unfold bv_mul_Z. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
+End unfolding.
+(** ** Properties of bv operations *)
+Section properties.
+  Context {n : N}.
+  Implicit Types (b : bv n).
+  Local Open Scope bv_scope.
+  Lemma bv_sub_add_opp b1 b2:
+    b1 - b2 = b1 + - b2.
+  Proof.
+    apply bv_eq. unfold bv_sub, bv_add, bv_opp. rewrite !Z_to_bv_unsigned.
+    bv_wrap_simplify_solve.
+  Qed.
+  Global Instance bv_add_assoc : Assoc (=) (@bv_add n).
+  Proof.
+    intros ???. unfold bv_add. apply bv_eq. rewrite !Z_to_bv_unsigned.
+    bv_wrap_simplify_solve.
+  Qed.
+  Global Instance bv_mul_assoc : Assoc (=) (@bv_mul n).
+  Proof.
+    intros ???. unfold bv_mul. apply bv_eq. rewrite !Z_to_bv_unsigned.
+    bv_wrap_simplify_solve.
+  Qed.
+  Lemma bv_add_0_l b1 b2 :
+    bv_unsigned b1 = 0%Z →
+    b1 + b2 = b2.
+  Proof.
+    intros Hb. apply bv_eq.
+    rewrite bv_add_unsigned, Hb, Z.add_0_l, bv_wrap_small; [done|apply bv_unsigned_in_range].
+  Qed.
+  Lemma bv_add_0_r b1 b2 :
+    bv_unsigned b2 = 0%Z →
+    b1 + b2 = b1.
+  Proof.
+    intros Hb. apply bv_eq.
+    rewrite bv_add_unsigned, Hb, Z.add_0_r, bv_wrap_small; [done|apply bv_unsigned_in_range].
+  Qed.
+  Lemma bv_add_Z_0 b : b `+Z` 0 = b.
+  Proof.
+    unfold bv_add_Z. rewrite Z.add_0_r.
+    apply bv_eq. apply Z_to_bv_small. apply bv_unsigned_in_range.
+  Qed.
+  Lemma bv_add_Z_add_r b m o:
+    b `+Z` (m + o) = (b `+Z` o) `+Z` m.
+  Proof.
+    apply bv_eq. unfold bv_add_Z. rewrite !Z_to_bv_unsigned.
+     bv_wrap_simplify_solve.
+  Qed.
+  Lemma bv_add_Z_add_l b m o:
+    b `+Z` (m + o) = (b `+Z` m) `+Z` o.
+  Proof.
+    apply bv_eq. unfold bv_add_Z. rewrite !Z_to_bv_unsigned.
+     bv_wrap_simplify_solve.
+  Qed.
+  Lemma bv_add_Z_succ b m:
+    b `+Z` Z.succ m = (b `+Z` 1) `+Z` m.
+  Proof.
+    apply bv_eq. unfold bv_add_Z. rewrite !Z_to_bv_unsigned.
+    bv_wrap_simplify_solve.
+  Qed.
+  Lemma bv_add_Z_inj_l b i j:
+    0 ≤ i < bv_modulus n →
+    0 ≤ j < bv_modulus n →
+    b `+Z` i = b `+Z` j ↔ i = j.
+  Proof.
+    intros ??. split; [|naive_solver].
+    intros Heq%bv_eq. rewrite !bv_add_Z_unsigned, !(Z.add_comm (bv_unsigned _)) in Heq.
+    by rewrite <-bv_wrap_add_inj, !bv_wrap_small in Heq.
+  Qed.
+  Lemma bv_opp_not b:
+    - b `-Z` 1 = bv_not b.
+  Proof.
+    apply bv_eq.
+    rewrite bv_not_unsigned, bv_sub_Z_unsigned, bv_opp_unsigned, <-Z.opp_lnot.
+    bv_wrap_simplify_solve.
+  Qed.
+  Lemma bv_and_comm b1 b2:
+    bv_and b1 b2 = bv_and b2 b1.
+  Proof. apply bv_eq. by rewrite !bv_and_unsigned, Z.land_comm. Qed.
+  Lemma bv_or_comm b1 b2:
+    bv_or b1 b2 = bv_or b2 b1.
+  Proof. apply bv_eq. by rewrite !bv_or_unsigned, Z.lor_comm. Qed.
+  Lemma bv_or_0_l b1 b2 :
+    bv_unsigned b1 = 0%Z →
+    bv_or b1 b2 = b2.
+  Proof. intros Hb. apply bv_eq. by rewrite bv_or_unsigned, Hb, Z.lor_0_l. Qed.
+  Lemma bv_or_0_r b1 b2 :
+    bv_unsigned b2 = 0%Z →
+    bv_or b1 b2 = b1.
+  Proof. intros Hb. apply bv_eq. by rewrite bv_or_unsigned, Hb, Z.lor_0_r. Qed.
+  Lemma bv_extract_0_unsigned l b:
+    bv_unsigned (bv_extract 0 l b) = bv_wrap l (bv_unsigned b).
+  Proof. rewrite bv_extract_unsigned, Z.shiftr_0_r. done. Qed.
+  Lemma bv_extract_0_bv_add_distr l b1 b2:
+    (l ≤ n)%N →
+    bv_extract 0 l (bv_add b1 b2) = bv_add (bv_extract 0 l b1) (bv_extract 0 l b2).
+  Proof.
+    intros ?.
+    apply bv_eq. rewrite !bv_extract_0_unsigned, !bv_add_unsigned, !bv_extract_0_unsigned.
+    rewrite bv_wrap_bv_wrap by done.
+    bv_wrap_simplify_solve.
+  Qed.
+  Lemma bv_concat_0 m n2 b1 (b2 : bv n2) :
+    bv_unsigned b1 = 0%Z →
+    bv_concat m b1 b2 = bv_zero_extend m b2.
+  Proof.
+    intros Hb1. apply bv_eq.
+    by rewrite bv_zero_extend_unsigned', bv_concat_unsigned', Hb1, Z.shiftl_0_l, Z.lor_0_l.
+  Qed.
+  Lemma bv_zero_extend_idemp b:
+    bv_zero_extend n b = b.
+  Proof. apply bv_eq. by rewrite bv_zero_extend_unsigned. Qed.
+  Lemma bv_sign_extend_idemp b:
+    bv_sign_extend n b = b.
+  Proof. apply bv_eq_signed. by rewrite bv_sign_extend_signed. Qed.
+End properties.
+(** ** Lemmas about [bv_to_little] and [bv_of_little] *)
+Section little.
+  Lemma bv_to_litte_endian_unsigned m n z:
+    0 ≤ m →
+    bv_unsigned <$> bv_to_little_endian m n z = Z_to_little_endian m (Z.of_N n) z.
+  Proof.
+    intros ?. apply list_eq. intros i. unfold bv_to_little_endian.
+    rewrite list_lookup_fmap, list_lookup_fmap.
+    destruct (Z_to_little_endian m (Z.of_N n) z !! i) eqn: Heq; [simpl |done].
+    rewrite Z_to_bv_small; [done|].
+    eapply (Forall_forall (λ z, _ ≤ z < _)); [ |by eapply elem_of_list_lookup_2].
+    eapply Z_to_little_endian_bound; lia.
+  Qed.
+  Lemma bv_to_little_endian_to_bv m n bs:
+    m = Z.of_nat (length bs) →
+    bv_to_little_endian m n (little_endian_to_bv n bs) = bs.
+  Proof.
+    intros ->. apply (inj (fmap bv_unsigned)).
+    rewrite bv_to_litte_endian_unsigned; [|lia].
+    apply Z_to_little_endian_to_Z; [by rewrite length_fmap | lia |].
+    apply Forall_forall. intros ? [?[->?]]%elem_of_list_fmap_2. apply bv_unsigned_in_range.
+  Qed.
+  Lemma little_endian_to_bv_to_little_endian m n z:
+    0 ≤ m →
+    little_endian_to_bv n (bv_to_little_endian m n z) = z `mod` 2 ^ (m * Z.of_N n).
+  Proof.
+    intros ?. unfold little_endian_to_bv.
+    rewrite bv_to_litte_endian_unsigned; [|lia].
+    apply little_endian_to_Z_to_little_endian; lia.
+  Qed.
+  Lemma length_bv_to_little_endian m n z :
+    0 ≤ m →
+    length (bv_to_little_endian m n z) = Z.to_nat m.
+  Proof.
+    intros ?. unfold bv_to_little_endian. rewrite length_fmap.
+    apply Nat2Z.inj. rewrite length_Z_to_little_endian, ?Z2Nat.id; try lia.
+  Qed.
+  Lemma little_endian_to_bv_bound n bs :
+    0 ≤ little_endian_to_bv n bs < 2 ^ (Z.of_nat (length bs) * Z.of_N n).
+  Proof.
+    unfold little_endian_to_bv. rewrite <-(length_fmap bv_unsigned bs).
+    apply little_endian_to_Z_bound; [lia|].
+    apply Forall_forall. intros ? [? [-> ?]]%elem_of_list_fmap.
+    apply bv_unsigned_in_range.
+  Qed.
+  Lemma Z_to_bv_little_endian_to_bv_to_little_endian x m n (b : bv x):
+    0 ≤ m →
+    x = (Z.to_N m * n)%N →
+    Z_to_bv x (little_endian_to_bv n (bv_to_little_endian m n (bv_unsigned b))) = b.
+  Proof.
+    intros ? ->. rewrite little_endian_to_bv_to_little_endian, Z.mod_small; [| |lia].
+    - apply bv_eq. rewrite Z_to_bv_small; [done|]. apply bv_unsigned_in_range.
+    - pose proof bv_unsigned_in_range _ b as Hr. unfold bv_modulus in Hr.
+      by rewrite N2Z.inj_mul, Z2N.id in Hr.
+  Qed.
+  Lemma bv_to_little_endian_lookup_Some m n z (i : nat) x:
+    0 ≤ m → bv_to_little_endian m n z !! i = Some x ↔
+      Z.of_nat i < m ∧ x = Z_to_bv n (z ≫ (Z.of_nat i * Z.of_N n)).
+  Proof.
+    unfold bv_to_little_endian. intros Hm. rewrite list_lookup_fmap, fmap_Some.
+    split.
+    - intros [?[[??]%Z_to_little_endian_lookup_Some ?]]; [|lia..]; subst. split; [done|].
+      rewrite <-bv_wrap_land. apply bv_eq. by rewrite !Z_to_bv_unsigned, bv_wrap_bv_wrap.
+    - intros [?->]. eexists _. split; [apply Z_to_little_endian_lookup_Some; try done; lia| ].
+      rewrite <-bv_wrap_land. apply bv_eq. by rewrite !Z_to_bv_unsigned, bv_wrap_bv_wrap.
+  Qed.
+  Lemma little_endian_to_bv_spec n bs i b:
+    0 ≤ i → n ≠ 0%N →
+    bs !! Z.to_nat (i `div` Z.of_N n) = Some b →
+    Z.testbit (little_endian_to_bv n bs) i = Z.testbit (bv_unsigned b) (i `mod` Z.of_N n).
+  Proof.
+    intros ???. unfold little_endian_to_bv. apply little_endian_to_Z_spec; [lia|lia| |].
+    { apply Forall_fmap. apply Forall_true. intros ?; simpl. apply bv_unsigned_in_range. }
+    rewrite list_lookup_fmap. apply fmap_Some. naive_solver.
+  Qed.
+End little.
+(** ** Lemmas about [bv_seq] *)
+Section bv_seq.
+  Context {n : N}.
+  Implicit Types (b : bv n).
+  Lemma length_bv_seq b len:
+    length (bv_seq b len) = Z.to_nat len.
+  Proof. unfold bv_seq. by rewrite length_fmap, length_seqZ. Qed.
+  Lemma bv_seq_succ b m:
+    0 ≤ m →
+    bv_seq b (Z.succ m) = b :: bv_seq (b `+Z` 1) m.
+  Proof.
+    intros. unfold bv_seq. rewrite seqZ_cons by lia. csimpl.
+    rewrite bv_add_Z_0. f_equal.
+    assert (Z.succ 0 = 1 + 0) as -> by lia.
+    rewrite <-fmap_add_seqZ, <-list_fmap_compose, Z.pred_succ. apply list_fmap_ext.
+    intros i x. simpl. by rewrite bv_add_Z_add_l.
+  Qed.
+  Lemma NoDup_bv_seq b z:
+    0 ≤ z ≤ bv_modulus n →
+    NoDup (bv_seq b z).
+  Proof.
+    intros ?. apply NoDup_alt. intros i j b'. unfold bv_seq. rewrite !list_lookup_fmap.
+    intros [?[[??]%lookup_seqZ ?]]%fmap_Some ; simplify_eq.
+    intros [?[[->?]%lookup_seqZ ?%bv_add_Z_inj_l]]%fmap_Some; lia.
+  Qed.
+End bv_seq.
+(** ** Lemmas about [bv] and [bool] *)
+Section bv_bool.
+  Implicit Types (b : bool).
+  Lemma bool_to_bv_unsigned n b:
+    n ≠ 0%N →
+    bv_unsigned (bool_to_bv n b) = bool_to_Z b.
+  Proof.
+    intros ?. pose proof (bv_modulus_gt_1 n).
+    apply Z_to_bv_small. destruct b; simpl; lia.
+  Qed.
+  Lemma bv_extract_bool_to_bv n n2 b:
+    n ≠ 0%N → n2 ≠ 0%N →
+    bv_extract 0 n (bool_to_bv n2 b) = bool_to_bv n b.
+  Proof.
+    intros ??. apply bv_eq. pose proof (bv_modulus_gt_1 n).
+    rewrite bv_extract_unsigned, !bool_to_bv_unsigned, Z.shiftr_0_r by done.
+    rewrite bv_wrap_small; [done|]. destruct b; simpl; lia.
+  Qed.
+  Lemma bv_not_bool_to_bv b:
+    bv_not (bool_to_bv 1 b) = bool_to_bv 1 (negb b).
+  Proof. apply bv_eq. by destruct b. Qed.
+  Lemma bool_decide_bool_to_bv_0 b:
+    bool_decide (bv_unsigned (bool_to_bv 1 b) = 0) = negb b.
+  Proof. by destruct b. Qed.
+  Lemma bool_decide_bool_to_bv_1 b:
+    bool_decide (bv_unsigned (bool_to_bv 1 b) = 1) = b.
+  Proof. by destruct b. Qed.
+End bv_bool.
+Section bv_bits.
+  Context {n : N}.
+  Implicit Types (b : bv n).
+  Lemma length_bv_to_bits b : length (bv_to_bits b) = N.to_nat n.
+  Proof. unfold bv_to_bits. rewrite length_fmap, length_seqZ, <-Z_N_nat, N2Z.id. done. Qed.
+  Lemma bv_to_bits_lookup_Some b i x:
+    bv_to_bits b !! i = Some x ↔ (i < N.to_nat n)%nat ∧ x = Z.testbit (bv_unsigned b) (Z.of_nat i).
+  Proof.
+    unfold bv_to_bits. rewrite list_lookup_fmap, fmap_Some.
+    split.
+    - intros [?[?%lookup_seqZ?]]. naive_solver lia.
+    - intros [??]. eexists _. split; [|done]. apply lookup_seqZ. lia.
+  Qed.
+  Global Instance bv_to_bits_inj : Inj eq eq (@bv_to_bits n).
+  Proof.
+    unfold bv_to_bits. intros x y Hf.
+    apply bv_eq_wrap. apply Z.bits_inj_iff'. intros i Hi.
+    rewrite !bv_wrap_spec; [|lia..]. case_bool_decide; simpl; [|done].
+    eapply list_fmap_inj_1 in Hf; [done|]. apply elem_of_seqZ. lia.
+  Qed.
+End bv_bits.
+(** * [bvn] *)
+Record bvn := bv_to_bvn {
+  bvn_n : N;
+  bvn_val : bv bvn_n;
+}.
+Global Arguments bv_to_bvn {_} _.
+Add Printing Constructor bvn.
+Definition bvn_unsigned (b : bvn) := bv_unsigned (b.(bvn_val)).
+Lemma bvn_eq (b1 b2 : bvn) :
+  b1 = b2 ↔ b1.(bvn_n) = b2.(bvn_n) ∧ bvn_unsigned b1 = bvn_unsigned b2.
+Proof. split; [ naive_solver|]. destruct b1, b2; simpl; intros [??]. subst. f_equal. by apply bv_eq. Qed.
+Global Program Instance bvn_eq_dec : EqDecision bvn := λ '(@bv_to_bvn n1 b1) '(@bv_to_bvn n2 b2),
+   cast_if_and (decide (n1 = n2)) (decide (bv_unsigned b1 = bv_unsigned b2)).
+(* TODO: The following does not compute to eq_refl*)
+Next Obligation. intros. apply bvn_eq. naive_solver. Qed.
+Next Obligation. intros. intros ?%bvn_eq. naive_solver. Qed.
+Next Obligation. intros. intros ?%bvn_eq. naive_solver. Qed.
+Definition bvn_to_bv (n : N) (b : bvn) : option (bv n) :=
+  match decide (b.(bvn_n) = n) with
+  | left eq => Some (eq_rect (bvn_n b) (λ n0 : N, bv n0) (bvn_val b) n eq)
+  | right _ => None
+  end.
+Global Arguments bvn_to_bv !_ !_ /.
+Global Coercion bv_to_bvn : bv >-> bvn.
+(** * Opaqueness *)
+(** We mark all functions on bitvectors as opaque. *)
+Global Hint Opaque Z_to_bv
+       bv_0 bv_succ bv_pred
+       bv_add bv_sub bv_opp
+       bv_mul bv_divu bv_modu
+       bv_divs bv_quots bv_mods bv_rems
+       bv_shiftl bv_shiftr bv_ashiftr bv_or
+       bv_and bv_xor bv_not bv_zero_extend
+       bv_sign_extend bv_extract bv_concat
+       bv_add_Z bv_sub_Z bv_mul_Z
+       bool_to_bv bv_to_bits : typeclass_instances.
+Global Opaque Z_to_bv
+       bv_0 bv_succ bv_pred
+       bv_add bv_sub bv_opp
+       bv_mul bv_divu bv_modu
+       bv_divs bv_quots bv_mods bv_rems
+       bv_shiftl bv_shiftr bv_ashiftr bv_or
+       bv_and bv_xor bv_not bv_zero_extend
+       bv_sign_extend bv_extract bv_concat
+       bv_add_Z bv_sub_Z bv_mul_Z
+       bool_to_bv bv_to_bits.
--- a/stdpp_bitvector/dune
+++ b/stdpp_bitvector/dune
+(include_subdirs qualified)
+(coq.theory
+ (name stdpp.bitvector)
+ (package coq-stdpp-bitvector)
+ (theories stdpp))
--- a/stdpp_bitvector/tactics.v
+++ b/stdpp_bitvector/tactics.v
+(** This file is maintained by Michael Sammler. *)
+From stdpp.bitvector Require Export definitions.
+From stdpp Require Import options.
+(** * bitvector tactics *)
+(** This file provides tactics for the bitvector library in
+[bitvector.v]. In particular, it provides integration of bitvectors
+with the [bitblast] tactic and tactics for simplifying and solving
+bitvector expressions. The main tactic provided by this library is
+[bv_simplify] which performs the following steps:
+1. Simplify the goal by rewriting with the [bv_simplify] database.
+2. If the goal is an (in)equality (= or ≠) between bitvectors, turn it into
+an (in)equality between their unsigned values. (Using unsigned values here
+rather than signed is somewhat arbitrary but works well enough in practice.)
+3. Unfold [bv_unsigned] and [bv_signed] of operations on [bv n] to
+operations on [Z].
+4. Simplify the goal by rewriting with the [bv_unfolded_simplify]
+database.
+This file provides the following variants of the [bv_simplify] tactic:
+- [bv_simplify] applies the simplification procedure to the goal.
+- [bv_simplify H] applies the simplification procedure to the hypothesis [H].
+- [bv_simplify select pat] applies the simplification procedure to the hypothesis
+  matching [pat].
+- [bv_simplify_arith] applies the simplification procedure to the goal and
+  additionally rewrites with the [bv_unfolded_to_arith] database to turn the goal
+  into a more suitable shape for calling [lia].
+- [bv_simplify_arith H] same as [bv_simplify_arith], but in the hypothesis [H].
+- [bv_simplify_arith select pat] same as [bv_simplify_arith], but in the
+  hypothesis matching [pat].
+- [bv_solve] simplifies the goal using [bv_simplify_arith], learns bounds facts
+  about bitvector variables in the context and tries to solve the goal using [lia].
+This automation assumes that [lia] can handle [`mod`] and [`div`] as can be enabled
+via the one of the following flags:
+Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
+or
+Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations.
+or
+Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true).
+See https://coq.github.io/doc/master/refman/addendum/micromega.html#coq:tacn.zify
+for details.
+*)
+(** * Settings *)
+Local Open Scope Z_scope.
+(** * General tactics *)
+Ltac unfold_lets_in_context :=
+  repeat match goal with
+         | H := _ |- _ => unfold H in *; clear H
+         end.
+Tactic Notation "reduce_closed" constr(x) :=
+  is_closed_term x;
+  let r := eval vm_compute in x in
+  change_no_check x with r in *
+.
+(** * General lemmas *)
+Lemma bv_extract_concat_later m n1 n2 s l (b1 : bv n1) (b2 : bv n2):
+  (n2 ≤ s)%N →
+  (m = n1 + n2)%N →
+  bv_extract s l (bv_concat m b1 b2) = bv_extract (s - n2) l b1.
+Proof.
+  intros ? ->. apply bv_eq.
+  rewrite !bv_extract_unsigned, bv_concat_unsigned, !bv_wrap_land by done.
+  apply Z.bits_inj_iff' => ??.
+  rewrite !Z.land_spec, !Z.shiftr_spec, Z.lor_spec, Z.shiftl_spec, Z.ones_spec; [|lia..].
+  case_bool_decide; rewrite ?andb_false_r, ?andb_true_r; [|done].
+  rewrite <-(bv_wrap_bv_unsigned _ b2), bv_wrap_spec_high, ?orb_false_r; [|lia].
+  f_equal. lia.
+Qed.
+Lemma bv_extract_concat_here m n1 n2 s (b1 : bv n1) (b2 : bv n2):
+  s = 0%N →
+  (m = n1 + n2)%N →
+  bv_extract s n2 (bv_concat m b1 b2) = b2.
+Proof.
+  intros -> ->. apply bv_eq.
+  rewrite !bv_extract_unsigned, bv_concat_unsigned, !bv_wrap_land by done.
+  apply Z.bits_inj_iff' => ??.
+  rewrite !Z.land_spec, !Z.shiftr_spec, Z.lor_spec, Z.shiftl_spec, Z.ones_spec; [|lia..].
+  case_bool_decide; rewrite ?andb_false_r, ?andb_true_r.
+  - rewrite (Z.testbit_neg_r (bv_unsigned b1)); [|lia]. simpl. f_equal. lia.
+  - rewrite <-(bv_wrap_bv_unsigned _ b2), bv_wrap_spec_high, ?orb_false_l; lia.
+Qed.
+(** * [bv_simplify] rewrite database *)
+(** The [bv_simplify] database collects rewrite rules that rewrite
+bitvectors into other bitvectors. *)
+Create HintDb bv_simplify discriminated. (* Technically not necessary for rewrite db. *)
+Global Hint Rewrite @bv_concat_0 using done : bv_simplify.
+Global Hint Rewrite @bv_extract_concat_later
+  @bv_extract_concat_here using lia : bv_simplify.
+Global Hint Rewrite @bv_extract_bool_to_bv using lia : bv_simplify.
+Global Hint Rewrite @bv_not_bool_to_bv : bv_simplify.
+Global Hint Rewrite bool_decide_bool_to_bv_0 bool_decide_bool_to_bv_1 : bv_simplify.
+(** * [bv_unfold] *)
+Create HintDb bv_unfold_db discriminated.
+Global Hint Constants Opaque : bv_unfold_db.
+Global Hint Variables Opaque : bv_unfold_db.
+Global Hint Extern 1 (TCFastDone ?P) => (change P; fast_done) : bv_unfold_db.
+Global Hint Transparent BvWf andb Is_true Z.ltb Z.leb Z.compare Pos.compare
+  Pos.compare_cont bv_modulus Z.pow Z.pow_pos Pos.iter Z.mul Pos.mul Z.of_N
+  : bv_unfold_db.
+Notation bv_suwrap signed := (if signed then bv_swrap else bv_wrap).
+Class BvUnfold (n : N) (signed : bool) (wrapped : bool) (b : bv n) (z : Z) := {
+    bv_unfold_proof : ((if signed then bv_signed else bv_unsigned) b) =
+                        (if wrapped then bv_suwrap signed n z else z);
+}.
+Global Arguments bv_unfold_proof {_ _ _} _ _ {_}.
+Global Hint Mode BvUnfold + + + + - : bv_unfold_db.
+(** [BV_UNFOLD_BLOCK] is a marker that this occurrence of [bv_signed]
+or [bv_unsigned] has already been simplified. *)
+Definition BV_UNFOLD_BLOCK {A} (x : A) : A := x.
+Lemma bv_unfold_end s w n b :
+  BvUnfold n s w b ((if s then BV_UNFOLD_BLOCK bv_signed else BV_UNFOLD_BLOCK bv_unsigned) b).
+Proof.
+  constructor. unfold BV_UNFOLD_BLOCK.
+  destruct w, s; by rewrite ?bv_wrap_bv_unsigned, ?bv_swrap_bv_signed.
+Qed.
+Global Hint Resolve bv_unfold_end | 1000 : bv_unfold_db.
+Lemma bv_unfold_BV s w n z Hwf :
+  BvUnfold n s w (@BV _ z Hwf) (if w then z else if s then bv_swrap n z else z).
+Proof.
+  constructor. unfold bv_unsigned.
+  destruct w, s; simpl; try done; by rewrite bv_wrap_small by by apply bv_wf_in_range.
+Qed.
+Global Hint Resolve bv_unfold_BV | 10 : bv_unfold_db.
+Lemma bv_unfold_bv_0 s w n :
+  BvUnfold n s w (bv_0 n) 0.
+Proof. constructor. destruct w, s; rewrite ?bv_0_signed, ?bv_0_unsigned, ?bv_swrap_0; done. Qed.
+Global Hint Resolve bv_unfold_bv_0 | 10 : bv_unfold_db.
+Lemma bv_unfold_Z_to_bv s w n z :
+  BvUnfold n s w (Z_to_bv _ z) (if w then z else bv_suwrap s n z).
+Proof. constructor. destruct w, s; rewrite ?Z_to_bv_signed, ?Z_to_bv_unsigned; done. Qed.
+Global Hint Resolve bv_unfold_Z_to_bv | 10 : bv_unfold_db.
+Lemma bv_unfold_succ s w n b z :
+  BvUnfold n s true b z →
+  BvUnfold n s w (bv_succ b) (if w then Z.succ z else bv_suwrap s n (Z.succ z)).
+Proof.
+  intros [Hz]. constructor.
+  destruct w, s; rewrite ?bv_succ_signed, ?bv_succ_unsigned, ?Hz; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_succ | 10 : bv_unfold_db.
+Lemma bv_unfold_pred s w n b z :
+  BvUnfold n s true b z →
+  BvUnfold n s w (bv_pred b) (if w then Z.pred z else bv_suwrap s n (Z.pred z)).
+Proof.
+  intros [Hz]. constructor.
+  destruct w, s; rewrite ?bv_pred_signed, ?bv_pred_unsigned, ?Hz; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_pred | 10 : bv_unfold_db.
+Lemma bv_unfold_add s w n b1 b2 z1 z2 :
+  BvUnfold n s true b1 z1 →
+  BvUnfold n s true b2 z2 →
+  BvUnfold n s w (bv_add b1 b2) (if w then z1 + z2 else bv_suwrap s n (z1 + z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_add_signed, ?bv_add_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_add | 10 : bv_unfold_db.
+Lemma bv_unfold_sub s w n b1 b2 z1 z2 :
+  BvUnfold n s true b1 z1 →
+  BvUnfold n s true b2 z2 →
+  BvUnfold n s w (bv_sub b1 b2) (if w then z1 - z2 else bv_suwrap s n (z1 - z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_sub_signed, ?bv_sub_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_sub | 10 : bv_unfold_db.
+Lemma bv_unfold_opp s w n b z :
+  BvUnfold n s true b z →
+  BvUnfold n s w (bv_opp b) (if w then - z else bv_suwrap s n (- z)).
+Proof.
+  intros [Hz]. constructor.
+  destruct w, s; rewrite ?bv_opp_signed, ?bv_opp_unsigned, ?Hz; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_opp | 10 : bv_unfold_db.
+Lemma bv_unfold_mul s w n b1 b2 z1 z2 :
+  BvUnfold n s true b1 z1 →
+  BvUnfold n s true b2 z2 →
+  BvUnfold n s w (bv_mul b1 b2) (if w then z1 * z2 else bv_suwrap s n (z1 * z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_mul_signed, ?bv_mul_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_mul | 10 : bv_unfold_db.
+Lemma bv_unfold_divu s w n b1 b2 z1 z2 :
+  BvUnfold n false false b1 z1 →
+  BvUnfold n false false b2 z2 →
+  BvUnfold n s w (bv_divu b1 b2) (if w then z1 `div` z2 else if s then bv_swrap n (z1 `div` z2) else z1 `div` z2).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_divu_signed, ?bv_divu_unsigned, ?Hz1, ?Hz2; try bv_wrap_simplify_solve.
+  - pose proof (bv_unsigned_in_range _ (bv_divu b1 b2)) as Hr. rewrite bv_divu_unsigned in Hr. subst.
+    by rewrite bv_wrap_small.
+  - done.
+Qed.
+Global Hint Resolve bv_unfold_divu | 10 : bv_unfold_db.
+Lemma bv_unfold_modu s w n b1 b2 z1 z2 :
+  BvUnfold n false false b1 z1 →
+  BvUnfold n false false b2 z2 →
+  BvUnfold n s w (bv_modu b1 b2) (if w then z1 `mod` z2 else if s then bv_swrap n (z1 `mod` z2) else z1 `mod` z2).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_modu_signed, ?bv_modu_unsigned, ?Hz1, ?Hz2; try bv_wrap_simplify_solve.
+  - pose proof (bv_unsigned_in_range _ (bv_modu b1 b2)) as Hr. rewrite bv_modu_unsigned in Hr. subst.
+    by rewrite bv_wrap_small.
+  - done.
+Qed.
+Global Hint Resolve bv_unfold_modu | 10 : bv_unfold_db.
+Lemma bv_unfold_divs s w n b1 b2 z1 z2 :
+  BvUnfold n true false b1 z1 →
+  BvUnfold n true false b2 z2 →
+  BvUnfold n s w (bv_divs b1 b2) (if w then z1 `div` z2 else bv_suwrap s n (z1 `div` z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_divs_signed, ?bv_divs_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_divs | 10 : bv_unfold_db.
+Lemma bv_unfold_quots s w n b1 b2 z1 z2 :
+  BvUnfold n true false b1 z1 →
+  BvUnfold n true false b2 z2 →
+  BvUnfold n s w (bv_quots b1 b2) (if w then z1 `quot` z2 else bv_suwrap s n (z1 `quot` z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_quots_signed, ?bv_quots_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_quots | 10 : bv_unfold_db.
+Lemma bv_unfold_mods s w n b1 b2 z1 z2 :
+  BvUnfold n true false b1 z1 →
+  BvUnfold n true false b2 z2 →
+  BvUnfold n s w (bv_mods b1 b2) (if w then z1 `mod` z2 else bv_suwrap s n (z1 `mod` z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_mods_signed, ?bv_mods_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_mods | 10 : bv_unfold_db.
+Lemma bv_unfold_rems s w n b1 b2 z1 z2 :
+  BvUnfold n true false b1 z1 →
+  BvUnfold n true false b2 z2 →
+  BvUnfold n s w (bv_rems b1 b2) (if w then z1 `rem` z2 else bv_suwrap s n (z1 `rem` z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_rems_signed, ?bv_rems_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_rems | 10 : bv_unfold_db.
+Lemma bv_unfold_shiftl s w n b1 b2 z1 z2 :
+  BvUnfold n false false b1 z1 →
+  BvUnfold n false false b2 z2 →
+  BvUnfold n s w (bv_shiftl b1 b2) (if w then z1 ≪ z2 else bv_suwrap s n (z1 ≪ z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_shiftl_signed, ?bv_shiftl_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_shiftl | 10 : bv_unfold_db.
+Lemma bv_unfold_shiftr s w n b1 b2 z1 z2 :
+  BvUnfold n false false b1 z1 →
+  BvUnfold n false false b2 z2 →
+  BvUnfold n s w (bv_shiftr b1 b2) (if w then z1 ≫ z2 else if s then bv_swrap n (z1 ≫ z2) else (z1 ≫ z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_shiftr_signed, ?bv_shiftr_unsigned, ?Hz1, ?Hz2; try bv_wrap_simplify_solve.
+  - pose proof (bv_unsigned_in_range _ (bv_shiftr b1 b2)) as Hr. rewrite bv_shiftr_unsigned in Hr. subst.
+    by rewrite bv_wrap_small.
+  - done.
+Qed.
+Global Hint Resolve bv_unfold_shiftr | 10 : bv_unfold_db.
+Lemma bv_unfold_ashiftr s w n b1 b2 z1 z2 :
+  BvUnfold n true false b1 z1 →
+  BvUnfold n false false b2 z2 →
+  BvUnfold n s w (bv_ashiftr b1 b2) (if w then z1 ≫ z2 else bv_suwrap s n (z1 ≫ z2)).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_ashiftr_signed, ?bv_ashiftr_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_ashiftr | 10 : bv_unfold_db.
+Lemma bv_unfold_or s w n b1 b2 z1 z2 :
+  BvUnfold n false false b1 z1 →
+  BvUnfold n false false b2 z2 →
+  BvUnfold n s w (bv_or b1 b2) (if w then Z.lor z1 z2 else if s then bv_swrap n (Z.lor z1 z2) else Z.lor z1 z2).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_or_signed, ?bv_or_unsigned, ?Hz1, ?Hz2; try bv_wrap_simplify_solve.
+  - pose proof (bv_unsigned_in_range _ (bv_or b1 b2)) as Hr. rewrite bv_or_unsigned in Hr. subst.
+    by rewrite bv_wrap_small.
+  - done.
+Qed.
+Global Hint Resolve bv_unfold_or | 10 : bv_unfold_db.
+Lemma bv_unfold_and s w n b1 b2 z1 z2 :
+  BvUnfold n false false b1 z1 →
+  BvUnfold n false false b2 z2 →
+  BvUnfold n s w (bv_and b1 b2) (if w then Z.land z1 z2 else if s then bv_swrap n (Z.land z1 z2) else Z.land z1 z2).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_and_signed, ?bv_and_unsigned, ?Hz1, ?Hz2; try bv_wrap_simplify_solve.
+  - pose proof (bv_unsigned_in_range _ (bv_and b1 b2)) as Hr. rewrite bv_and_unsigned in Hr. subst.
+    by rewrite bv_wrap_small.
+  - done.
+Qed.
+Global Hint Resolve bv_unfold_and | 10 : bv_unfold_db.
+Lemma bv_unfold_xor s w n b1 b2 z1 z2 :
+  BvUnfold n false false b1 z1 →
+  BvUnfold n false false b2 z2 →
+  BvUnfold n s w (bv_xor b1 b2) (if w then Z.lxor z1 z2 else if s then bv_swrap n (Z.lxor z1 z2) else Z.lxor z1 z2).
+Proof.
+  intros [Hz1] [Hz2]. constructor.
+  destruct w, s; rewrite ?bv_xor_signed, ?bv_xor_unsigned, ?Hz1, ?Hz2; try bv_wrap_simplify_solve.
+  - pose proof (bv_unsigned_in_range _ (bv_xor b1 b2)) as Hr. rewrite bv_xor_unsigned in Hr. subst.
+    by rewrite bv_wrap_small.
+  - done.
+Qed.
+Global Hint Resolve bv_unfold_xor | 10 : bv_unfold_db.
+Lemma bv_unfold_not s w n b z :
+  BvUnfold n false false b z →
+  BvUnfold n s w (bv_not b) (if w then Z.lnot z else bv_suwrap s n (Z.lnot z)).
+Proof.
+  intros [Hz]. constructor.
+  destruct w, s; rewrite ?bv_not_signed, ?bv_not_unsigned, ?Hz; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_not | 10 : bv_unfold_db.
+Lemma bv_unfold_zero_extend s w n n' b z `{!TCFastDone (n' <=? n = true)%N} :
+  BvUnfold n' false false b z →
+  BvUnfold n s w (bv_zero_extend n b) (if w then z else if s then bv_swrap n z else z).
+Proof.
+  intros [Hz]. constructor. unfold TCFastDone in *. rewrite ->?N.leb_le in *.
+  destruct w, s; rewrite ?bv_zero_extend_signed, ?bv_zero_extend_unsigned, ?Hz by done;
+    try bv_wrap_simplify_solve.
+  - rewrite <-Hz, bv_wrap_small; [done|]. bv_saturate. pose proof (bv_modulus_le_mono n' n). lia.
+  - done.
+Qed.
+Global Hint Resolve bv_unfold_zero_extend | 10 : bv_unfold_db.
+Lemma bv_unfold_sign_extend s w n n' b z `{!TCFastDone (n' <=? n = true)%N} :
+  BvUnfold n' true false b z →
+  BvUnfold n s w (bv_sign_extend n b) (if w then z else if s then z else bv_wrap n z).
+Proof.
+  intros [Hz]. constructor. unfold TCFastDone in *. rewrite ->?N.leb_le in *.
+  destruct w, s; rewrite ?bv_sign_extend_signed, ?bv_sign_extend_unsigned, ?Hz by done;
+    try bv_wrap_simplify_solve.
+  - subst. rewrite <-(bv_sign_extend_signed n) at 2 by done. by rewrite bv_swrap_bv_signed, bv_sign_extend_signed.
+  - done.
+Qed.
+Global Hint Resolve bv_unfold_sign_extend | 10 : bv_unfold_db.
+Lemma bv_unfold_extract s w n n' n1 b z :
+  BvUnfold n' false false b z →
+  BvUnfold n s w (bv_extract n1 n b) (if w then z ≫ Z.of_N n1 else bv_suwrap s n (z ≫ Z.of_N n1)).
+Proof.
+  intros [Hz]. constructor.
+  destruct w, s; rewrite ?bv_extract_signed, ?bv_extract_unsigned, ?Hz; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_extract | 10 : bv_unfold_db.
+Lemma bv_unfold_concat s w n n1 n2 b1 b2 z1 z2 `{!TCFastDone (n = n1 + n2)%N} :
+  BvUnfold n1 false false b1 z1 →
+  BvUnfold n2 false false b2 z2 →
+  BvUnfold n s w (bv_concat n b1 b2) (if w then Z.lor (z1 ≪ Z.of_N n2) z2 else if s then  bv_swrap n (Z.lor (z1 ≪ Z.of_N n2) z2) else Z.lor (z1 ≪ Z.of_N n2) z2).
+Proof.
+  intros [Hz1] [Hz2]. constructor. unfold TCFastDone in *.
+  destruct w, s; rewrite ?bv_concat_signed, ?bv_concat_unsigned, ?Hz1, ?Hz2 by done;
+    try bv_wrap_simplify_solve.
+  - subst. rewrite <-(bv_concat_unsigned (n1 + n2)) at 2 by done.
+    by rewrite bv_wrap_bv_unsigned, bv_concat_unsigned.
+  - done.
+Qed.
+Global Hint Resolve bv_unfold_concat | 10 : bv_unfold_db.
+Lemma bv_unfold_add_Z s w n b1 z1 z2 :
+  BvUnfold n s true b1 z1 →
+  BvUnfold n s w (bv_add_Z b1 z2) (if w then z1 + z2 else bv_suwrap s n (z1 + z2)).
+Proof.
+  intros [Hz1]. constructor.
+  destruct w, s; rewrite ?bv_add_Z_signed, ?bv_add_Z_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_add_Z | 10 : bv_unfold_db.
+Lemma bv_unfold_sub_Z s w n b1 z1 z2 :
+  BvUnfold n s true b1 z1 →
+  BvUnfold n s w (bv_sub_Z b1 z2) (if w then z1 - z2 else bv_suwrap s n (z1 - z2)).
+Proof.
+  intros [Hz1]. constructor.
+  destruct w, s; rewrite ?bv_sub_Z_signed, ?bv_sub_Z_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_sub_Z | 10 : bv_unfold_db.
+Lemma bv_unfold_mul_Z s w n b1 z1 z2 :
+  BvUnfold n s true b1 z1 →
+  BvUnfold n s w (bv_mul_Z b1 z2) (if w then z1 * z2 else bv_suwrap s n (z1 * z2)).
+Proof.
+  intros [Hz1]. constructor.
+  destruct w, s; rewrite ?bv_mul_Z_signed, ?bv_mul_Z_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
+Qed.
+Global Hint Resolve bv_unfold_mul_Z | 10 : bv_unfold_db.
+Ltac bv_unfold_eq :=
+  lazymatch goal with
+  | |- @bv_unsigned ?n ?b = ?z =>
+      simple notypeclasses refine (@bv_unfold_proof n false false b z _)
+  | |- @bv_signed ?n ?b = ?z =>
+      simple notypeclasses refine (@bv_unfold_proof n true false b z _)
+  end;
+  typeclasses eauto with bv_unfold_db.
+Ltac bv_unfold :=
+  repeat (match goal with
+            (* TODO: Detect if there is a bv_wrap around the
+            bv_unsigned (like after applying bv_eq_wrapped) *)
+          | |- context [@bv_unsigned ?n ?b] =>
+              pattern (@bv_unsigned n b);
+              simple refine (eq_rec_r _ _ _); [shelve| |bv_unfold_eq]; cbn beta
+          | |- context [@bv_signed ?n ?b] =>
+              pattern (@bv_signed n b);
+              simple refine (eq_rec_r _ _ _); [shelve| |bv_unfold_eq]; cbn beta
+          end); unfold BV_UNFOLD_BLOCK.
+(** * [bv_unfolded_simplify] rewrite database *)
+(** The [bv_unfolded_simplify] database collects rewrite rules that
+should be used to simplify the goal after Z is bv_unfolded. *)
+Create HintDb bv_unfolded_simplify discriminated. (* Technically not necessary for rewrite db. *)
+Global Hint Rewrite Z.shiftr_0_r Z.lor_0_r Z.lor_0_l : bv_unfolded_simplify.
+Global Hint Rewrite Z.land_ones using lia : bv_unfolded_simplify.
+Global Hint Rewrite bv_wrap_bv_wrap using lia : bv_unfolded_simplify.
+Global Hint Rewrite
+  Z_to_bv_small using unfold bv_modulus; lia : bv_unfolded_simplify.
+(** * [bv_unfolded_to_arith] rewrite database *)
+(** The [bv_unfolded_to_arith] database collects rewrite rules that
+convert bitwise operations to arithmetic operations in preparation for lia. *)
+Create HintDb bv_unfolded_to_arith discriminated. (* Technically not necessary for rewrite db. *)
+Global Hint Rewrite <-Z.opp_lnot : bv_unfolded_to_arith.
+Global Hint Rewrite Z.shiftl_mul_pow2 Z.shiftr_div_pow2 using lia : bv_unfolded_to_arith.
+(** * Reduction of closed terms *)
+Ltac reduce_closed_N_tac := idtac.
+Ltac reduce_closed_N :=
+  idtac;
+  reduce_closed_N_tac;
+  repeat match goal with
+  | |- context [N.add ?a ?b] => progress reduce_closed (N.add a b)
+  | H : context [N.add ?a ?b] |- _ => progress reduce_closed (N.add a b)
+  end.
+Ltac reduce_closed_bv_simplify_tac := idtac.
+Ltac reduce_closed_bv_simplify :=
+  idtac;
+  reduce_closed_bv_simplify_tac;
+  (* reduce closed logical operators that lia does not understand *)
+  repeat match goal with
+  | |- context [Z.lor ?a ?b] => progress reduce_closed (Z.lor a b)
+  | H : context [Z.lor ?a ?b] |- _ => progress reduce_closed (Z.lor a b)
+  | |- context [Z.land ?a ?b] => progress reduce_closed (Z.land a b)
+  | H : context [Z.land ?a ?b] |- _ => progress reduce_closed (Z.land a b)
+  | |- context [Z.lxor ?a ?b] => progress reduce_closed (Z.lxor a b)
+  | H : context [Z.lxor ?a ?b] |- _ => progress reduce_closed (Z.lxor a b)
+  end.
+(** * [bv_simplify] tactic *)
+Tactic Notation "bv_simplify" :=
+  unfold_lets_in_context;
+  (* We need to reduce operations on N in indices of bv because
+  otherwise lia can get confused (it does not perform unification when
+  finding identical subterms). This sometimes leads to problems
+  with length of lists of bytes. *)
+  reduce_closed_N;
+  autorewrite with bv_simplify;
+  lazymatch goal with
+  | |- _ =@{bv _} _ => apply bv_eq_wrap
+  | |- not (_ =@{bv _} _) => apply bv_neq_wrap
+  | _ => idtac
+  end;
+  bv_unfold;
+  autorewrite with bv_unfolded_simplify.
+Tactic Notation "bv_simplify" ident(H) :=
+  unfold_lets_in_context;
+  autorewrite with bv_simplify in H;
+  lazymatch (type of H) with
+  | _ =@{bv _} _ => apply bv_eq in H
+  | not (_ =@{bv _} _) => apply bv_neq in H
+  | _ => idtac
+  end;
+  do [bv_unfold] in H;
+  autorewrite with bv_unfolded_simplify in H.
+Tactic Notation "bv_simplify" "select" open_constr(pat) :=
+  select pat (fun H => bv_simplify H).
+Tactic Notation "bv_simplify_arith" :=
+  bv_simplify;
+  autorewrite with bv_unfolded_to_arith;
+  reduce_closed_bv_simplify.
+Tactic Notation "bv_simplify_arith" ident(H) :=
+  bv_simplify H;
+  autorewrite with bv_unfolded_to_arith in H;
+  reduce_closed_bv_simplify.
+Tactic Notation "bv_simplify_arith" "select" open_constr(pat) :=
+  select pat (fun H => bv_simplify_arith H).
+(** * [bv_solve] tactic *)
+Ltac bv_solve_unfold_tac := idtac.
+Ltac bv_solve :=
+  bv_simplify_arith;
+  (* we unfold signed so we just need to saturate unsigned *)
+  bv_saturate_unsigned;
+  bv_solve_unfold_tac;
+  unfold bv_signed, bv_swrap, bv_wrap, bv_half_modulus, bv_modulus, bv_unsigned in *;
+  simpl;
+  lia.
+Class BvSolve (P : Prop) : Prop := bv_solve_proof : P.
+Global Hint Extern 1 (BvSolve ?P) => (change P; bv_solve) : typeclass_instances.
--- a/stdpp_unstable/bitblast.v
+++ b/stdpp_unstable/bitblast.v
+(* This file is still experimental. See its tracking issue
+https://gitlab.mpi-sws.org/iris/stdpp/-/issues/141 for details on remaining
+issues before stabilization. This file is maintained by Michael Sammler. *)
+From Coq Require Import ssreflect.
+From Coq.btauto Require Export Btauto.
+From stdpp.bitvector Require Import definitions.
+From stdpp Require Export tactics numbers list.
+From stdpp Require Import options.
+(** * [bitblast] tactic: Solve integer goals by bitwise reasoning *)
+(** This file provides the [bitblast] tactic for bitwise reasoning
+about [Z] via [Z.testbit]. Concretely, [bitblast] first turns an
+equality [a = b] into [∀ n, Z.testbit a n = Z.testbit b n], then
+simplifies the [Z.testbit] expressions using lemmas like
+[Z.testbit (Z.land a b) n = Z.testbit a n && Z.testbit b n], or
+[Z.testbit (Z.ones z) n = bool_decide (0 ≤ n < z) || bool_decide (z < 0 ∧ 0 ≤ n)]
+and finally simplifies the resulting boolean expression by performing case
+distinction on all [bool_decide] in the goal and pruning impossible cases.
+This library provides the following variants of the [bitblast] tactic:
+- [bitblast]: applies the bitblasting technique described above to the goal.
+  If the goal already contains a [Z.testbit], the first step (which introduces
+  [Z.testbit] to prove equalities between [Z]) is skipped.
+- [bitblast as n] behaves the same as [bitblast], but it allows naming the [n]
+  introduced in the first step. Fails if the goal is not an equality between [Z].
+- [bitblast H] applies the simplification of [Z.testbit] in the hypothesis [H]
+  (but does not perform case distinction).
+- [bitblast H with n as H'] deduces from the equality [H] of the form [z1 = z2]
+  that the [n]-th bit of [z1] and [z2] are equal, simplifies the resulting
+  equation, and adds it as the hypothesis [H'].
+- [bitblast H with n] is the same as [bitblast H with n as H'], but using a fresh
+  name for [H'].
+See also https://github.com/mit-plv/coqutil/blob/master/src/coqutil/Z/bitblast.v
+for another implementation of the same idea.
+*)
+(** * Settings *)
+Local Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
+Local Open Scope Z_scope.
+(** * Helper lemmas to upstream *)
+Lemma Nat_eqb_eq n1 n2 :
+  (n1 =? n2)%nat = bool_decide (n1 = n2).
+Proof. case_bool_decide; [by apply Nat.eqb_eq | by apply Nat.eqb_neq]. Qed.
+Lemma Z_eqb_eq n1 n2 :
+  (n1 =? n2)%Z = bool_decide (n1 = n2).
+Proof. case_bool_decide; [by apply Z.eqb_eq | by apply Z.eqb_neq]. Qed.
+Lemma Z_testbit_pos_testbit p n :
+  (0 ≤ n)%Z →
+  Z.testbit (Z.pos p) n = Pos.testbit p (Z.to_N n).
+Proof. by destruct n, p. Qed.
+Lemma negb_forallb {A} (ls : list A) f :
+   negb (forallb f ls) = existsb (negb ∘ f) ls.
+Proof. induction ls; [done|]; simpl. rewrite negb_andb. congruence. Qed.
+Lemma Z_bits_inj'' a b :
+  a = b → (∀ n : Z, 0 ≤ n → Z.testbit a n = Z.testbit b n).
+Proof. apply Z.bits_inj_iff'. Qed.
+Lemma tac_tactic_in_hyp (P1 P2 : Prop) :
+  P1 → (P1 → P2) → P2.
+Proof. eauto. Qed.
+(** TODO: replace this with [do [ tac ] in H] from ssreflect? *)
+Tactic Notation "tactic" tactic3(tac) "in" ident(H) :=
+  let H' := fresh in
+  unshelve epose proof (tac_tactic_in_hyp _ _ H _) as H'; [shelve|
+    tac; let H := fresh H in intros H; exact H |];
+  clear H; rename H' into H.
+(** ** bitranges *)
+Fixpoint pos_to_bit_ranges_aux (p : positive) : (nat * nat) * list (nat * nat) :=
+  match p with
+  | xH => ((0, 1)%nat, [])
+  | xO p' =>
+      let x := pos_to_bit_ranges_aux p' in
+      ((S x.1.1, x.1.2), prod_map S id <$> x.2)
+  | xI p' =>
+      let x := pos_to_bit_ranges_aux p' in
+      if (x.1.1 =? 0)%nat then
+        ((0%nat, S x.1.2), prod_map S id <$> x.2)
+      else
+        ((0%nat, 1%nat), prod_map S id <$> (x.1 :: x.2))
+  end.
+(** [pos_to_bit_ranges p] computes the list of (start, length) pairs
+describing which bits of [p] are [1]. The following examples show the
+behavior of [pos_to_bit_ranges]: *)
+(* Compute (pos_to_bit_ranges 1%positive). (** 0b  1  [(0, 1)] *) *)
+(* Compute (pos_to_bit_ranges 2%positive). (** 0b 10  [(1, 1)] *) *)
+(* Compute (pos_to_bit_ranges 3%positive). (** 0b 11  [(0, 2)] *) *)
+(* Compute (pos_to_bit_ranges 4%positive). (** 0b100  [(2, 1)] *) *)
+(* Compute (pos_to_bit_ranges 5%positive). (** 0b101  [(0, 1); (2, 1)] *) *)
+(* Compute (pos_to_bit_ranges 6%positive). (** 0b110  [(1, 2)] *) *)
+(* Compute (pos_to_bit_ranges 7%positive). (** 0b111  [(0, 3)] *) *)
+(* Compute (pos_to_bit_ranges 21%positive). (** 0b10101  [(0, 1); (2, 1); (4, 1)] *) *)
+Definition pos_to_bit_ranges (p : positive) : list (nat * nat) :=
+  let x := pos_to_bit_ranges_aux p in x.1::x.2.
+Lemma pos_to_bit_ranges_spec p rs :
+  pos_to_bit_ranges p = rs →
+  (∀ n, Pos.testbit p n ↔ ∃ r, r ∈ rs ∧ (N.of_nat r.1 ≤ n ∧ n < N.of_nat r.1 + N.of_nat r.2)%N).
+Proof.
+  unfold pos_to_bit_ranges => <-.
+  elim: p => //; csimpl.
+  - move => p IH n. rewrite Nat_eqb_eq. case_match; subst.
+    + split; [|done] => _. case_match.
+      all: eexists _; split; [by apply elem_of_list_here|] => /=; lia.
+    + rewrite {}IH. split; move => [r[/elem_of_cons[Heq|Hin] ?]]; simplify_eq/=.
+      * (* r = (pos_to_bit_ranges_aux p).1 *)
+        case_bool_decide as Heq; simplify_eq/=.
+        -- eexists _. split; [by apply elem_of_list_here|] => /=. lia.
+        -- eexists _. split. { apply elem_of_list_further. apply elem_of_list_here. }
+          simplify_eq/=. lia.
+      * (* r ∈ (pos_to_bit_ranges_aux p).2 *)
+        case_bool_decide as Heq; simplify_eq/=.
+        -- eexists _. split. { apply elem_of_list_further. apply elem_of_list_fmap. by eexists _. }
+           simplify_eq/=. lia.
+        -- eexists _. split. { do 2 apply elem_of_list_further. apply elem_of_list_fmap. by eexists _. }
+           simplify_eq/=. lia.
+      * eexists _. split; [by apply elem_of_list_here|]. case_bool_decide as Heq; simplify_eq/=; lia.
+      * case_bool_decide as Heq; simplify_eq/=.
+        -- move: Hin => /= /elem_of_list_fmap[?[??]]; subst. eexists _. split; [by apply elem_of_list_further |].
+           simplify_eq/=. lia.
+        -- rewrite -fmap_cons in Hin. move: Hin => /elem_of_list_fmap[?[??]]; subst. naive_solver lia.
+  - move => p IH n. case_match; subst.
+    + split; [done|] => -[[l h][/elem_of_cons[?|/(elem_of_list_fmap_2 _ _ _)[[??][??]]]?]]; simplify_eq/=; lia.
+    + rewrite IH. split; move => [r[/elem_of_cons[Heq|Hin] ?]]; simplify_eq/=.
+      * eexists _. split; [by apply elem_of_list_here|] => /=; lia.
+      * eexists _. split. { apply elem_of_list_further. apply elem_of_list_fmap. by eexists _. }
+        destruct r; simplify_eq/=. lia.
+      * eexists _. split; [by apply elem_of_list_here|] => /=; lia.
+      * move: Hin => /elem_of_list_fmap[r'[??]]; subst. eexists _. split; [by apply elem_of_list_further|].
+         destruct r'; simplify_eq/=. lia.
+  - move => n. setoid_rewrite elem_of_list_singleton. case_match; split => //; subst; naive_solver lia.
+Qed.
+Definition Z_to_bit_ranges (z : Z) : list (nat * nat) :=
+  match z with
+  | Z0 => []
+  | Z.pos p => pos_to_bit_ranges p
+  | Z.neg p => []
+  end.
+Lemma Z_to_bit_ranges_spec z n rs :
+  (0 ≤ n)%Z →
+  (0 ≤ z)%Z →
+  Z_to_bit_ranges z = rs →
+  Z.testbit z n ↔ Exists (λ r, Z.of_nat r.1 ≤ n ∧ n < Z.of_nat r.1 + Z.of_nat r.2) rs.
+Proof.
+  move => /= ??.
+  destruct z => //=.
+  + move => <-. rewrite Z.bits_0 Exists_nil. done.
+  + move => /pos_to_bit_ranges_spec Hbit. rewrite Z_testbit_pos_testbit // Hbit Exists_exists. naive_solver lia.
+Qed.
+(** * [simpl_bool] *)
+Ltac simpl_bool_cbn := cbn [andb orb negb].
+Ltac simpl_bool :=
+  repeat match goal with
+         | |- context C [true && ?b] => simpl_bool_cbn
+         | |- context C [false && ?b] => simpl_bool_cbn
+         | |- context C [true || ?b] => simpl_bool_cbn
+         | |- context C [false || ?b] => simpl_bool_cbn
+         | |- context C [negb true] => simpl_bool_cbn
+         | |- context C [negb false] => simpl_bool_cbn
+         | |- context C [?b && true] => rewrite (Bool.andb_true_r b)
+         | |- context C [?b && false] => rewrite (Bool.andb_false_r b)
+         | |- context C [?b || true] => rewrite (Bool.orb_true_r b)
+         | |- context C [?b || false] => rewrite (Bool.orb_false_r b)
+         | |- context C [xorb ?b true] => rewrite (Bool.xorb_true_r b)
+         | |- context C [xorb ?b false] => rewrite (Bool.xorb_false_r b)
+         | |- context C [xorb true ?b] => rewrite (Bool.orb_true_l b)
+         | |- context C [xorb false ?b] => rewrite (Bool.orb_false_l b)
+         end.
+(** * [simplify_bitblast_index] *)
+Create HintDb simplify_bitblast_index_db discriminated.
+Global Hint Rewrite
+  Z.sub_add
+  Z.add_simpl_r
+  : simplify_bitblast_index_db.
+Local Ltac simplify_bitblast_index := autorewrite with simplify_bitblast_index_db.
+(** * Main typeclasses for bitblast *)
+Create HintDb bitblast discriminated.
+Global Hint Constants Opaque : bitblast.
+Global Hint Variables Opaque : bitblast.
+(** ** [IsPowerOfTwo] *)
+Class IsPowerOfTwo (z n : Z) := {
+  is_power_of_two_proof : z = 2 ^ n;
+}.
+Global Arguments is_power_of_two_proof _ _ {_}.
+Global Hint Mode IsPowerOfTwo + - : bitblast.
+Lemma is_power_of_two_pow2 n :
+  IsPowerOfTwo (2 ^ n) n.
+Proof. constructor. done. Qed.
+Global Hint Resolve is_power_of_two_pow2 | 10 : bitblast.
+Lemma is_power_of_two_const n p :
+  (∀ x, [(n, 1%nat)] = x → prod_map Z.of_nat id <$> Z_to_bit_ranges (Z.pos p) = x) →
+  IsPowerOfTwo (Z.pos p) n.
+Proof.
+  move => Hn. constructor. have {}Hn := Hn _ ltac:(done).
+  apply Z.bits_inj_iff' => i ?.
+  apply eq_bool_prop_intro. rewrite Z_to_bit_ranges_spec; [|done|lia|done].
+  move: Hn => /(fmap_cons_inv _ _ _)[[n' ?][?/=[[??][/(@eq_sym _ _ _)/fmap_nil_inv->->]]]]. subst.
+  rewrite Exists_cons Exists_nil /=.
+  rewrite Z.pow2_bits_eqb ?Z_eqb_eq ?bool_decide_spec; lia.
+Qed.
+Global Hint Extern 10 (IsPowerOfTwo (Z.pos ?p) _) =>
+  lazymatch isPcst p with | true => idtac end;
+  simple notypeclasses refine (is_power_of_two_const _ _ _);
+   let H := fresh in intros ? H; vm_compute; apply H
+  : bitblast.
+(** ** [BitblastBounded] *)
+Class BitblastBounded (z n : Z) := {
+  bitblast_bounded_proof : 0 ≤ z < 2 ^ n;
+}.
+Global Arguments bitblast_bounded_proof _ _ {_}.
+Global Hint Mode BitblastBounded + - : bitblast.
+Global Hint Extern 10 (BitblastBounded _ _) =>
+  constructor; first [ split; [lia|done] | done]
+  : bitblast.
+(** ** [Bitblast] *)
+Class Bitblast (z n : Z) (b : bool) := {
+  bitblast_proof : Z.testbit z n = b;
+}.
+Global Arguments bitblast_proof _ _ _ {_}.
+Global Hint Mode Bitblast + + - : bitblast.
+Definition BITBLAST_TESTBIT := Z.testbit.
+Lemma bitblast_id z n :
+  Bitblast z n (bool_decide (0 ≤ n) && BITBLAST_TESTBIT z n).
+Proof. constructor. case_bool_decide => //=. rewrite Z.testbit_neg_r //; lia. Qed.
+Global Hint Resolve bitblast_id | 1000 : bitblast.
+Lemma bitblast_id_bounded z z' n :
+  BitblastBounded z z' →
+  Bitblast z n (bool_decide (0 ≤ n < z') && BITBLAST_TESTBIT z n).
+Proof.
+  move => [Hb]. constructor.
+  move: (Hb) => /Z.bounded_iff_bits_nonneg' Hn.
+  case_bool_decide => //=.
+  destruct (decide (0 ≤ n)); [|rewrite Z.testbit_neg_r //; lia].
+  apply Hn; try lia.
+  destruct (decide (0 ≤ z')) => //.
+  rewrite Z.pow_neg_r in Hb; lia.
+Qed.
+Global Hint Resolve bitblast_id_bounded | 990 : bitblast.
+Lemma bitblast_0 n :
+  Bitblast 0 n false.
+Proof. constructor. by rewrite Z.bits_0. Qed.
+Global Hint Resolve bitblast_0 | 10 : bitblast.
+Lemma bitblast_pos p n rs b :
+  (∀ x, rs = x → (λ p, (Z.of_nat p.1, Z.of_nat p.1 + Z.of_nat p.2)) <$> Z_to_bit_ranges (Z.pos p) = x) →
+  existsb (λ '(r1, r2), bool_decide (r1 ≤ n ∧ n < r2)) rs = b →
+  Bitblast (Z.pos p) n b.
+Proof.
+  move => Hr <-. constructor. rewrite -(Hr rs) //.
+  destruct (decide (0 ≤ n)). 2: {
+    rewrite Z.testbit_neg_r; [|lia]. elim: (Z_to_bit_ranges (Z.pos p)) => // [??]; csimpl => <-.
+    case_bool_decide => //; lia.
+  }
+  apply eq_bool_prop_intro. rewrite Z_to_bit_ranges_spec; [|done..]. rewrite existb_True Exists_fmap.
+  f_equiv => -[??] /=. by rewrite bool_decide_spec.
+Qed.
+Global Hint Extern 10 (Bitblast (Z.pos ?p) _ _) =>
+  lazymatch isPcst p with | true => idtac end;
+  simple notypeclasses refine (bitblast_pos _ _ _ _ _ _);[shelve|
+   let H := fresh in intros ? H; vm_compute; apply H |
+   cbv [existsb]; exact eq_refl]
+  : bitblast.
+Lemma bitblast_neg p n rs b :
+  (∀ x, rs = x → (λ p, (Z.of_nat p.1, Z.of_nat p.1 + Z.of_nat p.2)) <$> Z_to_bit_ranges (Z.pred (Z.pos p)) = x) →
+  forallb (λ '(r1, r2), bool_decide (n < r1 ∨ r2 ≤ n)) rs = b →
+  Bitblast (Z.neg p) n (bool_decide (0 ≤ n) && b).
+Proof.
+  move => Hr <-. constructor. rewrite -(Hr rs) //.
+  case_bool_decide => /=; [|rewrite Z.testbit_neg_r; [done|lia]].
+  have -> : Z.neg p = Z.lnot (Z.pred (Z.pos p)).
+  { rewrite -Pos2Z.opp_pos. have := Z.add_lnot_diag (Z.pred (Z.pos p)). lia. }
+  rewrite Z.lnot_spec //. symmetry. apply negb_sym.
+  apply eq_bool_prop_intro. rewrite Z_to_bit_ranges_spec; [|done|lia|done].
+  rewrite negb_forallb existb_True Exists_fmap.
+  f_equiv => -[??] /=. rewrite negb_True bool_decide_spec. lia.
+Qed.
+Global Hint Extern 10 (Bitblast (Z.neg ?p) _ _) =>
+  lazymatch isPcst p with | true => idtac end;
+  simple notypeclasses refine (bitblast_neg _ _ _ _ _ _);[shelve|shelve|
+   let H := fresh in intros ? H; vm_compute; apply H |
+   cbv [forallb]; exact eq_refl]
+    : bitblast.
+Lemma bitblast_land z1 z2 n b1 b2 :
+  Bitblast z1 n b1 →
+  Bitblast z2 n b2 →
+  Bitblast (Z.land z1 z2) n (b1 && b2).
+Proof. move => [<-] [<-]. constructor. by rewrite Z.land_spec. Qed.
+Global Hint Resolve bitblast_land | 10 : bitblast.
+Lemma bitblast_lor z1 z2 n b1 b2 :
+  Bitblast z1 n b1 →
+  Bitblast z2 n b2 →
+  Bitblast (Z.lor z1 z2) n (b1 || b2).
+Proof. move => [<-] [<-]. constructor. by rewrite Z.lor_spec. Qed.
+Global Hint Resolve bitblast_lor | 10 : bitblast.
+Lemma bitblast_lxor z1 z2 n b1 b2 :
+  Bitblast z1 n b1 →
+  Bitblast z2 n b2 →
+  Bitblast (Z.lxor z1 z2) n (xorb b1 b2).
+Proof. move => [<-] [<-]. constructor. by rewrite Z.lxor_spec. Qed.
+Global Hint Resolve bitblast_lxor | 10 : bitblast.
+Lemma bitblast_shiftr z1 z2 n b1 :
+  Bitblast z1 (n + z2) b1 →
+  Bitblast (z1 ≫ z2) n (bool_decide (0 ≤ n) && b1).
+Proof.
+  move => [<-]. constructor.
+  case_bool_decide => /=; [by rewrite Z.shiftr_spec| rewrite Z.testbit_neg_r //; lia].
+Qed.
+Global Hint Resolve bitblast_shiftr | 10 : bitblast.
+Lemma bitblast_shiftl z1 z2 n b1 :
+  Bitblast z1 (n - z2) b1 →
+  Bitblast (z1 ≪ z2) n (bool_decide (0 ≤ n) && b1).
+Proof.
+  move => [<-]. constructor.
+  case_bool_decide => /=; [by rewrite Z.shiftl_spec| rewrite Z.testbit_neg_r //; lia].
+Qed.
+Global Hint Resolve bitblast_shiftl | 10 : bitblast.
+Lemma bitblast_lnot z1 n b1 :
+  Bitblast z1 n b1 →
+  Bitblast (Z.lnot z1) n (bool_decide (0 ≤ n) && negb b1).
+Proof.
+  move => [<-]. constructor.
+  case_bool_decide => /=; [by rewrite Z.lnot_spec| rewrite Z.testbit_neg_r //; lia].
+Qed.
+Global Hint Resolve bitblast_lnot | 10 : bitblast.
+Lemma bitblast_ldiff z1 z2 n b1 b2 :
+  Bitblast z1 n b1 →
+  Bitblast z2 n b2 →
+  Bitblast (Z.ldiff z1 z2) n (b1 && negb b2).
+Proof. move => [<-] [<-]. constructor. by rewrite Z.ldiff_spec. Qed.
+Global Hint Resolve bitblast_ldiff | 10 : bitblast.
+Lemma bitblast_ones z1 n :
+  Bitblast (Z.ones z1) n (bool_decide (0 ≤ n < z1) || bool_decide (z1 < 0 ∧ 0 ≤ n)).
+Proof.
+  constructor. case_bool_decide; [by apply Z.ones_spec_low|] => /=.
+  case_bool_decide.
+  - rewrite Z.ones_equiv Z.pow_neg_r; [|lia]. apply Z.bits_m1. lia.
+  - destruct (decide (0 ≤ n)); [|rewrite Z.testbit_neg_r //; lia].
+    apply Z.ones_spec_high; lia.
+Qed.
+Global Hint Resolve bitblast_ones | 10 : bitblast.
+Lemma bitblast_pow2 n n' :
+  Bitblast (2 ^ n') n (bool_decide (n = n' ∧ 0 ≤ n)).
+Proof.
+  constructor. case_bool_decide; destruct_and?; subst; [by apply Z.pow2_bits_true|].
+  destruct (decide (0 ≤ n)); [|rewrite Z.testbit_neg_r //; lia].
+  apply Z.pow2_bits_false. lia.
+Qed.
+Global Hint Resolve bitblast_pow2 | 10 : bitblast.
+Lemma bitblast_setbit z1 n b1 n' :
+  Bitblast (Z.lor z1 (2 ^ n')) n b1 →
+  Bitblast (Z.setbit z1 n') n b1.
+Proof. by rewrite Z.setbit_spec'. Qed.
+Global Hint Resolve bitblast_setbit | 10 : bitblast.
+Lemma bitblast_mod z1 z2 z2' n b1 :
+  IsPowerOfTwo z2 z2' →
+  Bitblast z1 n b1 →
+  Bitblast (z1 `mod` z2) n ((bool_decide (z2' < 0 ∧ 0 ≤ n) || bool_decide (n < z2')) && b1).
+Proof.
+  move => [->] [<-]. constructor.
+  case_bool_decide => /=. { rewrite Z.pow_neg_r ?Zmod_0_r; [done|lia]. }
+  destruct (decide (0 ≤ n)). 2: { rewrite !Z.testbit_neg_r ?andb_false_r //; lia. }
+  rewrite -Z.land_ones; [|lia]. rewrite Z.land_spec Z.ones_spec; [|lia..].
+  by rewrite andb_comm.
+Qed.
+Global Hint Resolve bitblast_mod | 10 : bitblast.
+(* TODO: What are good instances for +? Maybe something based on Z_add_nocarry_lor? *)
+Lemma bitblast_add_0 z1 z2 b1 b2 :
+  Bitblast z1 0 b1 →
+  Bitblast z2 0 b2 →
+  Bitblast (z1 + z2) 0 (xorb b1 b2).
+Proof. move => [<-] [<-]. constructor. apply Z.add_bit0. Qed.
+Global Hint Resolve bitblast_add_0 | 5 : bitblast.
+Lemma bitblast_add_1 z1 z2 b10 b11 b20 b21 :
+  Bitblast z1 0 b10 →
+  Bitblast z2 0 b20 →
+  Bitblast z1 1 b11 →
+  Bitblast z2 1 b21 →
+  Bitblast (z1 + z2) 1 (xorb (xorb b11 b21) (b10 && b20)).
+Proof. move => [<-] [<-] [<-] [<-]. constructor. apply Z.add_bit1. Qed.
+Global Hint Resolve bitblast_add_1 | 5 : bitblast.
+Lemma bitblast_clearbit z n b m :
+  Bitblast z n b →
+  Bitblast (Z.clearbit z m) n (bool_decide (n ≠ m) && b).
+Proof.
+  move => [<-]. constructor.
+  case_bool_decide; subst => /=.
+  - by apply Z.clearbit_neq.
+  - by apply Z.clearbit_eq.
+Qed.
+Global Hint Resolve bitblast_clearbit | 10 : bitblast.
+Lemma bitblast_bool_to_Z b n:
+  Bitblast (bool_to_Z b) n (bool_decide (n = 0) && b).
+Proof.
+  constructor. destruct b; simpl_bool; repeat case_bool_decide;
+    subst; try done; rewrite ?Z.bits_0; by destruct n.
+Qed.
+Global Hint Resolve bitblast_bool_to_Z | 10 : bitblast.
+(** Instances for [bv] *)
+Lemma bitblast_bv_wrap z1 n n1 b1:
+  Bitblast z1 n b1 →
+  Bitblast (bv_wrap n1 z1) n (bool_decide (n < Z.of_N n1) && b1).
+Proof.
+  intros [<-]. constructor.
+  destruct (decide (0 ≤ n)); [by rewrite bv_wrap_spec| rewrite !Z.testbit_neg_r; [|lia..]; btauto].
+Qed.
+Global Hint Resolve bitblast_bv_wrap | 10 : bitblast.
+Lemma bitblast_bounded_bv_unsigned n (b : bv n):
+  BitblastBounded (bv_unsigned b) (Z.of_N n).
+Proof. constructor. apply bv_unsigned_in_range. Qed.
+Global Hint Resolve bitblast_bounded_bv_unsigned | 15 : bitblast.
+(** * Tactics *)
+(** ** Helper definitions and lemmas for the tactics *)
+Definition BITBLAST_BOOL_DECIDE := @bool_decide.
+Global Arguments BITBLAST_BOOL_DECIDE _ {_}.
+Lemma tac_bitblast_bool_decide_true G (P : Prop) `{!Decision P} :
+  P →
+  G true →
+  G (bool_decide P).
+Proof. move => ??. by rewrite bool_decide_eq_true_2. Qed.
+Lemma tac_bitblast_bool_decide_false G (P : Prop) `{!Decision P} :
+  ¬ P →
+  G false →
+  G (bool_decide P).
+Proof. move => ??. by rewrite bool_decide_eq_false_2. Qed.
+Lemma tac_bitblast_bool_decide_split G (P : Prop) `{!Decision P} :
+  (P → G true) →
+  (¬ P → G false) →
+  G (bool_decide P).
+Proof. move => ??. case_bool_decide; eauto. Qed.
+(** ** Core tactics *)
+Ltac bitblast_done :=
+  solve [ first [ done | lia | btauto ] ].
+(** [bitblast_blast_eq] applies to goals of the form [Z.testbit _ _ = ?x] and bitblasts the
+  Z.testbit using the [Bitblast] typeclass. *)
+Ltac bitblast_blast_eq :=
+  lazymatch goal with |- Z.testbit _ _ = _ => idtac end;
+  etrans; [ notypeclasses refine (bitblast_proof _ _ _); typeclasses eauto with bitblast | ];
+  simplify_bitblast_index;
+  exact eq_refl.
+(** [bitblast_bool_decide_simplify] get rids of unnecessary bool_decide in the goal. *)
+Ltac bitblast_bool_decide_simplify :=
+  repeat lazymatch goal with
+         | |- context [@bool_decide ?P ?Dec] =>
+             pattern (@bool_decide P Dec);
+             lazymatch goal with
+             | |- ?G _ =>
+                 first [
+                     refine (@tac_bitblast_bool_decide_true G P Dec _ _); [lia|];
+                     simpl_bool_cbn
+                   |
+                     refine (@tac_bitblast_bool_decide_false G P Dec _ _); [lia|];
+                     simpl_bool_cbn
+                   |
+                     change_no_check (G (@BITBLAST_BOOL_DECIDE P Dec))
+               ]
+             end;
+             cbv beta
+         end;
+  (** simpl_bool contains rewriting so it can be quite slow and thus we only do it at the end. *)
+  simpl_bool;
+  lazymatch goal with
+  | |- ?G => let x := eval unfold BITBLAST_BOOL_DECIDE in G in change_no_check x
+  end.
+(** [bitblast_bool_decide_split] performs a case distinction on a bool_decide in the goal. *)
+Ltac bitblast_bool_decide_split :=
+  lazymatch goal with
+  | |- context [@bool_decide ?P ?Dec] =>
+      pattern (@bool_decide P Dec);
+      lazymatch goal with
+      | |- ?G _ =>
+          refine (@tac_bitblast_bool_decide_split G P Dec _ _) => ?; cbv beta; simpl_bool
+      end
+  end.
+(** [bitblast_unfold] bitblasts all [Z.testbit] in the goal. *)
+Ltac bitblast_unfold :=
+  repeat lazymatch goal with
+  | |- context [Z.testbit ?z ?n] =>
+      pattern (Z.testbit z n);
+      simple refine (eq_rec_r _ _ _); [shelve| |bitblast_blast_eq]; cbv beta
+  end;
+  lazymatch goal with
+  | |- ?G => let x := eval unfold BITBLAST_TESTBIT in G in change_no_check x
+  end.
+(** [bitblast_raw] bitblasts all [Z.testbit] in the goal and simplifies the result. *)
+Ltac bitblast_raw :=
+  bitblast_unfold;
+  bitblast_bool_decide_simplify;
+  try bitblast_done;
+  repeat (bitblast_bool_decide_split; bitblast_bool_decide_simplify; try bitblast_done).
+(** ** Tactic notations *)
+Tactic Notation "bitblast" "as" ident(i) :=
+  apply Z.bits_inj_iff'; intros i => ?; bitblast_raw.
+Tactic Notation "bitblast" :=
+  lazymatch goal with
+  | |- context [Z.testbit _ _] => idtac
+  | _ => apply Z.bits_inj_iff' => ??
+  end;
+  bitblast_raw.
+Tactic Notation "bitblast" ident(H) :=
+  tactic bitblast_unfold in H;
+  tactic bitblast_bool_decide_simplify in H.
+Tactic Notation "bitblast" ident(H) "with" constr(i) "as" ident(H') :=
+  lazymatch type of H with
+  (* We cannot use [efeed pose proof] since this causes weird failures
+  in combination with [Set Mangle Names]. *)
+  | @eq Z _ _ => opose proof* (Z_bits_inj'' _ _ H i) as H'; [try bitblast_done..|]
+  | ∀ x, _ => opose proof* (H i) as H'; [try bitblast_done..|]
+  end; bitblast H'.
+Tactic Notation "bitblast" ident(H) "with" constr(i) :=
+  let H' := fresh "H" in bitblast H with i as H'.
--- a/stdpp_unstable/dune
+++ b/stdpp_unstable/dune
+(include_subdirs qualified)
+(coq.theory
+ (name stdpp.unstable)
+ (package coq-stdpp-unstable)
+ (theories stdpp stdpp.bitvector))
--- a/test-normalizer.sed
+++ b/test-normalizer.sed
+# locations in Fail added in https://github.com/coq/coq/pull/15174
+/^File/d
--- a/tests/ascii.ref
+++ b/tests/ascii.ref
+"a"
+     : string
+"a"%char
+     : ascii
+"a"
+     : ascii
+"a"%stdpp
+     : string
No results found