Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 22
    • Merge requests 22
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #222
Closed
Open
Issue created Dec 03, 2018 by Paolo G. Giarrusso@BlaisorbladeContributor

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
Assignee
Assign to
Time tracking