(***************************************************************************)
(* 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.
Require Export general_tactics.

(*************************************************)
(* Variable isolation tactic                     *)
(*************************************************)

(* 
This module defines a few tactics :

   IsoleVar x H isolates one occurence of x in H 
   Warning it does not factorize, but it is still usefull.

(* Goal: @eq F a (Fopp (Fopp a)) *)
   NormalizeRing H normalize the hypothesis H using ring.
   RewriteVar x H, isolates x in H and then substitutes x 
   everywhere.     
*)


Ltac NormalizeRing H :=
  match goal with
  | i:(?X1 = ?X2) |- _ =>
      match constr:(i) with
      | H => generalize H; ring_simplify X1 X2; clear H; intro H
      | _ => fail
      end
  end. 

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

Lemma Lcinv : forall a b : F, a - b = 0 -> a = b.
(* Goal: forall (a b c : F) (_ : not (@eq F b F0)) (_ : not (@eq F c F0)) (_ : @eq F (Fdiv a b) c), @eq F b (Fdiv a c) *)
intros.
(* Goal: @eq F a b *)
assert (a - b + b = 0 + b).
(* Goal: @eq F (Fplus (Fminus a b) b) (Fplus F0 b) *)
(* Goal: @eq F a b *)
rewrite H.
(* Goal: @eq F a b *)
auto.
(* Goal: @eq F a b *)
NormalizeRing H0.
(* Goal: @eq F a b *)
auto.
Qed.

Lemma Lcp1 : forall a b c : F, a + b = c -> a = c - b.
(* Goal: forall (a b c : F) (_ : not (@eq F b F0)) (_ : not (@eq F c F0)) (_ : @eq F (Fdiv a b) c), @eq F b (Fdiv a c) *)
intros.
(* Goal: @eq F a (Fopp b) *)
rewrite <- H.
(* Goal: @eq F a (Fopp (Fopp a)) *)
ring.
Qed.

Lemma Lcp2 : forall a b c : F, a + b = c -> b = c - a.
(* Goal: forall (a b c : F) (_ : not (@eq F b F0)) (_ : not (@eq F c F0)) (_ : @eq F (Fdiv a b) c), @eq F b (Fdiv a c) *)
intros.
(* Goal: @eq F a (Fopp b) *)
rewrite <- H.
(* Goal: @eq F a (Fopp (Fopp a)) *)
ring.
Qed.

Lemma Lcm1 : forall a b c : F, a - b = c -> a = c + b.
(* Goal: forall (a b c : F) (_ : not (@eq F b F0)) (_ : not (@eq F c F0)) (_ : @eq F (Fdiv a b) c), @eq F b (Fdiv a c) *)
intros.
(* Goal: @eq F a (Fopp b) *)
rewrite <- H.
(* Goal: @eq F a (Fopp (Fopp a)) *)
ring.
Qed.

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

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

Lemma Lcmult1 : forall a b c : F, b <> 0 -> a * b = c -> a = c / b.
(* Goal: @eq F a b *)
intros; field_simplify_eq; auto.
Qed.

Lemma Lcmult2 : forall a b c : F, a <> 0 -> a * b = c -> b = c / a.
(* Goal: forall (a b c : F) (_ : not (@eq F b F0)) (_ : not (@eq F c F0)) (_ : @eq F (Fdiv a b) c), @eq F b (Fdiv a c) *)
intros.
(* Goal: @eq F b (Fdiv c a) *)
rewrite <- H0; field_simplify_eq; trivial.
Qed.

Lemma Lcdiv1 : forall a b c : F, b <> 0 -> a / b = c -> a = b * c.
(* Goal: forall (a b c : F) (_ : not (@eq F b F0)) (_ : not (@eq F c F0)) (_ : @eq F (Fdiv a b) c), @eq F b (Fdiv a c) *)
intros.
(* Goal: @eq F a (Fmult b c) *)
rewrite <- H0.
(* Goal: @eq F b (Fdiv a (Fdiv a b)) *)
field.
(* Goal: not (@eq F b F0) *)
trivial.
Qed.

Lemma Lcdiv2 : forall a b c : F, b <> 0 -> c <> 0 -> a / b = c -> b = a / c.
(* Goal: forall (a b c : F) (_ : not (@eq F b F0)) (_ : not (@eq F c F0)) (_ : @eq F (Fdiv a b) c), @eq F b (Fdiv a c) *)
intros.
(* Goal: @eq F c F0 *)
rewrite <- H1.
(* Goal: @eq F b (Fdiv a (Fdiv a b)) *)
field.
(* Goal: not (@eq F b F0) *)
split; trivial.
(* Goal: not (@eq F a F0) *)
intuition.
(* Goal: False *)
apply H0.
(* Goal: @eq F c F0 *)
rewrite <- H1 in |- *.
(* Goal: @eq F (Fdiv a b) F0 *)
rewrite H2 in |- *.
(* Goal: @eq F a (Fopp (Fopp a)) *)
unfold Fdiv in |- *;  ring.
Qed.


Ltac IsoleVarAux1 var H T Hyp :=
  match constr:(T) with
  | (var = ?X2 :>?X1) =>
      assert (Hypazerty : T);
       [ exact H | clear Hyp; rename Hypazerty into Hyp ]
  | (?X1 + ?X2 = ?X3 :>?X4) =>
      IsoleVarAux1 var (Lcp1 X1 X2 X3 H) (X1 = X3 - X2 :>X4) Hyp ||
        IsoleVarAux1 var (Lcp2 X1 X2 X3 H) (X2 = X3 - X1 :>X4) Hyp
  | (?X1 - ?X2 = ?X3 :>?X4) =>
      IsoleVarAux1 var (Lcm1 X1 X2 X3 H) (X1 = X3 + X2 :>X4) Hyp ||
        IsoleVarAux1 var (Lcm2 X1 X2 X3 H) (X2 = X1 - X3 :>X4) Hyp
  | (?X1 / ?X2 = ?X3 :>?X4) =>
      match goal with
      | Hop:(?X2 <> 0) |- _ =>
          IsoleVarAux1 var (Lcdiv1 X1 X2 X3 Hop H) (X1 = X2 * X3 :>X4) Hyp
      | _ =>
          cut (X2 <> 0);
           [ intro;
              match goal with
              | Hop:(?X2 <> 0) |- _ =>
                  IsoleVarAux1 var (Lcdiv1 X1 X2 X3 Hop H)
                   (X1 = X2 * X3 :>X4) Hyp
              end
           | idtac ]
      end ||
        match goal with
        | Hop1:(?X2 <> 0),Hop2:(?X3 <> 0) |- _ =>
            IsoleVarAux1 var (Lcdiv2 X1 X2 X3 Hop1 Hop2 H)
             (X2 = X1 / X3 :>X4) Hyp
        | Hop1:(?X2 <> 0) |- _ =>
            cut (X3 <> 0);
             [ intro;
                match goal with
                | Hop2:(?X3 <> 0) |- _ =>
                    IsoleVarAux1 var (Lcdiv2 X1 X2 X3 Hop1 Hop2 H)
                     (X2 = X1 / X3 :>X4) Hyp
                end
             | idtac ]
        | Hop2:(?X3 <> 0) |- _ =>
            cut (X2 <> 0);
             [ intro;
                match goal with
                | Hop1:(?X2 <> 0) |- _ =>
                    IsoleVarAux1 var (Lcdiv2 X1 X2 X3 Hop1 Hop2 H)
                     (X2 = X1 / X3 :>X4) Hyp
                end
             | idtac ]
        | _ =>
            cut (X2 <> 0);
             [ intro; cut (X3 <> 0);
                [ intro;
                   match goal with
                   | Hop1:(?X2 <> 0),Hop2:(?X3 <> 0) |- _ =>
                       IsoleVarAux1 var (Lcdiv2 X1 X2 X3 Hop1 Hop2 H)
                        (X2 = X1 / X3 :>X4) Hyp
                   end
                | trivial ]
             | trivial ]
        end
  | (?X1 * ?X2 = ?X3 :>?X4) =>
      match goal with
      | Hop:(?X2 <> 0) |- _ =>
          IsoleVarAux1 var (Lcmult1 X1 X2 X3 Hop H) (X1 = X3 / X2 :>X4) Hyp
      | _ =>
          cut (X2 <> 0);
           [ intro;
              match goal with
              | Hop:(?X2 <> 0) |- _ =>
                  IsoleVarAux1 var (Lcmult1 X1 X2 X3 Hop H)
                   (X1 = X3 / X2 :>X4) Hyp
              end
           | idtac ]
      end ||
        match goal with
        | Hop:(?X1 <> 0) |- _ =>
            IsoleVarAux1 var (Lcmult2 X1 X2 X3 Hop H) (X2 = X3 / X1 :>X4) Hyp
        | _ =>
            cut (X1 <> 0);
             [ intro;
                match goal with
                | Hop:(?X1 <> 0) |- _ =>
                    IsoleVarAux1 var (Lcmult2 X1 X2 X3 Hop H)
                     (X2 = X3 / X1 :>X4) Hyp
                end
             | idtac ]
        end
  | (- ?X1 = ?X3 :>?X4) =>
      IsoleVarAux1 var (Lcop1 X1 X3 H) (X1 = - X3 :>X4) Hyp
  | _ => fail
  end.


Ltac IsoleVarAux var H T Hyp :=
  match constr:(T) with
  | (?X2 = ?X3 :>?X1) =>
      IsoleVarAux1 var H T Hyp ||
        IsoleVarAux1 var (sym_eq H) (X3 = X2 :>X1) Hyp
  end.

Ltac TypeOf H :=
  match goal with
  | id:?X1 |- _ => match constr:(id) with
                   | H => constr:(X1)
                   | _ => fail
                   end
  end.

Ltac IsoleVar var H := let T := TypeOf H in
                       IsoleVarAux var H T H.

(* Tactic Definition IsoleVar var H := (IsoleVarAux 'var 'H (TypeOf ? H) H). *)

Ltac IsoleVarRing var H := IsoleVar var H; NormalizeRing H.

Ltac RewriteVar var H := IsoleVarRing var H; try rewrite H in *.

(* Tests *)
(*
Lemma test_isole_var_1 : forall a b,  a+b=0 -> a = -b.
Proof.
(* Goal: forall (a b c : F) (_ : not (@eq F b F0)) (_ : not (@eq F c F0)) (_ : @eq F (Fdiv a b) c), @eq F b (Fdiv a c) *)
intros.
IsoleVar a H.
(* Goal: @eq F a (Fopp (Fopp a)) *)
rewrite H; ring.
Qed.

Lemma test_isole_var_2 : forall a b,  a-b=0 -> a = b.
Proof.
(* Goal: forall (a b c : F) (_ : not (@eq F b F0)) (_ : not (@eq F c F0)) (_ : @eq F (Fdiv a b) c), @eq F b (Fdiv a c) *)
intros.
IsoleVar a H.
NormalizeRing H.
assumption.
Qed.

Lemma test_isole_var_3 : forall a b,  b<>0 -> a*b=0 -> a = 0.
Proof.
(* Goal: forall (a b c : F) (_ : not (@eq F b F0)) (_ : not (@eq F c F0)) (_ : @eq F (Fdiv a b) c), @eq F b (Fdiv a c) *)
intros.
IsoleVar a H0.
rewrite H0.
(* Goal: @eq F b (Fdiv a (Fdiv a b)) *)
field.
assumption.
Qed.

Lemma test_isole_var_4 : forall a b,  b<>0 -> a/b=0 -> a = 0.
Proof.
(* Goal: forall (a b c : F) (_ : not (@eq F b F0)) (_ : not (@eq F c F0)) (_ : @eq F (Fdiv a b) c), @eq F b (Fdiv a c) *)
intros.
IsoleVar a H0.
(* Goal: @eq F a b *)
NormalizeRing H0.
assumption.
Qed.

Theorem premier_degre : forall a b x,  a<>0 -> a*x+b=0 -> x = -b/a.
Proof.
(* Goal: forall (a b c : F) (_ : not (@eq F b F0)) (_ : not (@eq F c F0)) (_ : @eq F (Fdiv a b) c), @eq F b (Fdiv a c) *)
intros.
IsoleVar x H0.
rewrite H0.
(* Goal: @eq F b (Fdiv a (Fdiv a b)) *)
field.
assumption.
Qed.

*)
