tests/notation.ref

+test_2 = {[10 := {[10 := 1]}; 20 := {[20 := 2]}]}
+     : M (M nat)
+test_3 =
+{[10 := {[10 := 1]}; 20 := {[20 := 2]}; 30 := {[30 := 3]}]}
+     : M (M nat)
+test_4 =
+{[10 := {[10 := 1]}; 20 := {[20 := 2]}; 30 := {[30 := 3]}; 40 := {[40 := 4]}]}
+     : M (M nat)
+test_op_2 =
+{[10 := {[10 ^ 2 := 99]}; 10 + 1 := {[10 - 100 := 42 * 1337]}]}
+     : M (M nat)
+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 =
+{[10 := {[20 - 2 := [11];
+          1 := [22];
+          3 := [23];
+          4 := [1; 2; 3; 4; 5; 6; 7; 8; 9]]};
+  20 := {[99 + length [1] := [1; 2; 3]]};
+  4 := {[4 := [4]]};
+  5 := {[5 := [5]]}]}
+     : M (M (list nat))
+test_gmultiset_1 = {[+ 10 +]}
+     : gmultiset nat
+test_gmultiset_2 = {[+ 10; 11 +]}
+     : gmultiset nat
+test_gmultiset_3 = {[+ 10; 11; 2 - 2 +]}
+     : gmultiset nat
+test_gmultiset_4 =
+{[+ {[+ 10 +]}; ∅; {[+ 2 - 2; 10 +]} +]}
+     : gmultiset (gmultiset nat)

tests/notation.v

-From stdpp Require Import base tactics.
+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) :
@@ -7,3 +7,47 @@ Lemma test_equiv_annot_sections `{!Equiv A, !Equivalence (≡@{A})} (x : A) :
   ( x ≡@{A} x) ∧ ( x ≡.) x ∧
   (x ≡@{A} x ) ∧ (≡@{A} ) x x ∧ (.≡ x ) x.
 Proof. naive_solver. Qed.
+
+(** Test that notations for maps with multiple elements can be parsed and printed correctly. *)
+Section map_notations.
+  (* 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]};
+    30 := {[ 30 := 3]} ]}.
+  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 := {[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] ]};
+    20 := {[ 99 + length ([1]) := [1;2;3] ]}; 4 := {[ 4:=[4] ]} ; 5 := {[ 5 := [5] ]} ]}.
+
+  Definition test_op_4 : M (M (list nat)) :=
+    ({[ 10 := {[ 20 - 2 := [11]; 1 := [22]; 3 := [23]; 4:=[1;2;3;4;5;6;7;8;9]]};
+      20 := {[ 99 + length ([1]) := [1;2;3] ]}; 4 := {[ 4:=[4] ]} ; 5 := {[ 5 := [5] ]} ]}).
+
+  Print test_2.
+  Print test_3.
+  Print test_4.
+  Print test_op_2.
+  Print test_op_3.
+  Print test_op_4.
+End map_notations.
+
+(** Test that notations for maps with multiple elements can be parsed and printed correctly. *)
+Section multiset_notations.
+  Definition test_gmultiset_1 : gmultiset nat := {[+ 10 +]}.
+  Definition test_gmultiset_2 : gmultiset nat := {[+ 10; 11 +]}.
+  Definition test_gmultiset_3 : gmultiset nat := {[+ 10; 11; 2 - 2 +]}.
+  Definition test_gmultiset_4 : gmultiset (gmultiset nat) :=
+    {[+ {[+ 10 +]}; ∅; {[+ 2 - 2; 10 +]} +]}.
+
+  Print test_gmultiset_1.
+  Print test_gmultiset_2.
+  Print test_gmultiset_3.
+  Print test_gmultiset_4.
+End multiset_notations.

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.

tests/numbers_import.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_import.v

+From stdpp Require base numbers prelude.
+
+(** Check that we always get the [le] and [lt] functions on [nat]. *)
+Module test1.
+  Import stdpp.base.
+  Check le.
+  Check lt.
+End test1.
+
+Module test2.
+  Import stdpp.prelude.
+  Check le.
+  Check lt.
+End test2.
+
+Module test3.
+  Import stdpp.numbers.
+  Check le.
+  Check lt.
+End test3.
+
+Module test4.
+  Import stdpp.list.
+  Check le.
+  Check lt.
+End test4.

tests/pretty.v

+From stdpp Require Import pretty.
+From Coq Require Import Ascii.
+
+Section N.
+  Local Open Scope N_scope.
+
+  Lemma pretty_N_0 : pretty 0 = "0".
+  Proof. reflexivity. Qed.
+  Lemma pretty_N_1 : pretty 1 = "1".
+  Proof. reflexivity. Qed.
+  Lemma pretty_N_9 : pretty 9 = "9".
+  Proof. reflexivity. Qed.
+  Lemma pretty_N_10 : pretty 10 = "10".
+  Proof. reflexivity. Qed.
+  Lemma pretty_N_100 : pretty 100 = "100".
+  Proof. reflexivity. Qed.
+  Lemma pretty_N_123456789 : pretty 123456789 = "123456789".
+  Proof. reflexivity. Qed.
+End N.
+
+(** Minimized version of:
+
+  https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Stack.20overflow.20in.20Qed.2E
+
+Fixed by making the [wp_guard] in [pretty_N_go] proportional to the
+size of the input so that it blocks in case the input is an open term. *)
+Lemma test_no_stack_overflow p n :
+  String.get n (pretty (N.pos p)) ≠ Some "_"%char →
+  String.get (S n) ("-" +:+ pretty (N.pos p)) ≠ Some "_"%char.
+Proof. intros Hlem. apply Hlem. Qed.
+
+Section nat.
+  Local Open Scope nat_scope.
+
+  Lemma pretty_nat_0 : pretty 0 = "0".
+  Proof. reflexivity. Qed.
+  Lemma pretty_nat_1 : pretty 1 = "1".
+  Proof. reflexivity. Qed.
+  Lemma pretty_nat_9 : pretty 9 = "9".
+  Proof. reflexivity. Qed.
+  Lemma pretty_nat_10 : pretty 10 = "10".
+  Proof. reflexivity. Qed.
+  Lemma pretty_nat_100 : pretty 100 = "100".
+  Proof. reflexivity. Qed.
+  Lemma pretty_nat_1234 : pretty 1234 = "1234".
+  Proof. reflexivity. Qed.
+End nat.
+
+Section Z.
+  Local Open Scope Z_scope.
+
+  Lemma pretty_Z_0 : pretty 0 = "0".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_1 : pretty 1 = "1".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_9 : pretty 9 = "9".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_10 : pretty 10 = "10".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_100 : pretty 100 = "100".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_123456789 : pretty 123456789 = "123456789".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_opp_1 : pretty (-1) = "-1".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_opp_9 : pretty (-9) = "-9".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_opp_10 : pretty (-10) = "-10".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_opp_100 : pretty (-100) = "-100".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_opp_123456789 : pretty (-123456789) = "-123456789".
+  Proof. reflexivity. Qed.
+End Z.
\ No newline at end of file

tests/proper.v

+From stdpp Require Import prelude fin_maps propset.
+
+Global Instance from_option_proper_test1 `{Equiv A} {B} (R : relation B) (f : A → B) :
+  Proper ((≡) ==> R) f → Proper (R ==> (≡) ==> R) (from_option f).
+Proof. apply _. Qed.
+Global Instance from_option_proper_test2 `{Equiv A} {B} (R : relation B) (f : A → B) :
+  Proper ((≡) ==> R) f → Proper (R ==> (≡) ==> R) (from_option f).
+Proof. solve_proper. Qed.
+
+Section map_tests.
+  Context `{FinMap K M} `{Equiv A}.
+
+  (** For higher-order functions on maps (like [map_with_with], [fmap], etc)
+  we use "higher-order [Proper] instances" [Proper ((≡) ==> (≡)) ==> ...)]
+  that also allow the function to differ. We test that we can derive simpler
+  [Proper]s for a fixed function using both type class inference ([apply _])
+  and std++'s [solve_proper] tactic. *)
+  Global Instance map_alter_proper_test (f : A → A) i :
+    Proper ((≡) ==> (≡)) f →
+    Proper ((≡) ==> (≡)) (alter (M:=M A) f i).
+  Proof.
+    apply _.
+  Restart. Proof.
+    solve_proper.
+  Abort.
+  Global Instance map_zip_proper_test `{Equiv B} :
+    Proper ((≡@{M A}) ==> (≡@{M B}) ==> (≡@{M (A * B)})) map_zip.
+  Proof.
+    apply _.
+  Restart. Proof.
+    solve_proper.
+  Abort.
+  Global Instance map_zip_with_proper_test `{Equiv B, Equiv C} (f : A → B → C) :
+    Proper ((≡) ==> (≡) ==> (≡)) f →
+    Proper ((≡) ==> (≡) ==> (≡)) (map_zip_with (M:=M) f).
+  Proof.
+    apply _.
+  Restart. Proof.
+    solve_proper.
+  Abort.
+  Global Instance map_fmap_proper_test `{Equiv B} (f : A → B) :
+    Proper ((≡) ==> (≡)) f →
+    Proper ((≡) ==> (≡@{M _})) (fmap f).
+  Proof.
+    apply _.
+  Restart. Proof.
+    solve_proper.
+  Abort.
+  Global Instance map_omap_proper_test `{Equiv B} (f : A → option B) :
+    Proper ((≡) ==> (≡)) f →
+    Proper ((≡) ==> (≡@{M _})) (omap f).
+  Proof.
+    apply _.
+  Restart. Proof.
+    solve_proper.
+  Abort.
+End map_tests.
+
+(** And similarly for lists *)
+Global Instance list_alter_proper_test `{!Equiv A} (f : A → A) i :
+  Proper ((≡) ==> (≡)) f →
+  Proper ((≡) ==> (≡)) (alter (M:=list A) f i).
+Proof.
+  apply _.
+Restart. Proof.
+  solve_proper.
+Abort.
+Global Instance list_fmap_proper_test `{!Equiv A, !Equiv B} (f : A → B) :
+  Proper ((≡) ==> (≡)) f → Proper ((≡@{list A}) ==> (≡)) (fmap f).
+Proof.
+  apply _.
+Restart. Proof.
+  solve_proper.
+Abort.
+Global Instance list_bind_proper_test `{!Equiv A, !Equiv B} (f : A → list B) :
+  Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (mbind f).
+Proof.
+  apply _.
+Restart. Proof.
+  solve_proper.
+Abort.
+Global Instance mapM_proper_test `{!Equiv A, !Equiv B} (f : A → option B) :
+  Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (mapM f).
+Proof.
+  apply _.
+Restart. Proof.
+  solve_proper.
+Abort.
+
+Lemma test_prod_equivalence (X1 X2 X3 Y : propset nat * propset nat) :
+  X3 ≡ X2 → X2 ≡ X1 → (X1,Y) ≡ (X3,Y).
+Proof. intros H1 H2. by rewrite H1, <-H2. Qed.

tests/propset.v

+From stdpp Require Import propset.
+
+Lemma diagonal : {[ (a,b) : nat * nat | a = b ]} ≡ (λ x, (x,x)) <$> ⊤.
+Proof. set_unfold. intros []. naive_solver. Qed.
+
+Lemma diagonal2 : {[ (a,b) | a =@{nat} b ]} ≡ {[ x | x.1 = x.2 ]}.
+Proof. set_unfold. intros []. naive_solver. Qed.
+
+Lemma firstis42 : {[ (x, _) : nat * nat | x = 42 ]} ≡ (42,.) <$> ⊤.
+Proof. set_unfold. intros []. naive_solver. Qed.
+
+Inductive foo := Foo (n : nat).
+
+Definition set_of_positive_foos : {[ Foo x | x ≠ 0 ]} ≡ Foo <$> (Pos.to_nat <$> ⊤).
+Proof.
+  set_unfold. intros [[]]; naive_solver by (rewrite SuccNat2Pos.id_succ || lia).
+Qed.
+
+Lemma simple_pattern_does_not_match : {[ x : nat | x = x]} = PropSet (λ x, x = x).
+Proof. exact eq_refl. Qed.

tests/sets.v

-From stdpp Require Import sets.
+From stdpp Require Import sets gmap.
 
 Lemma foo `{Set_ A C} (x : A) (X Y : C) : x ∈ X ∩ Y → x ∈ X.
 Proof. intros Hx. set_unfold in Hx. tauto. Qed.
+
+(** Test [set_unfold_list_bind]. *)
+Lemma elem_of_list_bind_again {A B} (x : B) (l : list A) f :
+  x ∈ l ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ l.
+Proof. set_solver. Qed.
+
+(** Should not leave any evars, see issue #163 *)
+Goal {[0]} ∪ dom (∅ : gmap nat nat) ≠ ∅.
+Proof. set_solver. Qed.
+
+(** Check that [set_solver] works with [set_Exists] and [set_Forall]. Test cases
+from issue #178. *)
+Lemma set_Exists_set_solver : set_Exists (.= 10) ({[ 10 ]} : gset nat).
+Proof. set_solver. Qed.
+
+Lemma set_Forall_set_solver `{Set_ A C} (X : C) x : set_Forall (.≠ x) X ↔ x ∉ X.
+Proof. set_solver. Qed.
+
+Lemma set_guard_case_guard `{MonadSet M} `{Decision P} A (x : A) (X : M A) :
+  x ∈ (guard P;; X) ↔ P ∧ x ∈ X.
+Proof.
+  (* Test that [case_guard] works for sets and indeed generates two goals *)
+  case_guard; [set_solver|set_solver].
+Restart. Proof.
+  (* Test that [set_solver] supports [guard]. *)
+  set_solver.
+Qed.

tests/solve_ndisj.v

 From stdpp Require Import namespaces strings.
 
-Lemma test1 (N1 N2 : namespace) :
+Section tests.
+Implicit Types (N : namespace) (E : coPset).
+
+Lemma test1 N1 N2 :
   N1 ## N2 → ↑N1 ⊆@{coPset} ⊤ ∖ ↑N2.
 Proof. solve_ndisj. Qed.
 
-Lemma test2 (N1 N2 : namespace) :
+Lemma test2 N1 N2 :
   N1 ## N2 → ↑N1.@"x" ⊆@{coPset} ⊤ ∖ ↑N1.@"y" ∖ ↑N2.
 Proof. solve_ndisj. Qed.
 
-Lemma test3 (N : namespace) :
+Lemma test3 N :
   ⊤ ∖ ↑N ⊆@{coPset} ⊤ ∖ ↑N.@"x".
 Proof. solve_ndisj. Qed.
 
-Lemma test4 (N : namespace) :
+Lemma test4 N :
   ⊤ ∖ ↑N ⊆@{coPset} ⊤ ∖ ↑N.@"x" ∖ ↑N.@"y".
 Proof. solve_ndisj. Qed.
 
-Lemma test5 (N1 N2 : namespace) :
+Lemma test5 N1 N2 :
   ⊤ ∖ ↑N1 ∖ ↑N2 ⊆@{coPset} ⊤ ∖ ↑N1.@"x" ∖ ↑N2 ∖ ↑N1.@"y".
 Proof. solve_ndisj. Qed.
+
+Lemma test_ndisjoint_difference_l N : ⊤ ∖ ↑N ##@{coPset} ↑N.
+Proof. solve_ndisj. Qed.
+Lemma test_ndisjoint_difference_r N : ↑N ##@{coPset} ⊤ ∖ ↑N.
+Proof. solve_ndisj. Qed.
+
+Lemma test6 E N :
+  ↑N ⊆ E → ↑N ⊆ ⊤ ∖ (E ∖ ↑N).
+Proof. solve_ndisj. Qed.
+
+Lemma test7 N :
+  ↑N ⊆@{coPset} ⊤ ∖ ∅.
+Proof. solve_ndisj. Qed.
+
+Lemma test8 N1 N2 :
+  ⊤ ∖ (↑N1 ∪ ↑N2) ⊆@{coPset} ⊤ ∖ ↑N1.@"counter".
+Proof. solve_ndisj. Qed.
+
+Lemma test9 N1 N2 :
+  ⊤ ∖ (↑N1 ∪ ↑N2) ⊆@{coPset} ⊤ ∖ ↑N1.@"counter" ∖ ↑N1.@"state" ∖ ↑N2.
+Proof. solve_ndisj. Qed.
+
+Lemma test10 N1 N2 E :
+  ↑N1 ∪ E ## ⊤ ∖ ↑N1 ∖ ↑N2 ∖ E.
+Proof. solve_ndisj. Qed.
+
+Lemma test11 N :
+  ↑N.@"other" ⊆@{coPset} ⊤ ∖ (↑N.@"this" ∪ ↑N.@"that").
+Proof. solve_ndisj. Qed.
+
+Lemma test12 N :
+  ↑N.@"other" ##@{coPset} ↑N.@"this" ∪ ↑N.@"that" ∧
+  ↑N.@"other" ∪ ↑N.@"this" ##@{coPset} ↑N.@"that".
+Proof. split; solve_ndisj. Qed.
+
+Lemma test13 E N :
+  ↑N ⊆ E →
+  ⊤ ∖ E ⊆ ⊤ ∖ (E ∖ ↑N) ∖ ↑N.
+Proof. solve_ndisj. Qed.

tests/solve_proper.v

-From stdpp Require Import prelude.
-
-(** Some tests for solve_proper. *)
-Section tests.
-  Context {A B : Type} `{!Equiv A, !Equiv B}.
-  Context (foo : A → A) (bar : A → B) (baz : B → A → A).
-  Context `{!Proper ((≡) ==> (≡)) foo,
-            !Proper ((≡) ==> (≡)) bar,
-            !Proper ((≡) ==> (≡) ==> (≡)) baz}.
-
-  Definition test1 (x : A) := baz (bar (foo x)) x.
-  Global Instance : Proper ((≡) ==> (≡)) test1.
-  Proof. solve_proper. Qed.
-
-  Definition test2 (b : bool) (x : A) :=
-    if b then bar (foo x) else bar x.
-  Global Instance : ∀ b, Proper ((≡) ==> (≡)) (test2 b).
-  Proof. solve_proper. Qed.
-
-  Definition test3 (f : nat → A) :=
-    baz (bar (f 0)) (f 2).
-  Global Instance : Proper (pointwise_relation nat (≡) ==> (≡)) test3.
-  Proof. solve_proper. Qed.
-End tests.

tests/strings.ref

+"foo"
+     : string
+"foo"
+     : string
+10 =? 10
+     : bool
+[10] ++ [12]
+     : list nat
+("foo" =? "bar")%string
+     : bool
+String.app "foo" "bar"
+     : string
+String.app
+     : string → string → string
+("a" ≤ "b")%string
+     : Prop
+     = true
+     : bool
+     = ["A"; "a"; "b"; "c"]
+     : list string

tests/strings.v

+From stdpp Require Import strings sorting.
+From Coq Require Ascii.
+
+(** Check that the string notation works without [%string]. *)
+Check "foo".
+
+(** And also with [%string], which should not be pretty printed) *)
+Check "foo"%string.
+
+(** Check that importing [strings] does not override notations for [nat] and
+[list]. *)
+Check (10 =? 10).
+Check ([10] ++ [12]).
+
+Check ("foo" =? "bar")%string.
+
+(** Check that append on strings is pretty printed correctly, and not as
+[(_ ++ _)%string]. *)
+Check ("foo" +:+ "bar").
+
+(** Should print as [String.app] *)
+Check String.app.
+
+(** Test notations and type class instances for [≤] *)
+Check ("a" ≤ "b")%string.
+Compute bool_decide ("a" ≤ "b")%string.
+
+(** Make sure [merge_sort] computes (which implies the [Decision] instances
+are correct. *)
+Compute merge_sort (≤)%string ["b"; "a"; "c"; "A"].
+
+(** And that we can prove it actually sorts (which implies the order-related
+instances are correct. *)
+Lemma test_merge_sort l :
+  StronglySorted (≤)%string (merge_sort (≤)%string l) ∧
+  merge_sort (≤)%string l ≡ₚ l.
+Proof.
+  split.
+  - apply (StronglySorted_merge_sort _).
+  - apply merge_sort_Permutation.
+Qed.

tests/tactics.ref

@@ -4,3 +4,70 @@ The command has indeed failed with message:
 Failed to progress.
 The command has indeed failed with message:
 Failed to progress.
+1 goal
+  
+  n : nat
+  H' : even n
+  ============================
+  even n
+"inv_test_num"
+     : string
+1 goal
+  
+  n : nat
+  H : True
+  H' : even n
+  ============================
+  even n
+1 goal
+  
+  n : nat
+  H : True
+  H' : even n
+  ============================
+  even n
+"otest"
+     : string
+The command has indeed failed with message:
+Cannot infer this placeholder of type "nat" in
+environment:
+P, Q, R : nat → Prop
+HPQR1 : ∀ m n : nat, P n → Q m → R (n + m)
+HPQR2 : ∀ m n : nat, P n → Q m → R (n + m) ∧ R 2
+HP0 : P 0
+HP1 : P 1
+HQ : Q 5
+The command has indeed failed with message:
+Tactic failure: ospecialize can only specialize a local hypothesis;
+use opose proof instead.
+"oinversion_test1"
+     : string
+1 goal
+  
+  n : nat
+  H : even (2 + n)
+  n' : nat
+  Hn' : even n
+  EQ : n' = n
+  ============================
+  even n
+"oinv_test2"
+     : string
+1 goal
+  
+  n : nat
+  H' : even n
+  ============================
+  even n
+1 goal
+  
+  n : nat
+  H' : even n
+  ============================
+  even n
+"notypeclasses_apply_error"
+     : string
+The command has indeed failed with message:
+The reference notypeclasses was not found in the current environment.
+The command has indeed failed with message:
+No such assumption.

tests/tactics.v

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