Library AreaMethod.elimination_prepare


Require Export area_elimination_lemmas.
Require Export py_elimination_lemmas.

Tactics to distinguish cases if necessary

If S A B C = 0 is in the context then Tac1 is used
If S A B C <>0 is in the context then Tac2 is used
othewise we use Col decidability and perform Tac1 and Tac2 in each branch
We do not use the defiinition Col, to save the burden of managing the unfold

Lemma col_decS : forall A B C:Point, S A B C = 0 \/ S A B C <>0.
Proof.
unfold Col.
apply col_dec.
Qed.

Ltac named_cases_colS A B C H := elim (col_decS A B C);intro H.

Ltac test_col A B C Tac1 Tac2 :=
 match goal with
| HCol : S A B C = 0 |- _ => Tac1 HCol
| HCol : S A B C <>0 |- _ => Tac2 HCol
| _ => let HCol := fresh in
      (named_cases_colS A B C HCol;
   [ Tac1 HCol | Tac2 HCol])
end.


Ltac test_parallel A B C D Tac1 Tac2 :=
 match goal with
| HPar : parallel A B C D |- _ => Tac1 HPar
| HPar : ~ parallel A B C D |- _ => Tac2 HPar
| _ => let HPar := fresh in
      (named_cases_parallel A B C D HPar;
   [ Tac1 HPar | Tac2 HPar])
end.

The same for point equality

Ltac test_equality A B Tac1 Tac2 :=
 match goal with
| H : A = B |- _ => Tac1 H
| H : A<>B |- _ => Tac2 H
| _ => let H := fresh in
      (named_cases_equality A B H;
   [ Tac1 H | Tac2 H])
end.

Change A<>B into B<>A

Ltac invdiffhyp A B :=
  let H := HypOfType (A <> B) in
  let Hnew := fresh in
  (assert (Hnew := ldiff A B H); clear H).

Unification tactic for signed areas but just concerning one point, and puting this point in last position, except for Py where we put it either on both side, in the middle or on the right
The use of this specific tactic during the elimination process is faster than normalization of signed areas for every quantities

Ltac put_on_the_right_areas P :=
  repeat match goal with
    | |- context[S P ?X1 ?X2] =>
         rewrite (S_1 P X1 X2) in *
    | |- context[S ?X1 P ?X2] =>
         rewrite (S_0 X1 P X2) in *
end.

Ltac put_on_the_right_pys P :=
  repeat match goal with
    | |- context[Py ?A P ?A] => rewrite (pyth_simpl_4 A P) in *
    | |- context[Py P ?X1 ?X2] => rewrite (pyth_sym P X1 X2) in *
end.

This tactics remove one parallel hypotheses and replace it by the new one

Ltac changeparhyp A B C D lpar :=
  let Hpar := HypOfType (parallel A B C D) in
  let HparNew := fresh in
  (assert (HparNew := lpar A B C D Hpar); clear Hpar).

Put Y on the upper right position

Ltac put_on_the_right_ratios Y :=
  repeat match goal with
  |_:_ |- context [(?X5 ** Y / Y ** ?X7)] =>
      replace (X5 ** Y / Y ** X7) with (- (X5 ** Y / X7 ** Y));
       [ changeparhyp X5 Y Y X7 lpar1; invdiffhyp Y X7
       | symmetry in |- *; apply dirseg_4; Geometry ]
  | _:_ |- context [(Y ** ?X5 / ?X7 ** Y)] =>
      replace (Y ** X5 / X7 ** Y) with (- (X5 ** Y / X7 ** Y));
       [ changeparhyp Y X5 X7 Y lpar2
       | symmetry in |- *; apply dirseg_4; Geometry ]
  | _:_ |- context [(Y ** ?X5 / ?X6 ** ?X7)] =>
      replace (Y ** X5 / X6 ** X7) with (X5 ** Y / X7 ** X6);
       [ changeparhyp Y X5 X6 X7 lpar3; invdiffhyp X6 X7 | Geometry ]
  | _:_ |- context [(?X5 ** ?X6 / Y ** ?X7)] =>
      replace (X5 ** X6 / Y ** X7) with (X6 ** X5 / X7 ** Y);
       [ changeparhyp X5 X6 Y X7 lpar3; invdiffhyp Y X7 | Geometry ]
end.

Ltac case_equal X5 X6 X7 Y Heq := rewrite Heq in *.

Lemma invariant_inverse_ratio : forall A B C D,
 A<>B -> C<>D -> C**D/ A**B <> 0.
intros.
apply nonzerodiv;Geometry.
Qed.

Ltac case_not_equal X5 X6 X7 Y Heq :=
 let T:= fresh in
  assert (T:X7**Y/X5**X6 <> 0);[apply (invariant_inverse_ratio X5 X6 X7 Y );try assumption|idtac];
 (replace (X5**X6 / X7**Y) with (1/(X7**Y / X5 ** X6));[changeparhyp X5 X6 X7 Y par_2|symmetry;apply inverse_ratio;Geometry]).

This tactic assumes that Y is on the right

Ltac put_on_the_upper_right_ratios Y :=
 repeat match goal with
   |_:_ |- context [(?X5 ** Y / ?X6 ** Y)] => fail 1
   |_:_ |- context [(?X5 ** ?X6 / ?X7**Y)] =>
          test_equality X5 X6 ltac:(case_equal X5 X6 X7 Y) ltac:(case_not_equal X5 X6 X7 Y)
end.

Ltac unify_signed_areas_point P :=
  repeat
   match goal with
   | |- context [(S ?X1 ?X1 ?X2)] =>
       replace (S X1 X1 X2) with 0; [ idtac | apply trivial_col1 ]
   | |- context [(S ?X2 ?X1 ?X1)] =>
       replace (S X2 X1 X1) with 0; [ idtac | apply trivial_col2 ]
   | |- context [(S ?X1 ?X2 ?X1)] =>
       replace (S X1 X2 X1) with 0; [ idtac | apply trivial_col3 ]
   | |- context [(S ?X1 ?X2 P)] =>
    ( let Truc := fresh in
    match goal with
       | |- context [(S ?X4 ?X5 P)] =>
            (assert (Truc : S X4 X5 P = - S X1 X2 P);
             [ apply S_3 || apply S_2 || apply S_4
             | rewrite Truc in *; clear Truc ]) ||
             (assert (Truc : S X4 X5 P = S X1 X2 P);
               [ apply S_0 || apply S_1 | rewrite Truc in *; clear Truc ])
       end)
   end.

This tactic prepares the elimination process by putting the point on the right and unifying the geometric quantities concerning the point

Ltac unify_signed_areas_and_put_on_the_right P :=
 put_on_the_right_areas P;
 put_on_the_right_pys P;
 put_on_the_right_ratios P;
 put_on_the_upper_right_ratios P;
 unify_signed_areas_point P.

Lemma test_1 : forall A B C, S A B C + S B A C = 0.
Proof.
intros.
unify_signed_areas_and_put_on_the_right B.
ring.
Qed.

Lemma test_2 : forall Y A C D, parallel Y A C D -> C<>D ->
 Y**A / C**D = (A**Y / D**C).
Proof.
intros.
put_on_the_right_ratios Y.
reflexivity.
Qed.

Lemma test_3 :forall Y A C D, parallel C D A Y -> A<>Y ->
C<>D -> C**D / A**Y = 1/(A**Y / C**D).
Proof.
intros.
unify_signed_areas_and_put_on_the_right Y.
reflexivity.
Qed.

Lemma test_4: forall A B Y, Py Y A B = Py B A Y.
Proof.
intros.
unify_signed_areas_and_put_on_the_right Y.
reflexivity.
Qed.

Lemma test_5: forall A Y, Py Y A Y = Py Y A Y.
Proof.
intros.
unify_signed_areas_and_put_on_the_right Y.
reflexivity.
Qed.

Lemma test_6: forall C B A E, Py B E B + Py E A C = Py E B E + Py C A E.
Proof.
intros.
unify_signed_areas_and_put_on_the_right E.
reflexivity.
Qed.