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'.

stdpp_unstable/dune

+(include_subdirs qualified)
+(coq.theory
+ (name stdpp.unstable)
+ (package coq-stdpp-unstable)
+ (theories stdpp stdpp.bitvector))

test-normalizer.sed

+# locations in Fail added in https://github.com/coq/coq/pull/15174
+/^File/d

tests/ascii.ref

+"a"
+     : string
+"a"%char
+     : ascii
+"a"
+     : ascii
+"a"%stdpp
+     : string

tests/ascii.v

+From stdpp Require Import strings.
+From Coq Require Import Ascii.
+
+Check "a". (* should be string *)
+
+Check "a"%char. (* should be ascii *)
+
+Open Scope char_scope.
+
+Check "a". (* should be ascii *)
+Check "a"%string. (* should be string *)

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/eunify.ref

+"eunify_test"
+     : string
+The command has indeed failed with message:
+No matching clauses for match.
+((fix add (n m : nat) {struct n} : nat :=
+    match n with
+    | 0 => m
+    | S p => S (add p m)
+    end) x y)
+"eunify_test_evars"
+     : string
+The command has indeed failed with message:
+No matching clauses for match.

tests/eunify.v

+From stdpp Require Import tactics strings.
+Unset Mangle Names.
+
+Check "eunify_test".
+Lemma eunify_test : ∀ x y, 0 < S x + y.
+Proof.
+  intros x y.
+  (* Test that Ltac matching fails, otherwise this test is pointless *)
+  Fail
+    match goal with
+    | |- 0 < S _ => idtac
+    end.
+  (* [eunify] succeeds *)
+  match goal with
+  | |- 0 < ?x => eunify x (S _)
+  end.
+  match goal with
+  | |- 0 < ?x => let y := open_constr:(_) in eunify x (S y); idtac y
+  end.
+  lia.
+Qed.
+
+Check "eunify_test_evars".
+Lemma eunify_test_evars : ∃ x y, 0 < S x + y.
+Proof.
+  eexists _, _.
+  (* Test that Ltac matching fails, otherwise this test is pointless *)
+  Fail
+    match goal with
+    | |- 0 < S _ => idtac
+    end.
+  (* [eunify] succeeds even if the goal contains evars *)
+  match goal with
+  | |- 0 < ?x => eunify x (S _)
+  end.
+  (* Let's try to use [eunify] to instantiate the first evar *)
+  match goal with
+  | |- 0 < ?x => eunify x (1 + _)
+  end.
+  (* And the other evar *)
+  match goal with
+  | |- 0 < ?x => eunify x 2
+  end.
+  lia.
+Qed.

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 (<[i:=x]> (<[j:=y]> (∅ : M A))).
+  Proof. set_solver. Qed.
+
+  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/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.