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.
Require Coq.micromega.Tauto.
Set Implicit Arguments.
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 : Type. 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 (@Equivalence_Reflexive _ _ (SORsetoid sor))
symmetry proved by (@Equivalence_Symmetric _ _ (SORsetoid sor))
transitivity proved by (@Equivalence_Transitive _ _ (SORsetoid sor))
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 : PolEnv -> PolC -> R :=
Pphi rplus rtimes phi.
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 :=
| PsatzLet: Psatz -> Psatz -> Psatz
| PsatzIn : nat -> Psatz
| PsatzSquare : PolC -> Psatz
| PsatzMulC : PolC -> Psatz -> Psatz
| PsatzMulE : Psatz -> Psatz -> Psatz
| PsatzAdd : Psatz -> Psatz -> Psatz
| PsatzC : C -> Psatz
| PsatzZ : Psatz.
Register PsatzLet as micromega.Psatz.PsatzLet.
Register PsatzIn as micromega.Psatz.PsatzIn.
Register PsatzSquare as micromega.Psatz.PsatzSquare.
Register PsatzMulC as micromega.Psatz.PsatzMulC.
Register PsatzMulE as micromega.Psatz.PsatzMulE.
Register PsatzAdd as micromega.Psatz.PsatzAdd.
Register PsatzC as micromega.Psatz.PsatzC.
Register PsatzZ as micromega.Psatz.PsatzZ.
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.
Arguments map_option [A B] f o.
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.
Arguments map_option2 [A B C] f o o'.
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
| PsatzLet p1 p2 => match eval_Psatz l p1 with
| None => None
| Some f => eval_Psatz (f::l) p2
end
| 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
| PsatzLet e1 e2 => xhyps_of_psatz base (xhyps_of_psatz (S base) acc e2) e1
end.
Fixpoint nhyps_of_psatz (base:nat) (prf : Psatz) : list nat :=
match prf with
| PsatzC _ | PsatzZ | PsatzSquare _ => nil
| PsatzMulC _ prf => nhyps_of_psatz base prf
| PsatzAdd e1 e2 | PsatzMulE e1 e2 => nhyps_of_psatz base e1 ++ nhyps_of_psatz base e2
| PsatzIn n => if ge_bool n base then (n::nil) else nil
| PsatzLet e1 e2 => nhyps_of_psatz base e1 ++ nhyps_of_psatz (S base) e2
end.
Fixpoint extract_hyps (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 extract_hyps_app : 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.
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.
Register OpEq as micromega.Op2.OpEq.
Register OpNEq as micromega.Op2.OpNEq.
Register OpLe as micromega.Op2.OpLe.
Register OpGe as micromega.Op2.OpGe.
Register OpLt as micromega.Op2.OpLt.
Register OpGt as micromega.Op2.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
}.
Register Formula as micromega.Formula.type.
Register Build_Formula as micromega.Formula.Build_Formula.
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
Fixpoint xdenorm (jmp : positive) (p: Pol C) : PExpr C :=
match p with
| Pc c => PEc c
| Pinj j p => xdenorm (Pos.add j jmp ) p
| PX p j q => PEadd
(PEmul (xdenorm jmp p) (PEpow (PEX jmp) (Npos j)))
(xdenorm (Pos.succ jmp) q)
end.
Lemma xdenorm_correct : forall p i env,
eval_pol (jump i env) p == eval_pexpr env (xdenorm (Pos.succ i) p).
Definition denorm := xdenorm xH.
Lemma denorm_correct : forall p env, eval_pol env p == eval_pexpr env (denorm p).
Sometimes it is convenient to make a distinction between "syntactic" coefficients and "real"
coefficients that are used to actually compute
Variable S : Type.
Variable C_of_S : S -> C.
Variable phiS : S -> R.
Variable phi_C_of_S : forall c, phiS c = phi (C_of_S c).
Fixpoint map_PExpr (e : PExpr S) : PExpr C :=
match e with
| PEc c => PEc (C_of_S c)
| PEX p => PEX p
| PEadd e1 e2 => PEadd (map_PExpr e1) (map_PExpr e2)
| PEsub e1 e2 => PEsub (map_PExpr e1) (map_PExpr e2)
| PEmul e1 e2 => PEmul (map_PExpr e1) (map_PExpr e2)
| PEopp e => PEopp (map_PExpr e)
| PEpow e n => PEpow (map_PExpr e) n
end.
Definition map_Formula (f : Formula S) : Formula C :=
let (l,o,r) := f in
Build_Formula (map_PExpr l) o (map_PExpr r).
Definition eval_sexpr : PolEnv -> PExpr S -> R :=
PEeval rplus rtimes rminus ropp phiS pow_phi rpow.
Definition eval_sformula (env : PolEnv) (f : Formula S) : Prop :=
let (lhs, op, rhs) := f in
(eval_op2 op) (eval_sexpr env lhs) (eval_sexpr env rhs).
Lemma eval_pexprSC : forall env s, eval_sexpr env s = eval_pexpr env (map_PExpr s).
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 , _ => PsatzZ
| _ , 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.