From 1bab53e624a7ba3f6233d49b0a579a4a89d9d079 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 26 Sep 2021 19:49:03 -0400
Subject: [PATCH] f_equiv: for consistency also match target relation in
parametric case
---
theories/tactics.v | 34 +++++++++++++++++++---------------
1 file changed, 19 insertions(+), 15 deletions(-)
diff --git a/theories/tactics.v b/theories/tactics.v
index 7097ce22..7916a602 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -382,21 +382,25 @@ Ltac f_equiv :=
| |- ?R (?f _ _ _ _ _) (?f _ _ _ _ _) => simple apply (_ : Proper (R ==> R ==> R ==> R ==> R ==> R) f)
(* For the case in which R is polymorphic, or an operational type class,
like equiv. *)
- | |- (?R _) (?f _) (?f _) => simple apply (_ : Proper (R _ ==> _) f)
- | |- (?R _ _) (?f _) (?f _) => simple apply (_ : Proper (R _ _ ==> _) f)
- | |- (?R _ _ _) (?f _) (?f _) => simple apply (_ : Proper (R _ _ _ ==> _) f)
- | |- (?R _) (?f _ _) (?f _ _) => simple apply (_ : Proper (R _ ==> R _ ==> _) f)
- | |- (?R _ _) (?f _ _) (?f _ _) => simple apply (_ : Proper (R _ _ ==> R _ _ ==> _) f)
- | |- (?R _ _ _) (?f _ _) (?f _ _) => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> _) f)
- | |- (?R _) (?f _ _ _) (?f _ _ _) => simple apply (_ : Proper (R _ ==> R _ ==> R _ ==> _) f)
- | |- (?R _ _) (?f _ _ _) (?f _ _ _) => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _ ==> _) f)
- | |- (?R _ _ _) (?f _ _ _) (?f _ _ _) => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ R _ _ _ ==> _) f)
- | |- (?R _) (?f _ _ _ _) (?f _ _ _ _) => simple apply (_ : Proper (R _ ==> R _ ==> R _ ==> R _ ==> _) f)
- | |- (?R _ _) (?f _ _ _ _) (?f _ _ _ _) => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _ ==> R _ _ ==> _) f)
- | |- (?R _ _ _) (?f _ _ _ _) (?f _ _ _ _) => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> _) f)
- | |- (?R _) (?f _ _ _ _ _) (?f _ _ _ _ _) => simple apply (_ : Proper (R _ ==> R _ ==> R _ ==> R _ ==> R _ ==> _) f)
- | |- (?R _ _) (?f _ _ _ _ _) (?f _ _ _ _ _) => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _ ==> R _ _ ==> R _ _ ==> _) f)
- | |- (?R _ _ _) (?f _ _ _ _ _) (?f _ _ _ _ _) => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> _) f)
+ | |- (?R _) (?f _) (?f _) => simple apply (_ : Proper (R _ ==> R _) f)
+ | |- (?R _ _) (?f _) (?f _) => simple apply (_ : Proper (R _ _ ==> R _ _) f)
+ | |- (?R _ _ _) (?f _) (?f _) => simple apply (_ : Proper (R _ _ _ ==> R _ _ _) f)
+
+ | |- (?R _) (?f _ _) (?f _ _) => simple apply (_ : Proper (R _ ==> R _ ==> R _) f)
+ | |- (?R _ _) (?f _ _) (?f _ _) => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _) f)
+ | |- (?R _ _ _) (?f _ _) (?f _ _) => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> R _ _ _) f)
+
+ | |- (?R _) (?f _ _ _) (?f _ _ _) => simple apply (_ : Proper (R _ ==> R _ ==> R _ ==> R _) f)
+ | |- (?R _ _) (?f _ _ _) (?f _ _ _) => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _ ==> R _ _) f)
+ | |- (?R _ _ _) (?f _ _ _) (?f _ _ _) => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _) f)
+
+ | |- (?R _) (?f _ _ _ _) (?f _ _ _ _) => simple apply (_ : Proper (R _ ==> R _ ==> R _ ==> R _ ==> R _) f)
+ | |- (?R _ _) (?f _ _ _ _) (?f _ _ _ _) => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _ ==> R _ _ ==> R _ _) f)
+ | |- (?R _ _ _) (?f _ _ _ _) (?f _ _ _ _) => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _) f)
+
+ | |- (?R _) (?f _ _ _ _ _) (?f _ _ _ _ _) => simple apply (_ : Proper (R _ ==> R _ ==> R _ ==> R _ ==> R _ ==> R _) f)
+ | |- (?R _ _) (?f _ _ _ _ _) (?f _ _ _ _ _) => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _ ==> R _ _ ==> R _ _ ==> R _ _) f)
+ | |- (?R _ _ _) (?f _ _ _ _ _) (?f _ _ _ _ _) => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _) f)
(* Next, try to infer the relation. Unfortunately, very often, it will turn
the goal into a Leibniz equality so we get stuck. *)
(* TODO: Can we exclude that instance? *)
--
GitLab