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 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.
Proof.
exact sor.(SORplus_wd).
Qed.
Add Morphism rtimes with signature req ==> req ==> req as rtimes_morph.
Proof.
exact sor.(SORtimes_wd).
Qed.
Add Morphism ropp with signature req ==> req as ropp_morph.
Proof.
exact sor.(SORopp_wd).
Qed.
Add Morphism rle with signature req ==> req ==> iff as rle_morph.
Proof.
exact sor.(SORle_wd).
Qed.
Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
Proof.
exact sor.(SORlt_wd).
Qed.
Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
Proof.
exact (rminus_morph sor). Qed.
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].
Proof.
exact addon.(SORcleb_morph).
Qed.
Lemma cneqb_sound : forall x y : C, x [~=] y = true -> [x] ~= [y].
Proof.
intros x y H1. apply addon.(SORcneqb_morph). unfold cneqb, negb in H1.
destruct (ceqb x y); now try discriminate.
Qed.
Lemma cltb_sound : forall x y : C, x [<] y = true -> [x] < [y].
Proof.
intros x y H. unfold cltb in H. apply andb_prop in H. destruct H as [H1 H2].
apply cleb_sound in H1. apply cneqb_sound in H2. apply <- (Rlt_le_neq sor). now split.
Qed.
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).
Proof.
unfold eval_op1; destruct o; simpl; intros o' om x y H1 H2 H3.
inversion H3. rewrite H1. now rewrite (Rtimes_0_l sor).
destruct o' ; inversion H3.
rewrite H2. now rewrite (Rtimes_0_r sor).
apply (Rtimes_neq_0 sor) ; auto.
destruct o' ; inversion H3.
rewrite H2; now rewrite (Rtimes_0_r sor).
now apply (Rtimes_pos_pos sor).
apply (Rtimes_nonneg_nonneg sor); [le_less | assumption].
destruct o' ; inversion H3.
rewrite H2; now rewrite (Rtimes_0_r sor).
apply (Rtimes_nonneg_nonneg sor); [assumption | le_less ].
now apply (Rtimes_nonneg_nonneg sor).
Qed.
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').
Proof.
unfold eval_op1; destruct o; simpl; intros o' oa e e' H1 H2 Hoa.
inversion Hoa. rewrite <- H0.
destruct o' ; rewrite H1 ; now rewrite (Rplus_0_l sor).
destruct o'.
inversion Hoa.
rewrite H2. now rewrite (Rplus_0_r sor).
discriminate.
discriminate.
discriminate.
destruct o'.
inversion Hoa.
rewrite H2. now rewrite (Rplus_0_r sor).
discriminate.
inversion Hoa.
now apply (Rplus_pos_pos sor).
inversion Hoa.
now apply (Rplus_pos_nonneg sor).
destruct o'.
inversion Hoa.
now rewrite H2, (Rplus_0_r sor).
discriminate.
inversion Hoa.
now apply (Rplus_nonneg_pos sor).
inversion Hoa.
now apply (Rplus_nonneg_nonneg sor).
Qed.
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.
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
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'.
Proof.
unfold pexpr_times_nformula.
destruct f.
intros. destruct o ; inversion H0 ; try discriminate.
simpl in *. unfold eval_pol in *.
rewrite (Pmul_ok sor.(SORsetoid) Rops_wd
(Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm)).
rewrite H. apply (Rtimes_0_r sor).
Qed.
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.
Proof.
unfold nformula_times_nformula.
destruct f1 ; destruct f2.
case_eq (OpMult o o0) ; simpl ; try discriminate.
intros. inversion H2 ; simpl.
unfold eval_pol.
destruct o1; simpl;
rewrite (Pmul_ok sor.(SORsetoid) Rops_wd
(Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm));
apply OpMult_sound with (3:= H);assumption.
Qed.
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.
Proof.
unfold nformula_plus_nformula.
destruct f1 ; destruct f2.
case_eq (OpAdd o o0) ; simpl ; try discriminate.
intros. inversion H2 ; simpl.
unfold eval_pol.
destruct o1; simpl;
rewrite (Padd_ok sor.(SORsetoid) Rops_wd
(Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm));
apply OpAdd_sound with (3:= H);assumption.
Qed.
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.
Proof.
induction e.
simpl ; intros.
destruct (nth_in_or_default n l (Pc cO, Equal)) as [Hin|Heq].
apply H. congruence.
inversion H0.
rewrite Heq. simpl.
now apply addon.(SORrm).(morph0).
simpl. intros. inversion H0.
simpl. unfold eval_pol.
rewrite (Psquare_ok sor.(SORsetoid) Rops_wd
(Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm));
now apply (Rtimes_square_nonneg sor).
simpl.
intro.
case_eq (eval_Psatz l e) ; simpl ; intros.
apply IHe in H0.
apply pexpr_times_nformula_correct with (1:=H0) (2:= H1).
discriminate.
simpl ; intro.
case_eq (eval_Psatz l e1) ; simpl ; try discriminate.
case_eq (eval_Psatz l e2) ; simpl ; try discriminate.
intros.
apply IHe1 in H1. apply IHe2 in H0.
apply (nformula_times_nformula_correct env n0 n) ; assumption.
simpl ; intro.
case_eq (eval_Psatz l e1) ; simpl ; try discriminate.
case_eq (eval_Psatz l e2) ; simpl ; try discriminate.
intros.
apply IHe1 in H1. apply IHe2 in H0.
apply (nformula_plus_nformula_correct env n0 n) ; assumption.
simpl.
intro. case_eq (cO [<] c).
intros. inversion H1. simpl.
rewrite <- addon.(SORrm).(morph0). now apply cltb_sound.
discriminate.
simpl. intros. inversion H0.
simpl. apply addon.(SORrm).(morph0).
Qed.
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.
Proof.
induction n; destruct m ; simpl; auto with arith.
specialize (IHn m). destruct (ge_bool); auto with arith.
Qed.
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 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).
Proof.
induction ln1.
reflexivity.
simpl.
intros.
rewrite IHln1. reflexivity.
Qed.
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).
Proof.
induction e ; intros.
simpl in *.
apply H0. intuition congruence.
simpl in *.
inv H.
simpl.
unfold eval_pol.
rewrite (Psquare_ok sor.(SORsetoid) Rops_wd
(Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm));
now apply (Rtimes_square_nonneg sor).
simpl in *.
case_eq (eval_Psatz l e).
intros. rewrite H1 in H. simpl in H.
apply pexpr_times_nformula_correct with (2:= H).
apply IHe with (1:= H1); auto.
intros. rewrite H1 in H. simpl in H ; discriminate.
simpl in *.
revert H.
case_eq (eval_Psatz l e1).
case_eq (eval_Psatz l e2) ; simpl ; intros.
apply nformula_times_nformula_correct with (3:= H2).
apply IHe1 with (1:= H1) ; auto.
intros. apply H0. rewrite extract_hyps_app.
apply in_or_app. tauto.
apply IHe2 with (1:= H) ; auto.
intros. apply H0. rewrite extract_hyps_app.
apply in_or_app. tauto.
discriminate. simpl. discriminate.
simpl in *.
revert H.
case_eq (eval_Psatz l e1).
case_eq (eval_Psatz l e2) ; simpl ; intros.
apply nformula_plus_nformula_correct with (3:= H2).
apply IHe1 with (1:= H1) ; auto.
intros. apply H0. rewrite extract_hyps_app.
apply in_or_app. tauto.
apply IHe2 with (1:= H) ; auto.
intros. apply H0. rewrite extract_hyps_app.
apply in_or_app. tauto.
discriminate. simpl. discriminate.
simpl in H.
case_eq (cO [<] c).
intros. rewrite H1 in H. inv H.
unfold eval_nformula. simpl.
rewrite <- addon.(SORrm).(morph0). now apply cltb_sound.
intros. rewrite H1 in H. discriminate.
simpl in *. inv H.
unfold eval_nformula. simpl.
apply addon.(SORrm).(morph0).
Qed.
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
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
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).
Proof.
intros p op H1 env. unfold check_inconsistent in H1.
destruct op; simpl ;
destruct p ; simpl; try discriminate H1;
try rewrite <- addon.(SORrm).(morph0); trivial.
now apply cneqb_sound.
apply addon.(SORrm).(morph_eq) in H1. congruence.
apply cleb_sound in H1. now apply -> (Rle_ngt sor).
apply cltb_sound in H1. now apply -> (Rlt_nge sor).
Qed.
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.
Proof.
intros l cm H env.
unfold check_normalised_formulas in H.
revert H.
case_eq (eval_Psatz l cm) ; [|discriminate].
intros nf. intros.
rewrite <- make_conj_impl. intro.
assert (H1' := make_conj_in _ _ H1).
assert (Hnf := @eval_Psatz_Sound _ _ H1' _ _ H).
destruct nf.
apply (@check_inconsistent_sound _ _ H0 env Hnf).
Qed.
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.
Record Formula (T:Type) : Type := {
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 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.
Proof.
intros.
apply (Psub_ok sor.(SORsetoid) Rops_wd
(Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm)).
Qed.
Lemma eval_pol_add : forall env lhs rhs, eval_pol env (padd lhs rhs) == eval_pol env lhs + eval_pol env rhs.
Proof.
intros.
apply (Padd_ok sor.(SORsetoid) Rops_wd
(Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm)).
Qed.
Lemma eval_pol_norm : forall env lhs, eval_pexpr env lhs == eval_pol env (norm lhs).
Proof.
intros.
apply (norm_aux_spec sor.(SORsetoid) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm) addon.(SORpower) ).
Qed.
Theorem normalise_sound :
forall (env : PolEnv) (f : Formula C),
eval_formula env f -> eval_nformula env (normalise f).
Proof.
intros env f H; destruct f as [lhs op rhs]; simpl in *.
destruct op; simpl in *; rewrite eval_pol_sub ; rewrite <- eval_pol_norm ; rewrite <- eval_pol_norm.
now apply <- (Rminus_eq_0 sor).
intros H1. apply -> (Rminus_eq_0 sor) in H1. now apply H.
now apply -> (Rle_le_minus sor).
now apply -> (Rle_le_minus sor).
now apply -> (Rlt_lt_minus sor).
now apply -> (Rlt_lt_minus sor).
Qed.
Theorem negate_correct :
forall (env : PolEnv) (f : Formula C),
eval_formula env f <-> ~ (eval_nformula env (negate f)).
Proof.
intros env f; destruct f as [lhs op rhs]; simpl.
destruct op; simpl in *; rewrite eval_pol_sub ; rewrite <- eval_pol_norm ; rewrite <- eval_pol_norm.
symmetry. rewrite (Rminus_eq_0 sor).
split; intro H; [symmetry; now apply -> (Req_dne sor) | symmetry in H; now apply <- (Req_dne sor)].
rewrite (Rminus_eq_0 sor). split; intro; now apply (Rneq_symm sor).
rewrite <- (Rlt_lt_minus sor). now rewrite <- (Rle_ngt sor).
rewrite <- (Rlt_lt_minus sor). now rewrite <- (Rle_ngt sor).
rewrite <- (Rle_le_minus sor). now rewrite <- (Rlt_nge sor).
rewrite <- (Rle_le_minus sor). now rewrite <- (Rlt_nge sor).
Qed.
Another normalisation - this is used for cnf conversion
Definition xnormalise (t:Formula C) : 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.
Import Coq.micromega.Tauto.
Definition cnf_normalise (t:Formula C) : 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.
Proof.
unfold cnf_normalise, xnormalise ; simpl ; intros env t.
unfold eval_cnf, eval_clause.
destruct t as [lhs o rhs]; case_eq o ; simpl;
repeat rewrite eval_pol_sub ; repeat rewrite <- eval_pol_norm in * ;
generalize (eval_pexpr env lhs);
generalize (eval_pexpr env rhs) ; intros z1 z2 ; intros.
apply sor.(SORle_antisymm).
rewrite (Rle_ngt sor). rewrite (Rlt_lt_minus sor). tauto.
rewrite (Rle_ngt sor). rewrite (Rlt_lt_minus sor). tauto.
now rewrite <- (Rminus_eq_0 sor).
rewrite (Rle_ngt sor). rewrite (Rlt_lt_minus sor). auto.
rewrite (Rle_ngt sor). rewrite (Rlt_lt_minus sor). auto.
rewrite (Rlt_nge sor). rewrite (Rle_le_minus sor). auto.
rewrite (Rlt_nge sor). rewrite (Rle_le_minus sor). auto.
Qed.
Definition xnegate (t:Formula C) : 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 C) : 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.
Proof.
unfold cnf_negate, xnegate ; simpl ; intros env t.
unfold eval_cnf, eval_clause.
destruct t as [lhs o rhs]; case_eq o ; simpl;
repeat rewrite eval_pol_sub ; repeat rewrite <- eval_pol_norm in * ;
generalize (eval_pexpr env lhs);
generalize (eval_pexpr env rhs) ; intros z1 z2 ; intros ; intuition.
apply H0.
rewrite H1 ; ring.
apply H1.
apply sor.(SORle_antisymm).
rewrite (Rle_ngt sor). rewrite (Rlt_lt_minus sor). tauto.
rewrite (Rle_ngt sor). rewrite (Rlt_lt_minus sor). tauto.
apply H0. now rewrite (Rle_le_minus sor) in H1.
apply H0. now rewrite (Rle_le_minus sor) in H1.
apply H0. now rewrite (Rlt_lt_minus sor) in H1.
apply H0. now rewrite (Rlt_lt_minus sor) in H1.
Qed.
Lemma eval_nformula_dec : forall env d, (eval_nformula env d) \/ ~ (eval_nformula env d).
Proof.
intros.
destruct d ; simpl.
generalize (eval_pol env p); intros.
destruct o ; simpl.
apply (Req_em sor r 0).
destruct (Req_em sor r 0) ; tauto.
rewrite <- (Rle_ngt sor r 0). generalize (Rle_gt_cases sor r 0). tauto.
rewrite <- (Rlt_nge sor r 0). generalize (Rle_gt_cases sor 0 r). tauto.
Qed.
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).
Proof.
unfold eval_pol.
induction p.
simpl. reflexivity.
simpl.
intros.
rewrite Pos.add_succ_r.
rewrite <- IHp.
symmetry.
rewrite Pos.add_comm.
rewrite Pjump_add. reflexivity.
simpl.
intros.
rewrite <- IHp1, <- IHp2.
unfold Env.tail , Env.hd.
rewrite <- Pjump_add.
rewrite Pos.add_1_r.
unfold Env.nth.
unfold jump at 2.
rewrite <- Pos.add_1_l.
rewrite addon.(SORpower).(rpow_pow_N).
unfold pow_N. ring.
Qed.
Definition denorm := xdenorm xH.
Lemma denorm_correct : forall p env, eval_pol env p == eval_pexpr env (denorm p).
Proof.
unfold denorm.
induction p.
reflexivity.
simpl.
rewrite Pos.add_1_r.
apply xdenorm_correct.
simpl.
intros.
rewrite IHp1.
unfold Env.tail.
rewrite xdenorm_correct.
change (Pos.succ xH) with 2%positive.
rewrite addon.(SORpower).(rpow_pow_N).
simpl. reflexivity.
Qed.
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).
Proof.
unfold eval_pexpr, eval_sexpr.
induction s ; simpl ; try (rewrite IHs1 ; rewrite IHs2) ; try reflexivity.
apply phi_C_of_S.
rewrite IHs. reflexivity.
rewrite IHs. reflexivity.
Qed.
equality migth be (too) strong
Lemma eval_formulaSC : forall env f, eval_sformula env f = eval_formula env (map_Formula f).
Proof.
destruct f.
simpl.
repeat rewrite eval_pexprSC.
reflexivity.
Qed.
Proof.
destruct f.
simpl.
repeat rewrite eval_pexprSC.
reflexivity.
Qed.
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.