Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
I
Iris
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 116
    • Issues 116
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 23
    • Merge Requests 23
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Iris
  • Iris
  • Issues
  • #76

Closed
Open
Opened Mar 14, 2017 by Robbert@robbertkrebbersMaintainer

`iDestruct` for big ops

Together with @jung and @jjourdan we discussed that it would be useful if iDestruct (and tactics like iSplit and iFrame) would have better support for big ops, in particular, that when having:

H : [∗ list] k ↦ x ∈ y :: l, Φ k x

we could use iDestruct "H" as "[H1 H2]" to turn it into:

H1 : Φ 0 y
H2 : [∗ list] k ↦ x ∈ l, Φ (S k) x

Although this is not particularly difficult to implement (it just requires one to declare suitable IntoAnd instances), it gives rise to some potential ambiguity, namely, what is going to happen when having:

H : [∗ list] k ↦ x ∈ y :: l, Φ k x ∗ Ψ k x

Will it split through the cons, or through the star inside of the predicate in the big op?

Currently, it will split through the ∗ due to the instance into_and_big_sepL. Declaring yet another IntoAnd instance for the cons case is a bad idea, as it will give rise to the ambiguity above, and we end up with tactics that will behave unpredictably.

However, I think that the cons instance would be much more useful than the ∗ instance, hence I propose to drop the current ∗ instance, and instead declare instances for cons (and possibly app, which does not lead to ambiguity).

Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: iris/iris#76