(* PR-006 (dalil al-imkan, step 1): every existent is either necessary in
   itself (wajib al-wujud bi-dhatihi) or possible in itself (mumkin al-wujud
   bi-dhatihi), but not both.

   Definitions follow Ibn Sina: an existent is necessary in itself when its
   existence is from its essence, and possible in itself when it is not.
   Whether the possible needs a cause (its iḥtiyaj) is NOT part of the
   definition; it is a later step (step 3), to be proved.

   Logical principle used: excluded middle (classic), for exhaustiveness
   only.  Nothing else is assumed.  Nothing is assumed to exist.  No notion of
   time appears. *)

From Stdlib Require Import Classical.

Section Div.

(* Primitive vocabulary.  Nothing is assumed about any of these. *)
Variable Thing : Type.
Variable Exists : Thing -> Prop.                    (* x exists *)
Variable EssenceIncludesExistence : Thing -> Prop.  (* x's existence is from its essence *)

(* Conditional definitions. *)
Definition NecessaryInItself (x : Thing) : Prop :=
  Exists x /\ EssenceIncludesExistence x.
Definition PossibleInItself (x : Thing) : Prop :=
  Exists x /\ ~ EssenceIncludesExistence x.

(* Step 1, exhaustive: every existent is necessary or possible in itself. *)
Theorem division_exhaustive : forall x,
  Exists x -> NecessaryInItself x \/ PossibleInItself x.
Proof.
  intros x Hx.
  destruct (classic (EssenceIncludesExistence x)) as [He | Hne].
  - left. split; assumption.
  - right. split; assumption.
Qed.

(* Step 1, exclusive: no existent is both. *)
Theorem division_exclusive : forall x,
  ~ (NecessaryInItself x /\ PossibleInItself x).
Proof.
  intros x [[_ He] [_ Hne]]. exact (Hne He).
Qed.

(* Step 1, as stated: every existent is one or the other, but not both. *)
Theorem division : forall x,
  Exists x ->
  (NecessaryInItself x \/ PossibleInItself x) /\
  ~ (NecessaryInItself x /\ PossibleInItself x).
Proof.
  intros x Hx. split.
  - exact (division_exhaustive x Hx).
  - exact (division_exclusive x).
Qed.

End Div.

(* ------------------------------------------------------------------ *)
(* Checks: both sides of the division really occur, so neither definition
   is empty.  Illustrations of logical possibility only. *)

(* A world with one necessary and one possible existent. *)
Example both_kinds_occur :
  let E := fun (_ : bool) => True in
  let Ess := fun (x : bool) => x = true in
  NecessaryInItself bool E Ess true /\ PossibleInItself bool E Ess false.
Proof.
  simpl. split.
  - split; [exact I | reflexivity].
  - split; [exact I | discriminate].
Qed.

Print Assumptions division_exhaustive.
Print Assumptions division_exclusive.
Print Assumptions division.
Print Assumptions both_kinds_occur.