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 84
    • Issues 84
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 9
    • Merge requests 9
  • 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
  • Merge requests
  • !256

`_True`/`_False` lemmas for `decide` and `mguard`

  • Review changes

  • Download
  • Patches
  • Plain diff
Merged Robbert Krebbers requested to merge robbert/True_False_lemmas into master Apr 28, 2021
  • Overview 12
  • Commits 6
  • Pipelines 0
  • Changes 3

For decide we currently have the following lemmas:

Lemma decide_True {A} `{Decision P} (x y : A) : P → (if decide P then x else y) = x.
Lemma decide_False {A} `{Decision P} (x y : A) : ¬P → (if decide P then x else y) = y.
Lemma decide_left `{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP.
Lemma decide_right `{Decision P, !ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP.

The first two are most commonly used, whereas the last two are also applicable if you do a match on decide and use the proof of P or ¬P.

For guard we have similar lemmas that correspond to the first two lemmas for decide.

Lemma option_guard_True {A} P `{Decision P} (mx : option A) : P → (guard P; mx) = mx.
Lemma option_guard_False {A} P `{Decision P} (mx : option A) : ¬P → (guard P; mx) = None.

However, these don't work for guard P as HP; ... something containing HP ..., so I wanted to have lemmas like the last two for decide. The one for False can be generalized trivially, but (like decide) the one for True only works if the proposition is proof irrelevant:

Lemma option_guard_True_pi {A} P `{Decision P, ProofIrrel P} (f : P → option A) (HP : P) : mguard P f = f HP.
Lemma option_guard_False {A} P `{Decision P} (f : P → option A) : ¬P → mguard P f = None.

(Note that guard P as HP; y is notation for mguard P (λ HP, y)).

The main problem, as usual, is naming... The _left and _right suffixes for decide make no sense for guard. So instead, I propose the _pi suffix for proof irrelevant. Opinions about that?

Edited Apr 28, 2021 by Robbert Krebbers
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: robbert/True_False_lemmas