Skip to content

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

Robbert Krebbers requested to merge robbert/True_False_lemmas into master

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 by Robbert Krebbers

Merge request reports