diff --git a/theories/decidable.v b/theories/decidable.v index a259df8772da984b5fbf87812a0784336c6916b7..e8dd5172fe40c888203c071a2fe4c3e134b72287 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 55966090c453ed9d08485f4b1ddb40085f421e17..b9e583d0479792e4f8565b1bfbe2c4fc18302466 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 4a61167deefa6b77ab317ec2ef2bda98da4006ef..56cd5340838942ff529960dc12cf559b4a76d25d 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)}