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 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 22
    • Merge requests 22
  • 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
  • Issues
  • #161
Closed
Open
Issue created Feb 26, 2018 by Jacques-Henri Jourdan@jjourdanMaintainer

Use `plainly_alt` as an axiom and replace most of the current ones

In the interface for plainly, we could have plainly_alt as an axiom. Here are the reasons this is not a completely absurd idea:

1- Most of the axioms can be removed. Namely, the only ones remaining are:

  • bi_persistently_impl_plainly, bi_plainly_impl_plainly (which I find kind of arbitrary anyway),
  • sbi_mixin_prop_ext (which is actually one of the few current axioms of plainly that actually /says/ something about the BI. So this is expected that it stays.
  • The axioms about the updates, but I would say these are rather about the update than about bi_plainly
  • sbi_mixin_later_plainly_2, which somehow I am not able to prove. But perhaps I am missing something.

Note that for some of these axioms (except bi_plainly_impl_plainly, sbi_mixin_prop_ext and the update axioms), we could replace "for all plain assertion P" by "for all equality", which make them understandable even without understanding what is plainly.

2- I would say the definition of plainly_alt is quite intuitive. Indeed, P /\ emp = emp is a way of internally saying emp |- P, which exactly means that P is valid. So this definition can directly be interpreted as the "internal validity".

Assignee
Assign to
Time tracking