From d3c2c3e8f895792985130a8a1b93bcae66fe2fad Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 25 Feb 2016 12:01:39 +0100
Subject: [PATCH] more f_equiv work.
---
theories/tactics.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/theories/tactics.v b/theories/tactics.v
index ce536877..6f9cf631 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -236,17 +236,17 @@ Ltac f_equiv :=
try lazymatch goal with
| |- pointwise_relation _ _ _ _ => intros ?
end;
+ (* Normalize away equalities. *)
+ subst;
(* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
first [ reflexivity | assumption | symmetry; assumption |
match goal with
(* We support matches on both sides, *if* they concern the same
- or provably equal variables.
+ variable.
TODO: We should support different variables, provided that we can
derive contradictions for the off-diagonal cases. *)
| |- ?R (match ?x with _ => _ end) (match ?x with _ => _ end) =>
destruct x; f_equiv
- | |- ?R (match ?x with _ => _ end) (match ?y with _ => _ end) =>
- subst y; f_equiv
(* First assume that the arguments need the same relation as the result *)
| |- ?R (?f ?x) (?f _) =>
let H := fresh "Proper" in
--
GitLab