From 8e8305ce2f8b006855faac80fd731570f26a6b73 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 31 May 2016 16:12:09 +0200
Subject: [PATCH] Make f_equiv slightly more robust.
Now, for example, when having equiv (Some x) (Some y) it will
try to find a Proper whose range is an equiv before hitting the
eq instance. My hack is general enough that it works for Forall2,
dist, and so on, too.
---
theories/tactics.v | 20 ++++++++++++++------
1 file changed, 14 insertions(+), 6 deletions(-)
diff --git a/theories/tactics.v b/theories/tactics.v
index 0e0adb0e..43155ebf 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -251,8 +251,10 @@ Ltac setoid_subst :=
end.
(** f_equiv works on goals of the form "f _ = f _", for any relation and any
- number of arguments. It looks for an appropriate "Proper" instance, and
- applies it. *)
+number of arguments. It looks for an appropriate "Proper" instance, and applies
+it. The tactic is somewhat limited, since it cannot be used to backtrack on
+the Proper instances that has been found. To that end, we try to ensure the
+trivial instance in which the resulting goals have an [eq]. *)
Ltac f_equiv :=
match goal with
| _ => reflexivity
@@ -263,10 +265,16 @@ Ltac f_equiv :=
| |- ?R (match ?x with _ => _ end) (match ?x with _ => _ end) =>
destruct x
(* First assume that the arguments need the same relation as the result *)
- | |- ?R (?f ?x) (?f _) =>
- apply (_ : Proper (R ==> R) f)
- | |- ?R (?f ?x ?y) (?f _ _) =>
- apply (_ : Proper (R ==> R ==> R) f)
+ | |- ?R (?f ?x) (?f _) => apply (_ : Proper (R ==> R) f)
+ (* For the case in which R is polymorphic, or an operational type class,
+ like equiv. *)
+ | |- (?R _) (?f ?x) (?f _) => apply (_ : Proper (R _ ==> _) f)
+ | |- (?R _ _) (?f ?x) (?f _) => apply (_ : Proper (R _ _ ==> _) f)
+ | |- (?R _ _ _) (?f ?x) (?f _) => apply (_ : Proper (R _ _ _ ==> _) f)
+ | |- (?R _) (?f ?x ?y) (?f _ _) => apply (_ : Proper (R _ ==> R _ ==> _) f)
+ | |- (?R _ _) (?f ?x ?y) (?f _ _) => apply (_ : Proper (R _ _ ==> R _ _ ==> _) f)
+ | |- (?R _ _ _) (?f ?x ?y) (?f _ _) => apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> _) f)
+ | |- (?R _ _ _ _) (?f ?x ?y) (?f _ _) => apply (_ : Proper (R _ _ _ _ ==> R _ _ _ _ ==> _) f)
(* Next, try to infer the relation. Unfortunately, there is an instance
of Proper for (eq ==> _), which will always be matched. *)
(* TODO: Can we exclude that instance? *)
--
GitLab