Library AreaMethod.constructed_points_elimination
Require Export ratios_elimination_lemmas.
Require Export py_elimination_lemmas.
Require Export area_coords_elimination.
Require Export elimination_prepare.
Require Export area_coords_elimination.
Ltac elimi_inter_ll_col A C D U V P Q Y H Hdenom Hpar Hneq HCol :=
let T1 := fresh in
(assert
(T1 :=non_zero_denom_inter_ll_2_length_ratio A C D U V P Q Y H HCol Hdenom Hneq Hpar);
rewrite
(elim_length_ratio_inter_ll_2 A C D U V P Q Y H HCol Hdenom Hpar Hneq) in *).
Ltac elimi_inter_ll_not_col A C D U V P Q Y H Hdenom Hpar HCol :=
let T1 := fresh in
(assert
(T1 :=non_zero_denom_inter_ll_1_length_ratio A C D U V P Q Y H HCol Hpar Hdenom);
rewrite
(elim_length_ratio_inter_ll_1 A C D U V P Q Y H HCol Hdenom Hpar) in *).
In the collinear case we don't have a special formula
Ltac elimi_inter_ll_col_spec A C D U V P Q Y H Hdenom Hpar Hneq HCol :=
rewrite (elim_length_ratio_inter_ll_2_spec A C U V P Q Y H HCol Hdenom Hpar Hneq) in *.
Ltac elimi_inter_ll_not_col_spec A C D U V P Q Y H Hdenom Hpar Hneq HCol :=
rewrite (elim_length_ratio_inter_ll_1_spec A C U V P Q Y H HCol Hdenom Hpar) in *.
Ltac elimi_inter_ll_spec A C D U V P Q Y H Hdenom Hpar Hneq :=
test_col A U V
ltac: (elimi_inter_ll_col_spec A C D U V P Q Y H Hdenom Hpar Hneq)
ltac: (elimi_inter_ll_not_col_spec A C D U V P Q Y H Hdenom Hpar Hneq).
Ltac test_equality_and_subst Hc A B Tac :=
match goal with
| H : A = B |- _ => rewrite <- H in *;rewrite H in Hc
| H : A<>B |- _ => Tac H
| _ => let H := fresh in
(named_cases_equality A B H;
[ rewrite <- H in *; rewrite H in Hc | Tac H])
end.
Ltac test_equality_and_subst_2 Hc A B Tac Tac2 :=
match goal with
| H : A = B |- _ => rewrite <- H in *;try rewrite H in Hc;Tac2
| H : A<>B |- _ => Tac H
| _ => let H := fresh in
(named_cases_equality A B H;
[ (rewrite <- H in *; try rewrite H in Hc;Tac2) |
Tac H])
end.
Ltac elimi_inter_ll_gen P Q U V A Y C D H Hneq :=
let Hdenom := HypOfType (C <> D) in
let Hpar := HypOfType (parallel A Y C D) in
test_col A U V
ltac: (elimi_inter_ll_col A C D U V P Q Y H Hdenom Hpar Hneq)
ltac: (elimi_inter_ll_not_col A C D U V P Q Y H Hdenom Hpar).
Ltac elimi_inter_ll P Q U V A Y C D H :=
let Hi := fresh in
(assert (Hi : C <> D); [ Geometry | idtac ];
match constr:(A, (C, D)) with
rewrite (elim_length_ratio_inter_ll_2_spec A C U V P Q Y H HCol Hdenom Hpar Hneq) in *.
Ltac elimi_inter_ll_not_col_spec A C D U V P Q Y H Hdenom Hpar Hneq HCol :=
rewrite (elim_length_ratio_inter_ll_1_spec A C U V P Q Y H HCol Hdenom Hpar) in *.
Ltac elimi_inter_ll_spec A C D U V P Q Y H Hdenom Hpar Hneq :=
test_col A U V
ltac: (elimi_inter_ll_col_spec A C D U V P Q Y H Hdenom Hpar Hneq)
ltac: (elimi_inter_ll_not_col_spec A C D U V P Q Y H Hdenom Hpar Hneq).
Ltac test_equality_and_subst Hc A B Tac :=
match goal with
| H : A = B |- _ => rewrite <- H in *;rewrite H in Hc
| H : A<>B |- _ => Tac H
| _ => let H := fresh in
(named_cases_equality A B H;
[ rewrite <- H in *; rewrite H in Hc | Tac H])
end.
Ltac test_equality_and_subst_2 Hc A B Tac Tac2 :=
match goal with
| H : A = B |- _ => rewrite <- H in *;try rewrite H in Hc;Tac2
| H : A<>B |- _ => Tac H
| _ => let H := fresh in
(named_cases_equality A B H;
[ (rewrite <- H in *; try rewrite H in Hc;Tac2) |
Tac H])
end.
Ltac elimi_inter_ll_gen P Q U V A Y C D H Hneq :=
let Hdenom := HypOfType (C <> D) in
let Hpar := HypOfType (parallel A Y C D) in
test_col A U V
ltac: (elimi_inter_ll_col A C D U V P Q Y H Hdenom Hpar Hneq)
ltac: (elimi_inter_ll_not_col A C D U V P Q Y H Hdenom Hpar).
Ltac elimi_inter_ll P Q U V A Y C D H :=
let Hi := fresh in
(assert (Hi : C <> D); [ Geometry | idtac ];
match constr:(A, (C, D)) with
In the first cases we know the points are collinear
| (U, (V, Y)) =>
let Hfresh := fresh in
assert (Hfresh := aux_co_side_1 P Q U V Y Hi H);
rewrite (co_side_elim_1 P Q U V Y Hi H) in *;clear Hi
| (V, (U, Y)) =>
let Hfresh := fresh in
assert (Hfresh := aux_co_side_2 P Q U V Y Hi H);
rewrite (co_side_elim_2 P Q U V Y Hi H) in *;clear Hi
| (P, (Q, Y)) =>
let Hfresh := fresh in
assert (Hfresh := aux_co_side_3 P Q U V Y Hi H);
rewrite (co_side_elim_3 P Q U V Y Hi H) in *;clear Hi
| (Q, (P, Y)) =>
let Hfresh := fresh in
assert (Hfresh := aux_co_side_4 P Q U V Y Hi H);
rewrite (co_side_elim_4 P Q U V Y Hi H) in *;clear Hi
let Hfresh := fresh in
assert (Hfresh := aux_co_side_1 P Q U V Y Hi H);
rewrite (co_side_elim_1 P Q U V Y Hi H) in *;clear Hi
| (V, (U, Y)) =>
let Hfresh := fresh in
assert (Hfresh := aux_co_side_2 P Q U V Y Hi H);
rewrite (co_side_elim_2 P Q U V Y Hi H) in *;clear Hi
| (P, (Q, Y)) =>
let Hfresh := fresh in
assert (Hfresh := aux_co_side_3 P Q U V Y Hi H);
rewrite (co_side_elim_3 P Q U V Y Hi H) in *;clear Hi
| (Q, (P, Y)) =>
let Hfresh := fresh in
assert (Hfresh := aux_co_side_4 P Q U V Y Hi H);
rewrite (co_side_elim_4 P Q U V Y Hi H) in *;clear Hi
In the other cases we have to perform classical reasoning.
| (A,(C,Y)) => idtac "here";
let Hdenom := HypOfType (C <> D) in
let Hpar := HypOfType (parallel A Y C D) in
test_equality_and_subst H A Y
ltac:(elimi_inter_ll_spec A C D U V P Q Y H Hdenom Hpar)
let Hdenom := HypOfType (C <> D) in
let Hpar := HypOfType (parallel A Y C D) in
test_equality_and_subst H A Y
ltac:(elimi_inter_ll_spec A C D U V P Q Y H Hdenom Hpar)
The most general case
| _ =>
test_equality_and_subst H A Y ltac: (elimi_inter_ll_gen P Q U V A Y C D H )
end).
test_equality_and_subst H A Y ltac: (elimi_inter_ll_gen P Q U V A Y C D H )
end).
on_line_d : elimination in length ratio in the case Col
Ltac elimi_on_line_d_col_aux P Q lambda A Y C D H Hdenom Hpar HCol Hdiff :=
let T3 := fresh in (assert
(T3 :=
invariant_par_on_line_d_1_length_ratio_2 A C D P Q Y lambda H HCol Hdiff Hpar);
rewrite
(elim_length_ratio_on_line_d_1 A C D P Q Y lambda H HCol Hdenom) in *).
Ltac elimi_on_line_d_col P Q lambda A Y C D H Hdenom Hpar HCol:=
let T1 := fresh in
(assert (T1 := non_zero_denom_on_line_d_1_length_ratio Y P Q lambda H);
let T3 := fresh in
(assert (T3 := non_zero_denom_on_line_d_1_length_ratio_seg Y P Q lambda H);
let T2 := fresh in
(assert (T2 := invariant_par_on_line_d_1_length_ratio A C D P Q Y lambda H HCol Hpar);
let T4 := fresh in
(assert (T4 :=invariant_par_on_line_d_1_length_ratio_3 A C D P Q Y lambda H HCol Hpar);
test_equality_and_subst H A Y
ltac:(elimi_on_line_d_col_aux P Q lambda A Y C D H Hdenom Hpar HCol)
)))).
on_line_d : elimination in length ratio in the case not Col
Ltac elimi_on_line_d_not_col P Q lambda A Y C D H Hdenom Hpar HCol :=
let T := fresh in
(assert (T := non_zero_denom_on_line_d_2_length_ratio A C D P Q Y lambda H HCol Hpar Hdenom));
rewrite
(elim_length_ratio_on_line_d_2 A C D P Q Y lambda H HCol Hdenom Hpar) in *.
Ltac elimi_on_line_d P Q lambda A Y C D H :=
let Hdenom := HypOfType (C <> D) in
let Hpar := HypOfType (parallel A Y C D) in
test_col A P Q
ltac: (elimi_on_line_d_col P Q lambda A Y C D H Hdenom Hpar)
ltac: (elimi_on_line_d_not_col P Q lambda A Y C D H Hdenom Hpar).
on_parallel_d : elimination in length ratio
Ltac elimi_on_parallel_d_col_aux_2 R P Q lambda A Y C D H Hdenom Hpar HCol Hneq Hneq2 :=
let T1 := fresh in
(assert
(T1 := non_zero_denom_on_parallel_d_1_length_ratio A C D P Q R Y lambda H HCol);
let T2 := fresh in
(assert
(T2 :=
invariant_par_on_parallel_d_1_length_ratio A C D P Q R Y lambda H HCol Hneq Hpar);
let T3 := fresh in
(assert
(T3 :=
invariant_par_on_parallel_d_1_length_ratio_2 A C D P Q R Y lambda H HCol Hneq
Hneq2 Hpar);
rewrite
(elim_length_ratio_on_parallel_d_1 A C D P Q R Y lambda H HCol Hdenom) in *))).
There are two case-distinctions on point equality
Ltac elimi_on_parallel_d_col_aux R P Q lambda A Y C D H Hdenom Hpar HCol Hneq :=
test_equality_and_subst H A Y
ltac:(elimi_on_parallel_d_col_aux_2 R P Q lambda A Y C D H Hdenom Hpar HCol Hneq).
Ltac elimi_on_parallel_d_col R P Q lambda A Y C D H Hdenom Hpar HCol :=
test_equality_and_subst H R Y
ltac:(elimi_on_parallel_d_col_aux R P Q lambda A Y C D H Hdenom Hpar HCol).
Ltac elimi_on_parallel_d R P Q lambda A Y C D H :=
let Hdenom := HypOfType (C <> D) in
let Hpar := HypOfType (parallel A Y C D) in
let HCol := fresh in
(named_cases_col A R Y HCol;
[ elimi_on_parallel_d_col R P Q lambda A Y C D H Hdenom Hpar HCol
| let T1 := fresh in
(assert
(T1 := non_zero_denom_on_parallel_d_2_length_ratio A C D P Q R Y lambda H Hpar Hdenom HCol);
rewrite
(elim_length_ratio_on_parallel_d_2 A C D P Q R Y lambda H HCol Hdenom Hpar) in *) ]).
Ltac elimi_area_on_inter_line_parallel X4 X5 X1 X2 X3 Y X6 X7 H Hneq :=
assert (S4 X4 X2 X5 X3 <> 0);
[ exact (non_zero_denom_on_inter_line_parallel_area Y X1 X2 X3 X4 X5 H) | idtac ];
rewrite (elim_area_on_inter_line_parallel X4 X5 X1 X2 X3 Y X6 X7 H Hneq) in *.
Ltac elimi_on_foot_col_aux R P Q A Y C D H HCol HDiff :=
rewrite (elim_ratio_on_foot_a Y R P Q A C D H HCol) in * by assumption.
Ltac elimi_on_foot_col R P Q A Y C D H HCol :=
assert (Py C D C <> 0) by (apply (elim_ratio_on_foot_a_invariant C D);assumption);
test_equality_and_subst H A Y
ltac:(elimi_on_foot_col_aux R P Q A Y C D H HCol).
Ltac elimi_on_foot_notcol R P Q A Y C D H HCol :=
assert (S4 C P D Q <> 0) by (apply (elim_ratio_on_foot_b_invariant Y R P Q A C D H HCol);assumption);
rewrite (elim_ratio_on_foot_b Y R P Q A C D H HCol) in * by assumption.
Ltac elimi_on_foot R P Q A Y C D H := test_col A P Q
ltac: (elimi_on_foot_col R P Q A Y C D H)
ltac: (elimi_on_foot_notcol R P Q A Y C D H).
Ltac elimi_on_perp_d_col Y P Q r A C D H HCol :=
rewrite (elim_ratio_on_perp_d_a Y P Q A C D r H HCol) in *.
Ltac elimi_on_perp_d_notcol Y P Q r A C D H HCol := idtac.
Ltac elimi_on_perp_d P Q r A Y C D H :=
test_col A P Y
ltac: (elimi_on_perp_d_col Y P Q r A C D H)
ltac: (elimi_on_perp_d_notcol Y P Q r A C D H).
Ltac elimi_inter_parallel_parallel_par Y R P Q W U V A C D H HPar :=
rewrite ( elim_length_ratio_on_inter_parallel_parallel_2 A C D P Q R U V W Y H HPar) by auto.
Ltac elimi_inter_parallel_parallel_notpar Y R P Q W U V A C D H HPar :=
rewrite ( elim_length_ratio_on_inter_parallel_parallel_1 A C D P Q R U V W Y H HPar) by auto.
Ltac elimi_inter_parallel_parallel Y R P Q W U V A C D H :=
test_parallel A Y P Q
ltac: ( elimi_inter_parallel_parallel_par Y R P Q W U V A C D H)
ltac: ( elimi_inter_parallel_parallel_notpar Y R P Q W U V A C D H).
Ltac elimi Y :=
match goal with
| H:(on_line_d Y ?X1 ?X2 ?X3) |- context [(S ?X5 ?X6 Y)] =>
rewrite (elim_area_on_line_d X5 X6 X1 X2 Y X3 H) in *
| H:(inter_ll Y ?X1 ?X2 ?X3 ?X4) |- context [(S ?X5 ?X6 Y)] =>
assert (S4 X1 X3 X2 X4 <> 0);
[ exact (non_zero_denom_inter_ll_area Y X1 X2 X3 X4 H) | idtac ];
rewrite (elim_area_inter_ll X5 X6 X1 X2 X3 X4 Y H) in *
| H:(on_parallel_d Y ?X1 ?X2 ?X3 ?X4) |- context [(S ?X5 ?X6 Y)] =>
rewrite (elim_area_on_parallel_d X5 X6 X2 X3 X1 Y X4 H) in *
| H:(a_ratio Y ?O ?U ?V ?ro ?ru ?rv) |- context [(S ?A ?B Y)] =>
rewrite (elim_signed_area_a_ratio Y O U V A B ro ru rv H) in *
| H:(on_inter_line_parallel Y ?X1 ?X2 ?X3 ?X4 ?X5) |- context [(S ?X6 ?X7 Y)] =>
test_equality_and_subst H X1 Y ltac:(elimi_area_on_inter_line_parallel X4 X5 X1 X2 X3 Y X6 X7 H )
| H:(on_inter_parallel_parallel Y ?X1 ?X2 ?X3 ?X4 ?X5 ?X6) |- context [(S ?X7 ?X8 Y)] =>
let Hneq := fresh in
(named_cases_equality X1 Y Hneq;[rewrite <- Hneq in *;rewrite Hneq in H|
assert (S4 X2 X5 X3 X6 <> 0);
[ exact (non_zero_denom_on_inter_parallel_parallel_area Y X1 X2 X3 X4 X5 X6 H) | idtac ];
rewrite
(elim_area_on_inter_parallel_parallel X2 X3 X1 X5 X6 X4 Y X7 X8 H Hneq) in *])
| H:(on_foot Y ?X1 ?X2 ?X3) |- context [(S ?A ?B Y)] =>
let T:= fresh in assert (T:=elim_area_on_foot_invariant A B X1 X2 X3 Y H);
rewrite (elim_area_on_foot A B X1 X2 X3 Y H) in *
| H:(on_perp_d Y ?X1 ?X2 ?R) |- context [(S ?A ?B Y)] =>
rewrite (elim_area_on_perp_d A B X1 X2 Y R H) in *
| H:(on_line_d Y ?X1 ?X2 ?X3) |- context [(?X5 ** Y / ?X6 ** ?X7)] =>
elimi_on_line_d X1 X2 X3 X5 Y X6 X7 H
| H:(inter_ll Y ?X1 ?X2 ?X3 ?X4) |- context [(?X5 ** Y / ?X6 ** ?X7)] =>
elimi_inter_ll X1 X2 X3 X4 X5 Y X6 X7 H
| H:(on_parallel_d Y ?X1 ?X2 ?X3 ?X4) |- context [(?X5 ** Y / ?X6 ** ?X7)] =>
elimi_on_parallel_d X1 X2 X3 X4 X5 Y X6 X7 H
| H:(on_inter_line_parallel Y ?X1 ?X2 ?X3 ?X4 ?X8) |- context [(?X5 ** Y / ?X6 ** ?X7)] =>
fail 5 "case ratio on inter line parallel"
| H:(on_inter_parallel_parallel Y ?R ?P ?Q ?W ?U ?V) |- context [(?A ** Y / ?C ** ?D)] =>
elimi_inter_parallel_parallel Y R P Q W U V A C D H
| H:(on_foot Y ?R ?P ?Q) |- context [(?A ** Y / ?C ** ?D)] =>
elimi_on_foot R P Q A Y C D H
| H:(on_perp_d Y ?X1 ?X2 ?r) |- context [(?A ** Y / ?C ** ?D)] =>
elimi_on_perp_d X1 X2 r A Y C D H
| H:(on_line_d Y ?X1 ?X2 ?X3) |- context [Py Y ?A Y] =>
rewrite (elim_py_on_line_d_left_right A X1 X2 Y X3 H) in *
| H:(inter_ll Y ?X1 ?X2 ?X3 ?X4) |- context [Py Y ?A Y] =>
let T := fresh in
assert (T:= elim_py_inter_ll_left_right_invariant A X1 X2 X3 X4 Y H);
rewrite (elim_py_inter_ll_left_right A X1 X2 X3 X4 Y H) in *
| H:(on_parallel_d Y ?X1 ?X2 ?X3 ?X4) |- context [Py Y ?A Y] =>
rewrite (elim_py_on_parallel_d_left_right A X1 X2 X3 Y X4 H) in *
| H:(on_foot Y ?X1 ?X2 ?X3) |- context [Py Y ?A Y] =>
let T := fresh in
assert (T:= elim_py_on_foot_left_right_invariant A X1 X2 X3 Y H);
rewrite (elim_py_on_foot_left_right A X1 X2 X3 Y H) in *
| H:(on_perp_d Y ?U ?V ?r) |- context [Py Y ?A Y] =>
rewrite (elim_py_on_perp_d_left_right A U V Y r H) in *
| H:(a_ratio Y ?O ?U ?V ?ro ?ru ?rv) |- context [Py Y ?A Y] =>
rewrite (elim_py_a_ratio_left_right Y O U V A ro ru rv H) in *
| H:(on_line_d Y ?X1 ?X2 ?X3) |- context [Py ?A ?B Y] =>
rewrite (elim_py_on_line_d_right A B X1 X2 Y X3 H) in *
| H:(inter_ll Y ?X1 ?X2 ?X3 ?X4) |- context [Py ?A ?B Y] =>
let T:= fresh in
assert (T:=elim_py_inter_ll_right_invariant A B X1 X2 X3 X4 Y H);
rewrite (elim_py_inter_ll_right A B X1 X2 X3 X4 Y H) in *
| H:(on_parallel_d Y ?X1 ?X2 ?X3 ?X4) |- context [Py ?A ?B Y] =>
rewrite (elim_py_on_parallel_d_right A B X1 X2 X3 Y X4 H) in *
| H:(on_inter_line_parallel Y ?X1 ?X2 ?X3 ?X4 ?X8) |- context [Py ?A ?B Y] =>
fail 5 "case py right on inter line parallel"
| H:(on_inter_parallel_parallel Y ?X1 ?X2 ?X3 ?X4 ?X8 ?X9) |- context [Py ?A ?B Y] =>
fail 5 "case py right on inter parallel parallel"
| H:(on_foot Y ?X1 ?X2 ?X3) |- context [Py ?A ?B Y] =>
let T:= fresh in
assert (T:=elim_py_on_foot_right_invariant A B X1 X2 X3 Y H);
rewrite (elim_py_on_foot_right A B X1 X2 X3 Y H) in *
| H:(on_perp_d Y ?P ?Q ?r) |- context [Py ?A ?B Y] =>
rewrite (elim_py_on_perp_d_right A B P Q Y r H) in *
| H:(a_ratio Y ?O ?U ?V ?ro ?ru ?rv) |- context [Py ?A ?B Y] =>
rewrite (elim_py_a_ratio_right Y O U V A B ro ru rv H) in *
| H:(on_inter_line_perp Y ?X1 ?X2 ?X3 ?X4 ?X5) |- context [Py ?A ?B Y] =>
fail 5 "case py right on inter line perp"
| H:(on_line_d Y ?X1 ?X2 ?X3) |- context [Py ?A Y ?B] =>
rewrite (elim_py_on_line_d_middle A B X1 X2 Y X3 H) in *
| H:(inter_ll Y ?X1 ?X2 ?X3 ?X4) |- context [Py ?A Y ?B] =>
let T:= fresh in assert (T:= elim_py_inter_ll_middle_invariant A B X1 X2 X3 X4 Y H);
rewrite (elim_py_inter_ll_middle A B X1 X2 X3 X4 Y H) in *
| H:(on_parallel_d Y ?X1 ?X2 ?X3 ?X4) |- context [Py ?A Y ?B] =>
rewrite (elim_py_on_parallel_d_middle A B X1 X2 X3 Y X4 H) in *
| H:(on_inter_line_parallel Y ?X1 ?X2 ?X3 ?X4 ?X8) |- context [Py ?A Y ?B] =>
fail 5 "case py midlle on inter line parallel"
| H:(on_inter_parallel_parallel Y ?X1 ?X2 ?X3 ?X4 ?X8 ?X9) |- context [Py ?A Y ?B] =>
fail 5 "case py midlle on inter parallel parallel"
| H:(on_foot Y ?X1 ?X2 ?X3) |- context [Py ?A Y ?B] =>
let T:= fresh in assert (T:= elim_py_on_foot_middle_invariant A B X1 X2 X3 Y H);
rewrite (elim_py_on_foot_middle A B X1 X2 X3 Y H) in *
| H:(on_perp_d Y ?P ?Q ?r) |- context [Py ?A Y ?B] =>
rewrite (elim_py_on_perp_d_middle A B P Q Y r H) in *
| H:(a_ratio Y ?O ?U ?V ?ro ?ru ?rv) |- context [Py ?A Y ?B] =>
rewrite (elim_py_a_ratio_middle Y O U V A B ro ru rv H) in *
| H:(on_inter_line_perp Y ?X1 ?X2 ?X3 ?X4 ?X5) |- context [Py ?A Y ?B] =>
fail 5 "case py midlle on inter line perp"
end.
Ltac ClearConstructedPointDef Y :=
match goal with
| H:(on_line Y _ _) |- _ => fail 5 "Please report : should have been transformed into on_line_d before"
| H:(on_line_d Y _ _ _) |- _ => clear H
| H:(inter_ll Y _ _ _ _) |- _ => clear H
| H:(on_parallel Y _ _ _) |- _ => fail 5 "Please report : should have been transformed into on_parallel_d before"
| H:(on_parallel_d Y _ _ _ _) |- _ => clear H
| H:(on_inter_line_parallel Y _ _ _ _ _) |- _ => clear H
| H:(on_inter_parallel_parallel Y _ _ _ _ _ _) |- _ => clear H
| H:(on_foot Y _ _ _) |- _ => clear H
| H:(on_perp Y _ _ ) |- _ => fail 5 "Please report : should have been transformed into on_perp_d before"
| H:(on_perp_d Y _ _ _) |- _ => clear H
| H:(on_inter_line_perp Y _ _ _ _ _) |- _ => clear H
| H:(a_ratio Y _ _ _ _ _ _) |- _ => clear H
end.
Warning this definition suppose that we have no extra assumptions
A constructed point is defined only by its construction
Ltac ClearConstructedPointNDG Y :=
repeat
match goal with
| H:(parallel Y _ _ _) |- _ => clear H
| H:(parallel _ Y _ _) |- _ => clear H
| H:(parallel _ _ Y _) |- _ => clear H
| H:(parallel _ _ _ Y) |- _ => clear H
| H:(_ <> Y) |- _ => clear H
| H:(Y <> _) |- _ => clear H
end.
Ltac eliminate_aux Y :=
unify_signed_areas_and_put_on_the_right Y;
repeat elimi Y;
CleanDuplicatedHyps;
ClearConstructedPointDef Y.
Computes the point that is constructed with A
and so on until no point is constructed with A
Ltac is_used_to_construct A :=
match goal with
| H:(on_line ?X1 A _) |- _ =>
is_used_to_construct X1
| H:(on_line ?X1 _ A) |- _ =>
is_used_to_construct X1
| H:(on_line_d ?X1 A _ _) |- _ =>
is_used_to_construct X1
| H:(on_line_d ?X1 _ A _) |- _ =>
is_used_to_construct X1
| H:(inter_ll ?X1 A _ _ _) |- _ =>
is_used_to_construct X1
| H:(inter_ll ?X1 _ A _ _) |- _ =>
is_used_to_construct X1
| H:(inter_ll ?X1 _ _ A _) |- _ =>
is_used_to_construct X1
| H:(inter_ll ?X1 _ _ _ A) |- _ =>
is_used_to_construct X1
| H:(on_parallel ?X1 A _ _) |- _ =>
is_used_to_construct X1
| H:(on_parallel ?X1 _ A _) |- _ =>
is_used_to_construct X1
| H:(on_parallel ?X1 _ _ A) |- _ =>
is_used_to_construct X1
| H:(on_parallel_d ?X1 A _ _ _) |- _ =>
is_used_to_construct X1
| H:(on_parallel_d ?X1 _ A _ _) |- _ =>
is_used_to_construct X1
| H:(on_parallel_d ?X1 _ _ A _) |- _ =>
is_used_to_construct X1
| H:(on_inter_line_parallel ?X1 A _ _ _ _) |- _ =>
is_used_to_construct X1
| H:(on_inter_line_parallel ?X1 _ A _ _ _) |- _ =>
is_used_to_construct X1
| H:(on_inter_line_parallel ?X1 _ _ A _ _) |- _ =>
is_used_to_construct X1
| H:(on_inter_line_parallel ?X1 _ _ _ A _) |- _ =>
is_used_to_construct X1
| H:(on_inter_line_parallel ?X1 _ _ _ _ A) |- _ =>
is_used_to_construct X1
| H:(on_inter_parallel_parallel ?X1 A _ _ _ _ _) |- _ =>
is_used_to_construct X1
| H:(on_inter_parallel_parallel ?X1 _ A _ _ _ _) |- _ =>
is_used_to_construct X1
| H:(on_inter_parallel_parallel ?X1 _ _ A _ _ _) |- _ =>
is_used_to_construct X1
| H:(on_inter_parallel_parallel ?X1 _ _ _ A _ _) |- _ =>
is_used_to_construct X1
| H:(on_inter_parallel_parallel ?X1 _ _ _ _ A _) |- _ =>
is_used_to_construct X1
| H:(on_inter_parallel_parallel ?X1 _ _ _ _ _ A) |- _ =>
is_used_to_construct X1
| H:(on_foot ?X1 A _ _) |- _ =>
is_used_to_construct X1
| H:(on_foot ?X1 _ A _) |- _ =>
is_used_to_construct X1
| H:(on_foot ?X1 _ _ A) |- _ =>
is_used_to_construct X1
| H:(on_perp ?X1 A _ ) |- _ =>
is_used_to_construct X1
| H:(on_perp ?X1 _ A ) |- _ =>
is_used_to_construct X1
| H:(on_perp_d ?X1 A _ _ ) |- _ =>
is_used_to_construct X1
| H:(on_perp_d ?X1 _ A _ ) |- _ =>
is_used_to_construct X1
| H:(on_inter_line_perp ?X1 A _ _ _ _) |- _ =>
is_used_to_construct X1
| H:(on_inter_line_perp ?X1 _ A _ _ _) |- _ =>
is_used_to_construct X1
| H:(on_inter_line_perp ?X1 _ _ A _ _) |- _ =>
is_used_to_construct X1
| H:(on_inter_line_perp ?X1 _ _ _ A _) |- _ =>
is_used_to_construct X1
| H:(on_inter_line_perp ?X1 _ _ _ _ A) |- _ =>
is_used_to_construct X1
| H:(a_ratio ?Y A _ _ _ _ _) |- _ =>
is_used_to_construct Y
| H:(a_ratio ?Y _ A _ _ _ _) |- _ =>
is_used_to_construct Y
| H:(a_ratio ?Y _ _ A _ _ _) |- _ =>
is_used_to_construct Y
| H:(a_ratio ?Y _ _ _ A _ _) |- _ =>
is_used_to_construct Y
| H:(a_ratio ?Y _ _ _ _ A _) |- _ =>
is_used_to_construct Y
| H:(a_ratio ?Y _ _ _ _ _ A) |- _ =>
is_used_to_construct Y
| _ => A
end.
Ltac check_proper_elimination A := match goal with
H:_ |- context [A] => fail 2 "Elimination failed, please report."
end || idtac.
Ltac eliminate A := idtac " elimination of point :" A;eliminate_aux A;
unfold S4, Py4 in *;
basic_simpl;
check_proper_elimination A; try (clear A); idtac " we need to show that:";print_goal.
Ltac Remove_last A :=
eliminate ltac:(is_used_to_construct A).
Ltac eliminate_All :=
repeat
match goal with
| H:(on_line ?X1 _ _) |- _ =>
Remove_last X1
| H:(on_line_d ?X1 _ _ _) |- _ =>
Remove_last X1
| H:(inter_ll ?X1 _ _ _ _) |- _ =>
Remove_last X1
| H:(on_parallel ?X1 _ _ _) |- _ =>
Remove_last X1
| H:(on_parallel_d ?X1 _ _ _ _) |- _ =>
Remove_last X1
| H:(on_inter_line_parallel ?X1 _ _ _ _ _) |- _ =>
Remove_last X1
| H:(on_inter_parallel_parallel ?X1 _ _ _ _ _ _) |- _ =>
Remove_last X1
| H:(on_foot ?X1 _ _ _) |- _ =>
Remove_last X1
| H:(on_perp ?X1 _ _ ) |- _ =>
Remove_last X1
| H:(on_perp_d ?X1 _ _ _) |- _ =>
Remove_last X1
| H:(on_inter_line_perp ?X1 _ _ _ _ _) |- _ =>
Remove_last X1
| H:(a_ratio ?X1 _ _ _ _ _ _) |- _ =>
Remove_last X1
end.