Skip to content
Snippets Groups Projects

add 'notypeclasses apply' tactic

Merged Ralf Jung requested to merge ralf/notypeclasses-apply into master
All threads resolved!

notypeclasses apply is like notypeclasses refine except that it adds sufficiently many underscores automatically, thus making it less fragile to use.

This version adds underscores until the term is not a function any more. That is less smart than apply/apply:, so maybe we should pick a different name? We could also try applying after each _, though that could be slow if unification goes wrong.

@msammler I found a case in the bitvector lib that seems like it could use the new tactic. I hope it is covered by tests, otherwise I am not sure if it still works.^^

Fixes #220 (closed)

Merge request reports

Merge request pipeline #115655 passed

Merge request pipeline passed for 6d672976

Merged by Ralf JungRalf Jung 2 weeks ago (Feb 4, 2025 9:47pm UTC)

Loading

Pipeline #115659 passed

Pipeline passed for ada66bd2 on master

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Yes, this bitvector tactic is used mostly in the Section unfolding. later in the file. So I think your change to the bitvector tactic is tested adequately and should work.

  • This version adds underscores until the term is not a function any more. That is less smart than apply/apply:, so maybe we should pick a different name? We could also try applying after each _, though that could be slow if unification goes wrong.

    That behavior does not seem too great, and indeed makes it quite different from apply/apply:. It makes it especially awkward since refine does not respect transparency at all, so if the definition internally contains an arrow/forall, _s will be applied for those.

    That said, I do not have a clear vision of the potential use cases of this tactic. I guess it will mostly be a building block for other tactics, so perhaps it's OK to fix this problem later when it shows up in practice.

  • Robbert Krebbers
  • Author Owner

    It makes it especially awkward since refine does not respect transparency at all, so if the definition internally contains an arrow/forall, _s will be applied for those.

    No that does not follow. We use opose_specialize_foralls_core to determine how many _ to add, which IIRC is entirely syntactic and does not unfold anything.

    That said, I do not have a clear vision of the potential use cases of this tactic. I guess it will mostly be a building block for other tactics, so perhaps it's OK to fix this problem later when it shows up in practice.

    My current vision is "replace all the notypeclasses refine with long sequences of _ in the Iris Proof Mode".

  • Ralf Jung added 1 commit

    added 1 commit

    Compare with previous version

  • Modulo tiny nit and CHANGELOG this looks good to me.

  • Ralf Jung added 9 commits

    added 9 commits

    Compare with previous version

  • Author Owner

    I updated the comment hopefully in the spirit of your suggestion, and added a changelog.

  • I am happy, feel free to land.

  • Ralf Jung resolved all threads

    resolved all threads

  • Ralf Jung mentioned in commit ada66bd2

    mentioned in commit ada66bd2

  • merged

  • Please register or sign in to reply
    Loading