Library Coq.Bool.IfProp
Require
Import
Bool
.
Inductive
IfProp
(
A
B
:
Prop
) :
bool
->
Prop
:=
|
Iftrue
:
A
->
IfProp
A
B
true
|
Iffalse
:
B
->
IfProp
A
B
false
.
Hint Resolve
Iftrue
Iffalse
:
bool
.
Lemma
Iftrue_inv
:
forall
(
A
B
:
Prop
) (
b
:
bool
),
IfProp
A
B
b
->
b
=
true
->
A
.
Lemma
Iffalse_inv
:
forall
(
A
B
:
Prop
) (
b
:
bool
),
IfProp
A
B
b
->
b
=
false
->
B
.
Lemma
IfProp_true
:
forall
A
B
:
Prop
,
IfProp
A
B
true
->
A
.
Lemma
IfProp_false
:
forall
A
B
:
Prop
,
IfProp
A
B
false
->
B
.
Lemma
IfProp_or
:
forall
(
A
B
:
Prop
) (
b
:
bool
),
IfProp
A
B
b
->
A
\/
B
.
Lemma
IfProp_sum
:
forall
(
A
B
:
Prop
) (
b
:
bool
),
IfProp
A
B
b
->
{
A
}
+
{
B
}
.