From 6fe27bb507e22b80d02683db4e689eb6752d9295 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 25 Feb 2016 11:47:49 +0100
Subject: [PATCH] improve f_equiv and solve_proper; use them in a few more
places
---
theories/tactics.v | 17 ++++++++++++++---
1 file changed, 14 insertions(+), 3 deletions(-)
diff --git a/theories/tactics.v b/theories/tactics.v
index ba6fe7a8..746fec70 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -257,22 +257,28 @@ Ltac f_equiv :=
let H := fresh "Proper" in
assert (Proper (R ==> R ==> R) f) as H by (eapply _);
apply H; clear H; f_equiv
- (* Next, try to infer the relation *)
+ (* 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? *)
(* TODO: If some of the arguments are the same, we could also
query for "pointwise_relation"'s. But that leads to a combinatorial
explosion about which arguments are and which are not the same. *)
| |- ?R (?f ?x) (?f _) =>
- let R1 := fresh "R" in let H := fresh "Proper" in
+ let R1 := fresh "R" in let H := fresh "HProp" in
let T := type of x in evar (R1: relation T);
assert (Proper (R1 ==> R) f) as H by (subst R1; eapply _);
subst R1; apply H; clear H; f_equiv
| |- ?R (?f ?x ?y) (?f _ _) =>
let R1 := fresh "R" in let R2 := fresh "R" in
- let H := fresh "Proper" in
+ let H := fresh "HProp" in
let T1 := type of x in evar (R1: relation T1);
let T2 := type of y in evar (R2: relation T2);
assert (Proper (R1 ==> R2 ==> R) f) as H by (subst R1 R2; eapply _);
subst R1 R2; apply H; clear H; f_equiv
+ (* In case the function symbol differs, but the arguments are the same,
+ maybe we have a pointwise_relation in our context. *)
+ | H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) =>
+ apply H; f_equiv
end | idtac (* Let the user solve this goal *)
].
@@ -289,6 +295,10 @@ Ltac solve_proper :=
end;
(* Unfold the head symbol, which is the one we are proving a new property about *)
lazymatch goal with
+ | |- ?R (?f _ _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _ _) => unfold f
+ | |- ?R (?f _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _) => unfold f
+ | |- ?R (?f _ _ _ _ _ _) (?f _ _ _ _ _ _) => unfold f
+ | |- ?R (?f _ _ _ _ _) (?f _ _ _ _ _) => unfold f
| |- ?R (?f _ _ _ _) (?f _ _ _ _) => unfold f
| |- ?R (?f _ _ _) (?f _ _ _) => unfold f
| |- ?R (?f _ _) (?f _ _) => unfold f
@@ -296,6 +306,7 @@ Ltac solve_proper :=
end;
solve [ f_equiv ].
+
(** Given a tactic [tac2] generating a list of terms, [iter tac1 tac2]
runs [tac x] for each element [x] until [tac x] succeeds. If it does not
suceed for any element of the generated list, the whole tactic wil fail. *)
--
GitLab