Commit 60645f9b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Rename `decide_left` → `decide_True_pi`, `decide_right` → `decide_False_pi`.

parent acb221eb
......@@ -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
......
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