# Library Coq.micromega.RingMicromega

Require Import NArith.
Require Import Relation_Definitions.
Require Import Setoid.
Require Import Env.
Require Import EnvRing.
Require Import List.
Require Import Bool.
Require Import OrderedRing.
Require Import Refl.
Import OrderedRingSyntax.
Section Micromega.
Variable R : Type.
Variables rO rI : R.
Variables rplus rtimes rminus: R -> R -> R.
Variable ropp : R -> R.
Variables req rle rlt : R -> R -> Prop.
Variable sor : SOR rO rI rplus rtimes rminus ropp req rle rlt.
Notation "0" := rO.
Notation "1" := rI.
Notation "x + y" := (rplus x y).
Notation "x * y " := (rtimes x y).
Notation "x - y " := (rminus x y).
Notation "- x" := (ropp x).
Notation "x == y" := (req x y).
Notation "x ~= y" := (~ req x y).
Notation "x <= y" := (rle x y).
Notation "x < y" := (rlt x y).
Variable C : Type.
Variables cO cI : C.
Variables cplus ctimes cminus: C -> C -> C.
Variable copp : C -> C.
Variables ceqb cleb : C -> C -> bool.
Variable phi : C -> R.
Variable E : Set. Variable pow_phi : N -> E.
Variable rpow : R -> E -> R.
Notation "[ x ]" := (phi x).
Notation "x [=] y" := (ceqb x y).
Notation "x [<=] y" := (cleb x y).
Record SORaddon := mk_SOR_addon {
SORrm : ring_morph 0 1 rplus rtimes rminus ropp req cO cI cplus ctimes cminus copp ceqb phi;
SORpower : power_theory rI rtimes req pow_phi rpow;
SORcneqb_morph : forall x y : C, x [=] y = false -> [x] ~= [y];
SORcleb_morph : forall x y : C, x [<=] y = true -> [x] <= [y]
}.
Variable addon : SORaddon.
Add Relation R req
reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _ )
symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _ )
transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _ )
as micomega_sor_setoid.
Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
Add Morphism rtimes with signature req ==> req ==> req as rtimes_morph.
Add Morphism ropp with signature req ==> req as ropp_morph.
Add Morphism rle with signature req ==> req ==> iff as rle_morph.
Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
Definition cneqb (x y : C) := negb (ceqb x y).
Definition cltb (x y : C) := (cleb x y) && (cneqb x y).
Notation "x [~=] y" := (cneqb x y).
Notation "x [<] y" := (cltb x y).
Ltac le_less := rewrite (Rle_lt_eq sor); left; try assumption.
Ltac le_equal := rewrite (Rle_lt_eq sor); right; try reflexivity; try assumption.
Ltac le_elim H := rewrite (Rle_lt_eq sor) in H; destruct H as [H | H].
Lemma cleb_sound : forall x y : C, x [<=] y = true -> [x] <= [y].
Lemma cneqb_sound : forall x y : C, x [~=] y = true -> [x] ~= [y].
Lemma cltb_sound : forall x y : C, x [<] y = true -> [x] < [y].
Definition PolC := Pol C. Definition PolEnv := Env R. Definition eval_pol (env : PolEnv) (p:PolC) : R :=
Pphi 0 rplus rtimes phi env p.
Inductive Op1 : Set :=
| Equal
| NonEqual
| Strict
| NonStrict .
Definition NFormula := (PolC * Op1)%type.
Definition eval_op1 (o : Op1) : R -> Prop :=
match o with
| Equal => fun x => x == 0
| NonEqual => fun x : R => x ~= 0
| Strict => fun x : R => 0 < x
| NonStrict => fun x : R => 0 <= x
end.
Definition eval_nformula (env : PolEnv) (f : NFormula) : Prop :=
let (p, op) := f in eval_op1 op (eval_pol env p).
Rule of "signs" for addition and multiplication. An arbitrary result is coded buy None.
Definition OpMult (o o' : Op1) : option Op1 :=
match o with
| Equal => Some Equal
| NonStrict =>
match o' with
| Equal => Some Equal
| NonEqual => None
| Strict => Some NonStrict
| NonStrict => Some NonStrict
end
| Strict => match o' with
| NonEqual => None
| _ => Some o'
end
| NonEqual => match o' with
| Equal => Some Equal
| NonEqual => Some NonEqual
| _ => None
end
end.
Definition OpAdd (o o': Op1) : option Op1 :=
match o with
| Equal => Some o'
| NonStrict =>
match o' with
| Strict => Some Strict
| NonEqual => None
| _ => Some NonStrict
end
| Strict => match o' with
| NonEqual => None
| _ => Some Strict
end
| NonEqual => match o' with
| Equal => Some NonEqual
| _ => None
end
end.
Lemma OpMult_sound :
forall (o o' om: Op1) (x y : R),
eval_op1 o x -> eval_op1 o' y -> OpMult o o' = Some om -> eval_op1 om (x * y).
Lemma OpAdd_sound :
forall (o o' oa : Op1) (e e' : R),
eval_op1 o e -> eval_op1 o' e' -> OpAdd o o' = Some oa -> eval_op1 oa (e + e').
Inductive Psatz : Type :=
| PsatzIn : nat -> Psatz
| PsatzSquare : PolC -> Psatz
| PsatzMulC : PolC -> Psatz -> Psatz
| PsatzMulE : Psatz -> Psatz -> Psatz
| PsatzAdd : Psatz -> Psatz -> Psatz
| PsatzC : C -> Psatz
| PsatzZ : Psatz.
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.
Implicit Arguments map_option [A B].
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.
Implicit Arguments map_option2 [A B C].
Definition Rops_wd := mk_reqe rplus rtimes ropp req
sor.(SORplus_wd)
sor.(SORtimes_wd)
sor.(SORopp_wd).
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.
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 rplus rtimes ropp req
sor.(SORplus_wd)
sor.(SORtimes_wd)
sor.(SORopp_wd) in
PsubC_ok sor.(SORsetoid) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt))
addon.(SORrm).
Definition PaddC_ok : forall c P env, eval_pol env (paddC P c) == eval_pol env P + [c] :=
let Rops_wd := mk_reqe rplus rtimes ropp req
sor.(SORplus_wd)
sor.(SORtimes_wd)
sor.(SORopp_wd) in
PaddC_ok sor.(SORsetoid) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt))
addon.(SORrm).
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 (l : PolEnv) (pe : PExpr C) : R := PEeval rplus rtimes rminus ropp phi pow_phi rpow l pe.
Record Formula : Type := {
Flhs : PExpr C;
Fop : Op2;
Frhs : PExpr C
}.
Definition eval_formula (env : PolEnv) (f : Formula) : 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 normalise (f : Formula) : 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) : 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_norm : forall env lhs, eval_pexpr env lhs == eval_pol env (norm lhs).
Theorem normalise_sound :
forall (env : PolEnv) (f : Formula),
eval_formula env f -> eval_nformula env (normalise f).
Theorem negate_correct :
forall (env : PolEnv) (f : Formula),
eval_formula env f <-> ~ (eval_nformula env (negate f)).
Another normalistion - this is used for cnf conversion
Definition xnormalise (t:Formula) : list (NFormula) :=
let (lhs,o,rhs) := t in
let lhs := norm lhs in
let rhs := norm rhs in
match o with
| OpEq =>
(psub lhs rhs, Strict)::(psub rhs lhs , Strict)::nil
| OpNEq => (psub lhs rhs,Equal) :: nil
| OpGt => (psub rhs lhs,NonStrict) :: nil
| OpLt => (psub lhs rhs,NonStrict) :: nil
| OpGe => (psub rhs lhs , Strict) :: nil
| OpLe => (psub lhs rhs ,Strict) :: nil
end.
Require Import Tauto.
Definition cnf_normalise (t:Formula) : cnf (NFormula) :=
List.map (fun x => x::nil) (xnormalise t).
Add Ring SORRing : sor.(SORrt).
Lemma cnf_normalise_correct : forall env t, eval_cnf (eval_nformula env) (cnf_normalise t) -> eval_formula env t.
Definition xnegate (t:Formula) : list (NFormula) :=
let (lhs,o,rhs) := t in
let lhs := norm lhs in
let rhs := norm rhs in
match o with
| OpEq => (psub lhs rhs,Equal) :: nil
| OpNEq => (psub lhs rhs ,Strict)::(psub rhs lhs,Strict)::nil
| OpGt => (psub lhs rhs,Strict) :: nil
| OpLt => (psub rhs lhs,Strict) :: nil
| OpGe => (psub lhs rhs,NonStrict) :: nil
| OpLe => (psub rhs lhs,NonStrict) :: nil
end.
Definition cnf_negate (t:Formula) : cnf (NFormula) :=
List.map (fun x => x::nil) (xnegate t).
Lemma cnf_negate_correct : forall env t, eval_cnf (eval_nformula env) (cnf_negate t) -> ~ eval_formula env t.
Lemma eval_nformula_dec : forall env d, (eval_nformula env d) \/ ~ (eval_nformula env d).
Reverse transformation
Fixpoint xdenorm (jmp : positive) (p: Pol C) : PExpr C :=
match p with
| Pc c => PEc c
| Pinj j p => xdenorm (Pplus j jmp ) p
| PX p j q => PEadd
(PEmul (xdenorm jmp p) (PEpow (PEX _ jmp) (Npos j)))
(xdenorm (Psucc jmp) q)
end.
Lemma xdenorm_correct : forall p i env, eval_pol (jump i env) p == eval_pexpr env (xdenorm (Psucc i) p).
Definition denorm (p : Pol C) := xdenorm xH p.
Lemma denorm_correct : forall p env, eval_pol env p == eval_pexpr env (denorm p).
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.