Skip to content
Snippets Groups Projects

Make `iFrame` fail if more work remains

Open Make `iFrame` fail if more work remains
robbert/iFrame_fail_more_work into master
2 unresolved threads
Open Robbert Krebbers requested to merge robbert/iFrame_fail_more_work into master
2 unresolved threads

This addresses #582

Simple example:

Lemma foo `{BiAffine PROP} (P Q : PROP) : P -∗ Q -∗ P.
Proof.
  iIntros "HP HQ".
  Fail iFrame "HP HQ". (* Framing [HP] turns the goal into [True], but more work
  (framing [HQ]) remains, hence [iFrame] fails. *)
  Fail iFrame "HQ HP". (* Fails because [HQ] cannot be framed in the first place. *)
Abort.
Edited by Robbert Krebbers

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Tej Chajed
    Tej Chajed @tchajed ·
    Maintainer

    Thanks! This looks like exactly the solution I wanted.

  • Robbert Krebbers added 1 commit

    added 1 commit

    Compare with previous version

  • Robbert Krebbers resolved all threads

    resolved all threads

  • Ralf Jung
    Ralf Jung @jung started a thread on an old version of a file
    • iris/proofmode/ltac_tactics.v
  • Robbert Krebbers added 23 commits

    added 23 commits

    Compare with previous version

    Toggle commit list
  • Robbert Krebbers added 1 commit

    added 1 commit

    • ee4dc96c - Add comment and fix inconsistency with the comment.

    Compare with previous version

  • Robbert Krebbers added 1 commit

    added 1 commit

    • 79309366 - Add comment and fix inconsistency with the comment.

    Compare with previous version

  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
    • iris/proofmode/ltac_tactics.v
    437 449 | [] => idtac
    438 | SelPure :: ?Hs => iFrameAnyPure; _iFrame_go Hs
    439 | SelIntuitionistic :: ?Hs => iFrameAnyIntuitionistic; _iFrame_go Hs
    440 | SelSpatial :: ?Hs => iFrameAnySpatial; _iFrame_go Hs
    441 | SelIdent ?H :: ?Hs => iFrameHyp H; _iFrame_go Hs
    450 | SelPure :: ?Hs => _iFrameAnyPure; _iFrame_go Hs
    451 | SelIntuitionistic :: ?Hs => _iFrameAnyIntuitionistic; _iFrame_go Hs
    452 | SelSpatial :: ?Hs => _iFrameAnySpatial; _iFrame_go Hs
    453 | SelIdent ?H :: ?Hs => _iFrameHyp H; _iFrame_go Hs
    442 454 end.
    443 455
    444 456 Ltac _iFrame0 Hs :=
    445 457 let Hs := sel_pat.parse Hs in
    446 _iFrame_go Hs.
    458 (** An explicit call to frame nothing (i.e., [iFrame ""]) should not
    459 accidentally close the goal using [_iFrameFinish]. *)
    • Comment on lines +458 to +459
      Ralf Jung
      Ralf Jung @jung ·
      Owner

      Why not? If iFrame "HP" closes a goal consisting of P ∗ True, then it would make sense for iFrame "" to close a goal consisting of True.

    • Robbert Krebbers
      Robbert Krebbers @robbertkrebbers ·
      Author Owner

      For tactic programming it turned out to be more convenient if it does not close the goal. Consider iSpecialize ("H []") versus iSpecialize ("H [$H]"). Currently the first always gives a goal, even if it's True/emp. The second will close the goal if framing H results in True/emp

      Of course, we could change the behavior of iSpecialize or have an iFrame wrapper for iSpecialize. But since iFrame "" is really an uninteresting edge case for users, I don't think this is worth the effort.

    • Ralf Jung
      Ralf Jung @jung ·
      Owner

      Hm, I somewhat dislike a quirk of specialization patterns affecting the behavior of iFrame.

      Why would spec patterns even call any iFrame tactic on iSpecialize ("H []")?

    • Robbert Krebbers
      Robbert Krebbers @robbertkrebbers ·
      Author Owner

      The parser turns the specialization pattern in an element of record spec_goal, which contains a list of hypotheses that should be framed. The spec pattern code then just calls iFrame on that list.

      If you care strongly about this edge case, we can either inline the case distinction in iSpecializeArgs_go or create a wrapper function for iFrame that is called there.

      Edited by Robbert Krebbers
    • Ralf Jung
      Ralf Jung @jung ·
      Owner

      The parser turns the specialization pattern in an element of record spec_goal, which contains a list of hypotheses that should be framed. The spec pattern code then just calls iFrame on that list.

      I guess I expected this to be an option list so that we avoid calling iFrame if there was no $ pattern.

      I don't care super strongly but it does seem a bit clear, so if it's easy maybe we should do it?

    • Please register or sign in to reply
  • Ralf Jung added S-waiting-for-author label

    added S-waiting-for-author label

    • Please register or sign in to reply