Library ProjectiveGeometry.Space.field_variable_isolation_tactic

Require Export Reals.
Require Export ProjectiveGeometry.Space.general_tactics.

Open Scope R_scope.



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 : R, a = b -> a - b = 0.
intros.
rewrite H.
ring.
Qed.

Lemma Lcinv : forall a b : R, a - b = 0 -> a = b.
intros.
assert (a - b + b = 0 + b).
rewrite H.
auto.
NormalizeRing H0.
auto.
Qed.

Lemma Lcp1 : forall a b c : R, a + b = c -> a = c - b.
intros.
rewrite <- H.
ring.
Qed.

Lemma Lcp2 : forall a b c : R, a + b = c -> b = c - a.
intros.
rewrite <- H.
ring.
Qed.

Lemma Lcm1 : forall a b c : R, a - b = c -> a = c + b.
intros.
rewrite <- H.
ring.
Qed.

Lemma Lcm2 : forall a b c : R, a - b = c -> b = a - c.
intros.
rewrite <- H.
ring.
Qed.

Lemma Lcop1 : forall a b : R, - a = b -> a = - b.
intros.
rewrite <- H.
ring.
Qed.

Lemma Lcmult1 : forall a b c : R, b <> 0 -> a * b = c -> a = c / b.
intros; field_simplify_eq; auto.
Qed.

Lemma Lcmult2 : forall a b c : R, a <> 0 -> a * b = c -> b = c / a.
intros.
rewrite <- H0; field_simplify_eq; trivial.
Qed.

Lemma Lcdiv1 : forall a b c : R, b <> 0 -> a / b = c -> a = b * c.
intros.
rewrite <- H0.
field.
trivial.
Qed.

Lemma Lcdiv2 : forall a b c : R, b <> 0 -> c <> 0 -> a / b = c -> b = a / c.
intros.
rewrite <- H1.
field.
split; trivial.
intuition.
apply H0.
rewrite <- H1 in |- *.
rewrite H2 in |- *.
unfold Rdiv 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.


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

Ltac RewriteVar var H := IsoleVarRing var H; rewrite_all H.