Library Coq.micromega.Refl
Require
Import
List
.
Require
Setoid
.
Set Implicit Arguments
.
Fixpoint
make_impl
(
A
:
Type
) (
eval
:
A
->
Prop
) (
l
:
list
A
) (
goal
:
Prop
) {
struct
l
} :
Prop
:=
match
l
with
|
nil
=>
goal
|
cons
e
l
=>
(
eval
e
)
->
(
make_impl
eval
l
goal
)
end
.
Theorem
make_impl_true
:
forall
(
A
:
Type
) (
eval
:
A
->
Prop
) (
l
:
list
A
),
make_impl
eval
l
True
.
Fixpoint
make_conj
(
A
:
Type
) (
eval
:
A
->
Prop
) (
l
:
list
A
) {
struct
l
} :
Prop
:=
match
l
with
|
nil
=>
True
|
cons
e
nil
=> (
eval
e
)
|
cons
e
l2
=> (
(
eval
e
)
/\
(
make_conj
eval
l2
)
)
end
.
Theorem
make_conj_cons
:
forall
(
A
:
Type
) (
eval
:
A
->
Prop
) (
a
:
A
) (
l
:
list
A
),
make_conj
eval
(
a
::
l
)
<->
eval
a
/\
make_conj
eval
l
.
Lemma
make_conj_impl
:
forall
(
A
:
Type
) (
eval
:
A
->
Prop
) (
l
:
list
A
) (
g
:
Prop
),
(
make_conj
eval
l
->
g
)
<->
make_impl
eval
l
g
.
Lemma
make_conj_in
:
forall
(
A
:
Type
) (
eval
:
A
->
Prop
) (
l
:
list
A
),
make_conj
eval
l
->
(
forall
p
,
In
p
l
->
eval
p
)
.
Lemma
make_conj_app
:
forall
A
eval
l1
l2
, @
make_conj
A
eval
(
l1
++
l2
)
<->
@
make_conj
A
eval
l1
/\
@
make_conj
A
eval
l2
.
Lemma
not_make_conj_cons
:
forall
(
A
:
Type
) (
t
:
A
)
a
eval
(
no_middle_eval
:
(
eval
t
)
\/
~
(
eval
t
)
),
~
make_conj
eval
(
t
::
a
)
->
~
(
eval
t
)
\/
(
~
make_conj
eval
a
)
.
Lemma
not_make_conj_app
:
forall
(
A
:
Type
) (
t
:
list
A
)
a
eval
(
no_middle_eval
:
forall
d
,
eval
d
\/
~
eval
d
) ,
~
make_conj
eval
(
t
++
a
)
->
(
~
make_conj
eval
t
)
\/
(
~
make_conj
eval
a
)
.