tests/bitblast.v

+From stdpp.unstable Require Import bitblast.
+
+Local Open Scope Z_scope.
+
+Goal ∀ x a k,
+  Z.land x (Z.land (Z.ones k) (Z.ones k) ≪ a) =
+  Z.land (Z.land (x ≫ a) (Z.ones k)) (Z.ones k) ≪ a.
+Proof. intros. bitblast. Qed.
+
+Goal ∀ i,
+  1 ≪ i = Z.land (Z.ones 1) (Z.ones 1) ≪ i.
+Proof. intros. bitblast. Qed.
+
+Goal ∀ N k,
+  0 ≤ k ≤ N → Z.ones N ≫ (N - k) = Z.ones k.
+Proof. intros. bitblast. Qed.
+
+Goal ∀ z,
+  Z.land z (-1) = z.
+Proof. intros. bitblast. Qed.
+
+Goal ∀ z,
+  Z.land z 0x20000 = 0 →
+  Z.land (z ≫ 17) (Z.ones 1) = 0.
+Proof.
+  intros ? Hz. bitblast as n.
+  by bitblast Hz with (n + 17).
+Qed.
+
+Goal ∀ z, 0 ≤ z < 2 ^ 64 →
+   Z.land z 0xfff0000000000007 = 0 ↔ z < 2 ^ 52 ∧ z `mod` 8 = 0.
+Proof.
+  intros z ?. split.
+  - intros Hx. split.
+    + apply Z.bounded_iff_bits_nonneg; [lia..|]. intros n ?. bitblast.
+      by bitblast Hx with n.
+    + bitblast as n. by bitblast Hx with n.
+  - intros [H1 H2]. bitblast as n. by bitblast H2 with n.
+Qed.

tests/bitvector_definitions.ref

+"notation_test"
+     : string
+3%bv = 5%bv
+     : Prop
+The command has indeed failed with message:
+The term "5%bv" has type "bv 10" while it is expected to have type "bv 2".
+3%bv = 5%bv
+     : Prop
+4%bv = 4%bv
+     : Prop
+Z_to_bv 7 (-1) = Z_to_bv 7 (-1)
+     : Prop
+"bvn_to_bv_test"
+     : string
+1 goal
+  
+  ============================
+  Some 3%bv = Some 3%bv

tests/bitvector_definitions.v

+From stdpp Require Import strings.
+From stdpp.bitvector Require Import definitions.
+
+Check "notation_test".
+Check (BV 10 3 = BV 10 5).
+Fail Check (BV 2 3 = BV 10 5).
+Check (BV 2 3 =@{bvn} BV 10 5).
+Check (4%bv = BV 4 4).
+Check ((-1)%bv = Z_to_bv 7 (-1)).
+Goal (-1 =@{bv 5} 31)%bv. compute_done. Qed.
+
+Check "bvn_to_bv_test".
+Goal bvn_to_bv 2 (BV 2 3) = Some (BV 2 3). Proof. simpl. Show. done. Abort.

tests/bitvector_tactics.ref

+1 goal
+  
+  a : Z
+  ============================
+  bv_wrap 64 (a + 1) = bv_wrap 64 (Z.succ a)
+1 goal
+  
+  l, r, xs : bv 64
+  data : list (bv 64)
+  H : bv_unsigned l < bv_unsigned r
+  H0 : bv_unsigned r ≤ Z.of_nat (length data)
+  H1 : bv_unsigned xs + Z.of_nat (length data) * 8 < 2 ^ 52
+  ============================
+  bv_wrap 64
+    (bv_unsigned xs +
+     (bv_unsigned l + bv_wrap 64 (bv_unsigned r - bv_unsigned l) `div` 2 ^ 1) *
+     8) < 2 ^ 52
+2 goals
+  
+  l, r : bv 64
+  data : list (bv 64)
+  H : bv_unsigned l < bv_unsigned r
+  H0 : bv_unsigned r ≤ Z.of_nat (length data)
+  H1 :
+    ¬ bv_swrap 128 (bv_unsigned l) >=
+      bv_swrap 128
+        (bv_wrap 64
+           (bv_wrap 64 (bv_unsigned r - bv_unsigned l) `div` 2 ^ 1 +
+            bv_unsigned l + 0))
+  ============================
+  bv_unsigned l <
+  bv_wrap 64
+    (bv_wrap 64 (bv_unsigned r - bv_unsigned l) `div` 2 ^ 1 + bv_unsigned l +
+     0)
+
+goal 2 is:
+ bv_wrap 64
+   (bv_wrap 64 (bv_unsigned r - bv_unsigned l) `div` 2 ^ 1 + bv_unsigned l +
+    0) ≤ Z.of_nat (length data)
+1 goal
+  
+  r1 : bv 64
+  H : bv_unsigned r1 ≠ 22%Z
+  ============================
+  bv_wrap 64 (bv_unsigned r1 + 18446744073709551593 + 1) ≠ bv_wrap 64 0
+1 goal
+  
+  i, n : bv 64
+  H : bv_unsigned i < bv_unsigned n
+  H0 :
+    bv_wrap 64
+      (bv_unsigned n + bv_wrap 64 (- bv_wrap 64 (bv_unsigned i + 1) - 1) + 1)
+    ≠ 0%Z
+  ============================
+  bv_wrap 64 (bv_unsigned i + 1) < bv_unsigned n
+1 goal
+  
+  b : bv 16
+  v : bv 64
+  ============================
+  bv_wrap 64
+    (Z.lor (Z.land (bv_unsigned v) 18446744069414649855)
+       (bv_wrap 64 (bv_unsigned b ≪ 16))) =
+  bv_wrap 64
+    (Z.lor
+       (bv_wrap (16 * 2) (bv_unsigned v ≫ Z.of_N (16 * 2)) ≪ Z.of_N (16 * 2))
+       (Z.lor (bv_unsigned b ≪ Z.of_N (16 * 1))
+          (bv_wrap (16 * 1) (bv_unsigned v))))
+1 goal
+  
+  b : bv 16
+  ============================
+  bv_wrap 16 (bv_unsigned b) = bv_wrap 16 (bv_unsigned b)
+1 goal
+  
+  b : bv 16
+  ============================
+  bv_wrap 16 (bv_unsigned b) ≠ bv_wrap 16 (bv_unsigned b + 1)
+1 goal
+  
+  b : bv 16
+  H : bv_unsigned b = bv_unsigned b
+  ============================
+  True
+1 goal
+  
+  b : bv 16
+  H : bv_unsigned b ≠ bv_wrap 16 (bv_unsigned b + 1)
+  ============================
+  True

tests/bitvector_tactics.v

+From stdpp Require Import strings.
+From stdpp.bitvector Require Import tactics.
+From stdpp.unstable Require Import bitblast.
+Unset Mangle Names.
+
+Local Open Scope Z_scope.
+Local Open Scope bv_scope.
+
+Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
+
+(** * Smoke tests *)
+
+(** Simple test *)
+Goal ∀ a : Z, Z_to_bv 64 a `+Z` 1 = Z_to_bv 64 (Z.succ a).
+Proof.
+  intros. bv_simplify. Show.
+Restart. Proof.
+  intros. bv_solve.
+Qed.
+
+(** More complex test *)
+Goal ∀ l r xs : bv 64, ∀ data : list (bv 64),
+    bv_unsigned l < bv_unsigned r →
+    bv_unsigned r ≤ Z.of_nat (length data) →
+    bv_unsigned xs + Z.of_nat (length data) * 8 < 2 ^ 52 →
+    bv_unsigned (xs + (bv_extract 0 64 (bv_zero_extend 128 l) +
+                       bv_extract 0 64 (bv_zero_extend 128 ((r - l) ≫ 1))) * 8) < 2 ^ 52.
+Proof.
+  intros. bv_simplify_arith. Show.
+Restart. Proof.
+  intros. bv_solve.
+Qed.
+
+(** Testing simplification in hypothesis *)
+Goal ∀ l r : bv 64, ∀ data : list (bv 64),
+  bv_unsigned l < bv_unsigned r →
+  bv_unsigned r ≤ Z.of_nat (length data) →
+  ¬ bv_signed (bv_zero_extend 128 l) >=
+    bv_signed (bv_zero_extend 128 (bv_zero_extend 128 ((r - l) ≫ 1 + l + 0))) →
+  bv_unsigned l < bv_unsigned ((r - l) ≫ 1 + l + 0) ≤ Z.of_nat (length data).
+Proof.
+  intros. bv_simplify_arith select (¬ _ >= _). bv_simplify_arith.
+  split. (* We need to split since the [_ < _ ≤ _] notation differs between Coq versions. *) Show.
+Restart. Proof.
+  intros. bv_simplify_arith select (¬ _ >= _). bv_solve.
+Qed.
+
+(** Testing inequality in goal. *)
+Goal ∀ r1 : bv 64,
+  bv_unsigned r1 ≠ 22%Z →
+  bv_extract 0 64 (bv_zero_extend 128 r1 + 0xffffffffffffffe9 + 1) ≠ 0.
+Proof.
+  intros. bv_simplify. Show.
+Restart. Proof.
+  intros. bv_solve.
+Qed.
+
+(** Testing inequality in hypothesis. *)
+Goal ∀ i n : bv 64,
+  bv_unsigned i < bv_unsigned n →
+  bv_extract 0 64 (bv_zero_extend 128 n + bv_zero_extend 128 (bv_not (bv_extract 0 64 (bv_zero_extend 128 i)
+          + 1)) +  1) ≠ 0 →
+  bv_unsigned (bv_extract 0 64 (bv_zero_extend 128 i) + 1) < bv_unsigned n.
+Proof.
+  intros. bv_simplify_arith select (bv_extract _ _ _ ≠ _). bv_simplify. Show.
+Restart. Proof.
+  intros. bv_simplify_arith select (bv_extract _ _ _ ≠ _). bv_solve.
+Qed.
+
+(** Testing combination of bitvector and bitblast. *)
+Goal ∀ b : bv 16, ∀ v : bv 64,
+  bv_or (bv_and v 0xffffffff0000ffff) (bv_zero_extend 64 b ≪ 16) =
+  bv_concat 64 (bv_extract (16 * (1 + 1)) (16 * 2) v) (bv_concat (16 * (1 + 1)) b (bv_extract 0 (16 * 1) v)).
+Proof.
+  intros. bv_simplify. Show. bitblast.
+Qed.
+
+(** Regression test for https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/411 *)
+Goal ∀ b : bv 16, bv_wrap 16 (bv_unsigned b) = bv_wrap 16 (bv_unsigned b).
+Proof.
+  intros. bv_simplify. Show.
+Restart. Proof.
+  intros. bv_solve.
+Qed.
+Goal ∀ b : bv 16, bv_wrap 16 (bv_unsigned b) ≠ bv_wrap 16 (bv_unsigned (b + 1)).
+Proof.
+  intros. bv_simplify. Show.
+Restart. Proof.
+  intros. bv_solve.
+Qed.
+
+Goal ∀ b : bv 16, bv_unsigned b = bv_unsigned b → True.
+Proof. intros ? H. bv_simplify H. Show. Abort.
+Goal ∀ b : bv 16, bv_unsigned b ≠ bv_unsigned (b + 1) → True.
+Proof. intros ? H. bv_simplify H. Show. Abort.

tests/decidable.ref

+The command has indeed failed with message:
+No applicable tactic.

tests/decidable.v

+From stdpp Require Import list.
+
+(** Test that Coq does not infer [x ∈ xs] as [False] by eagerly using
+[False_dec] on a goal with unresolved type class instances. *)
+Example issue_165 (x : nat) :
+  ¬ ∃ xs : list nat, (guard (x ∈ xs);; Some x) ≠ None.
+Proof.
+  intros [xs Hxs]. case_guard; [|done].
+  Fail done. (* Would succeed if the instance backing [x ∈ xs] is inferred as
+  [False]. *)
+Abort.

tests/fin.v

+From stdpp Require Import fin.
+
+Definition f n m (p : fin n) := m < p.
+
+Lemma test : f 47 13 32.
+Proof. vm_compute. lia. Qed.

tests/fin_maps.ref

+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  {[1; 2; 3]} = ∅
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  elements {[1; 2; 3]} = []
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  {[1; 2; 3]} ∖ {[1]} ∪ {[4]} ∩ {[10]} = ∅ ∖ {[2]}
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  1%positive ∈ dom (<[1%positive:=2]> ∅)
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  1 ∈ dom (<[1:=2]> ∅)
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  bool_decide (∅ = {[1; 2; 3]}) = false
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  bool_decide (∅ ≡ {[1; 2; 3]}) = false
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  bool_decide (1 ∈ {[1; 2; 3]}) = true
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  bool_decide (∅ ## {[1; 2; 3]}) = true
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  bool_decide (∅ ⊆ {[1; 2; 3]}) = true
+The command has indeed failed with message:
+Nothing to inject.
+The command has indeed failed with message:
+Nothing to inject.
+The command has indeed failed with message:
+Failed to progress.
+"pmap_insert_positives_test"
+     : string
+     = true
+     : bool
+     = true
+     : bool
+     = true
+     : bool
+"gmap_insert_positives_test"
+     : string
+     = true
+     : bool
+     = true
+     : bool
+     = true
+     : bool
+"pmap_insert_comm"
+     : string
+1 goal
+  
+  ============================
+  {[3%positive := false; 2%positive := true]} =
+  {[2%positive := true; 3%positive := false]}
+"pmap_lookup_concrete"
+     : string
+1 goal
+  
+  ============================
+  {[3%positive := false; 2%positive := true]} !! 2%positive = Some true
+"gmap_insert_comm"
+     : string
+1 goal
+  
+  ============================
+  {[3 := false; 2 := true]} = {[2 := true; 3 := false]}
+"gmap_lookup_concrete"
+     : string
+1 goal
+  
+  ============================
+  {[3 := false; 2 := true]} !! 2 = Some true

tests/fin_maps.v

 From stdpp Require Import fin_maps fin_map_dom.
+From stdpp Require Import strings pmap gmap.
 
+(** * Tests involving the [FinMap] interfaces, i.e., tests that are not specific
+to an implementation of finite maps. *)
 Section map_disjoint.
   Context `{FinMap K M}.
 
   Lemma solve_map_disjoint_singleton_1 {A} (m1 m2 : M A) i x :
     m1 ##ₘ <[i:=x]> m2 → {[ i:= x ]} ∪ m2 ##ₘ m1 ∧ m2 ##ₘ ∅.
   Proof. intros. solve_map_disjoint. Qed.
-
   Lemma solve_map_disjoint_singleton_2 {A} (m1 m2 : M A) i x :
     m2 !! i = None → m1 ##ₘ {[ i := x ]} ∪ m2 → m2 ##ₘ <[i:=x]> m1 ∧ m1 !! i = None.
   Proof. intros. solve_map_disjoint. Qed.
+
+  Lemma solve_map_disjoint_compose_l_singleton_1 {A} (n : M K) (m1 m2 : M A) i x :
+    m1 ##ₘ <[i:=x]> m2 → ({[ i:= x ]} ∪ m2) ∘ₘ n ##ₘ m1 ∘ₘ n ∧ m2 ##ₘ ∅.
+  Proof. intros. solve_map_disjoint. Qed.
+  Lemma solve_map_disjoint_compose_l_singleton_2 {A} (n : M K) (m1 m2 : M A) i x :
+    m2 !! i = None → m1 ##ₘ {[ i := x ]} ∪ m2 → m2 ∘ₘ n ##ₘ <[i:=x]> m1 ∘ₘ n ∧ m1 !! i = None.
+  Proof. intros. solve_map_disjoint. Qed.
+
+  Lemma solve_map_disjoint_compose_r_singleton_1 {A} (m1 m2 : M K) (n : M A) i x :
+    m1 ##ₘ <[i:=x]> m2 → n ∘ₘ ({[ i:= x ]} ∪ m2) ##ₘ n ∘ₘ m1 ∧ m2 ##ₘ ∅.
+  Proof. intros. solve_map_disjoint. Qed.
+  Lemma solve_map_disjoint_compose_r_singleton_2 {A} (m1 m2 : M K) (n : M A) i x :
+    m2 !! i = None → m1 ##ₘ {[ i := x ]} ∪ m2 → n ∘ₘ m2 ##ₘ n ∘ₘ <[i:=x]> m1 ∧ m1 !! i = None.
+  Proof. intros. solve_map_disjoint. Qed.
 End map_disjoint.
 
 Section map_dom.
   Context `{FinMapDom K M D}.
 
   Lemma set_solver_dom_subseteq {A} (i j : K) (x y : A) :
-    {[i; j]} ⊆ dom D (<[i:=x]> (<[j:=y]> (∅ : M A))).
+    {[i; j]} ⊆ dom (<[i:=x]> (<[j:=y]> (∅ : M A))).
   Proof. set_solver. Qed.
 
-  Lemma set_solver_dom_disjoint {A} (X : D) : dom D (∅ : M A) ## X.
+  Lemma set_solver_dom_disjoint {A} (X : D) : dom (∅ : M A) ## X.
   Proof. set_solver. Qed.
 End map_dom.
+
+Section map_img.
+  Context `{FinMap K M, Set_ A SA}.
+
+  Lemma set_solver_map_img i x :
+    map_img (∅ : M A) ⊆@{SA} map_img ({[ i := x ]} : M A).
+  Proof. set_unfold. set_solver. Qed.
+End map_img.
+
+(** * Tests for the [Pmap] and [gmap] instances. *)
+
+(** TODO: Fix [Pset] so that it satisfies the same [cbn]/[simpl] tests as
+[gset] below. *)
+
+Goal {[1; 2; 3]} =@{gset nat} ∅.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+Abort.
+
+Goal elements (C := gset nat) {[1; 2; 3]} = [].
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+Abort.
+
+Goal
+  {[1; 2; 3]} ∖ {[ 1 ]} ∪ {[ 4 ]} ∩ {[ 10 ]} =@{gset nat} ∅ ∖ {[ 2 ]}.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+Abort.
+
+Goal 1%positive ∈ dom (M := Pmap nat) (<[ 1%positive := 2 ]> ∅).
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+Abort.
+
+Goal 1 ∈ dom (M := gmap nat nat) (<[ 1 := 2 ]> ∅).
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+Abort.
+
+Goal bool_decide (∅ =@{gset nat} {[ 1; 2; 3 ]}) = false.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+  reflexivity.
+Qed.
+
+Goal bool_decide (∅ ≡@{gset nat} {[ 1; 2; 3 ]}) = false.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+  reflexivity.
+Qed.
+
+Goal bool_decide (1 ∈@{gset nat} {[ 1; 2; 3 ]}) = true.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+  reflexivity.
+Qed.
+
+Goal bool_decide (∅ ##@{gset nat} {[ 1; 2; 3 ]}) = true.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+  reflexivity.
+Qed.
+
+Goal bool_decide (∅ ⊆@{gset nat} {[ 1; 2; 3 ]}) = true.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+  reflexivity.
+Qed.
+
+Lemma should_not_unfold (m1 m2 : gmap nat nat) k x :
+  dom m1 = dom m2 →
+  <[k:=x]> m1 = <[k:=x]> m2 →
+  True.
+Proof.
+  (** Make sure that [injection]/[simplify_eq] does not unfold constructs on
+  [gmap] and [gset]. *)
+  intros Hdom Hinsert.
+  Fail injection Hdom.
+  Fail injection Hinsert.
+  Fail progress simplify_eq.
+  done.
+Qed.
+
+(** Test case for issue #139 *)
+
+Lemma test_issue_139 (m : gmap nat nat) : ∃ x, x ∉ dom m.
+Proof.
+  destruct (exist_fresh (dom m)); eauto.
+Qed.
+
+(** Make sure that unification does not eagerly unfold [map_fold] *)
+
+Definition only_evens (m : gmap nat nat) : gmap nat nat :=
+  filter (λ '(_,x), (x | 2)) m.
+
+Lemma only_evens_Some m i n : only_evens m !! i = Some n → (n | 2).
+Proof.
+  intros Hev.
+  apply map_lookup_filter_Some in Hev as [??]. done.
+Qed.
+
+(** Make sure that [pmap] and [gmap] compute *)
+
+Definition pmap_insert_positives (start step num : positive) : Pmap unit :=
+  Pos.iter (λ rec p m,
+    rec (p + step)%positive (<[p:=tt]> m)) (λ _ m, m) num start ∅.
+Definition pmap_insert_positives_rev (start step num : positive) : Pmap unit :=
+  Pos.iter (λ rec p m,
+    rec (p - step)%positive (<[p:=tt]> m)) (λ _ m, m) num start ∅.
+
+Definition pmap_insert_positives_test (num : positive) : bool :=
+  bool_decide (pmap_insert_positives 1 1 num = pmap_insert_positives_rev num 1 num).
+
+Definition pmap_insert_positives_union_test (num : positive) : bool :=
+  bool_decide (pmap_insert_positives 1 1 num =
+    pmap_insert_positives 2 2 (Pos.div2_up num) ∪
+    pmap_insert_positives 1 2 (Pos.div2_up num)).
+
+Definition pmap_insert_positives_filter_test (num : positive) : bool :=
+  bool_decide (pmap_insert_positives 1 2 (Pos.div2_up num) =
+    filter (λ '(p,_), Z.odd (Z.pos p)) (pmap_insert_positives 1 1 num)).
+
+(* Test that the time is approximately n-log-n. We cannot test this on CI since
+you get different timings all the time. Instead we just test for [128000], which
+likely takes forever if the complexity is not n-log-n. *)
+(*
+Time Eval vm_compute in pmap_insert_positives_test 1000.
+Time Eval vm_compute in pmap_insert_positives_test 2000.
+Time Eval vm_compute in pmap_insert_positives_test 4000.
+Time Eval vm_compute in pmap_insert_positives_test 8000.
+Time Eval vm_compute in pmap_insert_positives_test 16000.
+Time Eval vm_compute in pmap_insert_positives_test 32000.
+Time Eval vm_compute in pmap_insert_positives_test 64000.
+Time Eval vm_compute in pmap_insert_positives_test 128000.
+Time Eval vm_compute in pmap_insert_positives_test 256000.
+Time Eval vm_compute in pmap_insert_positives_test 512000.
+Time Eval vm_compute in pmap_insert_positives_test 1000000.
+*)
+Check "pmap_insert_positives_test".
+Eval vm_compute in pmap_insert_positives_test 128000.
+Eval vm_compute in pmap_insert_positives_union_test 128000.
+Eval vm_compute in pmap_insert_positives_filter_test 128000.
+
+Definition gmap_insert_positives (start step num : positive) : gmap positive unit :=
+  Pos.iter (λ rec p m,
+    rec (p + step)%positive (<[p:=tt]> m)) (λ _ m, m) num start ∅.
+Definition gmap_insert_positives_rev (start step num : positive) : gmap positive unit :=
+  Pos.iter (λ rec p m,
+    rec (p - step)%positive (<[p:=tt]> m)) (λ _ m, m) num start ∅.
+
+(* Test that the time increases linearly *)
+Definition gmap_insert_positives_test (num : positive) : bool :=
+  bool_decide (gmap_insert_positives 1 1 num = gmap_insert_positives_rev num 1 num).
+
+Definition gmap_insert_positives_union_test (num : positive) : bool :=
+  bool_decide (gmap_insert_positives 1 1 num =
+    gmap_insert_positives 2 2 (Pos.div2_up num) ∪
+    gmap_insert_positives 1 2 (Pos.div2_up num)).
+
+Definition gmap_insert_positives_filter_test (num : positive) : bool :=
+  bool_decide (gmap_insert_positives 1 2 (Pos.div2_up num) =
+    filter (λ '(p,_), Z.odd (Z.pos p)) (gmap_insert_positives 1 1 num)).
+
+(* Test that the time is approximately n-log-n. We cannot test this on CI since
+you get different timings all the time. Instead we just test for [128000], which
+likely takes forever if the complexity is not n-log-n. *)
+(*
+Time Eval vm_compute in gmap_insert_positives_test 1000.
+Time Eval vm_compute in gmap_insert_positives_test 2000.
+Time Eval vm_compute in gmap_insert_positives_test 4000.
+Time Eval vm_compute in gmap_insert_positives_test 8000.
+Time Eval vm_compute in gmap_insert_positives_test 16000.
+Time Eval vm_compute in gmap_insert_positives_test 32000.
+Time Eval vm_compute in gmap_insert_positives_test 64000.
+Time Eval vm_compute in gmap_insert_positives_test 128000.
+Time Eval vm_compute in gmap_insert_positives_test 256000.
+Time Eval vm_compute in gmap_insert_positives_test 512000.
+Time Eval vm_compute in gmap_insert_positives_test 1000000.
+*)
+Check "gmap_insert_positives_test".
+Eval vm_compute in gmap_insert_positives_test 128000.
+Eval vm_compute in gmap_insert_positives_union_test 128000.
+Eval vm_compute in gmap_insert_positives_filter_test 128000.
+
+(** Make sure that [pmap] and [gmap] have canonical representations, and compute
+reasonably efficiently even with [reflexivity]. *)
+
+Check "pmap_insert_comm".
+Theorem pmap_insert_comm :
+  {[ 3:=false; 2:=true]}%positive =@{Pmap bool} {[ 2:=true; 3:=false ]}%positive.
+Proof. simpl. Show. reflexivity. Qed.
+
+Check "pmap_lookup_concrete".
+Theorem pmap_lookup_concrete :
+  lookup (M:=Pmap bool) 2%positive {[ 3:=false; 2:=true ]}%positive = Some true.
+Proof. simpl. Show. reflexivity. Qed.
+
+Theorem pmap_insert_positives_reflexivity_500 :
+  pmap_insert_positives 1 1 500 = pmap_insert_positives_rev 500 1 500.
+Proof. reflexivity. Qed.
+Theorem pmap_insert_positives_reflexivity_1000 :
+  pmap_insert_positives 1 1 1000 = pmap_insert_positives_rev 1000 1 1000.
+Proof. (* this should take less than a second *) reflexivity. Qed.
+
+Theorem pmap_insert_positives_union_reflexivity_500 :
+  (pmap_insert_positives_rev 1 1 400) ∪
+    (pmap_insert_positives 1 1 500 ∖ pmap_insert_positives_rev 1 1 400)
+  = pmap_insert_positives 1 1 500.
+Proof. reflexivity. Qed.
+Theorem pmap_insert_positives_union_reflexivity_1000 :
+  (pmap_insert_positives_rev 1 1 800) ∪
+    (pmap_insert_positives 1 1 1000 ∖ pmap_insert_positives_rev 1 1 800)
+  = pmap_insert_positives 1 1 1000.
+Proof. (* this should less than a second *) reflexivity. Qed.
+
+Check "gmap_insert_comm".
+Theorem gmap_insert_comm :
+  {[ 3:=false; 2:=true]} =@{gmap nat bool} {[ 2:=true; 3:=false ]}.
+Proof. simpl. Show. reflexivity. Qed.
+
+Check "gmap_lookup_concrete".
+Theorem gmap_lookup_concrete :
+  lookup (M:=gmap nat bool) 2 {[ 3:=false; 2:=true ]} = Some true.
+Proof. simpl. Show. reflexivity. Qed.
+
+Theorem gmap_insert_positives_reflexivity_500 :
+  gmap_insert_positives 1 1 500 = gmap_insert_positives_rev 500 1 500.
+Proof. reflexivity. Qed.
+Theorem gmap_insert_positives_reflexivity_1000 :
+  gmap_insert_positives 1 1 1000 = gmap_insert_positives_rev 1000 1 1000.
+Proof. (* this should less than a second *) reflexivity. Qed.
+
+Theorem gmap_insert_positives_union_reflexivity_500 :
+  (gmap_insert_positives_rev 1 1 400) ∪
+    (gmap_insert_positives 1 1 500 ∖ gmap_insert_positives_rev 1 1 400)
+  = gmap_insert_positives 1 1 500.
+Proof. reflexivity. Qed.
+Theorem gmap_insert_positives_union_reflexivity_1000 :
+  (gmap_insert_positives_rev 1 1 800) ∪
+    (gmap_insert_positives 1 1 1000 ∖ gmap_insert_positives_rev 1 1 800)
+  = gmap_insert_positives 1 1 1000.
+Proof. (* this should less than a second *) reflexivity. Qed.
+
+(** This should be immediate, see std++ issue #183 *)
+Goal dom ((<[10%positive:=1]> ∅) : Pmap _) = dom ((<[10%positive:=2]> ∅) : Pmap _).
+Proof. reflexivity. Qed.
+
+Goal dom ((<["f":=1]> ∅) : gmap _ _) = dom ((<["f":=2]> ∅) : gmap _ _).
+Proof. reflexivity. Qed.
+
+(** Make sure that [pmap] and [gmap] can be used in nested inductive
+definitions *)
+
+Inductive test := Test : Pmap test → test.
+
+Fixpoint test_size (t : test) : nat :=
+  let 'Test ts := t in S (map_fold (λ _ t', plus (test_size t')) 0 ts).
+
+Fixpoint test_merge (t1 t2 : test) : test :=
+  match t1, t2 with
+  | Test ts1, Test ts2 =>
+     Test $ union_with (λ t1 t2, Some (test_merge t1 t2)) ts1 ts2
+  end.
+
+Lemma test_size_merge :
+  test_size (test_merge
+    (Test {[ 10%positive := Test ∅; 50%positive := Test ∅ ]})
+    (Test {[ 10%positive := Test ∅; 32%positive := Test ∅ ]})) = 4.
+Proof. reflexivity. Qed.
+
+Global Instance test_eq_dec : EqDecision test.
+Proof.
+  refine (fix go t1 t2 :=
+    let _ : EqDecision test := @go in
+    match t1, t2 with
+    | Test ts1, Test ts2 => cast_if (decide (ts1 = ts2))
+    end); abstract congruence.
+Defined.
+
+Inductive gtest K `{Countable K} := GTest : gmap K (gtest K) → gtest K.
+Arguments GTest {_ _ _} _.
+
+Fixpoint gtest_size `{Countable K} (t : gtest K) : nat :=
+  let 'GTest ts := t in S (map_fold (λ _ t', plus (gtest_size t')) 0 ts).
+
+Fixpoint gtest_merge `{Countable K} (t1 t2 : gtest K) : gtest K :=
+  match t1, t2 with
+  | GTest ts1, GTest ts2 =>
+     GTest $ union_with (λ t1 t2, Some (gtest_merge t1 t2)) ts1 ts2
+  end.
+
+Lemma gtest_size_merge :
+  gtest_size (gtest_merge
+    (GTest {[ 10 := GTest ∅; 50 := GTest ∅ ]})
+    (GTest {[ 10 := GTest ∅; 32 := GTest ∅ ]})) = 4.
+Proof. reflexivity. Qed.
+
+Lemma gtest_size_merge_string :
+  gtest_size (gtest_merge
+    (GTest {[ "foo" := GTest ∅; "bar" := GTest ∅ ]})
+    (GTest {[ "foo" := GTest ∅; "baz" := GTest ∅ ]})) = 4.
+Proof. reflexivity. Qed.
+
+Global Instance gtest_eq_dec `{Countable K} : EqDecision (gtest K).
+Proof.
+  refine (fix go t1 t2 :=
+    let _ : EqDecision (gtest K) := @go in
+    match t1, t2 with
+    | GTest ts1, GTest ts2 => cast_if (decide (ts1 = ts2))
+    end); abstract congruence.
+Defined.
+
+Lemma gtest_ind' `{Countable K} (P : gtest K → Prop) :
+  (∀ ts, map_Forall (λ _, P) ts → P (GTest ts)) →
+  ∀ t, P t.
+Proof.
+  intros Hnode t.
+  remember (gtest_size t) as n eqn:Hn. revert t Hn.
+  induction (lt_wf n) as [n _ IH]; intros [ts] ->; simpl in *.
+  apply Hnode. induction ts as [|k t m ? Hfold IHm] using map_first_key_ind.
+  - apply map_Forall_empty.
+  - apply map_Forall_insert; [done|]. split.
+    + eapply IH; [|done]. rewrite map_fold_insert_first_key by done. lia.
+    + eapply IHm. intros; eapply IH; [|done].
+      rewrite map_fold_insert_first_key by done. lia.
+Qed.
+
+(** We show that [gtest K] is countable itself. This means that we can use
+[gtest K] (which involves nested uses of [gmap]) as keys in [gmap]/[gset], i.e.,
+[gmap (gtest K) V] and [gset (gtest K)]. And even [gtest (gtest K)].
+
+Showing that [gtest K] is countable is not trivial due to its nested-inductive
+nature. We need to write [encode] and [decode] functions, and prove that they
+are inverses. We do this by converting to/from [gen_tree]. This shows that Coq's
+guardedness checker accepts non-trivial recursive definitions involving [gtest],
+and we can do non-trivial induction proofs about [gtest]. *)
+Global Program Instance gtest_countable `{Countable K} : Countable (gtest K) :=
+  let enc :=
+    fix go t :=
+      let 'GTest ts := t return _ in
+      GenNode 0 (map_fold (λ (k : K) t rec, GenLeaf k :: go t :: rec) [] ts) in
+  let dec_list := λ dec : gen_tree K → gtest K,
+    fix go ts :=
+      match ts return gmap K (gtest K) with
+      | GenLeaf k :: t :: ts => <[k:=dec t]> (go ts)
+      | _ => ∅
+      end in
+  let dec :=
+    fix go t :=
+      match t return _ with
+      | GenNode 0 ts => GTest (dec_list go ts)
+      | _ => GTest ∅ (* dummy *)
+      end in
+  inj_countable' enc dec _.
+Next Obligation.
+  intros K ?? enc dec_list dec t.
+  induction (Nat.lt_wf_0_projected gtest_size t) as [[ts] _ IH]. f_equal/=.
+  induction ts as [|i t ts ? Hfold IHts] using map_first_key_ind; [done|].
+  rewrite map_fold_insert_first_key by done. f_equal/=.
+  - eapply IH. rewrite map_fold_insert_L by auto with lia. lia.
+  - apply IHts; intros t' ?. eapply IH.
+    rewrite map_fold_insert_L by auto with lia. lia.
+Qed.
+
+Goal
+  ({[ GTest {[ 1 := GTest ∅ ]} := "foo" ]} : gmap (gtest nat) string)
+  !! GTest {[ 1 := GTest ∅ ]} = Some "foo".
+Proof. reflexivity. Qed.
+
+Goal {[ GTest {[ 1 := GTest ∅ ]} ]} ≠@{gset (gtest nat)} {[ GTest ∅ ]}.
+Proof. discriminate. Qed.
+
+Goal GTest {[ GTest {[ 1 := GTest ∅ ]} := GTest ∅ ]} ≠@{gtest (gtest nat)} GTest ∅.
+Proof. discriminate. Qed.
+
+(** Test that a fixpoint can be recursively invoked in the closure argument
+of [map_imap]. *)
+Fixpoint gtest_imap `{Countable K} (j : K) (t : gtest K) : gtest K :=
+  let '(GTest ts) := t in
+  GTest (map_imap (λ i t, guard (i = j);; Some (gtest_imap j t)) ts).
+
+(** Test that [map_Forall P] and [map_Forall2 P] can be used in an inductive
+definition with a recursive occurence in the predicate/relation [P] without
+bothering the positivity checker. *)
+Inductive gtest_pred `{Countable K} : gtest K → Prop :=
+  | GTest_pred ts :
+     map_Forall (λ _, gtest_pred) ts → gtest_pred (GTest ts).
+
+Inductive gtest_rel `{Countable K} : relation (gtest K) :=
+  | GTest_rel ts1 ts2 :
+     map_Forall2 (λ _, gtest_rel) ts1 ts2 → gtest_rel (GTest ts1) (GTest ts2).

tests/gmap.ref

-The command has indeed failed with message:
-Failed to progress.
-The command has indeed failed with message:
-Failed to progress.
-1 goal
-  
-  ============================
-  {[1; 2; 3]} = ∅
-The command has indeed failed with message:
-Failed to progress.
-The command has indeed failed with message:
-Failed to progress.
-1 goal
-  
-  ============================
-  elements {[1; 2; 3]} = []
-The command has indeed failed with message:
-Failed to progress.
-The command has indeed failed with message:
-Failed to progress.
-1 goal
-  
-  ============================
-  {[1; 2; 3]} ∖ {[1]} ∪ {[4]} ∩ {[10]} = ∅ ∖ {[2]}
-The command has indeed failed with message:
-Failed to progress.
-The command has indeed failed with message:
-Failed to progress.
-1 goal
-  
-  ============================
-  1 ∈ dom (gset nat) (<[1:=2]> ∅)
-The command has indeed failed with message:
-Failed to progress.
-The command has indeed failed with message:
-Failed to progress.
-1 goal
-  
-  ============================
-  bool_decide (∅ = {[1; 2; 3]}) = false
-The command has indeed failed with message:
-Failed to progress.
-The command has indeed failed with message:
-Failed to progress.
-1 goal
-  
-  ============================
-  bool_decide (∅ ≡ {[1; 2; 3]}) = false
-The command has indeed failed with message:
-Failed to progress.
-The command has indeed failed with message:
-Failed to progress.
-1 goal
-  
-  ============================
-  bool_decide (1 ∈ {[1; 2; 3]}) = true
-The command has indeed failed with message:
-Failed to progress.
-The command has indeed failed with message:
-Failed to progress.
-1 goal
-  
-  ============================
-  bool_decide (∅ ## {[1; 2; 3]}) = true
-The command has indeed failed with message:
-Failed to progress.
-The command has indeed failed with message:
-Failed to progress.
-1 goal
-  
-  ============================
-  bool_decide (∅ ⊆ {[1; 2; 3]}) = true

tests/gmap.v

-From stdpp Require Import gmap.
-
-Goal {[1; 2; 3]} =@{gset nat} ∅.
-Proof.
-  Fail progress simpl.
-  Fail progress cbn.
-  Show.
-Abort.
-
-Goal elements (C := gset nat) {[1; 2; 3]} = [].
-Proof.
-  Fail progress simpl.
-  Fail progress cbn.
-  Show.
-Abort.
-
-Goal
-  {[1; 2; 3]} ∖ {[ 1 ]} ∪ {[ 4 ]} ∩ {[ 10 ]} =@{gset nat} ∅ ∖ {[ 2 ]}.
-Proof.
-  Fail progress simpl.
-  Fail progress cbn.
-  Show.
-Abort.
-
-Goal 1 ∈ dom (M := gmap nat nat) (gset nat) (<[ 1 := 2 ]> ∅).
-Proof.
-  Fail progress simpl.
-  Fail progress cbn.
-  Show.
-Abort.
-
-Goal bool_decide (∅ =@{gset nat} {[ 1; 2; 3 ]}) = false.
-Proof.
-  Fail progress simpl.
-  Fail progress cbn.
-  Show.
-  reflexivity.
-Qed.
-
-Goal bool_decide (∅ ≡@{gset nat} {[ 1; 2; 3 ]}) = false.
-Proof.
-  Fail progress simpl.
-  Fail progress cbn.
-  Show.
-  reflexivity.
-Qed.
-
-Goal bool_decide (1 ∈@{gset nat} {[ 1; 2; 3 ]}) = true.
-Proof.
-  Fail progress simpl.
-  Fail progress cbn.
-  Show.
-  reflexivity.
-Qed.
-
-Goal bool_decide (∅ ##@{gset nat} {[ 1; 2; 3 ]}) = true.
-Proof.
-  Fail progress simpl.
-  Fail progress cbn.
-  Show.
-  reflexivity.
-Qed.
-
-Goal bool_decide (∅ ⊆@{gset nat} {[ 1; 2; 3 ]}) = true.
-Proof.
-  Fail progress simpl.
-  Fail progress cbn.
-  Show.
-  reflexivity.
-Qed.

tests/is_closed_term.ref

+"is_closed_term_test"
+     : string
+The command has indeed failed with message:
+Tactic failure: The term x is not closed.
+The command has indeed failed with message:
+Tactic failure: The term (x + 1) is not closed.
+The command has indeed failed with message:
+Tactic failure: The term (x + y) is not closed.
+The command has indeed failed with message:
+Tactic failure: The term section_variable is not closed.
+The command has indeed failed with message:
+Tactic failure: The term (section_variable + 1) is not closed.
+The command has indeed failed with message:
+Tactic failure: The term P is not closed.
+The command has indeed failed with message:
+Tactic failure: The term (P ∧ True) is not closed.

tests/is_closed_term.v

+From stdpp Require Import tactics strings.
+Unset Mangle Names.
+
+Section test.
+  Context (section_variable : nat).
+
+  Axiom axiom : nat.
+
+  Check "is_closed_term_test".
+  Lemma is_closed_term_test :
+    ∀ x y (P : Prop),
+      let a := 10 in
+      a = a →
+      let b := (a + 11) in
+      x + y = y + x.
+  Proof.
+    intros x y P a H b.
+    (* Constructors are closed. *)
+    is_closed_term 1.
+
+    (* Functions on closed terms are closed. *)
+    is_closed_term (1 + 1).
+
+    (* Variables bound in the context are not closed. *)
+    Fail is_closed_term x.
+    Fail is_closed_term (x + 1).
+    Fail is_closed_term (x + y).
+
+    (* Section variables are not closed. *)
+    Fail is_closed_term section_variable.
+    Fail is_closed_term (section_variable + 1).
+
+    (* Axioms are considered closed. (Arguably this is a bug, but
+    there is nothing we can do about it.) *)
+    is_closed_term axiom.
+    is_closed_term (axiom + 1).
+
+    (* Let-bindings are considered closed. *)
+    is_closed_term a.
+    is_closed_term (a + 1).
+    is_closed_term b.
+    is_closed_term (b + 1).
+
+    (* is_closed_term also works for propositions. *)
+    is_closed_term True.
+    is_closed_term (True ∧ True).
+    Fail is_closed_term P.
+    Fail is_closed_term (P ∧ True).
+
+    lia.
+  Qed.
+End test.

tests/multiset_solver.v

-From stdpp Require Import gmultiset.
+From stdpp Require Import gmultiset sets.
 
 Section test.
   Context `{Countable A}.
@@ -11,6 +11,12 @@ Section test.
     {[+ z +]} ⊎ X = {[+ y +]} ⊎ Y →
     {[+ x; z +]} ⊎ X = {[+ y; x +]} ⊎ Y.
   Proof. multiset_solver. Qed.
+  Lemma test_eq_3 x :
+    {[+ x; x +]} =@{gmultiset _} 2 *: {[+ x +]}.
+  Proof. multiset_solver. Qed.
+  Lemma test_eq_4 x y :
+    {[+ x; y; x +]} =@{gmultiset _} 2 *: {[+ x +]} ⊎ {[+ y +]}.
+  Proof. multiset_solver. Qed.
 
   Lemma test_neq_1 x y X : {[+ x; y +]} ⊎ X ≠ ∅.
   Proof. multiset_solver. Qed.
@@ -32,6 +38,12 @@ Section test.
   Lemma test_multiplicity_3 x X :
     multiplicity x X < 3 → {[+ x; x; x +]} ⊈ X.
   Proof. multiset_solver. Qed.
+  Lemma test_multiplicity_4 x X :
+    2 < multiplicity x X → 3 *: {[+ x +]} ⊆ X.
+  Proof. multiset_solver. Qed.
+  Lemma test_multiplicity_5 x X :
+    multiplicity x X < 3 → 3 *: {[+ x +]} ⊈ X.
+  Proof. multiset_solver. Qed.
 
   Lemma test_elem_of_1 x X : x ∈ X ↔ {[+ x +]} ⊎ ∅ ⊆ X.
   Proof. multiset_solver. Qed.
@@ -46,6 +58,22 @@ Section test.
   Lemma test_elem_of_6 x y X : {[+ x; y +]} ⊆ X → x ∈ X ∧ y ∈ X.
   Proof. multiset_solver. Qed.
 
+  Lemma test_elem_of_dom x X : x ∈ dom X ↔ x ∈ X.
+  Proof. multiset_solver. Qed.
+
+  (** Tests where the goals do not involve the multiset connectives *)
+  Lemma test_goal_1 x y X : {[+ x +]} ∪ X ⊆ {[+ y +]} → x = y.
+  Proof. multiset_solver. Qed.
+  Lemma test_goal_2 x y X : {[+ x +]} ∪ X ⊆ {[+ y +]} → [x] = [y].
+  Proof. multiset_solver. Qed.
+  Lemma test_goal_3 x y X l :
+    {[+ x +]} ∪ X ⊆ {[+ y +]} → [x] `suffix_of` l ++ [y].
+  Proof.
+    (* [multiset_solver] will first substitute [x]/[y], and then [eauto] is used
+    on the leaf. *)
+    multiset_solver by eauto using suffix_app_r.
+  Qed.
+
   Lemma test_big_1 x1 x2 x3 x4 :
     {[+ x1; x2; x3; x4; x4 +]} ⊆@{gmultiset A} {[+ x1; x1; x2; x3; x4; x4 +]}.
   Proof. multiset_solver. Qed.
@@ -63,6 +91,11 @@ Section test.
     ⊆@{gmultiset A}
       {[+ x1; x1; x2; x3; x4; x4 +]} ⊎ {[+ x5; x5; x6; x7; x9; x8; x8 +]}.
   Proof. multiset_solver. Qed.
+  Lemma test_big_5 x1 x2 x3 x4 x5 x6 x7 x8 x9 :
+    2 *: {[+ x1; x2; x4 +]} ⊎ 2 *: {[+ x5; x6; x7; x8; x8; x9 +]}
+    ⊆@{gmultiset A}
+      {[+ x1; x1; x2; x3; x4; x4; x2 +]} ⊎ 3 *: {[+ x5; x5; x6; x7; x9; x8; x8 +]}.
+  Proof. multiset_solver. Qed.
 
   Lemma test_firstorder_1 (P : A → Prop) x X :
     P x ∧ (∀ y, y ∈ X → P y) ↔ (∀ y, y ∈ {[+ x +]} ⊎ X → P y).

tests/notation.ref

 test_2 = {[10 := {[10 := 1]}; 20 := {[20 := 2]}]}
      : M (M nat)
-test_3 = 
+test_3 =
 {[10 := {[10 := 1]}; 20 := {[20 := 2]}; 30 := {[30 := 3]}]}
      : M (M nat)
-test_4 = 
+test_4 =
 {[10 := {[10 := 1]}; 20 := {[20 := 2]}; 30 := {[30 := 3]}; 40 := {[40 := 4]}]}
      : M (M nat)
-test_op_2 = 
+test_op_2 =
 {[10 := {[10 ^ 2 := 99]}; 10 + 1 := {[10 - 100 := 42 * 1337]}]}
      : M (M nat)
-test_op_3 = 
+test_op_3 =
 {[10 := {[20 - 2 := [11]; 1 := [22]]};
   20 := {[99 + length [1] := [1; 2; 3]]};
   4 := {[4 := [4]]};
   5 := {[5 := [5]]}]}
      : M (M (list nat))
-test_op_4 = 
+test_op_4 =
 {[10 := {[20 - 2 := [11];
           1 := [22];
           3 := [23];
@@ -30,6 +30,6 @@ test_gmultiset_2 = {[+ 10; 11 +]}
      : gmultiset nat
 test_gmultiset_3 = {[+ 10; 11; 2 - 2 +]}
      : gmultiset nat
-test_gmultiset_4 = 
+test_gmultiset_4 =
 {[+ {[+ 10 +]}; ∅; {[+ 2 - 2; 10 +]} +]}
      : gmultiset (gmultiset nat)

tests/notation.v

-From stdpp Require Import base tactics fin_maps gmultiset.
+From stdpp Require Import base tactics fin_maps gmap gmultiset.
 
 (** Test parsing of variants of [(≡)] notation. *)
 Lemma test_equiv_annot_sections `{!Equiv A, !Equivalence (≡@{A})} (x : A) :
@@ -10,7 +10,9 @@ Proof. naive_solver. Qed.
 
 (** Test that notations for maps with multiple elements can be parsed and printed correctly. *)
 Section map_notations.
-  Context `{FinMap nat M}.
+  (* Avoiding section variables so output is not affected by
+  https://github.com/coq/coq/pull/16208 *)
+  Notation M := (gmap nat).
 
   Definition test_2 : M (M nat) := {[ 10 := {[ 10 := 1 ]}; 20 := {[ 20 := 2]} ]}.
   Definition test_3 : M (M nat) := {[ 10 := {[ 10 := 1 ]}; 20 := {[ 20 := 2]};
@@ -18,7 +20,7 @@ Section map_notations.
   Definition test_4 : M (M nat) := {[ 10 := {[ 10 := 1 ]}; 20 := {[ 20 := 2]};
     30 := {[ 30 := 3]}; 40 := {[ 40 := 4 ]} ]}.
 
-  Definition test_op_2 : M (M nat) := {[ 10 := {[pow 10 2 := 99]};
+  Definition test_op_2 : M (M nat) := {[ 10 := {[Nat.pow 10 2 := 99]};
     10 + 1 := {[ 10 - 100 := 42 * 1337 ]} ]}.
 
   Definition test_op_3 : M (M (list nat)) := {[ 10 := {[ 20 - 2 := [11]; 1 := [22] ]};
@@ -48,4 +50,4 @@ Section multiset_notations.
   Print test_gmultiset_2.
   Print test_gmultiset_3.
   Print test_gmultiset_4.
-End multiset_notations.
+End multiset_notations.
\ No newline at end of file

tests/numbers.ref

-le
-     : nat → nat → Prop
-lt
-     : nat → nat → Prop
-le
-     : nat → nat → Prop
-lt
-     : nat → nat → Prop
-le
-     : nat → nat → Prop
-lt
-     : nat → nat → Prop
-le
-     : nat → nat → Prop
-lt
-     : nat → nat → Prop

tests/numbers.v

-From stdpp Require base numbers prelude.
+From stdpp Require Import list.
 
-(** Check that we always get the [le] and [lt] functions on [nat]. *)
-Module test1.
-  Import stdpp.base.
-  Check le.
-  Check lt.
-End test1.
+(** Simple example of measure induction on lists using [Nat.lt_wf_0_projected]. *)
+Fixpoint evens {A} (l : list A) : list A :=
+  match l with
+  | x :: _ :: l => x :: evens l
+  | [x] => [x]
+  | _ => []
+  end.
 
-Module test2.
-  Import stdpp.prelude.
-  Check le.
-  Check lt.
-End test2.
+Fixpoint odds {A} (l : list A) : list A :=
+  match l with
+  | _ :: y :: l => y :: odds l
+  | _ => []
+  end.
 
-Module test3.
-  Import stdpp.numbers.
-  Check le.
-  Check lt.
-End test3.
-
-Module test4.
-  Import stdpp.list.
-  Check le.
-  Check lt.
-End test4.
+Lemma lt_wf_projected_induction_sample {A} (l : list A) :
+  evens l ++ odds l ≡ₚ l.
+Proof.
+  (** Note that we do not use [induction .. using ..]. The term
+  [Nat.lt_wf_0_projected length l] has type [Acc ..], so we perform induction
+  on the [Acc] predicate. *)
+  induction (Nat.lt_wf_0_projected length l) as [l _ IH].
+  destruct l as [|x [|y l]]; simpl; [done..|].
+  rewrite <-Permutation_middle. rewrite IH by (simpl; lia). done.
+Qed.