Require Import GeoCoq.Axioms.continuity_axioms.
Require Import GeoCoq.Tarski_dev.Definitions.

Require Import Logic.ChoiceFacts.

Section first_order.

Context `{Tn:Tarski_neutral_dimensionless}.

(** Dedekind's axiom of continuity implies the Tarski's axiom schema of continuity *)

Lemma dedekind__fod : dedekind_s_axiom -> first_order_dedekind.
Proof.
(* Goal: forall _ : @dedekind_s_axiom Tn, @first_order_dedekind Tn *)
  intros dedekind Alpha Beta HAlpha HBeta HA.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => forall (X Y : @Tpoint Tn) (_ : Alpha X) (_ : Beta Y), @Bet Tn X B Y) *)
  apply dedekind, HA.
Qed.

(** This is a type whose members describe first-order formulas *)

Inductive tFOF :=
  eq_fof1 : Tpoint -> Tpoint -> tFOF
| bet_fof1 : Tpoint -> Tpoint -> Tpoint -> tFOF
| cong_fof1 : Tpoint -> Tpoint -> Tpoint -> Tpoint -> tFOF
| not_fof1 : tFOF -> tFOF
| and_fof1 : tFOF -> tFOF -> tFOF
| or_fof1 : tFOF -> tFOF -> tFOF
| implies_fof1 : tFOF -> tFOF -> tFOF
| forall_fof1 : (Tpoint -> tFOF) -> tFOF
| exists_fof1 : (Tpoint -> tFOF) -> tFOF.

(** This function interperts tFOF elements as Prop *)

Fixpoint fof1_prop (F:tFOF) := match F with
  eq_fof1 A B => A = B
| bet_fof1 A B C => Bet A B C
| cong_fof1 A B C D => Cong A B C D
| not_fof1 F1 => ~ fof1_prop F1
| and_fof1 F1 F2 => fof1_prop F1 /\ fof1_prop F2
| or_fof1 F1 F2 => fof1_prop F1 \/ fof1_prop F2
| implies_fof1 F1 F2 => fof1_prop F1 -> fof1_prop F2
| forall_fof1 P => forall A, fof1_prop (P A)
| exists_fof1 P => exists A, fof1_prop (P A) end.

(** Every first-order formula is equivalent to a Prop built with fof1_prop *)

Lemma fof__fof1 : FunctionalChoice_on Tpoint tFOF ->
  forall F, FOF F -> exists F1,  F <-> fof1_prop F1 .
Proof.
(* Goal: forall (_ : FunctionalChoice_on (@Tpoint Tn) tFOF) (F : Prop) (_ : @FOF Tn F), @ex tFOF (fun F1 : tFOF => iff F (fof1_prop F1)) *)
  intros choice F HFOF.
(* Goal: @ex tFOF (fun F1 : tFOF => iff F (fof1_prop F1)) *)
  induction HFOF.
  - exists (eq_fof1 A B); intuition.
  - exists (bet_fof1 A B C); intuition.
  - exists (cong_fof1 A B C D); intuition.
  - destruct IHHFOF as [F1]. exists (not_fof1 F1). simpl; intuition.
  - destruct IHHFOF1 as [F1]; destruct IHHFOF2 as [F2]; exists (and_fof1 F1 F2); simpl; intuition.
  - destruct IHHFOF1 as [F1]; destruct IHHFOF2 as [F2]; exists (or_fof1 F1 F2); simpl; intuition.
  - destruct IHHFOF1 as [F1]; destruct IHHFOF2 as [F2]; exists (implies_fof1 F1 F2); simpl; intuition.
  - destruct (choice (fun A => (fun F1 => P A <-> fof1_prop F1)) H0) as [f].
(* Goal: @ex tFOF (fun F1 : tFOF => iff (forall A : @Tpoint Tn, P A) (fof1_prop F1)) *)
    exists (forall_fof1 f); simpl.
(* Goal: iff (forall A : @Tpoint Tn, P A) (forall A : @Tpoint Tn, fof1_prop (f A)) *)
    split; intros HH A; apply H1, HH.
  - destruct (choice (fun A => (fun F1 => P A <-> fof1_prop F1)) H0) as [f].
(* Goal: @ex tFOF (fun F1 : tFOF => iff (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => P A)) (fof1_prop F1)) *)
    exists (exists_fof1 f); simpl.
(* Goal: iff (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => P A)) (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => fof1_prop (f A))) *)
    split; intros [A HA]; exists A; apply H1, HA.
Qed.

(** Every Prop built with fof1_prop is a first-order formula *)

Lemma fof1__fof : forall F1, FOF (fof1_prop F1).
Proof.
(* Goal: forall F1 : tFOF, @FOF Tn (fof1_prop F1) *)
  induction F1; constructor; assumption.
Qed.

End first_order.