Library Coq.micromega.CheckerMaker
Require
Import
Setoid
.
Require
Import
Decidable
.
Require
Import
List
.
Require
Import
Refl
.
Section
CheckerMaker
.
Variable
Formula
:
Type
.
Variable
Env
:
Type
.
Variable
eval
:
Env
->
Formula
->
Prop
.
Variable
Formula'
:
Type
.
Variable
eval'
:
Env
->
Formula'
->
Prop
.
Variable
normalise
:
Formula
->
Formula'
.
Variable
negate
:
Formula
->
Formula'
.
Hypothesis
normalise_sound
:
forall
(
env
:
Env
) (
t
:
Formula
),
eval
env
t
->
eval'
env
(
normalise
t
).
Hypothesis
negate_correct
:
forall
(
env
:
Env
) (
t
:
Formula
),
eval
env
t
<->
~
(
eval'
env
(
negate
t
)
)
.
Variable
Witness
:
Type
.
Variable
check_formulas'
:
list
Formula'
->
Witness
->
bool
.
Hypothesis
check_formulas'_sound
:
forall
(
l
:
list
Formula'
) (
w
:
Witness
),
check_formulas'
l
w
=
true
->
forall
env
:
Env
,
make_impl
(
eval'
env
)
l
False
.
Definition
normalise_list
:
list
Formula
->
list
Formula'
:=
map
normalise
.
Definition
negate_list
:
list
Formula
->
list
Formula'
:=
map
negate
.
Definition
check_formulas
(
l
:
list
Formula
) (
w
:
Witness
) :
bool
:=
check_formulas'
(
map
normalise
l
)
w
.
Lemma
normalise_sound_contr
:
forall
(
env
:
Env
) (
l
:
list
Formula
),
make_impl
(
eval'
env
) (
map
normalise
l
)
False
->
make_impl
(
eval
env
)
l
False
.
Theorem
check_formulas_sound
:
forall
(
l
:
list
Formula
) (
w
:
Witness
),
check_formulas
l
w
=
true
->
forall
env
:
Env
,
make_impl
(
eval
env
)
l
False
.
Fixpoint
check_conj_formulas'
(
t1
:
list
Formula'
) (
wits
:
list
Witness
) (
t2
:
list
Formula'
) {
struct
wits
} :
bool
:=
match
t2
with
|
nil
=>
true
|
t'
::
rt2
=>
match
wits
with
|
nil
=>
false
|
w
::
rwits
=>
match
check_formulas'
(
t'
::
t1
)
w
with
|
true
=>
check_conj_formulas'
t1
rwits
rt2
|
false
=>
false
end
end
end
.
Definition
check_conj_formulas
(
t1
:
list
Formula
) (
wits
:
list
Witness
) (
t2
:
list
Formula
) :
bool
:=
check_conj_formulas'
(
normalise_list
t1
)
wits
(
negate_list
t2
).
Theorem
check_conj_formulas_sound
:
forall
(
t1
:
list
Formula
) (
t2
:
list
Formula
) (
wits
:
list
Witness
),
check_conj_formulas
t1
wits
t2
=
true
->
forall
env
:
Env
,
make_impl
(
eval
env
)
t1
(
make_conj
(
eval
env
)
t2
).
End
CheckerMaker
.