Module proof_irrel
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.
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
)}
(
x
:
sig
P
)
p
: `
x
↾
p
=
x
.
Proof.
by
apply
(
sig_eq_pi
_
). Qed.