Library AreaMethod.area_method

Require Export general_tactics.
Require Export Rgeometry_tools.
Require Export constructed_points_elimination.
Require Export free_points_elimination.
Require Export simplify_constructions.
Require Export construction_tactics.
Require Export my_field_tac.


Ltac decomp_non_zero_mult_div H :=
  (apply (multnonzero) in H || apply (divnonzero) in H; use H).

Ltac decomp_all_non_zero_mult_div := repeat match goal with
 H: ?X <> 0 |- _ => decomp_non_zero_mult_div H
end.

Ltac field_and_conclude :=
  (abstract (field;decomp_all_non_zero_mult_div;solve_conds)) ||
  (abstract (Ffield)).


Ltac DecomposeMratio :=
  repeat
   match goal with
   | H:(mratio _ _ _ _) |- _ =>
       unfold mratio in H; decompose [and] H; clear H
   end.

Ltac prepare_half_free_construction :=
repeat match goal with
   | H:(on_line ?X1 ?X2 ?X3) |- _ =>
    let T:= fresh in
    (assert (T:=(on_line_to_on_line_d X1 X2 X3 H));clear H;set ((X2**X1)/(X2**X3)) in * )
   | H:(on_parallel ?X1 ?X2 ?X3 ?X4) |- _ =>
    let T:= fresh in
    (assert (T:=(on_parallel_to_on_parallel_d X1 X2 X3 X4 H));clear H;set ((X2**X1)/(X3**X4)) in * )
   | H:(on_perp ?X1 ?X2 ?X3 ) |- _ =>
    let T:= fresh in
    (assert (T:=(on_perp_to_on_perp_d X1 X2 X3 H));clear H;set ((2 + 2) * S X2 X3 X1 / Py X2 X3 X2) in * )

end.

Ltac add_non_zero_hyps :=
 repeat
 match goal with
   | H:?A<>?B |- _ =>
           assert_if_not_exist (A**B<>0);[apply neq_not_zero;assumption|revert H]
end;intros.

Ltac check_ratio_hyps_aux A B C D :=
    ((match goal with
 | H : parallel A B C D , H2 : C<>D |- _ => fail 2
end) || fail 3 "Error, one the following hypotheses are missing : parallel" A B C D ", " C "<>" D) || idtac.

Ltac check_ratio_hyps :=
 try match goal with
| H : _ |- context [?A**?B/?C**?D] => check_ratio_hyps_aux A B C D
end.

Lemma test_check_ratio_hyp : forall A B C D,
   parallel A B C D ->
C<>D ->
 A**B / C**D = A**B/C**D.
Proof.
intros.
check_ratio_hyps.
reflexivity.
Qed.

Ltac unfold_non_primitive_constructions :=
 unfold is_midpoint, m_ratio, on_circle, inter_lc,
  inversion, eq_angle, eq_distance, co_circle, harmonic in *.


Definition parallel_s (A B C D : Point) : Prop := S A C B = S B A D.

Lemma parallel_equiv : forall A B C D, parallel_s A B C D <-> parallel A B C D.
Proof.
intros.
unfold parallel_s, parallel, S4.
split.
intro.
rewrite H.
uniformize_signed_areas.
ring.
intro.
IsoleVar (S A C B) H.
rewrite H.
uniformize_signed_areas.
ring.
Qed.

Ltac assert_non_zero_hyps_circum_ortho_center :=
  repeat
( match goal with
| H: is_circumcenter ?O ?A ?B ?C |- _ =>
 assert_if_not_exist (2 * (Py A B A * Py A C A - Py B A C * Py B A C) <> 0);
 [(apply (is_circumcenter_non_zero O A B C H))|idtac]
| H: is_orthocenter ?O ?A ?B ?C |- _ =>
 assert_if_not_exist ((Py A B A * Py A C A - Py B A C * Py B A C) <> 0);
 [(apply (is_orthocenter_non_zero O A B C H))|idtac]
end).



Ltac geoInit :=
  unfold_non_primitive_constructions; intros;
  unfold perp, S4, Py4 in |- *;
  unfold Col in *; DecomposeMratio;
  prepare_half_free_construction;
  DecompAndAll;
  check_ratio_hyps;
  assert_non_zero_hyps_circum_ortho_center;
  unfold is_circumcenter, is_orthocenter, is_centroid, is_Lemoine in *;
  add_non_zero_hyps;
  put_on_inter_line_parallel;repeat split;
  try (apply -> parallel_equiv);
  unfold parallel_s.

Ltac simpl_left := apply f_equal2;[solve [ring] | idtac];idtac "simpl gauche".
Ltac simpl_right := apply f_equal2;[idtac | solve[ring]];idtac "simpl droite".
Ltac simpl_left_right := repeat (simpl_left || simpl_right).

Lemma f_equal2_sym:
  forall (f : F -> F -> F),
  (forall x y, f x y = f y x) ->
  forall (x1 y1 : F) (x2 y2 : F),
       x1 = y1 -> x2 = y2 -> f x1 x2 = f y2 y1.
Proof.
intros.
rewrite H.
apply f_equal2;auto.
Qed.

Ltac simpl_left_sym :=
  apply (f_equal2_sym Fplus Fplus_sym);[solve [ring] | idtac];idtac "simpl gauche sym".

Ltac simpl_right_sym :=
  apply (f_equal2_sym Fplus Fplus_sym);[idtac | solve[ring]];idtac "simpl droite sym".

Ltac simpl_left_right_sym := repeat (simpl_left_sym || simpl_right_sym).

Ltac simpl_eq := simpl_left_right;simpl_left_right_sym.

Lemma eq_simpl_1 : forall a b c,
        b=c -> a+b = a+c .
Proof.
intros.
subst.
auto.
Qed.

Lemma eq_simpl_2 : forall a b c,
        b=c -> b+a = c+a .
Proof.
intros.
subst.
auto.
Qed.

Lemma eq_simpl_3 : forall a b c,
        b=c -> a+b = c+a .
Proof.
intros.
subst.
ring.
Qed.

Lemma eq_simpl_4 : forall a b c,
        b=c -> b+a = a+c .
Proof.
intros.
subst.
ring.
Qed.

Lemma eq_simpl_5 : forall a b c,
        b=c -> a*b = a*c .
Proof.
intros.
subst.
auto.
Qed.

Lemma eq_simpl_6 : forall a b c,
        b=c -> b*a = c*a .
Proof.
intros.
subst.
auto.
Qed.

Lemma eq_simpl_7 : forall a b c,
        b=c -> a*b = c*a .
Proof.
intros.
subst.
ring.
Qed.

Lemma eq_simpl_8 : forall a b c,
        b=c -> b/a = c/a .
Proof.
intros.
subst.
ring.
Qed.

Lemma eq_simpl_9 : forall b c,
        b=c -> -b = -c .
Proof.
intros.
subst.
ring.
Qed.

Lemma eq_simpl_10 : forall a b c,
        b=c -> a-b = a-c .
Proof.
intros.
subst.
auto.
Qed.

Lemma test_simpl_left_right_1 : forall a b c,
(a)+(c+b) = (a+a-a)+(b+c).
Proof.
intros.
simpl_eq.
ring.
Qed.

Lemma test_simpl_left_right_2 : forall a b c,
(c+b)+((a)+(c+b)) = (c+b)+ ((a+a-a)+(b+c)).
Proof.
intros.
simpl_eq.
ring.
Qed.

Lemma test_simpl_left_right_3 : forall a b c,
a+(b+c) = (c+b)+a.
Proof.
intros.
simpl_eq.
ring.
Qed.

Ltac turn_into_ring_eq :=
  try (field_simplify_eq;
  [idtac|solve [repeat split; repeat apply nonzeromult;auto with Geom]]).

Ltac am_before_field := idtac " initialisation...";geoInit;idtac " elimination..."; eliminate_All; idtac " uniformize areas...";
  uniformize_pys;Runiformize_signed_areas;idtac " simplification...";basic_simpl.

Ltac set_all := repeat
   match goal with
   | H:context[(S ?X1 ?X2 ?X3)] |- _ => set (S X1 X2 X3) in *
   | _:_ |- context[(S ?X1 ?X2 ?X3)] => set (S X1 X2 X3) in *
   end.

Ltac unfold_Py :=
 repeat (rewrite pyth_simpl_3 in *); unfold Py in *.

Ltac area_method :=
  idtac "Area method:";
  am_before_field;
  idtac " before field...";
 
  (solve [set_all; unfold_Py; basic_simpl; uniformize_dir_seg; field_and_conclude ] ||
  (idtac " we need to make geometric quantities independant...";
  only_use_area_coordinates;set_all; field_and_conclude)).