From 8323568a8ab1b7ed915bdae1cd79db0053f6f1ef Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 11 Aug 2022 13:57:13 -0400
Subject: [PATCH] add some very basic f_equiv tests

---
 tests/proper.ref |  2 ++
 tests/proper.v   | 32 +++++++++++++++++++++++++++++++-
 2 files changed, 33 insertions(+), 1 deletion(-)

diff --git a/tests/proper.ref b/tests/proper.ref
index e69de29b..e54b63c7 100644
--- a/tests/proper.ref
+++ b/tests/proper.ref
@@ -0,0 +1,2 @@
+The command has indeed failed with message:
+No such assumption.
diff --git a/tests/proper.v b/tests/proper.v
index 36249631..79195a13 100644
--- a/tests/proper.v
+++ b/tests/proper.v
@@ -1,6 +1,36 @@
 From stdpp Require Import prelude fin_maps propset.
 
-(** Some tests for solve_proper. *)
+(** Some tests for f_equiv. *)
+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.
+    intros. f_equiv. assumption.
+  Qed.
+End f_equiv.
+
+(** Some tests for solve_proper (also testing f_equiv indirectly). *)
 Section tests.
   Context {A B : Type} `{!Equiv A, !Equiv B}.
   Context (foo : A → A) (bar : A → B) (baz : B → A → A).
-- 
GitLab