Commit f7c9c556 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'robbert/True_False_lemmas' into 'master'

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

See merge request !256
parents d9aa2025 e703b4c9
Pipeline #46145 passed with stage
in 10 minutes and 52 seconds
......@@ -19,6 +19,17 @@ API-breaking change is listed.
longer work for multisets.
- Make `Qc_of_Z'` not an implicit coercion (from `Z` to `Qc`) any more.
- Make `Z.of_nat'` not an implicit coercion (from `nat` to `Z`) any more.
- Rename `decide_left``decide_True_pi` and `decide_right``decide_False_pi`.
- Add `option_guard_True_pi`.
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
```
sed -i -E '
s/\bdecide_left\b/decide_True_pi/g
s/\bdecide_right\b/decide_False_pi/g
' $(find theories -name "*.v")
```
## std++ 1.5.0
......
......@@ -25,9 +25,9 @@ Lemma decide_iff {A} P Q `{Decision P, Decision Q} (x y : A) :
(P Q) (if decide P then x else y) = (if decide Q then x else y).
Proof. intros [??]. destruct (decide P), (decide Q); tauto. Qed.
Lemma decide_left `{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP.
Lemma decide_True_pi `{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP.
Proof. destruct (decide P); [|contradiction]. f_equal. apply proof_irrel. Qed.
Lemma decide_right `{Decision P, !ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP.
Lemma decide_False_pi `{Decision P, !ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP.
Proof. destruct (decide P); [contradiction|]. f_equal. apply proof_irrel. Qed.
(** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the
......
......@@ -339,10 +339,14 @@ Tactic Notation "case_option_guard" :=
let H := fresh in case_option_guard as H.
Lemma option_guard_True {A} P `{Decision P} (mx : option A) :
P (guard P; mx) = mx.
P mguard P (λ _, mx) = mx.
Proof. intros. by case_option_guard. Qed.
Lemma option_guard_False {A} P `{Decision P} (mx : option A) :
¬P (guard P; mx) = None.
Lemma option_guard_True_pi {A} P `{Decision P, ProofIrrel P} (f : P option A)
(HP : P) :
mguard P f = f HP.
Proof. intros. case_option_guard; [|done]. f_equal; apply proof_irrel. Qed.
Lemma option_guard_False {A} P `{Decision P} (f : P option A) :
¬P mguard P f = None.
Proof. intros. by case_option_guard. Qed.
Lemma option_guard_iff {A} P Q `{Decision P, Decision Q} (mx : option A) :
(P Q) (guard P; mx) = guard Q; mx.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment