Commit 46304c52 authored by Robbert Krebbers's avatar Robbert Krebbers

Misc prelude changes.

parent 472ccca0
......@@ -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.
......
......@@ -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 *)
......
......@@ -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)}
......
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