proof_irrel.v 1.29 KB
 Robbert Krebbers committed Feb 08, 2015 1 ``````(* Copyright (c) 2012-2015, Robbert Krebbers. *) `````` Robbert Krebbers committed Mar 14, 2013 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 ``````(* This file is distributed under the terms of the BSD license. *) (** This file collects facts on proof irrelevant types/propositions. *) Require Export Eqdep_dec tactics. Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances. Instance: ProofIrrel True. Proof. by intros [] []. Qed. Instance: ProofIrrel False. Proof. by intros []. Qed. Instance and_pi (A B : Prop) : ProofIrrel A → ProofIrrel B → ProofIrrel (A ∧ B). Proof. intros ?? [??] [??]. by f_equal. Qed. Instance prod_pi (A B : Type) : ProofIrrel A → ProofIrrel B → ProofIrrel (A * B). Proof. intros ?? [??] [??]. by f_equal. Qed. Instance eq_pi {A} `{∀ x y : A, Decision (x = y)} (x y : A) : ProofIrrel (x = y). Proof. intros ??. apply eq_proofs_unicity. intros x' y'. destruct (decide (x' = y')); tauto. Qed. Instance Is_true_pi (b : bool) : ProofIrrel (Is_true b). 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. `````` Robbert Krebbers committed Jun 24, 2013 29 30 31 `````` split; [by intros <- |]. destruct x as [x Hx], y as [y Hy]; simpl; intros; subst. f_equal. apply proof_irrel. `````` Robbert Krebbers committed Mar 14, 2013 32 33 34 35 ``````Qed. Lemma exists_proj1_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)} (x : sig P) p : `x ↾ p = x. Proof. by apply (sig_eq_pi _). Qed.``````