Library Coq.micromega.RingMicromega
Rule of "signs" for addition and multiplication.
An arbitrary result is coded buy None.
Given a list l of NFormula and an extended polynomial expression
e, if eval_Psatz l e succeeds (= Some f) then f is a
logic consequence of the conjunction of the formulae in l.
Moreover, the polynomial expression is obtained by replacing the (PsatzIn n)
by the nth polynomial expression in l and the sign is computed by the "rule of sign"
Definition map_option (
A B:
Type) (
f :
A -> option B) (
o :
option A) :
option B :=
match o with
|
None =>
None
|
Some x =>
f x
end.
Definition map_option2 (
A B C :
Type) (
f :
A -> B -> option C)
(
o:
option A) (
o':
option B) :
option C :=
match o ,
o' with
|
None ,
_ =>
None
|
_ ,
None =>
None
|
Some x ,
Some x' =>
f x x'
end.
Definition Rops_wd :=
mk_reqe
(
SORplus_wd sor)
(
SORtimes_wd sor)
(
SORopp_wd sor).
Definition pexpr_times_nformula (
e:
PolC) (
f :
NFormula) :
option NFormula :=
let (
ef,
o) :=
f in
match o with
|
Equal =>
Some (Pmul cO cI cplus ctimes ceqb e ef , Equal)
|
_ =>
None
end.
Definition nformula_times_nformula (
f1 f2 :
NFormula) :
option NFormula :=
let (
e1,
o1) :=
f1 in
let (
e2,
o2) :=
f2 in
map_option (
fun x => (
Some (Pmul cO cI cplus ctimes ceqb e1 e2,x))) (
OpMult o1 o2).
Definition nformula_plus_nformula (
f1 f2 :
NFormula) :
option NFormula :=
let (
e1,
o1) :=
f1 in
let (
e2,
o2) :=
f2 in
map_option (
fun x => (
Some (Padd cO cplus ceqb e1 e2,x))) (
OpAdd o1 o2).
Fixpoint eval_Psatz (
l :
list NFormula) (
e :
Psatz) {
struct e} :
option NFormula :=
match e with
|
PsatzIn n =>
Some (
nth n l (Pc cO, Equal))
|
PsatzSquare e =>
Some (Psquare cO cI cplus ctimes ceqb e , NonStrict)
|
PsatzMulC re e =>
map_option (
pexpr_times_nformula re) (
eval_Psatz l e)
|
PsatzMulE f1 f2 =>
map_option2 nformula_times_nformula (
eval_Psatz l f1) (
eval_Psatz l f2)
|
PsatzAdd f1 f2 =>
map_option2 nformula_plus_nformula (
eval_Psatz l f1) (
eval_Psatz l f2)
|
PsatzC c =>
if cltb cO c then Some (Pc c, Strict) else None
|
PsatzZ =>
Some (Pc cO, Equal)
end.
Lemma pexpr_times_nformula_correct :
forall (
env:
PolEnv) (
e:
PolC) (
f f' :
NFormula),
eval_nformula env f -> pexpr_times_nformula e f = Some f' ->
eval_nformula env f'.
Lemma nformula_times_nformula_correct :
forall (
env:
PolEnv)
(
f1 f2 f :
NFormula),
eval_nformula env f1 -> eval_nformula env f2 ->
nformula_times_nformula f1 f2 = Some f ->
eval_nformula env f.
Lemma nformula_plus_nformula_correct :
forall (
env:
PolEnv)
(
f1 f2 f :
NFormula),
eval_nformula env f1 -> eval_nformula env f2 ->
nformula_plus_nformula f1 f2 = Some f ->
eval_nformula env f.
Lemma eval_Psatz_Sound :
forall (
l :
list NFormula) (
env :
PolEnv),
(forall (
f :
NFormula),
In f l -> eval_nformula env f) ->
forall (
e :
Psatz) (
f :
NFormula),
eval_Psatz l e = Some f ->
eval_nformula env f.
Fixpoint ge_bool (
n m :
nat) :
bool :=
match n with
|
O =>
match m with
|
O =>
true
|
S _ =>
false
end
|
S n =>
match m with
|
O =>
true
|
S m =>
ge_bool n m
end
end.
Lemma ge_bool_cases :
forall n m,
(
if ge_bool n m then n >= m else n < m)%
nat.
Fixpoint xhyps_of_psatz (
base:
nat) (
acc :
list nat) (
prf :
Psatz) :
list nat :=
match prf with
|
PsatzC _ |
PsatzZ |
PsatzSquare _ =>
acc
|
PsatzMulC _ prf =>
xhyps_of_psatz base acc prf
|
PsatzAdd e1 e2 |
PsatzMulE e1 e2 =>
xhyps_of_psatz base (
xhyps_of_psatz base acc e2)
e1
|
PsatzIn n =>
if ge_bool n base then (
n::acc)
else acc
end.
Fixpoint nhyps_of_psatz (
prf :
Psatz) :
list nat :=
match prf with
|
PsatzC _ |
PsatzZ |
PsatzSquare _ =>
nil
|
PsatzMulC _ prf =>
nhyps_of_psatz prf
|
PsatzAdd e1 e2 |
PsatzMulE e1 e2 =>
nhyps_of_psatz e1 ++ nhyps_of_psatz e2
|
PsatzIn n =>
n :: nil
end.
Fixpoint (
l:
list NFormula) (
ln :
list nat) :
list NFormula :=
match ln with
|
nil =>
nil
|
n::ln =>
nth n l (Pc cO, Equal) :: extract_hyps l ln
end.
Lemma :
forall l ln1 ln2,
extract_hyps l (
ln1 ++ ln2)
= (extract_hyps l ln1) ++ (extract_hyps l ln2).
Ltac inv H :=
inversion H ;
try subst ;
clear H.
Lemma nhyps_of_psatz_correct :
forall (
env :
PolEnv) (
e:
Psatz) (
l :
list NFormula) (
f:
NFormula),
eval_Psatz l e = Some f ->
((forall f',
In f' (
extract_hyps l (
nhyps_of_psatz e))
-> eval_nformula env f') -> eval_nformula env f).
Definition paddC :=
PaddC cplus.
Definition psubC :=
PsubC cminus.
Definition PsubC_ok :
forall c P env,
eval_pol env (
psubC P c)
== eval_pol env P - [c] :=
let Rops_wd :=
mk_reqe
(
SORplus_wd sor)
(
SORtimes_wd sor)
(
SORopp_wd sor)
in
PsubC_ok (
SORsetoid sor)
Rops_wd (
Rth_ARth (
SORsetoid sor)
Rops_wd (
SORrt sor))
(
SORrm addon).
Definition PaddC_ok :
forall c P env,
eval_pol env (
paddC P c)
== eval_pol env P + [c] :=
let Rops_wd :=
mk_reqe
(
SORplus_wd sor)
(
SORtimes_wd sor)
(
SORopp_wd sor)
in
PaddC_ok (
SORsetoid sor)
Rops_wd (
Rth_ARth (
SORsetoid sor)
Rops_wd (
SORrt sor))
(
SORrm addon).
Definition check_inconsistent (
f :
NFormula) :
bool :=
let (
e,
op) :=
f in
match e with
|
Pc c =>
match op with
|
Equal =>
cneqb c cO
|
NonStrict =>
c [<] cO
|
Strict =>
c [<=] cO
|
NonEqual =>
c [=] cO
end
|
_ =>
false
end.
Lemma check_inconsistent_sound :
forall (
p :
PolC) (
op :
Op1),
check_inconsistent (p, op) = true -> forall env,
~ eval_op1 op (
eval_pol env p).
Definition check_normalised_formulas :
list NFormula -> Psatz -> bool :=
fun l cm =>
match eval_Psatz l cm with
|
None =>
false
|
Some f =>
check_inconsistent f
end.
Lemma checker_nf_sound :
forall (
l :
list NFormula) (
cm :
Psatz),
check_normalised_formulas l cm = true ->
forall env :
PolEnv,
make_impl (
eval_nformula env)
l False.
Normalisation of formulae
Inductive Op2 :
Set :=
|
OpEq
|
OpNEq
|
OpLe
|
OpGe
|
OpLt
|
OpGt.
Definition eval_op2 (
o :
Op2) :
R -> R -> Prop :=
match o with
|
OpEq =>
req
|
OpNEq =>
fun x y :
R =>
x ~= y
|
OpLe =>
rle
|
OpGe =>
fun x y :
R =>
y <= x
|
OpLt =>
fun x y :
R =>
x < y
|
OpGt =>
fun x y :
R =>
y < x
end.
Definition eval_pexpr :
PolEnv -> PExpr C -> R :=
PEeval rplus rtimes rminus ropp phi pow_phi rpow.
#[
universes(
template)]
Record Formula (
T:
Type) :
Type :=
Build_Formula{
Flhs :
PExpr T;
Fop :
Op2;
Frhs :
PExpr T
}.
Definition eval_formula (
env :
PolEnv) (
f :
Formula C) :
Prop :=
let (
lhs,
op,
rhs) :=
f in
(
eval_op2 op) (
eval_pexpr env lhs) (
eval_pexpr env rhs).
Definition norm :=
norm_aux cO cI cplus ctimes cminus copp ceqb.
Definition psub :=
Psub cO cplus cminus copp ceqb.
Definition padd :=
Padd cO cplus ceqb.
Definition pmul :=
Pmul cO cI cplus ctimes ceqb.
Definition popp :=
Popp copp.
Definition normalise (
f :
Formula C) :
NFormula :=
let (
lhs,
op,
rhs) :=
f in
let lhs :=
norm lhs in
let rhs :=
norm rhs in
match op with
|
OpEq =>
(psub lhs rhs, Equal)
|
OpNEq =>
(psub lhs rhs, NonEqual)
|
OpLe =>
(psub rhs lhs, NonStrict)
|
OpGe =>
(psub lhs rhs, NonStrict)
|
OpGt =>
(psub lhs rhs, Strict)
|
OpLt =>
(psub rhs lhs, Strict)
end.
Definition negate (
f :
Formula C) :
NFormula :=
let (
lhs,
op,
rhs) :=
f in
let lhs :=
norm lhs in
let rhs :=
norm rhs in
match op with
|
OpEq =>
(psub rhs lhs, NonEqual)
|
OpNEq =>
(psub rhs lhs, Equal)
|
OpLe =>
(psub lhs rhs, Strict)
|
OpGe =>
(psub rhs lhs, Strict)
|
OpGt =>
(psub rhs lhs, NonStrict)
|
OpLt =>
(psub lhs rhs, NonStrict)
end.
Lemma eval_pol_sub :
forall env lhs rhs,
eval_pol env (
psub lhs rhs)
== eval_pol env lhs - eval_pol env rhs.
Lemma eval_pol_add :
forall env lhs rhs,
eval_pol env (
padd lhs rhs)
== eval_pol env lhs + eval_pol env rhs.
Lemma eval_pol_mul :
forall env lhs rhs,
eval_pol env (
pmul lhs rhs)
== eval_pol env lhs * eval_pol env rhs.
Lemma eval_pol_opp :
forall env e,
eval_pol env (
popp e)
== - eval_pol env e.
Lemma eval_pol_norm :
forall env lhs,
eval_pexpr env lhs == eval_pol env (
norm lhs).
Theorem normalise_sound :
forall (
env :
PolEnv) (
f :
Formula C),
eval_formula env f <-> eval_nformula env (
normalise f).
Theorem negate_correct :
forall (
env :
PolEnv) (
f :
Formula C),
eval_formula env f <-> ~ (eval_nformula env (
negate f)
).
Another normalisation - this is used for cnf conversion
Definition xnormalise (
f:
NFormula) :
list (
NFormula) :=
let (
e,
o) :=
f in
match o with
|
Equal =>
(e , Strict) :: (popp e, Strict) :: nil
|
NonEqual =>
(e , Equal) :: nil
|
Strict =>
(popp e, NonStrict) :: nil
|
NonStrict =>
(popp e, Strict) :: nil
end.
Definition xnegate (
t:
NFormula) :
list (
NFormula) :=
let (
e,
o) :=
t in
match o with
|
Equal =>
(e,Equal) :: nil
|
NonEqual =>
(e,Strict)::(popp e,Strict)::nil
|
Strict =>
(e,Strict) :: nil
|
NonStrict =>
(e,NonStrict) :: nil
end.
Import Coq.micromega.Tauto.
Definition cnf_of_list {
T :
Type} (
l:
list NFormula) (
tg :
T) :
cnf NFormula T :=
List.fold_right (
fun x acc =>
if check_inconsistent x then acc else ((x,tg)::nil)::acc)
(
cnf_tt _ _)
l.
Add Ring SORRing : (
SORrt sor).
Lemma cnf_of_list_correct :
forall (
T :
Type)
env l tg,
eval_cnf (
Annot:=
T)
eval_nformula env (
cnf_of_list l tg)
<->
make_conj (
fun x :
NFormula =>
eval_nformula env x -> False)
l.
Definition cnf_normalise {
T:
Type} (
t:
Formula C) (
tg:
T) :
cnf NFormula T :=
let f :=
normalise t in
if check_inconsistent f then cnf_ff _ _
else cnf_of_list (
xnormalise f)
tg.
Definition cnf_negate {
T:
Type} (
t:
Formula C) (
tg:
T) :
cnf NFormula T :=
let f :=
normalise t in
if check_inconsistent f then cnf_tt _ _
else cnf_of_list (
xnegate f)
tg.
Lemma eq0_cnf :
forall x,
(0
< x -> False) /\ (0
< - x -> False) <-> x == 0.
Lemma xnormalise_correct :
forall env f,
(make_conj (
fun x =>
eval_nformula env x -> False) (
xnormalise f)
) <-> eval_nformula env f.
Lemma xnegate_correct :
forall env f,
(make_conj (
fun x =>
eval_nformula env x -> False) (
xnegate f)
) <-> ~ eval_nformula env f.
Lemma cnf_normalise_correct :
forall (
T :
Type)
env t tg,
eval_cnf (
Annot:=
T)
eval_nformula env (
cnf_normalise t tg)
<-> eval_formula env t.
Lemma cnf_negate_correct :
forall (
T :
Type)
env t (
tg:
T),
eval_cnf eval_nformula env (
cnf_negate t tg)
<-> ~ eval_formula env t.
Lemma eval_nformula_dec :
forall env d,
(eval_nformula env d) \/ ~ (eval_nformula env d).
Reverse transformation
Sometimes it is convenient to make a distinction between "syntactic" coefficients and "real"
coefficients that are used to actually compute
equality might be (too) strong
Some syntactic simplifications of expressions
Definition simpl_cone (
e:
Psatz) :
Psatz :=
match e with
|
PsatzSquare t =>
match t with
|
Pc c =>
if ceqb cO c then PsatzZ else PsatzC (
ctimes c c)
|
_ =>
PsatzSquare t
end
|
PsatzMulE t1 t2 =>
match t1 ,
t2 with
|
PsatzZ ,
x =>
PsatzZ
|
x ,
PsatzZ =>
PsatzZ
|
PsatzC c ,
PsatzC c' =>
PsatzC (
ctimes c c')
|
PsatzC p1 ,
PsatzMulE (
PsatzC p2)
x =>
PsatzMulE (
PsatzC (
ctimes p1 p2))
x
|
PsatzC p1 ,
PsatzMulE x (
PsatzC p2) =>
PsatzMulE (
PsatzC (
ctimes p1 p2))
x
|
PsatzMulE (
PsatzC p2)
x ,
PsatzC p1 =>
PsatzMulE (
PsatzC (
ctimes p1 p2))
x
|
PsatzMulE x (
PsatzC p2) ,
PsatzC p1 =>
PsatzMulE (
PsatzC (
ctimes p1 p2))
x
|
PsatzC x ,
PsatzAdd y z =>
PsatzAdd (
PsatzMulE (
PsatzC x)
y) (
PsatzMulE (
PsatzC x)
z)
|
PsatzC c ,
_ =>
if ceqb cI c then t2 else PsatzMulE t1 t2
|
_ ,
PsatzC c =>
if ceqb cI c then t1 else PsatzMulE t1 t2
|
_ ,
_ =>
e
end
|
PsatzAdd t1 t2 =>
match t1 ,
t2 with
|
PsatzZ ,
x =>
x
|
x ,
PsatzZ =>
x
|
x ,
y =>
PsatzAdd x y
end
|
_ =>
e
end.
End Micromega.