(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)
(*                      Evgeny Makarov, INRIA, 2007                     *)
(************************************************************************)

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.


Set Implicit Arguments.

Import OrderedRingSyntax.

Section Micromega.

(* Assume we have a strict(ly?) ordered ring *)

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).

(* Assume we have a type of coefficients C and a morphism from C to R *)

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.

(* Power coefficients *)
Variable E : Set. (* the type of exponents *)
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).

(* Let's collect all hypotheses in addition to the ordered ring axioms into
one structure *)

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). (* We already proved that minus is a morphism in OrderedRing.v *)
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.

(* Begin Micromega *)

Definition PExprC := PExpr C. (* arbitrary expressions built from +, *, - *)
Definition PolC := Pol C. (* polynomials in generalized Horner form, defined in Ring_polynom or EnvRing *)
(*****)
(*Definition Env := Env R. (* For interpreting PExprC *)*)
Definition PolEnv := Env R. (* For interpreting PolC *)
(*****)
(*Definition Env := list R.
Definition PolEnv := list R.*)
(*****)

(* What benefit do we get, in the case of EnvRing, from defining eval_pexpr
explicitely below and not through PEeval, as the following lemma says? The
function eval_pexpr seems to be a straightforward special case of PEeval
when the environment (i.e., the second last argument of PEeval) of type
off_map (which is (option positive * t)) is (None, env). *)

(*****)
Fixpoint eval_pexpr (l : PolEnv) (pe : PExprC) {struct pe} : R :=
match pe with
| PEc c => phi c
| PEX j =>  l j
| PEadd pe1 pe2 => (eval_pexpr l pe1) + (eval_pexpr l pe2)
| PEsub pe1 pe2 => (eval_pexpr l pe1) - (eval_pexpr l pe2)
| PEmul pe1 pe2 => (eval_pexpr l pe1) * (eval_pexpr l pe2)
| PEopp pe1 => - (eval_pexpr l pe1)
| PEpow pe1 n => rpow (eval_pexpr l pe1) (pow_phi n)
end.


Lemma eval_pexpr_simpl : forall  (l : PolEnv) (pe : PExprC),
  eval_pexpr l pe = 
  match pe with
    | PEc c => phi c
    | PEX j => l j
    | PEadd pe1 pe2 => (eval_pexpr l pe1) + (eval_pexpr l pe2)
    | PEsub pe1 pe2 => (eval_pexpr l pe1) - (eval_pexpr l pe2)
    | PEmul pe1 pe2 => (eval_pexpr l pe1) * (eval_pexpr l pe2)
    | PEopp pe1 => - (eval_pexpr l pe1)
    | PEpow pe1 n => rpow (eval_pexpr l pe1) (pow_phi n)
  end.
Proof.
  intros ; destruct pe ; reflexivity.
Qed.



Lemma eval_pexpr_PEeval : forall (env : PolEnv) (pe : PExprC),
  eval_pexpr env pe =
  PEeval rplus rtimes rminus ropp phi pow_phi rpow env pe.
Proof.
induction pe; simpl; intros.
reflexivity.
reflexivity.
rewrite <- IHpe1; rewrite <- IHpe2; reflexivity.
rewrite <- IHpe1; rewrite <- IHpe2; reflexivity.
rewrite <- IHpe1; rewrite <- IHpe2; reflexivity.
rewrite <- IHpe; reflexivity.
rewrite <- IHpe; reflexivity.
Qed.
(*****)
(*Definition eval_pexpr : Env -> PExprC -> R :=
  PEeval 0 rplus rtimes rminus ropp phi pow_phi rpow.*)
(*****)

Inductive Op1 : Set := (* relations with 0 *)
| Equal (* == 0 *)
| NonEqual (* ~= 0 *)
| Strict (* > 0 *)
| NonStrict (* >= 0 *).

Definition NFormula := (PExprC * Op1)%type. (* normalized formula *)

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_pexpr env p).


Definition OpMult (o o' : Op1) : Op1 :=
match o with
| Equal => Equal
| NonStrict => NonStrict (* (OpMult NonStrict Equal) could be defined as Equal *)
| Strict => o'
| NonEqual => NonEqual (* does not matter what we return here; see the following lemmas *)
end.

Definition OpAdd (o o': Op1) : Op1 :=
match o with
| Equal => o'
| NonStrict =>
  match o' with
  | Strict => Strict
  | _ => NonStrict
  end
| Strict => Strict
| NonEqual => NonEqual (* does not matter what we return here *)
end.

Lemma OpMultNonEqual :
  forall o o' : Op1, o <> NonEqual -> o' <> NonEqual -> OpMult o o' <> NonEqual.
Proof.
intros o o' H1 H2; destruct o; destruct o'; simpl; try discriminate;
try (intro H; apply H1; reflexivity);
try (intro H; apply H2; reflexivity).
Qed.

Lemma OpAdd_NonEqual :
  forall o o' : Op1, o <> NonEqual -> o' <> NonEqual -> OpAdd o o' <> NonEqual.
Proof.
intros o o' H1 H2; destruct o; destruct o'; simpl; try discriminate;
try (intro H; apply H1; reflexivity);
try (intro H; apply H2; reflexivity).
Qed.

Lemma OpMult_sound :
  forall (o o' : Op1) (x y : R), o <> NonEqual -> o' <> NonEqual ->
    eval_op1 o x -> eval_op1 o' y -> eval_op1 (OpMult o o') (x * y).
Proof.
unfold eval_op1; destruct o; simpl; intros o' x y H1 H2 H3 H4.
rewrite H3; now rewrite (Rtimes_0_l sor).
elimtype False; now apply H1.
destruct o'.
rewrite H4; now rewrite (Rtimes_0_r sor).
elimtype False; now apply H2.
now apply (Rtimes_pos_pos sor).
apply (Rtimes_nonneg_nonneg sor); [le_less | assumption].
destruct o'.
rewrite H4, (Rtimes_0_r sor); le_equal.
elimtype False; now apply H2.
apply (Rtimes_nonneg_nonneg sor); [assumption | le_less].
now apply (Rtimes_nonneg_nonneg sor).
Qed.

Lemma OpAdd_sound :
  forall (o o' : Op1) (e e' : R), o <> NonEqual -> o' <> NonEqual ->
    eval_op1 o e -> eval_op1 o' e' -> eval_op1 (OpAdd o o') (e + e').
Proof.
unfold eval_op1; destruct o; simpl; intros o' e e' H1 H2 H3 H4.
destruct o'.
now rewrite H3, H4, (Rplus_0_l sor).
elimtype False; now apply H2.
now rewrite H3, (Rplus_0_l sor).
now rewrite H3, (Rplus_0_l sor).
elimtype False; now apply H1.
destruct o'.
now rewrite H4, (Rplus_0_r sor).
elimtype False; now apply H2.
now apply (Rplus_pos_pos sor).
now apply (Rplus_pos_nonneg sor).
destruct o'.
now rewrite H4, (Rplus_0_r sor).
elimtype False; now apply H2.
now apply (Rplus_nonneg_pos sor).
now apply (Rplus_nonneg_nonneg sor).
Qed.

(* We consider a monoid whose generators are polynomials from the
hypotheses of the form (p ~= 0). Thus it follows from the hypotheses that
every element of the monoid (i.e., arbitrary product of generators) is ~=
0. Therefore, the square of every element is > 0. *)

Inductive Monoid (l : list NFormula) : PExprC -> Prop :=
| M_One : Monoid l (PEc cI)
| M_In : forall p : PExprC, In (p, NonEqual) l -> Monoid l p
| M_Mult : forall (e1 e2 : PExprC), Monoid l e1 -> Monoid l e2 -> Monoid l (PEmul e1 e2).

(* Do we really need to rely on the intermediate definition of monoid ?
   InC why the restriction NonEqual ?
   Could not we consider the IsIdeal as a IsMult ?
   The same for IsSquare ?
*)

Inductive Cone (l : list (NFormula)) : PExprC -> Op1 -> Prop :=
| InC : forall p op, In (p, op) l -> op <> NonEqual -> Cone l p op
| IsIdeal : forall p, Cone l p Equal -> forall p', Cone l (PEmul p p') Equal
| IsSquare : forall p, Cone l (PEmul p p) NonStrict
| IsMonoid : forall p, Monoid l p -> Cone l (PEmul p p) Strict
| IsMult : forall p op q oq, Cone l p op -> Cone l q oq -> Cone l (PEmul p q) (OpMult op oq)
| IsAdd : forall p op q oq, Cone l p op -> Cone l q oq -> Cone l (PEadd p q) (OpAdd op oq)
| IsPos : forall c : C, cltb cO c = true -> Cone l (PEc c) Strict
| IsZ : Cone l (PEc cO) Equal.

(* As promised, if all hypotheses are true in some environment, then every
member of the monoid is nonzero in this environment *)

Lemma monoid_nonzero : forall (l : list NFormula) (env : PolEnv),
  (forall f : NFormula, In f l -> eval_nformula env f) ->
    forall p : PExprC, Monoid l p -> eval_pexpr env p ~= 0.
Proof.
intros l env H1 p H2. induction H2 as [| f H | e1 e2 H3 IH1 H4 IH2]; simpl.
rewrite addon.(SORrm).(morph1). apply (Rneq_symm sor). apply (Rneq_0_1 sor).
apply H1 in H. now simpl in H.
simpl in IH1, IH2. apply (Rtimes_neq_0 sor). now split.
Qed.

(* If all members of a cone base are true in some environment, then every
member of the cone is true as well *)

Lemma cone_true :
  forall (l : list NFormula) (env : PolEnv),
    (forall (f : NFormula), In f l -> eval_nformula env f) ->
      forall (p : PExprC) (op : Op1), Cone l p op ->
        op <> NonEqual /\ eval_nformula env (p, op).
Proof.
intros l env H1 p op H2. induction H2; simpl in *.
split. assumption. apply H1 in H. now unfold eval_nformula in H.
split. discriminate. destruct IHCone as [_ H3]. rewrite H3. now rewrite (Rtimes_0_l sor).
split. discriminate. apply (Rtimes_square_nonneg sor).
split. discriminate. apply <- (Rlt_le_neq sor). split. apply (Rtimes_square_nonneg sor).
apply (Rneq_symm sor). apply (Rtimes_neq_0 sor). split; now apply monoid_nonzero with l.
destruct IHCone1 as [IH1 IH2]; destruct IHCone2 as [IH3 IH4].
split. now apply OpMultNonEqual. now apply OpMult_sound.
destruct IHCone1 as [IH1 IH2]; destruct IHCone2 as [IH3 IH4].
split. now apply OpAdd_NonEqual. now apply OpAdd_sound.
split. discriminate. rewrite <- addon.(SORrm).(morph0). now apply cltb_sound.
split. discriminate. apply addon.(SORrm).(morph0).
Qed.

(* Every element of a monoid is a product of some generators; therefore,
to determine an element we can give a list of generators' indices *)

Definition MonoidMember : Set := list nat.

Inductive ConeMember : Type :=
| S_In : nat -> ConeMember
| S_Ideal : PExprC -> ConeMember -> ConeMember
| S_Square : PExprC -> ConeMember
| S_Monoid : MonoidMember -> ConeMember
| S_Mult : ConeMember -> ConeMember -> ConeMember
| S_Add : ConeMember -> ConeMember -> ConeMember
| S_Pos : C -> ConeMember 
| S_Z : ConeMember.

Definition nformula_times (f f' : NFormula) : NFormula :=
let (p, op) := f in
  let (p', op') := f' in
    (PEmul p p', OpMult op op').

Definition nformula_plus (f f' : NFormula) : NFormula :=
let (p, op) := f in
  let (p', op') := f' in
    (PEadd p p', OpAdd op op').

Definition nformula_times_0 (p : PExprC) (f : NFormula) : NFormula :=
let (q, op) := f in
  match op with
  | Equal => (PEmul q p, Equal)
  | _ => f
  end.

Fixpoint eval_monoid (l : list NFormula) (ns : MonoidMember) {struct ns} : PExprC :=
match ns with
| nil => PEc cI
| n :: ns =>
  let p := match nth n l (PEc cI, NonEqual) with
           | (q, NonEqual) => q
           | _ => PEc cI
           end in
    PEmul p (eval_monoid l ns)
end.

Theorem eval_monoid_in_monoid :
  forall (l : list NFormula) (ns : MonoidMember), Monoid l (eval_monoid l ns).
Proof.
intro l; induction ns; simpl in *.
constructor.
apply M_Mult; [| assumption].
destruct (nth_in_or_default a l (PEc cI, NonEqual)).
destruct (nth a l (PEc cI, NonEqual)). destruct o; try constructor. assumption.
rewrite e; simpl. constructor.
Qed.

(* Provides the cone member from the witness, i.e., ConeMember *)
Fixpoint eval_cone (l : list NFormula) (cm : ConeMember) {struct cm} : NFormula :=
match cm with
| S_In n => match nth n l (PEc cO, Equal) with
            | (_, NonEqual) => (PEc cO, Equal)
            | f => f
            end
| S_Ideal p cm' => nformula_times_0 p (eval_cone l cm')
| S_Square p => (PEmul p p, NonStrict)
| S_Monoid m => let p := eval_monoid l m in (PEmul p p, Strict)
| S_Mult p q => nformula_times (eval_cone l p) (eval_cone l q)
| S_Add p q => nformula_plus (eval_cone l p) (eval_cone l q)
| S_Pos c  => if cltb cO c then (PEc c, Strict) else (PEc cO, Equal)
| S_Z => (PEc cO, Equal)
end.

Theorem eval_cone_in_cone :
  forall (l : list NFormula) (cm : ConeMember),
    let (p, op) := eval_cone l cm in Cone l p op.
Proof.
intros l cm; induction cm; simpl.
destruct (nth_in_or_default n l (PEc cO, Equal)).
destruct (nth n l (PEc cO, Equal)). destruct o; try (now apply InC). apply IsZ.
rewrite e. apply IsZ.
destruct (eval_cone l cm). destruct o; simpl; try assumption. now apply IsIdeal.
apply IsSquare.
apply IsMonoid. apply eval_monoid_in_monoid.
destruct (eval_cone l cm1). destruct (eval_cone l cm2). unfold nformula_times. now apply IsMult.
destruct (eval_cone l cm1). destruct (eval_cone l cm2). unfold nformula_plus. now apply IsAdd.
case_eq (cO [<] c) ; intros ; [apply IsPos ; auto| apply IsZ].
apply IsZ.
Qed.

(* (inconsistent_cone_member l p) means (p, op) is in the cone for some op
(> 0, >= 0, == 0, or ~= 0) and this formula is inconsistent. This fact
implies that l is inconsistent, as shown by the next lemma. Inconsistency
of a formula (p, op) can be established by normalizing p and showing that
it is a constant c for which (c, op) is false. (This is only a sufficient,
not necessary, condition, of course.) Membership in the cone can be
verified if we have a certificate. *)

Definition inconsistent_cone_member (l : list NFormula) (p : PExprC) :=
  exists op : Op1, Cone l p op /\
    forall env : PolEnv, ~ eval_op1 op (eval_pexpr env p).

(* If some element of a cone is inconsistent, then the base of the cone
is also inconsistent *)

Lemma prove_inconsistent :
  forall (l : list NFormula) (p : PExprC),
    inconsistent_cone_member l p -> forall env, make_impl (eval_nformula env) l False.
Proof.
intros l p H env.
destruct H as [o [wit H]].
apply -> make_conj_impl.
intro H1. apply H with env.
pose proof (@cone_true l env) as H2.
cut (forall f : NFormula, In f l -> eval_nformula env f). intro H3.
apply (proj2 (H2 H3 p o wit)). intro. now apply make_conj_in.
Qed.

Definition normalise_pexpr : PExprC -> PolC :=
  norm_aux cO cI cplus ctimes cminus copp ceqb.

(* The following definition we don't really need, hence it is commented *)
(*Definition eval_pol : PolEnv -> PolC -> R := Pphi 0 rplus rtimes phi.*)

(* roughly speaking, normalise_pexpr_correct is a proof of
  forall env p, eval_pexpr env p == eval_pol env (normalise_pexpr p) *)

(*****)
Definition normalise_pexpr_correct :=
let Rops_wd := mk_reqe rplus rtimes ropp req
                       sor.(SORplus_wd)
                       sor.(SORtimes_wd)
                       sor.(SORopp_wd) in
  norm_aux_spec sor.(SORsetoid) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt))
                addon.(SORrm) addon.(SORpower).
(*****)
(*Definition normalise_pexpr_correct :=
let Rops_wd := mk_reqe rplus rtimes ropp req
                       sor.(SORplus_wd)
                       sor.(SORtimes_wd)
                       sor.(SORopp_wd) in
  norm_aux_spec sor.(SORsetoid) Rops_wd (Rth_ARth sor.(SORsetoid) Rops_wd sor.(SORrt))
                addon.(SORrm) addon.(SORpower) nil.*)
(*****)

(* Check that a formula f is inconsistent by normalizing and comparing the
resulting constant with 0 *)

Definition check_inconsistent (f : NFormula) : bool :=
let (e, op) := f in
  match normalise_pexpr e with
  | Pc c =>
    match op with
    | Equal => cneqb c cO
    | NonStrict => c [<] cO
    | Strict => c [<=] cO
    | NonEqual => false (* eval_cone never returns (p, NonEqual) *)
    end
  | _ => false (* not a constant *)
  end.

Lemma check_inconsistent_sound :
  forall (p : PExprC) (op : Op1),
    check_inconsistent (p, op) = true -> forall env, ~ eval_op1 op (eval_pexpr env p).
Proof.
intros p op H1 env. unfold check_inconsistent, normalise_pexpr in H1.
destruct op; simpl;
(*****)
rewrite eval_pexpr_PEeval;
(*****)
(*unfold eval_pexpr;*)
(*****)
rewrite normalise_pexpr_correct;
destruct (norm_aux cO cI cplus ctimes cminus copp ceqb p); simpl; try discriminate H1;
try rewrite <- addon.(SORrm).(morph0); trivial.
now apply cneqb_sound.
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 -> ConeMember -> bool :=
  fun l cm => check_inconsistent (eval_cone l cm).

Lemma checker_nf_sound :
  forall (l : list NFormula) (cm : ConeMember),
    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.
case_eq (eval_cone l cm). intros p op H1.
apply prove_inconsistent with p. unfold inconsistent_cone_member. exists op. split.
pose proof (eval_cone_in_cone l cm) as H2. now rewrite H1 in H2.
apply check_inconsistent_sound. now rewrite <- H1.
Qed.

(** Normalisation of formulae **)

Inductive Op2 : Set := (* binary relations *)
| 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.

Record Formula : Type := {
  Flhs : PExprC;
  Fop : Op2;
  Frhs : PExprC
}.

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).

(* We normalize Formulas by moving terms to one side *)

Definition normalise (f : Formula) : NFormula :=
let (lhs, op, rhs) := f in
  match op with
  | OpEq => (PEsub lhs rhs, Equal)
  | OpNEq => (PEsub lhs rhs, NonEqual)
  | OpLe => (PEsub rhs lhs, NonStrict)
  | OpGe => (PEsub lhs rhs, NonStrict)
  | OpGt => (PEsub lhs rhs, Strict)
  | OpLt => (PEsub rhs lhs, Strict)
  end.

Definition negate (f : Formula) : NFormula :=
let (lhs, op, rhs) := f in
  match op with
  | OpEq => (PEsub rhs lhs, NonEqual)
  | OpNEq => (PEsub rhs lhs, Equal)
  | OpLe => (PEsub lhs rhs, Strict) (* e <= e' == ~ e > e' *)
  | OpGe => (PEsub rhs lhs, Strict)
  | OpGt => (PEsub rhs lhs, NonStrict)
  | OpLt => (PEsub lhs rhs, NonStrict)
end.

Theorem normalise_sound :
  forall (env : PolEnv) (f : Formula),
    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 *.
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),
    eval_formula env f <-> ~ (eval_nformula env (negate f)).
Proof.
intros env f; destruct f as [lhs op rhs]; simpl.
destruct op; simpl.
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 normalistion - this is used for cnf conversion **)

Definition xnormalise (t:Formula) : list (NFormula)  :=
  let (lhs,o,rhs) := t in
    match o with
      | OpEq => 
        (PEsub lhs  rhs, Strict)::(PEsub rhs lhs , Strict)::nil
      | OpNEq => (PEsub lhs rhs,Equal) :: nil
      | OpGt   => (PEsub rhs lhs,NonStrict) :: nil
      | OpLt => (PEsub lhs rhs,NonStrict) :: nil
      | OpGe => (PEsub rhs lhs , Strict) :: nil
      | OpLe => (PEsub 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.
Proof.
  unfold cnf_normalise, xnormalise ; simpl ; intros env t.
  unfold eval_cnf.
  destruct t as [lhs o rhs]; case_eq o ; simpl;    
    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) : list (NFormula)  :=
  let (lhs,o,rhs) := t in
    match o with
      | OpEq  => (PEsub lhs rhs,Equal) :: nil
      | OpNEq => (PEsub lhs  rhs ,Strict)::(PEsub rhs lhs,Strict)::nil
      | OpGt  => (PEsub lhs  rhs,Strict) :: nil
      | OpLt  => (PEsub rhs lhs,Strict) :: nil
      | OpGe  => (PEsub lhs rhs,NonStrict) :: nil
      | OpLe  => (PEsub 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.
Proof.
  unfold cnf_negate, xnegate ; simpl ; intros env t.
  unfold eval_cnf.
  destruct t as [lhs o rhs]; case_eq o ; simpl ;
    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_pexpr 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.

(** Some syntactic simplifications of expressions and cone elements *)


Fixpoint simpl_expr (e:PExprC) : PExprC :=
  match e with
    | PEmul y z => let y' := simpl_expr y in let z' := simpl_expr z in
      match y' , z' with
        | PEc c , z' => if ceqb c cI then z' else PEmul y' z'
        |     _     , _   => PEmul y' z'
      end
    | PEadd x  y => PEadd (simpl_expr x) (simpl_expr y)
    |   _    => e
  end.


Definition simpl_cone (e:ConeMember) : ConeMember :=
  match e with
    | S_Square t => match simpl_expr t with
                      | PEc c   => if ceqb cO c then S_Z else S_Pos (ctimes c c)
                      |       x     => S_Square x
                    end
    | S_Mult t1 t2 => 
      match t1 , t2 with
        | S_Z      , x        => S_Z 
        |    x     , S_Z      => S_Z 
        | S_Pos c ,  S_Pos c' => S_Pos (ctimes c c')
        | S_Pos p1 , S_Mult (S_Pos p2)  x => S_Mult (S_Pos (ctimes p1 p2)) x
        | S_Pos p1 , S_Mult x (S_Pos p2)  => S_Mult (S_Pos (ctimes p1 p2)) x
        | S_Mult (S_Pos p2)  x  , S_Pos p1   => S_Mult (S_Pos (ctimes p1 p2)) x
        | S_Mult x (S_Pos p2)   , S_Pos p1   => S_Mult (S_Pos (ctimes p1 p2)) x
        | S_Pos x   , S_Add y z   => S_Add (S_Mult (S_Pos x) y) (S_Mult (S_Pos x) z)
        | S_Pos c ,  _        => if ceqb cI c then t2 else S_Mult t1 t2
        | _ ,  S_Pos c        => if ceqb cI c then t1 else S_Mult t1 t2
        |     _     , _   => e
      end
    | S_Add t1 t2 => 
      match t1 ,  t2 with
        | S_Z     , x => x
        |   x     , S_Z => x
        |   x     , y   => S_Add x y
      end
    |   _     => e
  end.



End Micromega.