Sealing of uPred BI layer still causes major slowdowns
This problem occurs both with evarconv ("new" unification, apply:
and friends) and tactic unification ("old" unification, apply
and friends), see:
From iris.base_logic Require Import base_logic.
Goal ∀ (M : ucmra) (OWN : bool → bool → uPred M), ∃ b,
let n := 10 in
(Nat.iter n (λ P, OWN b false ∗ P)%I (OWN b false)
= Nat.iter n (λ P, OWN b false ∗ P)%I (OWN b true)).
Proof.
intros M OWN. eexists _. simpl.
Fail Timeout 4 apply: eq_refl.
Fail Timeout 4 reflexivity.
generalize (@bi_sep (uPred M))=> SEP.
Fail apply: eq_refl. (* immediate *)
Fail reflexivity. (* immediate *)
Abort.
Until n = 6
failure is still immediate. For more the time seems to grow exponentially. For the current n = 10
I am not sure it ever terminates.
This example is generalized from real code where OWN
is some ownership/representation predicate.