Nsatz Complex

Require Import Complex Cpow Ctacfield.

Require Import Nsatz.


Lemma Csth : Setoid_Theory C (@eq C).
constructor;red;intros;subst;trivial.
Qed.

Instance Cops: (@Ring_ops C C0 C1 Cadd Cmult Cminus Copp (@eq C)).

Instance Cri : (Ring (Ro:=Cops)).
constructor;
try (try apply Csth;
   try (unfold respectful, Proper; unfold equality; unfold eq_notation in *;
  intros; try rewrite H; try rewrite H0; reflexivity)).
 exact Cadd_0_l. exact Cadd_comm. symmetry. apply Cadd_assoc.
 exact Cmult_1_l.  exact Cmult_1_r. symmetry. apply Cmult_assoc.
 intros ; apply Cmult_add_distr_r. intros; apply Cmult_add_distr_l. 
exact Cadd_opp_r.
Defined.

Instance Ccri: (Cring (Rr:=Cri)).
red. exact Cmult_comm. Defined.

Instance Cdi : (Integral_domain (Rcr:=Ccri)).
constructor. 
exact Cmult_integral. exact C1_neq_C0. Defined.
 

Instance CPow : (Power (A := C) (B := nat)).
 exact Cpow. Defined.


(* Example taken from Pottier's paper.

x : Z
y : Z
H : x ^ 2 + x * y = 0
H0 : y ^ 2 + x * y = 0
============================
x + y = 0
*)


Instance RPow : (Power (A := R) (B := nat)). (* standard *)
 exact pow. Defined.


Goal forall (x y : R), x ^ 2%nat + x * y = 0 -> y ^ 2%nat + x * y = 0 -> x + y = 0.
intros ; apply psos_r1b ; repeat equalities_to_goal.
match goal with
  |- ?g => let lg   := lterm_goal g in
           let lvar := eval red in (list_reifyl (lterm := lg)) in
           match lvar with
           | (?fv, ?le) => reify_goal fv le lg end
           end.

Goal forall (x y : C), x ^ 2%nat + x * y = 0 -> y ^ 2%nat + x * y = 0 -> x + y = 0.
intros ; apply psos_r1b ; repeat equalities_to_goal.
nsatz_generic 6%N 1%Z (cons x (cons y nil)) (@nil C).
match goal with
  |- ?g => let lg   := lterm_goal g in
           let lvar := eval red in (list_reifyl (lterm := lg)) in
           match lvar with
           | (?fv, ?le) => reify_goal fv le lg end
           end.