Library Coq.nsatz.Nsatz



Require Import List.
Require Import Setoid.
Require Import BinPos.
Require Import BinList.
Require Import Znumtheory.
Require Import Ring_polynom Ring_tac InitialRing.
Require Export Morphisms Setoid Bool.


Class Zero (A : Type) := {zero : A}.
Notation "0" := zero.
Class One (A : Type) := {one : A}.
Notation "1" := one.
Class Addition (A : Type) := {addition : A -> A -> A}.
Notation "x + y" := (addition x y).
Class Multiplication (A : Type) := {multiplication : A -> A -> A}.
Notation "x * y" := (multiplication x y).
Class Subtraction (A : Type) := {subtraction : A -> A -> A}.
Notation "x - y" := (subtraction x y).
Class Opposite (A : Type) := {opposite : A -> A}.
Notation "- x" := (opposite x).

Class Ring (R:Type) := {
 ring0: R; ring1: R;
 ring_plus: R->R->R; ring_mult: R->R->R;
 ring_sub: R->R->R; ring_opp: R->R;
 ring_eq : R -> R -> Prop;
 ring_ring:
   ring_theory ring0 ring1 ring_plus ring_mult ring_sub
               ring_opp ring_eq;
 ring_setoid: Equivalence ring_eq;
 ring_plus_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_plus;
 ring_mult_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_mult;
 ring_sub_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_sub;
 ring_opp_comp: Proper (ring_eq==>ring_eq) ring_opp
}.

Class Domain (R : Type) := {
 domain_ring:> Ring R;
 domain_axiom_product:
   forall x y, ring_eq (ring_mult x y) ring0 -> (ring_eq x ring0) \/ (ring_eq y ring0);
 domain_axiom_one_zero: not (ring_eq ring1 ring0)}.

Section domain.

Variable R: Type.
Variable Rd: Domain R.


Add Ring Rr: (@ring_ring R (@domain_ring R Rd)).

Instance zero_ring : Zero R := {zero := ring0}.
Instance one_ring : One R := {one := ring1}.
Instance addition_ring : Addition R := {addition x y := ring_plus x y}.
Instance multiplication_ring : Multiplication R := {multiplication x y := ring_mult x y}.
Instance subtraction_ring : Subtraction R := {subtraction x y := ring_sub x y}.
Instance opposite_ring : Opposite R := {opposite x := ring_opp x}.

Infix "==" := ring_eq (at level 70, no associativity).

Lemma psos_r1b: forall x y:R, x - y == 0 -> x == y.

Lemma psos_r1: forall x y, x == y -> x - y == 0.

Lemma nsatzR_diff: forall x y:R, not (x == y) -> not (x - y == 0).

Require Import ZArith.

Definition PolZ := Pol Z.
Definition PEZ := PExpr Z.

Definition P0Z : PolZ := @P0 Z 0%Z.

Definition PolZadd : PolZ -> PolZ -> PolZ :=
  @Padd Z 0%Z Zplus Zeq_bool.

Definition PolZmul : PolZ -> PolZ -> PolZ :=
  @Pmul Z 0%Z 1%Z Zplus Zmult Zeq_bool.

Definition PolZeq := @Peq Z Zeq_bool.

Definition norm :=
  @norm_aux Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool.

Fixpoint mult_l (la : list PEZ) (lp: list PolZ) : PolZ :=
 match la, lp with
 | a::la, p::lp => PolZadd (PolZmul (norm a) p) (mult_l la lp)
 | _, _ => P0Z
 end.

Fixpoint compute_list (lla: list (list PEZ)) (lp:list PolZ) :=
 match lla with
 | List.nil => lp
 | la::lla => compute_list lla ((mult_l la lp)::lp)
 end.

Definition check (lpe:list PEZ) (qe:PEZ) (certif: list (list PEZ) * list PEZ) :=
 let (lla, lq) := certif in
 let lp := List.map norm lpe in
 PolZeq (norm qe) (mult_l lq (compute_list lla lp)).

Definition PhiR : list R -> PolZ -> R :=
  (Pphi 0 ring_plus ring_mult (gen_phiZ 0 1 ring_plus ring_mult ring_opp)).

Definition pow (r : R) (n : nat) := pow_N 1 ring_mult r (Nnat.N_of_nat n).

Definition PEevalR : list R -> PEZ -> R :=
   PEeval 0 ring_plus ring_mult ring_sub ring_opp
    (gen_phiZ 0 1 ring_plus ring_mult ring_opp)
         Nnat.nat_of_N pow.

Lemma P0Z_correct : forall l, PhiR l P0Z = 0.

Lemma Rext: ring_eq_ext ring_plus ring_mult ring_opp ring_eq.

Lemma Rset : Setoid_Theory R ring_eq.

Lemma PolZadd_correct : forall P' P l,
  PhiR l (PolZadd P P') == ((PhiR l P) + (PhiR l P')).

Lemma PolZmul_correct : forall P P' l,
  PhiR l (PolZmul P P') == ((PhiR l P) * (PhiR l P')).

Lemma R_power_theory
     : power_theory 1 ring_mult ring_eq Nnat.nat_of_N pow.

Lemma norm_correct :
  forall (l : list R) (pe : PEZ), PEevalR l pe == PhiR l (norm pe).

Lemma PolZeq_correct : forall P P' l,
  PolZeq P P' = true ->
  PhiR l P == PhiR l P'.

Fixpoint Cond0 (A:Type) (Interp:A->R) (l:list A) : Prop :=
  match l with
  | List.nil => True
  | a::l => Interp a == 0 /\ Cond0 A Interp l
  end.

Lemma mult_l_correct : forall l la lp,
  Cond0 PolZ (PhiR l) lp ->
  PhiR l (mult_l la lp) == 0.

Lemma compute_list_correct : forall l lla lp,
  Cond0 PolZ (PhiR l) lp ->
  Cond0 PolZ (PhiR l) (compute_list lla lp).

Lemma check_correct :
  forall l lpe qe certif,
    check lpe qe certif = true ->
    Cond0 PEZ (PEevalR l) lpe ->
    PEevalR l qe == 0.


Lemma pow_not_zero: forall p n, pow p n == 0 -> p == 0.

Lemma Rdomain_pow: forall c p r, ~c == ring0 -> ring_mult c (pow p r) == ring0 -> p == ring0.

Definition R2:= ring_plus ring1 ring1.

Fixpoint IPR p {struct p}: R :=
  match p with
    xH => ring1
  | xO xH => ring_plus ring1 ring1
  | xO p1 => ring_mult R2 (IPR p1)
  | xI xH => ring_plus ring1 (ring_plus ring1 ring1)
  | xI p1 => ring_plus ring1 (ring_mult R2 (IPR p1))
  end.

Definition IZR1 z :=
  match z with Z0 => ring0
             | Zpos p => IPR p
             | Zneg p => ring_opp(IPR p)
  end.

Fixpoint interpret3 t fv {struct t}: R :=
  match t with
  | (PEadd t1 t2) =>
       let v1 := interpret3 t1 fv in
       let v2 := interpret3 t2 fv in (ring_plus v1 v2)
  | (PEmul t1 t2) =>
       let v1 := interpret3 t1 fv in
       let v2 := interpret3 t2 fv in (ring_mult v1 v2)
  | (PEsub t1 t2) =>
       let v1 := interpret3 t1 fv in
       let v2 := interpret3 t2 fv in (ring_sub v1 v2)
  | (PEopp t1) =>
       let v1 := interpret3 t1 fv in (ring_opp v1)
  | (PEpow t1 t2) =>
       let v1 := interpret3 t1 fv in pow v1 (Nnat.nat_of_N t2)
  | (PEc t1) => (IZR1 t1)
  | (PEX n) => List.nth (pred (nat_of_P n)) fv 0
  end.

End domain.

Ltac equalities_to_goal :=
  lazymatch goal with
  | H: (@ring_eq _ _ ?x ?y) |- _ =>
          try generalize (@psos_r1 _ _ _ _ H); clear H
   end.

Ltac nsatz_domain_begin tacsimpl :=
  intros;
  try apply (@psos_r1b _ _);
  repeat equalities_to_goal;
  tacsimpl.

Ltac generalise_eq_hyps:=
  repeat
    (match goal with
     |h : (@ring_eq _ _ ?p ?q)|- _ => revert h
     end).

Ltac lpol_goal t :=
  match t with
  | ?a = ring0 -> ?b =>
    let r:= lpol_goal b in
    constr:(a::r)
  | ?a = ring0 => constr:(a::nil)
 end.


Ltac parametres_en_tete fv lp :=
    match fv with
     | (@nil _) => lp
     | (@cons _ ?x ?fv1) =>
       let res := AddFvTail x lp in
         parametres_en_tete fv1 res
    end.

Ltac append1 a l :=
 match l with
 | (@nil _) => constr:(cons a l)
 | (cons ?x ?l) => let l' := append1 a l in constr:(cons x l')
 end.

Ltac rev l :=
  match l with
   |(@nil _) => l
   | (cons ?x ?l) => let l' := rev l in append1 x l'
  end.

Ltac nsatz_call_n info nparam p rr lp kont :=
  
  let ll := constr:(PEc info :: PEc nparam :: PEpow p rr :: lp) in
  nsatz_compute ll;
  
  match goal with
  | |- (?c::PEpow _ ?r::?lq0)::?lci0 = _ -> _ =>
    intros _;
    set (lci:=lci0);
    set (lq:=lq0);
    kont c rr lq lci
  end.

Ltac nsatz_call radicalmax info nparam p lp kont :=
  let rec try_n n :=
    lazymatch n with
    | 0%N => fail
    | _ =>
        (let r := eval compute in (Nminus radicalmax (Npred n)) in
         nsatz_call_n info nparam p r lp kont) ||
         let n' := eval compute in (Npred n) in try_n n'
    end in
  try_n radicalmax.

Class Cclosed_seq T (l:list T) := {}.
Instance Iclosed_nil T : Cclosed_seq (T:=T) nil.
Instance Iclosed_cons T t l `{Cclosed_seq (T:=T) l} : Cclosed_seq (T:=T) (t::l).

Class Cfind_at (R:Type) (b:R) (l:list R) (i:nat) := {}.
Instance Ifind0 (R:Type) (b:R) l: Cfind_at b (b::l) 0.
Instance IfindS (R:Type) (b2 b1:R) l i `{Cfind_at R b1 l i} : Cfind_at b1 (b2::l) (S i) | 1.
Definition Ifind0' := Ifind0.
Definition IfindS' := IfindS.

Definition li_find_at (R:Type) (b:R) l i `{Cfind_at R b l i} {H:Cclosed_seq (T:=R) l} := (l,i).

Class Creify (R:Type) (e:PExpr Z) (l:list R) (b:R) := {}.
Instance Ireify_zero (R:Type) (Rd:Domain R) l : Creify (PEc 0%Z) l ring0.
Instance Ireify_one (R:Type) (Rd:Domain R) l : Creify (PEc 1%Z) l ring1.
Instance Ireify_plus (R:Type) (Rd:Domain R) e1 l b1 e2 b2 `{Creify R e1 l b1} `{Creify R e2 l b2}
 : Creify (PEadd e1 e2) l (ring_plus b1 b2).
Instance Ireify_mult (R:Type) (Rd:Domain R) e1 l b1 e2 b2 `{Creify R e1 l b1} `{Creify R e2 l b2}
 : Creify (PEmul e1 e2) l (ring_mult b1 b2).
Instance Ireify_sub (R:Type) (Rd:Domain R) e1 l b1 e2 b2 `{Creify R e1 l b1} `{Creify R e2 l b2}
 : Creify (PEsub e1 e2) l (ring_sub b1 b2).
Instance Ireify_opp (R:Type) (Rd:Domain R) e1 l b1 `{Creify R e1 l b1}
 : Creify (PEopp e1) l (ring_opp b1).
Instance Ireify_var (R:Type) b l i `{Cfind_at R b l i}
 : Creify (PEX _ (P_of_succ_nat i)) l b | 100.

Class Creifylist (R:Type) (le:list (PExpr Z)) (l:list R) (lb:list R) := {}.
Instance Creify_nil (R:Type) l : Creifylist nil l (@nil R).
Instance Creify_cons (R:Type) e1 l b1 le2 lb2 `{Creify R e1 l b1} `{Creifylist R le2 l lb2}
 : Creifylist (e1::le2) l (b1::lb2).

Definition li_reifyl (R:Type) le l lb `{Creifylist R le l lb}
 {H:Cclosed_seq (T:=R) l} := (l,le).


Ltac lterm_goal g :=
  match g with
  ring_eq ?b1 ?b2 => constr:(b1::b2::nil)
  | ring_eq ?b1 ?b2 -> ?g => let l := lterm_goal g in constr:(b1::b2::l)
  end.

Ltac reify_goal l le lb Rd:=
  match le with
     nil => idtac
   | ?e::?le1 =>
        match lb with
         ?b::?lb1 =>
           let x := fresh "B" in
           set (x:= b) at 1;
           change x with (@interpret3 _ Rd e l);
           clear x;
           reify_goal l le1 lb1 Rd
        end
  end.

Ltac get_lpol g :=
  match g with
  ring_eq (interpret3 _ _ ?p _) _ => constr:(p::nil)
  | ring_eq (interpret3 _ _ ?p _) _ -> ?g =>
       let l := get_lpol g in constr:(p::l)
  end.

Ltac nsatz_domain_generic radicalmax info lparam lvar tacsimpl Rd :=
  match goal with
  |- ?g => let lb := lterm_goal g in
     
     match eval red in (li_reifyl (lb:=lb)) with
     | (?fv, ?le) =>
        let fv := match lvar with
                     (@nil _) => fv
                    | _ => lvar
                  end in
        
        let nparam := eval compute in (Z_of_nat (List.length lparam)) in
        let fv := parametres_en_tete fv lparam in
        
        match eval red in (li_reifyl (l:=fv) (lb:=lb)) with
          | (?fv, ?le) =>
              
              reify_goal fv le lb Rd;
                match goal with
                   |- ?g =>
                       let lp := get_lpol g in
                       let lpol := eval compute in (List.rev lp) in
                       
                       tacsimpl; intros;
 
  let SplitPolyList kont :=
    match lpol with
    | ?p2::?lp2 => kont p2 lp2
    | _ => idtac "polynomial not in the ideal"
    end in
  tacsimpl;
  SplitPolyList ltac:(fun p lp =>
    set (p21:=p) ;
    set (lp21:=lp);
    
    nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci =>
      set (q := PEmul c (PEpow p21 r));
      let Hg := fresh "Hg" in
      assert (Hg:check lp21 q (lci,lq) = true);
      [ (vm_compute;reflexivity) || idtac "invalid nsatz certificate"
      | let Hg2 := fresh "Hg" in
            assert (Hg2: ring_eq (interpret3 _ Rd q fv) ring0);
        [ tacsimpl;
          apply (@check_correct _ Rd fv lp21 q (lci,lq) Hg);
          tacsimpl;
          repeat (split;[assumption|idtac]); exact I
        | simpl in Hg2; tacsimpl;
          apply Rdomain_pow with (interpret3 _ Rd c fv) (Nnat.nat_of_N r); auto with domain;
          tacsimpl; apply domain_axiom_one_zero
          || (simpl) || idtac "could not prove discrimination result"
        ]
      ]
)
)
end end end end .

Ltac nsatz_domainpv pretac radicalmax info lparam lvar tacsimpl rd :=
  pretac;
  nsatz_domain_begin tacsimpl; auto with domain;
  nsatz_domain_generic radicalmax info lparam lvar tacsimpl rd.

Ltac nsatz_domain:=
  intros;
  match goal with
    |- (@ring_eq _ (@domain_ring ?r ?rd) _ _ ) =>
          nsatz_domainpv ltac:idtac 6%N 1%Z (@nil r) (@nil r) ltac:(simpl) rd
  end.

Require Import Reals.
Require Import RealField.

Instance Rri : Ring R := {
  ring0 := 0%R;
  ring1 := 1%R;
  ring_plus := Rplus;
  ring_mult := Rmult;
  ring_sub := Rminus;
  ring_opp := Ropp;
  ring_eq := @eq R;
  ring_ring := RTheory}.

Lemma Raxiom_one_zero: 1%R <> 0%R.

Instance Rdi : Domain R := {
  domain_ring := Rri;
  domain_axiom_product := Rmult_integral;
  domain_axiom_one_zero := Raxiom_one_zero}.

Hint Resolve ring_setoid ring_plus_comp ring_mult_comp ring_sub_comp ring_opp_comp: domain.

Ltac replaceR:=
replace 0%R with (@ring0 _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity];
replace 1%R with (@ring1 _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity];
replace Rplus with (@ring_plus _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity];
replace Rmult with (@ring_mult _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity];
replace Rminus with (@ring_sub _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity];
replace Ropp with (@ring_opp _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity];
replace (@eq R) with (@ring_eq _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity].

Ltac simplR:=
  simpl; replaceR.

Ltac pretacR:=
  replaceR;
  replace Rri with (@domain_ring _ Rdi) in *; [idtac | reflexivity].

Ltac nsatz_domainR:=
  nsatz_domainpv ltac:pretacR 6%N 1%Z (@Datatypes.nil R) (@Datatypes.nil R)
    ltac:simplR Rdi;
  discrR.

Goal forall x y:R, x = y -> (x*x-x+1)%R = ((y*y-y)+1+0)%R.

Instance Zri : Ring Z := {
  ring0 := 0%Z;
  ring1 := 1%Z;
  ring_plus := Zplus;
  ring_mult := Zmult;
  ring_sub := Zminus;
  ring_opp := Zopp;
  ring_eq := (@eq Z);
  ring_ring := Zth}.

Lemma Zaxiom_one_zero: 1%Z <> 0%Z.

Instance Zdi : Domain Z := {
  domain_ring := Zri;
  domain_axiom_product := Zmult_integral;
  domain_axiom_one_zero := Zaxiom_one_zero}.

Ltac replaceZ :=
replace 0%Z with (@ring0 _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity];
replace 1%Z with (@ring1 _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity];
replace Zplus with (@ring_plus _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity];
replace Zmult with (@ring_mult _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity];
replace Zminus with (@ring_sub _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity];
replace Zopp with (@ring_opp _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity];
replace (@eq Z) with (@ring_eq _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity].

Ltac simplZ:=
  simpl; replaceZ.

Ltac pretacZ :=
replaceZ;
replace Zri with (@domain_ring _ Zdi) in *; [idtac | reflexivity].

Ltac nsatz_domainZ:=
nsatz_domainpv ltac:pretacZ 6%N 1%Z (@Datatypes.nil Z) (@Datatypes.nil Z) ltac:simplZ Zdi.

Require Import QArith.

Instance Qri : Ring Q := {
  ring0 := 0%Q;
  ring1 := 1%Q;
  ring_plus := Qplus;
  ring_mult := Qmult;
  ring_sub := Qminus;
  ring_opp := Qopp;
  ring_eq := Qeq;
  ring_ring := Qsrt}.

Lemma Qaxiom_one_zero: not (Qeq 1%Q 0%Q).

Instance Qdi : Domain Q := {
  domain_ring := Qri;
  domain_axiom_product := Qmult_integral;
  domain_axiom_one_zero := Qaxiom_one_zero}.

Ltac replaceQ :=
replace 0%Q with (@ring0 _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity];
replace 1%Q with (@ring1 _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity];
replace Qplus with (@ring_plus _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity];
replace Qmult with (@ring_mult _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity];
replace Qminus with (@ring_sub _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity];
replace Qopp with (@ring_opp _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity];
replace Qeq with (@ring_eq _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity].

Ltac simplQ:=
  simpl; replaceQ.

Ltac pretacQ :=
replaceQ;
replace Qri with (@domain_ring _ Qdi) in *; [idtac | reflexivity].

Ltac nsatz_domainQ:=
nsatz_domainpv ltac:pretacQ 6%N 1%Z (@Datatypes.nil Q) (@Datatypes.nil Q) ltac:simplQ Qdi.


Ltac nsatz :=
  intros;
  match goal with
   | |- (@eq R _ _) => nsatz_domainR
   | |- (@eq Z _ _) => nsatz_domainZ
   | |- (@Qeq _ _) => nsatz_domainQ
   | |- _ => nsatz_domain
  end.