From 9aed61c5e3f3ed30eddb5cfdd709894907707cbf 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.

---
 prelude/tactics.v          | 6 +++---
 program_logic/hoare.v      | 2 +-
 program_logic/viewshifts.v | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/prelude/tactics.v b/prelude/tactics.v
index f770fa9e8..9ca44595f 100644
--- a/prelude/tactics.v
+++ b/prelude/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
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 643f92e9c..e9bf2d02f 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -27,7 +27,7 @@ Import uPred.
 
 Global Instance ht_ne E n :
   Proper (dist n ==> eq==>pointwise_relation _ (dist n) ==> dist n) (@ht Λ Σ E).
-Proof. by intros P P' HP e ? <- Φ Φ' HΦ; rewrite /ht HP; setoid_rewrite HΦ. Qed.
+Proof. solve_proper. Qed.
 Global Instance ht_proper E :
   Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (@ht Λ Σ E).
 Proof. by intros P P' HP e ? <- Φ Φ' HΦ; rewrite /ht HP; setoid_rewrite HΦ. Qed.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 8ed30859e..014e0bdb9 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -30,7 +30,7 @@ Qed.
 
 Global Instance vs_ne E1 E2 n :
   Proper (dist n ==> dist n ==> dist n) (@vs Λ Σ E1 E2).
-Proof. by intros P P' HP Q Q' HQ; rewrite /vs HP HQ. Qed.
+Proof. solve_proper. Qed.
 
 Global Instance vs_proper E1 E2 : Proper ((≡) ==> (≡) ==> (≡)) (@vs Λ Σ E1 E2).
 Proof. apply ne_proper_2, _. Qed.
-- 
GitLab