eauto very slow when there is a chain of Iris quantifiers
Steps to reproduce:
- Change the
iIntros
hints inltac_tactics.v
toiIntros (?).
andiIntros "?".
. - Compile
ectx_lifting.v
wp_lift_atomic_head_step_no_fork
takes forever:
Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
to_val e1 = None →
(∀ σ1, state_interp σ1 ={E}=∗
⌜head_reducible e1 σ1⌝ ∗
▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
⌜efs = []⌝ ∗ state_interp σ2 ∗ default False (to_val e2) Φ)
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_atomic_head_step. done.
(* now it gets slow *) eauto.
Something seems to be exponential in the number of quantifiers. We currently use iIntros.
to introduce them all at once but that's more of a work-around. I can't even really figure out what is taking so long, but I can definitely see tons of FromAssumption
in the trace.