Can't iSpecialize/iDestruct with (("A" with "B") with "C")
iSpecialize (("HLT" with "Hg") with "HL").
fails with
Error:
In nested Ltac calls to "iSpecialize (open_constr)", "iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)" and
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)", last call failed.
Tactic failure: iSpecialize: ("HLT" with "Hg") should be a hypothesis, use iPoseProof instead.
While that's technically true, it seems unfortunate, and forces me to call two tactics for the job. I end up writing
iSpecialize ("HLT" with "Hg"); iDestruct ("HLT" with "HL") as "#HLT1"; auto.
instead of iDestruct (("HLT" with "Hg") with "HL") as "#HLT1"; auto.
, which fails with
Error:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)", "iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)", "iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"<iris.proofmode.ltac_tactics.iPoseProofCore_go>" and "<iris.proofmode.ltac_tactics.iIntoEmpValid>", last call
failed.
No applicable tactic.
FWIW here's my context. Things are persistent as I'm not yet using mutable state (only persistent ghost state).
1 subgoal (ID 3041)
Σ : gFunctors
HdotG : dotG Σ
Γ : list ty
T, L, U : ty
γ : gname
ρ : vls
l : label
v : vl
============================
"Hv" : γ ⤇ (λ ρ0 : leibnizC vls, ⟦ T ⟧ ρ0)
"Hg" : ⟦ Γ ⟧* ρ
"HLU" : ∀ (ρ0 : leibnizC vls) (v0 : vl), ⟦ Γ ⟧* ρ0 → ⟦ L ⟧ ρ0 v0 → ⟦ U ⟧ ρ0 v0
"HTU" : ∀ (ρ0 : leibnizC vls) (v0 : vl), ⟦ Γ ⟧* ρ0 → ▷ ⟦ T ⟧ ρ0 v0 → ▷ ⟦ U ⟧ ρ0 v0
"HLT" : ∀ (ρ0 : leibnizC vls) (v0 : vl), ⟦ Γ ⟧* ρ0 → ▷ ⟦ L ⟧ ρ0 v0 → ▷ ⟦ T ⟧ ρ0 v0
"HL" : ▷ ⟦ L ⟧ ρ v
--------------------------------------□
▷ □ ⟦ T ⟧ ρ v