GeoCoq in the browser

Require Export GeoCoq.Tarski_dev.Annexes.midpoint_theorems.

Section Logic.

Lemma example_0 : forall A B C : Prop, (A -> B) -> (B -> C) -> (A -> C).
Proof.
(*
intros A B C AB BC HA.
apply BC.
apply AB.
assumption.
*)
Admitted.

Lemma example_1 : forall A B C : Prop, (A /\ B -> C) <-> (A -> B -> C).
Proof.
(*
intros A B C.
split.
- intros HABC HA HB.
  apply HABC.
  split.
  + assumption.
  + assumption.
- intros HABC HAB.
  destruct HAB as [HA HB].
  apply HABC; assumption.
*)
Admitted.

Lemma example_2 : forall A B : Prop, A \/ B -> B \/ A.
Proof.
(*
intros A B HAB.
destruct HAB as [HA|HB].
- right; assumption.
- left; assumption.
*)
Admitted.

End Logic.

Section Varignon.

Context `{TE:Tarski_euclidean}.

Check cong3_conga.

Definition isosceles A B C :=
 Cong A B B C.
 
Lemma isosceles_conga : forall A B C,
  A<>C -> A<>B ->
  isosceles A B C ->
  CongA C A B A C B.
Proof.
Admitted.

(** This is the usual proof presented in classroom based on
the midpoint theorem but this proof suffers from two problems.
It needs the fact that IJK are not collinear,
which is not always the case when the quadrilateral is not convex.
It also needs the fact that A is different from C, and B is different from D.
The original proof by Varignon suffer from the same problem.
The original proof can be found page 138, Corollary IV:
http://polib.univ-lille3.fr/documents/B590092101_000000011.489_IMT.pdf
*)

Lemma varignon :
 forall A B C D I J K L,
  A<>C -> B<>D -> ~ Col I J K ->
  Midpoint I A B ->
  Midpoint J B C ->
  Midpoint K C D ->
  Midpoint L A D ->
  Parallelogram I J K L.
Proof.
intros.
assert_diffs.
assert (Par I L B D) (** Applying the midpoint theorem in the triangle BDA. *)
  by perm_apply (triangle_mid_par B D A L I).
assert (Par J K B D) (** Applying the midpoint theorem in the triangle BDC. *)
  by perm_apply (triangle_mid_par B D C K J).
assert (Par I L J K) (** Transitivity of parallelism *)
  by (apply par_trans with B D;finish).
assert (Par I J A C) (** Applying the midpoint theorem in the triangle ACB. *)
  by perm_apply (triangle_mid_par A C B J I).
assert (Par L K A C) (** Applying the midpoint theorem in the triangle ACD. *)
  by perm_apply (triangle_mid_par A C D K L).
assert (Par I J K L) (** Transitivity of parallelism *)
  by (apply par_trans with A C;finish).
apply par_2_plg;finish. (** If in the opposite side of quadrilatral are parallel and two opposite side are distinct
                            then it is a parallelogram. *)
Qed.

End Varignon.