Library Coq.micromega.Tauto
Require Import List.
Require Import Refl.
Require Import Bool.
Set Implicit Arguments.
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 eval_f_morph :
forall A (
ev ev' :
A -> Prop) (
f :
BFormula A),
(forall a,
ev a <-> ev' a) -> (eval_f ev f <-> eval_f ev' f).
Fixpoint map_bformula (
T U :
Type) (
fct :
T -> U) (
f :
BFormula T) :
BFormula U :=
match f with
|
TT _ =>
TT _
|
FF _ =>
FF _
|
X _ p =>
X _ p
|
A a =>
A (
fct a)
|
Cj f1 f2 =>
Cj (
map_bformula fct f1) (
map_bformula fct f2)
|
D f1 f2 =>
D (
map_bformula fct f1) (
map_bformula fct f2)
|
N f =>
N (
map_bformula fct f)
|
I f1 f2 =>
I (
map_bformula fct f1) (
map_bformula fct f2)
end.
Lemma eval_f_map :
forall T U (
fct:
T-> U)
env f ,
eval_f env (
map_bformula fct f)
= eval_f (
fun x =>
env (
fct x))
f.
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).
Variable unsat :
Term' -> bool.
Variable unsat_prop :
forall t,
unsat t = true ->
forall env,
eval' env t -> False.
Variable deduce :
Term' -> Term' -> option Term'.
Variable deduce_prop :
forall env t t' u,
eval' env t -> eval' env t' -> deduce t t' = Some u -> eval' env u.
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.
Fixpoint add_term (
t:
Term') (
cl :
clause) :
option clause :=
match cl with
|
nil =>
match deduce t t with
|
None =>
Some (
t ::nil)
|
Some u =>
if unsat u then None else Some (
t::nil)
end
|
t'::cl =>
match deduce t t' with
|
None =>
match add_term t cl with
|
None =>
None
|
Some cl' =>
Some (
t' :: cl')
end
|
Some u =>
if unsat u then None else
match add_term t cl with
|
None =>
None
|
Some cl' =>
Some (
t' :: cl')
end
end
end.
Fixpoint or_clause (
cl1 cl2 :
clause) :
option clause :=
match cl1 with
|
nil =>
Some cl2
|
t::cl =>
match add_term t cl2 with
|
None =>
None
|
Some cl' =>
or_clause cl cl'
end
end.
Definition or_clause_cnf (
t:
clause) (
f:
cnf) :
cnf :=
List.fold_right (
fun e acc =>
match or_clause t e with
|
None =>
acc
|
Some cl =>
cl :: acc
end)
nil 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_clause (
env :
Env) (
cl :
clause) :=
~ make_conj (
eval' env)
cl.
Definition eval_cnf (
env :
Env) (
f:
cnf) :=
make_conj (
eval_clause env)
f.
Lemma eval_cnf_app :
forall env x y,
eval_cnf env (
x++y)
-> eval_cnf env x /\ eval_cnf env y.
Definition eval_opt_clause (
env :
Env) (
cl:
option clause) :=
match cl with
|
None =>
True
|
Some cl =>
eval_clause env cl
end.
Lemma add_term_correct :
forall env t cl ,
eval_opt_clause env (
add_term t cl)
-> eval_clause env (
t::cl).
Lemma or_clause_correct :
forall cl cl' env,
eval_opt_clause env (
or_clause cl cl')
-> eval_clause env cl \/ eval_clause env cl'.
Lemma or_clause_cnf_correct :
forall env t f,
eval_cnf env (
or_clause_cnf t f)
-> (eval_clause env t) \/ (eval_cnf env f).
Lemma eval_cnf_cons :
forall env a f,
(~ make_conj (
eval' env)
a) -> eval_cnf env f -> eval_cnf env (
a::f).
Lemma or_cnf_correct :
forall env f f',
eval_cnf env (
or_cnf f f')
-> (eval_cnf env f) \/ (eval_cnf env f').
Variable normalise_correct :
forall env t,
eval_cnf env (
normalise t)
-> eval env t.
Variable negate_correct :
forall env t,
eval_cnf env (
negate t)
-> ~ eval env t.
Lemma xcnf_correct :
forall f pol env,
eval_cnf 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 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.