(***************************************************************************)
(* Formalization of the Chou, Gao and Zhang's decision procedure.          *)
(* Julien Narboux (Julien@narboux.fr)                                      *)
(* LIX/INRIA FUTURS 2004-2006                                              *)
(* University of Strasbourg 2008                                           *)
(***************************************************************************)

Require Export field_variable_isolation_tactic.

(****************************************************)
(*  General properties about fields                    *)
(****************************************************)

Lemma field_prop_1 : forall a b : F, a + b = a -> b = 0.
Proof with try solve [ ring | congruence ].
intros...
assert (a + b - a = a - a)...
assert (a - a = 0)...
rewrite H1 in H0...
assert (a + b - a = b)...
Qed.

Lemma field_prop_3 : forall a : F, a = 0 -> - a = 0.
(* Goal: forall (a b : F) (_ : not (@eq F a F0)) (_ : not (@eq F b F0)), @eq F (Fdiv a b) (Fdiv F1 (Fdiv b a)) *)
intros.
(* Goal: @eq F (Fopp a) F0 *)
rewrite H.
(* Goal: @eq F (Fopp F0) F0 *)
ring.
Qed.

Lemma field_prop_4 : forall a : F, - a = 0 -> a = 0.
Proof with try solve [ ring | congruence ].
intros...
assert (a + - a = a + 0)...
assert (a + - a = 0)...
rewrite H1 in H0...
assert (a + 0 = a)...
Qed.

Lemma field_prop_5 : forall a b : F, - a = - b -> a = b.
Proof with try solve [ ring | congruence ].
intros...
assert (- - a = - - b)...
assert (- - a = a)...
assert (- - b = b)...
Qed.

Lemma nonzeromult : forall a b : F, a <> 0 -> b <> 0 -> a * b <> 0.
Proof with try solve [ auto with field_hints | congruence ].
intros...
assert (a * b / b = a)...
field...
intuition...
assert (a * b / b = 0 / b)...
rewrite H1 in H3...
assert (a = 0)...
assert (0 / b = 0)...
field...
Qed.

Lemma nonzerodiv : forall a b : F, a <> 0 -> b <> 0 -> a / b <> 0.
Proof with try solve [ auto with field_hints | congruence ].
intros...
unfold not in |- *; intro...
IsoleVarRing a H1...
Qed.

Lemma nonzeroinv : forall a : F, a <> 0 -> / a <> 0.
Proof with try solve [ auto with field_hints | congruence ].
intros...
unfold not in |- *; intro...
assert (a * / a = 1)...
field...
assert (a * / a = a * 0)...
rewrite H1 in H2...
assert (a * 0 = 0)...
(* Goal: @eq F (Fopp F0) F0 *)
ring...
rewrite H3 in H2...
Qed.

Lemma opzero : forall a : F, a <> 0 -> - a <> 0.
Proof with try solve [ congruence ].
intros...
assert (a + - a = 0)...
apply Fplus_Fopp_r...
intuition...
rewrite H1 in H0...
assert (a = 0)...
assert (a + 0 = 0 + a)...
apply Fplus_sym...
rewrite H2 in H0...
assert (0 + a = a)...
apply Fplus_Ol...
Qed.

Theorem divnonzero: forall a b: F, a / b <> 0 -> a<>0.
(* Goal: @eq F (Fopp F0) F0 *)
  intros a b H1 H2; case H1; unfold Fdiv; rewrite H2; ring.
Qed.

Theorem multnonzero: forall a b: F, a*b<>0 -> a<>0 /\ b<>0.
(* Goal: @eq F (Fopp F0) F0 *)
  intros a b H1; split; intros H2; case H1; rewrite H2;ring.
Qed.

Theorem multnonzero_l: forall a b: F, a*b<>0 -> a<>0. 
(* Goal: @eq F (Fopp F0) F0 *)
  intros a b H1; intros H2; case H1; rewrite H2;ring.
Qed.

Theorem multnonzero_r: forall a b: F, a*b<>0 -> b<>0. 
(* Goal: @eq F (Fopp F0) F0 *)
  intros a b H1; intros H2; case H1; rewrite H2;ring.
Qed.


Lemma inverse_ratio : forall a b, a<>0 -> b<>0 -> a/b = 1 / (b/a).
Proof.
(* Goal: forall (a b : F) (_ : not (@eq F a F0)) (_ : not (@eq F b F0)), @eq F (Fdiv a b) (Fdiv F1 (Fdiv b a)) *)
intros.
(* Goal: @eq F (Fdiv a b) (Fdiv F1 (Fdiv b a)) *)
field; auto.
Qed.

Hint Resolve field_prop_1 field_prop_3 field_prop_4 field_prop_5 opzero
  nonzeromult nonzerodiv nonzeroinv inverse_ratio : field_hints.
