Library GeoCoq.Tactics.UnitTests.unit_tests

Require Import GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec.

Section UnitTests.

Context `{TE:Tarski_2D_euclidean}.

Goal A B I, A B Midpoint I A B I A I B.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal A B I, B A Midpoint I A B I A I B.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal A B I, IA Midpoint I A B I B A B.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal A B I, IB Midpoint I A B I A A B.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal A B I, AI Midpoint I A B I B A B.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal A B I, BI Midpoint I A B I A A B.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal A B I, AB Midpoint I A B A I I B.
Proof.
intros.
assert_diffs.
split;auto.
Qed.

Goal A B:Tpoint, AB BA True.
Proof.
intros.
first [not_exist_hyp_comm A B | clear H].
first [not_exist_hyp_comm A B | clear H0].
not_exist_hyp_comm A B.
auto.
Qed.

Goal A B C Q,
 B A Col A B C Midpoint Q A C
 A C B C Midpoint A B C
 Q C.
Proof.
intros.
assert_diffs.
assumption.
Qed.

Goal A B C D, Perp A B C D AB CD.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal A B C D, AB Perp A B C D AB CD.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal A B C D, AB Perp B A C D AB CD.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal A B C D, AB Perp B A D C AB CD.
Proof.
intros.
assert_diffs.
split;intuition.
Qed.

Goal A B C D, AB CD Perp B A D C AB CD.
Proof.
intros.
assert_diffs.
split;intuition.
Qed.

Goal A B C D, DC Perp B A D C AB CD.
Proof.
intros.
assert_diffs.
split;intuition.
Qed.

Goal X A B C D, Perp_at X A B C D AB CD.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal A B C D, Par A B C D AB CD.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal A B C D, Par_strict A B C D AB CD.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal A B C, Out A B C BA CA.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal A B C, Out A B C Col B A C.
Proof.
intros.
assert_cols.
Col.
Qed.

Goal A B C D, ¬ Col A B C ¬ Col A B D
  AD.
Proof.
intros.
assert_diffs.
intuition.
Qed.

Goal A B C D I,
  Midpoint I A B Par A B C D IA.
Proof.
intros.
assert_diffs.
assumption.
Qed.

Goal A B C D I,
  Midpoint I A B Par A I C D BA.
Proof.
intros.
assert_diffs.
intuition.
Qed.

Goal A B C D,
 Cong A B C D CD AB.
Proof.
intros.
assert_diffs.
intuition.
Qed.

Goal A B C D,
 Cong A B C D DC AB.
Proof.
intros.
assert_diffs.
intuition.
Qed.

Goal A B C D,
 Cong A B C D AB CD.
Proof.
intros.
assert_diffs.
intuition.
Qed.

Goal A B C D,
 Cong A B C D BA CD.
Proof.
intros.
assert_diffs.
intuition.
Qed.

Goal A B C D E,
 ¬ Col A B C
 ¬ Col B D E AB
  Col A B D Col A B E Col A B C.
Proof.
intros.
search_contradiction.
Qed.
Goal A B C D,
 Par_strict A B C D
 ¬ Col A B C.
Proof.
intros.
assert_diffs.
Col.
Qed.

Goal A B C, (AB BC AC Col A B C) Col A B C.
Proof.
intros.
assert_diffs_by_cases.
intuition.
Qed.
Goal A B C D, Parallelogram A B C D Cong A B C D.
Proof.
intros.
assert_congs_perm.
finish.
Qed.

Goal A B C, Midpoint A B C Cong A B C A.
Proof.
intros.
assert_congs_perm.
finish.
Qed.

Goal A B C, Bet A B C A B A C.
Proof.
intros.
assert_diffs.
assumption.
Qed.

Goal A B C, Bet A B C B A A C.
Proof.
intros.
assert_diffs.
assumption.
Qed.

Goal A B C, Bet A B C B C A C.
Proof.
intros.
assert_diffs.
assumption.
Qed.

Goal A B C, Bet A B C C B A C.
Proof.
intros.
assert_diffs.
assumption.
Qed.

Goal A B C, ¬ Bet A B C A B B C.
Proof.
intros.
assert_diffs.
split; assumption.
Qed.

Goal A B C D, TS A B C D A B A C A D B C B D C D.
Proof.
intros.
assert_diffs.
repeat split; assumption.
Qed.

Goal A B C D, OS A B C D A B A C A D B C B D.
Proof.
intros.
assert_diffs.
repeat split; assumption.
Qed.

Goal A B C D, A B Le A B C D C D.
Proof.
intros.
assert_diffs.
assumption.
Qed.

Goal A B C D, Lt A B C D C D.
Proof.
intros.
assert_diffs.
assumption.
Qed.

Goal A B C, Bet A B C Bet B A C A = B.
Proof.
intros.
treat_equalities.
trivial.
Qed.

Goal A B C, Bet A B C Bet A C B B = C.
Proof.
intros.
treat_equalities.
trivial.
Qed.

Goal A B C, Bet A B C Bet C A B A = B.
Proof.
intros.
treat_equalities.
trivial.
Qed.

Goal A B C, Bet A B C Bet B C A B = C.
Proof.
intros.
treat_equalities.
trivial.
Qed.

End UnitTests.