From 1c9e858188578a65bf014ed8a8a9404f87054848 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 19 Dec 2016 14:46:42 +0100 Subject: [PATCH] add decide_left, decide_right --- theories/prelude/decidable.v | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/theories/prelude/decidable.v b/theories/prelude/decidable.v index 9c7ec3ab4..ec5e19c4b 100644 --- a/theories/prelude/decidable.v +++ b/theories/prelude/decidable.v @@ -36,6 +36,11 @@ 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. +Proof. destruct (decide P) as [?|?]; [|contradiction]. f_equal. apply proof_irrel. Qed. +Lemma decide_right`{Decision P} `{!ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP. +Proof. destruct (decide P) as [?|?]; [contradiction|]. f_equal. apply proof_irrel. Qed. + (** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the components is double negated, it will try to remove the double negation. *) Tactic Notation "destruct_decide" constr(dec) "as" ident(H) := -- GitLab