proof_irrel.v 1.37 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects facts on proof irrelevant types/propositions. *)
4
From Coq Require Import Eqdep_dec.
5
From iris.prelude Require Export base.
Robbert Krebbers's avatar
Robbert Krebbers committed
6 7 8 9

Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances.

Instance: ProofIrrel True.
10
Proof. intros [] []; reflexivity. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
11
Instance: ProofIrrel False.
12
Proof. intros []. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
13 14
Instance and_pi (A B : Prop) :
  ProofIrrel A  ProofIrrel B  ProofIrrel (A  B).
15
Proof. intros ?? [??] [??]. f_equal; trivial. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
16 17
Instance prod_pi (A B : Type) :
  ProofIrrel A  ProofIrrel B  ProofIrrel (A * B).
18
Proof. intros ?? [??] [??]. f_equal; trivial. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
19 20 21 22 23 24 25 26 27 28 29
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.
30
  split; [intros <-; reflexivity|].
Robbert Krebbers's avatar
Robbert Krebbers committed
31 32 33 34 35
  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)}
  (x : sig P) p : `x  p = x.
36
Proof. apply (sig_eq_pi _); reflexivity. Qed.