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.
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 :=
| 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.


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

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

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

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.

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.

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

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.

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 migth be (too) strong
Lemma eval_formulaSC : forall env f, eval_sformula env f = eval_formula env (map_Formula f).

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.