Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 186
    • Issues 186
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 18
    • Merge requests 18
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Artifacts
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Model experiments
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #76

`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
Time tracking