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, I≠A → Midpoint I A B → I ≠ B ∧ A ≠ B.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal ∀ A B I, I≠B → Midpoint I A B → I ≠ A ∧ A ≠ B.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal ∀ A B I, A≠I → Midpoint I A B → I ≠ B ∧ A ≠ B.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal ∀ A B I, B≠I → Midpoint I A B → I ≠ A ∧ A ≠ B.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal ∀ A B I, A≠B → Midpoint I A B → A ≠ I ∧ I ≠ B.
Proof.
intros.
assert_diffs.
split;auto.
Qed.

Goal ∀ A B:Tpoint, A≠B → B≠A → 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 → A≠B ∧ C≠D.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal ∀ A B C D, A≠B → Perp A B C D → A≠B ∧ C≠D.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal ∀ A B C D, A≠B → Perp B A C D → A≠B ∧ C≠D.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal ∀ A B C D, A≠B → Perp B A D C → A≠B ∧ C≠D.
Proof.
intros.
assert_diffs.
split;intuition.
Qed.

Goal ∀ A B C D, A≠B → C≠D → Perp B A D C → A≠B ∧ C≠D.
Proof.
intros.
assert_diffs.
split;intuition.
Qed.

Goal ∀ A B C D, D≠C → Perp B A D C → A≠B ∧ C≠D.
Proof.
intros.
assert_diffs.
split;intuition.
Qed.

Goal ∀ X A B C D, Perp_at X A B C D → A≠B ∧ C≠D.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal ∀ A B C D, Par A B C D → A≠B ∧ C≠D.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal ∀ A B C D, Par_strict A B C D → A≠B ∧ C≠D.
Proof.
intros.
assert_diffs.
split;assumption.
Qed.

Goal ∀ A B C, Out A B C → B≠A ∧ C≠A.
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 →
  A≠D.
Proof.
intros.
assert_diffs.
intuition.
Qed.

Goal ∀ A B C D I,
  Midpoint I A B → Par A B C D → I≠A.
Proof.
intros.
assert_diffs.
assumption.
Qed.

Goal ∀ A B C D I,
  Midpoint I A B → Par A I C D → B≠A.
Proof.
intros.
assert_diffs.
intuition.
Qed.

Goal ∀ A B C D,
 Cong A B C D → C≠D → A≠B.
Proof.
intros.
assert_diffs.
intuition.
Qed.

Goal ∀ A B C D,
 Cong A B C D → D≠C → A≠B.
Proof.
intros.
assert_diffs.
intuition.
Qed.

Goal ∀ A B C D,
 Cong A B C D → A≠B → C≠D.
Proof.
intros.
assert_diffs.
intuition.
Qed.

Goal ∀ A B C D,
 Cong A B C D → B≠A → C≠D.
Proof.
intros.
assert_diffs.
intuition.
Qed.

Goal ∀ A B C D E,
 ¬ Col A B C →
 ¬ Col B D E → A≠B →
  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, (A≠B → B≠C → A≠C → 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.