Library Coq.btauto.Reflect
Require
Import
Bool
DecidableClass
Algebra
Ring
PArith
Lia
.
Section
Bool
.
Inductive
formula
:=
|
formula_var
:
positive
->
formula
|
formula_btm
:
formula
|
formula_top
:
formula
|
formula_cnj
:
formula
->
formula
->
formula
|
formula_dsj
:
formula
->
formula
->
formula
|
formula_neg
:
formula
->
formula
|
formula_xor
:
formula
->
formula
->
formula
|
formula_ifb
:
formula
->
formula
->
formula
->
formula
.
Fixpoint
formula_eval
var
f
:=
match
f
with
|
formula_var
x
=>
list_nth
x
var
false
|
formula_btm
=>
false
|
formula_top
=>
true
|
formula_cnj
fl
fr
=>
(
formula_eval
var
fl
)
&&
(
formula_eval
var
fr
)
|
formula_dsj
fl
fr
=>
(
formula_eval
var
fl
)
||
(
formula_eval
var
fr
)
|
formula_neg
f
=>
negb
(
formula_eval
var
f
)
|
formula_xor
fl
fr
=>
xorb
(
formula_eval
var
fl
) (
formula_eval
var
fr
)
|
formula_ifb
fc
fl
fr
=>
if
formula_eval
var
fc
then
formula_eval
var
fl
else
formula_eval
var
fr
end
.
End
Bool
.
Section
Translation
.
Fixpoint
poly_of_formula
f
:=
match
f
with
|
formula_var
x
=>
Poly
(
Cst
false
)
x
(
Cst
true
)
|
formula_btm
=>
Cst
false
|
formula_top
=>
Cst
true
|
formula_cnj
fl
fr
=>
let
pl
:=
poly_of_formula
fl
in
let
pr
:=
poly_of_formula
fr
in
poly_mul
pl
pr
|
formula_dsj
fl
fr
=>
let
pl
:=
poly_of_formula
fl
in
let
pr
:=
poly_of_formula
fr
in
poly_add
(
poly_add
pl
pr
) (
poly_mul
pl
pr
)
|
formula_neg
f
=>
poly_add
(
Cst
true
) (
poly_of_formula
f
)
|
formula_xor
fl
fr
=>
poly_add
(
poly_of_formula
fl
) (
poly_of_formula
fr
)
|
formula_ifb
fc
fl
fr
=>
let
pc
:=
poly_of_formula
fc
in
let
pl
:=
poly_of_formula
fl
in
let
pr
:=
poly_of_formula
fr
in
poly_add
pr
(
poly_add
(
poly_mul
pc
pl
) (
poly_mul
pc
pr
))
end
.
Opaque
poly_add
.
Lemma
poly_of_formula_eval_compat
:
forall
var
f
,
eval
var
(
poly_of_formula
f
)
=
formula_eval
var
f
.
Hint Extern
5 =>
change
0
with
(
min
0 0) :
core
.
Local Hint Resolve
poly_add_valid_compat
poly_mul_valid_compat
:
core
.
Local Hint Constructors
valid
:
core
.
Hint Extern
5 =>
lia
:
core
.
Lemma
poly_of_formula_valid_compat
:
forall
f
,
exists
n
,
valid
n
(
poly_of_formula
f
).
Lemma
poly_of_formula_sound
:
forall
fl
fr
var
,
poly_of_formula
fl
=
poly_of_formula
fr
->
formula_eval
var
fl
=
formula_eval
var
fr
.
End
Translation
.
Section
Completeness
.
Lemma
reduce_poly_of_formula_sound
:
forall
fl
fr
var
,
reduce
(
poly_of_formula
fl
)
=
reduce
(
poly_of_formula
fr
)
->
formula_eval
var
fl
=
formula_eval
var
fr
.
Definition
make_last
{
A
}
n
(
x
def
:
A
) :=
Pos.peano_rect
(
fun
_
=>
list
A
)
(
cons
x
nil
)
(
fun
_
F
=>
cons
def
F
)
n
.
Fixpoint
list_replace
l
n
b
:=
match
l
with
|
nil
=>
make_last
n
b
false
|
cons
a
l
=>
Pos.peano_rect
_
(
cons
b
l
) (
fun
n
_
=>
cons
a
(
list_replace
l
n
b
))
n
end
.
Extract a non-null witness from a polynomial
Fixpoint
boolean_witness
p
:=
match
p
with
|
Cst
c
=>
nil
|
Poly
p
i
q
=>
if
decide
(
null
p
)
then
let
var
:=
boolean_witness
q
in
list_replace
var
i
true
else
let
var
:=
boolean_witness
p
in
list_replace
var
i
false
end
.
Lemma
list_nth_base
:
forall
A
(
def
:
A
)
l
,
list_nth
1
l
def
=
match
l
with
nil
=>
def
|
cons
x
_
=>
x
end
.
Lemma
list_nth_succ
:
forall
A
n
(
def
:
A
)
l
,
list_nth
(
Pos.succ
n
)
l
def
=
match
l
with
nil
=>
def
|
cons
_
l
=>
list_nth
n
l
def
end
.
Lemma
list_nth_nil
:
forall
A
n
(
def
:
A
),
list_nth
n
nil
def
=
def
.
Lemma
make_last_nth_1
:
forall
A
n
i
x
def
,
i
<>
n
->
list_nth
i
(@
make_last
A
n
x
def
)
def
=
def
.
Lemma
make_last_nth_2
:
forall
A
n
x
def
,
list_nth
n
(@
make_last
A
n
x
def
)
def
=
x
.
Lemma
list_replace_nth_1
:
forall
var
i
j
x
,
i
<>
j
->
list_nth
i
(
list_replace
var
j
x
)
false
=
list_nth
i
var
false
.
Lemma
list_replace_nth_2
:
forall
var
i
x
,
list_nth
i
(
list_replace
var
i
x
)
false
=
x
.
Lemma
boolean_witness_nonzero
:
forall
k
p
,
linear
k
p
->
~
null
p
->
eval
(
boolean_witness
p
)
p
=
true
.
Lemma
reduce_poly_of_formula_sound_alt
:
forall
var
fl
fr
,
reduce
(
poly_add
(
poly_of_formula
fl
) (
poly_of_formula
fr
))
=
Cst
false
->
formula_eval
var
fl
=
formula_eval
var
fr
.
End
Completeness
.
Global Transparent
decide
poly_add
.