Library Coq.micromega.Tauto
Require Import List.
Require Import Refl.
Require Import Bool.
Inductive BFormula (
A:
Type) :
Type :=
|
TT :
BFormula A
|
FF :
BFormula A
|
X :
Prop ->
BFormula A
|
A :
A ->
BFormula A
|
Cj :
BFormula A ->
BFormula A ->
BFormula A
|
D :
BFormula A->
BFormula A ->
BFormula A
|
N :
BFormula A ->
BFormula A
|
I :
BFormula A->
BFormula A->
BFormula A.
Fixpoint eval_f (
A:
Type) (
ev:
A ->
Prop ) (
f:
BFormula A) {
struct f}:
Prop :=
match f with
|
TT =>
True
|
FF =>
False
|
A a =>
ev a
|
X p =>
p
|
Cj e1 e2 =>
(eval_f ev e1) /\ (eval_f ev e2)
|
D e1 e2 =>
(eval_f ev e1) \/ (eval_f ev e2)
|
N e =>
~ (eval_f ev e)
|
I f1 f2 => (
eval_f ev f1) -> (
eval_f ev f2)
end.
Lemma map_simpl :
forall A B f l, @
map A B f l = match l with
|
nil =>
nil
|
a :: l=>
(f a) :: (@
map A B f l)
end.
Section S.
Variable Env :
Type.
Variable Term :
Type.
Variable eval :
Env ->
Term ->
Prop.
Variable Term' :
Type.
Variable eval' :
Env ->
Term' ->
Prop.
Variable no_middle_eval' :
forall env d,
(eval' env d) \/ ~ (eval' env d).
Definition clause :=
list Term'.
Definition cnf :=
list clause.
Variable normalise :
Term ->
cnf.
Variable negate :
Term ->
cnf.
Definition tt :
cnf := @
nil clause.
Definition ff :
cnf :=
cons (@
nil Term')
nil.
Definition or_clause_cnf (
t:
clause) (
f:
cnf) :
cnf :=
List.map (
fun x => (
t++x))
f.
Fixpoint or_cnf (
f :
cnf) (
f' :
cnf) {
struct f}:
cnf :=
match f with
|
nil =>
tt
|
e :: rst =>
(or_cnf rst f') ++ (or_clause_cnf e f')
end.
Definition and_cnf (
f1 :
cnf) (
f2 :
cnf) :
cnf :=
f1 ++ f2.
Fixpoint xcnf (
pol :
bool) (
f :
BFormula Term) {
struct f}:
cnf :=
match f with
|
TT =>
if pol then tt else ff
|
FF =>
if pol then ff else tt
|
X p =>
if pol then ff else ff
|
A x =>
if pol then normalise x else negate x
|
N e =>
xcnf (
negb pol)
e
|
Cj e1 e2 =>
(
if pol then and_cnf else or_cnf) (
xcnf pol e1) (
xcnf pol e2)
|
D e1 e2 => (
if pol then or_cnf else and_cnf) (
xcnf pol e1) (
xcnf pol e2)
|
I e1 e2 => (
if pol then or_cnf else and_cnf) (
xcnf (
negb pol)
e1) (
xcnf pol e2)
end.
Definition eval_cnf (
env :
Term' ->
Prop) (
f:
cnf) :=
make_conj (
fun cl =>
~ make_conj env cl)
f.
Lemma eval_cnf_app :
forall env x y,
eval_cnf (
eval' env) (
x++y) ->
eval_cnf (
eval' env)
x /\ eval_cnf (
eval' env)
y.
Lemma or_clause_correct :
forall env t f,
eval_cnf (
eval' env) (
or_clause_cnf t f) ->
(~ make_conj (
eval' env)
t) \/ (eval_cnf (
eval' env)
f).
Lemma eval_cnf_cons :
forall env a f, (
~ make_conj (
eval' env)
a) ->
eval_cnf (
eval' env)
f ->
eval_cnf (
eval' env) (
a::f).
Lemma or_cnf_correct :
forall env f f',
eval_cnf (
eval' env) (
or_cnf f f') ->
(eval_cnf (
eval' env)
f) \/ (eval_cnf (
eval' env)
f').
Variable normalise_correct :
forall env t,
eval_cnf (
eval' env) (
normalise t) ->
eval env t.
Variable negate_correct :
forall env t,
eval_cnf (
eval' env) (
negate t) ->
~ eval env t.
Lemma xcnf_correct :
forall f pol env,
eval_cnf (
eval' env) (
xcnf pol f) ->
eval_f (
eval env) (
if pol then f else N f).
Variable Witness :
Type.
Variable checker :
list Term' ->
Witness ->
bool.
Variable checker_sound :
forall t w,
checker t w = true ->
forall env,
make_impl (
eval' env)
t False.
Fixpoint cnf_checker (
f :
cnf) (
l :
list Witness) {
struct f}:
bool :=
match f with
|
nil =>
true
|
e::f =>
match l with
|
nil =>
false
|
c::l =>
match checker e c with
|
true =>
cnf_checker f l
|
_ =>
false
end
end
end.
Lemma cnf_checker_sound :
forall t w,
cnf_checker t w = true ->
forall env,
eval_cnf (
eval' env)
t.
Definition tauto_checker (
f:
BFormula Term) (
w:
list Witness) :
bool :=
cnf_checker (
xcnf true f)
w.
Lemma tauto_checker_sound :
forall t w,
tauto_checker t w = true ->
forall env,
eval_f (
eval env)
t.
End S.