Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Register
  • Sign in
  • S stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 81
    • Issues 81
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 11
    • Merge requests 11
  • 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
  • stdpp
  • Issues
  • #34
Closed
Open
Issue created Jun 20, 2019 by Ralf Jung@jungOwner

solve_ndisj cannot solve `⊤ ∖ ↑N1 ∖ ↑N2 ⊆ ⊤ ∖ ↑N1.@"x" ∖ ↑N2 ∖ ↑N1.@"y"`

The following fails:

Lemma test5 (N1 N2 : namespace) :
  ⊤ ∖ ↑N1 ∖ ↑N2 ⊆@{coPset} ⊤ ∖ ↑N1.@"x" ∖ ↑N2 ∖ ↑N1.@"y".
Proof. solve_ndisj. Qed.

However, I think this is in the realm of what solve_ndisj should be able to handle, and the lemmas we got for it are indeed enough:

Lemma test5 (N1 N2 : namespace) :
  ⊤ ∖ ↑N1 ∖ ↑N2 ⊆@{coPset} ⊤ ∖ ↑N1.@"x" ∖ ↑N2 ∖ ↑N1.@"y".
Proof.
  apply namespace_subseteq_difference.
  { apply ndot_preserve_disjoint_r. set_solver. }
  solve_ndisj.
Qed.

The problem is related to the ordering of terms, the following goal can be solved:

Lemma test5' (N1 N2 : namespace) :
  ⊤ ∖ ↑N1 ∖ ↑N2 ⊆@{coPset} ⊤ ∖ ↑N1.@"x" ∖ ↑N1.@"y" ∖ ↑N2.

Notice how the N appear in the same order on both sides.

Edited Jun 20, 2019 by Ralf Jung
Assignee
Assign to
Time tracking