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 171
    • Issues 171
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 14
    • Merge requests 14
  • 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
  • Merge requests
  • !136

Implement `big_sepL_delete`

  • Review changes

  • Download
  • Email patches
  • Plain diff
Closed Dan Frumin requested to merge dfrumin/iris-coq:big_sepl_delete into master Mar 27, 2018
  • Overview 1
  • Commits 1
  • Pipelines 0
  • Changes 1

The big_sepL_delete lemma is quite useful and is akin to big_sepM_delete.

  Lemma big_sepL_delete Φ l i x :
    l !! i = Some x →
    ([∗ list] k↦y ∈ l, Φ k y) ⊣⊢ Φ i x ∗ [∗ list] k↦y ∈ l, ⌜ k ≠ i ⌝ → Φ k y.

I use it when big_sepL_lookup_acc is not enough, ie when I need to have access to the rest of the list as well.

I don't think that it can be implemented on the level of monoids, because it relies on the fact that we have this ⌜ k ≠ i ⌝ assumption. Furthermore, I was not able to come up with a shorter proof. If anyone knows how to compresses the two parts of the proof into one, I'd really appreciate that.

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: big_sepl_delete