From 4f836b8eaf6372f90ff43789a2a9e1f7ba9509f9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 27 Sep 2021 11:04:53 -0400
Subject: [PATCH] adjust for f_equiv optimizations

---
 iris/algebra/ofe.v              | 4 +++-
 iris/program_logic/weakestpre.v | 3 ---
 iris_heap_lang/proofmode.v      | 2 +-
 3 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index df78c64fe..b2c909d26 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -261,7 +261,9 @@ Ltac f_contractive :=
   | |- @dist_later ?A _ ?n ?x ?y =>
          destruct n as [|n]; [exact I|change (@dist A _ n x y)]
   end;
-  try simple apply reflexivity.
+  (* Only try reflexivity if the terms are syntactically equal. This avoids
+     very expensive failing unification. *)
+  try match goal with  |- _ ?x ?x => simple apply reflexivity end.
 
 Ltac solve_contractive :=
   solve_proper_core ltac:(fun _ => first [f_contractive | f_equiv]).
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index b918c2933..733294c4a 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -100,9 +100,6 @@ Global Instance wp_ne s E e n :
 Proof.
   revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
   rewrite !wp_unfold /wp_pre /=.
-  (* FIXME: figure out a way to properly automate this proof *)
-  (* FIXME: reflexivity, as being called many times by f_equiv and f_contractive
-  is very slow here *)
   do 24 (f_contractive || f_equiv).
   (* FIXME : simplify this proof once we have a good definition and a
      proper instance for step_fupdN. *)
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 2d78d4319..9d44d43ee 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -473,7 +473,7 @@ Lemma tac_twp_cmpxchg_fail Δ s E i K l q v v1 v2 Φ :
 Proof.
   rewrite envs_entails_eq. intros. rewrite -twp_bind.
   eapply wand_apply; first exact: twp_cmpxchg_fail.
-  rewrite envs_lookup_split //=. by do 2 f_equiv.
+  rewrite envs_lookup_split //=. simpl. by do 2 f_equiv.
 Qed.
 
 Lemma tac_wp_cmpxchg_suc Δ Δ' s E i K l v v1 v2 Φ :
-- 
GitLab