proof_irrel.v 1.78 KB
Newer Older
1
(** This file collects facts on proof irrelevant types/propositions. *)
2
From stdpp Require Export base.
Ralf Jung's avatar
Ralf Jung committed
3
From stdpp Require Import options.
4 5 6

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

7
Instance True_pi: ProofIrrel True.
8
Proof. intros [] []; reflexivity. Qed.
9
Instance False_pi: ProofIrrel False.
10
Proof. intros []. Qed.
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
11 12
Instance unit_pi: ProofIrrel ().
Proof. intros [] []; reflexivity. Qed.
13 14
Instance and_pi (A B : Prop) :
  ProofIrrel A  ProofIrrel B  ProofIrrel (A  B).
15
Proof. intros ?? [??] [??]. f_equal; trivial. Qed.
16 17
Instance prod_pi (A B : Type) :
  ProofIrrel A  ProofIrrel B  ProofIrrel (A * B).
18
Proof. intros ?? [??] [??]. f_equal; trivial. Qed.
19
Instance eq_pi {A} (x : A) `{ z, Decision (x = z)} (y : A) :
20 21
  ProofIrrel (x = y).
Proof.
22 23 24 25 26 27 28 29
  set (f z (H : x = z) :=
    match decide (x = z) return x = z with
    | left H => H | right H' => False_rect _ (H' H)
    end).
  assert ( z (H : x = z),
    eq_trans (eq_sym (f x (eq_refl x))) (f z H) = H) as help.
  { intros ? []. destruct (f x eq_refl); tauto. }
  intros p q. rewrite <-(help _ p), <-(help _ q).
30
  unfold f at 2 4. destruct (decide _); [reflexivity|]. exfalso; tauto.
31 32 33 34 35 36
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.
37
  split; [intros <-; reflexivity|].
Robbert Krebbers's avatar
Robbert Krebbers committed
38 39
  destruct x as [x Hx], y as [y Hy]; simpl; intros; subst.
  f_equal. apply proof_irrel.
40
Qed.
41 42 43
Instance proj1_sig_inj `(P : A  Prop) `{ x, ProofIrrel (P x)} :
  Inj (=) (=) (proj1_sig (P:=P)).
Proof. intros ??. apply (sig_eq_pi P). Qed.
44 45
Lemma exists_proj1_pi `(P : A  Prop) `{ x, ProofIrrel (P x)}
  (x : sig P) p : `x  p = x.
46
Proof. apply (sig_eq_pi _); reflexivity. Qed.