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 19
    • Merge Requests 19
  • 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
  • #304

Closed
Open
Opened Apr 06, 2020 by Ralf Jung@jungOwner

Direction of _op lemmas is inconsistent with _(p)core, _valid, _included

See the discussion at !403 (comment 47448): our _(p)core, _valid, _included lemmas generally push the named operation "in", e.g.

  Lemma pair_valid (a : A) (b : B) : ✓ (a, b) ↔ ✓ a ∧ ✓ b.
  Lemma pair_core `{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
    core (a, b) = (core a, core b).

However, most of our _op lemmas push the named operation "out":

  Lemma pair_op (a a' : A) (b b' : B) : (a ⋅ a', b ⋅ b') = (a, b) ⋅ (a', b').

Moreover, even with one "group" of lemmas, not all are consistent: singleton_op, discrete_fun_singleton_op, list_singleton_op push "in", while cmra_morphism_(p)core push "out" (and there might be more).

At the very least, we should make all lemmas within a "group" consistent. So, the minimal fix for this is to swap the 5 lemmas named in the last paragraph. However, we might also want to fix the larger inconsistency that the _op lemmas are going the other way, compared to the rest of them. The thing is, we already swapped half of them !303 (merged), so this starts to look like we are just going back and forth...

Edited Apr 06, 2020 by Ralf Jung
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: iris/iris#304