From 46304c52633a2bf6c159efb8bc9a6e57e2182c49 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 24 Jun 2013 10:42:47 +0200
Subject: [PATCH] Misc prelude changes.

---
 theories/decidable.v   | 4 ++--
 theories/option.v      | 7 +++++++
 theories/proof_irrel.v | 7 +++----
 3 files changed, 12 insertions(+), 6 deletions(-)

diff --git a/theories/decidable.v b/theories/decidable.v
index a259df87..e8dd5172 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -24,10 +24,10 @@ Lemma decide_rel_correct {A B} (R : A → B → Prop) `{∀ x y, Decision (R x y
   (x : A) (y : B) : decide_rel R x y = decide (R x y).
 Proof. done. Qed.
 
-Lemma decide_true {A} `{Decision P} (x y : A) :
+Lemma decide_True {A} `{Decision P} (x y : A) :
   P → (if decide P then x else y) = x.
 Proof. by destruct (decide P). Qed.
-Lemma decide_false {A} `{Decision P} (x y : A) :
+Lemma decide_False {A} `{Decision P} (x y : A) :
   ¬P → (if decide P then x else y) = y.
 Proof. by destruct (decide P). Qed.
 
diff --git a/theories/option.v b/theories/option.v
index 55966090..b9e583d0 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -137,6 +137,13 @@ Tactic Notation "case_option_guard" "as" ident(Hx) :=
 Tactic Notation "case_option_guard" :=
   let H := fresh in case_option_guard as H.
 
+Lemma option_guard_True {A} (P : Prop) `{Decision P} (x : option A) :
+  P → guard P; x = x.
+Proof. intros. by case_option_guard. Qed.
+Lemma option_guard_False {A} (P : Prop) `{Decision P} (x : option A) :
+  ¬P → guard P; x = None.
+Proof. intros. by case_option_guard. Qed.
+
 Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat
   match goal with
   | _ => progress (unfold default in *)
diff --git a/theories/proof_irrel.v b/theories/proof_irrel.v
index 4a61167d..56cd5340 100644
--- a/theories/proof_irrel.v
+++ b/theories/proof_irrel.v
@@ -30,10 +30,9 @@ Proof. destruct b; simpl; apply _. Qed.
 Lemma sig_eq_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
   (x y : sig P) : x = y ↔ `x = `y.
 Proof.
-  split.
-  * destruct x, y. apply proj1_sig_inj.
-  * destruct x as [x Hx], y as [y Hy]; simpl; intros; subst.
-    f_equal. apply proof_irrel.
+  split; [by intros <- |].
+  destruct x as [x Hx], y as [y Hy]; simpl; intros; subst.
+  f_equal. apply proof_irrel.
 Qed.
 
 Lemma exists_proj1_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
-- 
GitLab