`iIntros (?%lemma) "H"` fails if the lemma opens side-conditions
Test case:
Lemma test_iIntros_subgoals (m : gmap nat nat) i x :
⊢@{PROP} ⌜kmap (M2 :=gmap nat) id m !! i = Some x⌝ → True → True.
Proof. iStartProof. iIntros (?%lookup_kmap_Some) "H".
If we fix this we should be able to revert the hack from !964 (merged).
As @robbertkrebbers says the fix is probably to put first
in the right places, but the annoying thing is that first
fails when there are 0 goals, and 0 goals is also a real possibility (when destructing False
, for instance). We want to run our remaining tactics on "the first goal, but only if any goal exists" -- I don't know how to do that.
Also _iIntros_go
has a startproof
variable that is set to false
in a bunch of random places without any comment that would explain why, so refactoring that code is very hard. I think we should be able to just do iStartProof
once upfront instead of all of that mess, but that is blocked on #535, and even then maybe it breaks whatever logic that startproof
variable is supposed to capture.