(* PR-007 (dalil al-imkan, step 2): if an existent is necessary in itself, its
   non-existence is not possible.

   Rests on:
   - PR-006, reused for its definitions of "necessary in itself" and
     "possible in itself";
   - meaning postulate MP-007, stated below as an explicit condition.
   No axiom is used.  Nothing is assumed to exist.  No notion of time
   appears.

   Possibility is modelled with worlds (ways things could be): "the
   non-existence of x is possible" means some world lacks x; "x exists" means
   x exists in the actual world. *)

Require PR006.Division.

Section Step2.

(* Primitive vocabulary.  Nothing is assumed about any of these. *)
Variable Thing : Type.
Variable World : Type.
Variable actual : World.
Variable ExistsIn : World -> Thing -> Prop.
Variable EssenceIncludesExistence : Thing -> Prop.

Definition Exists (x : Thing) : Prop := ExistsIn actual x.

(* Reused from PR-006. *)
Definition NecessaryInItself : Thing -> Prop :=
  Division.NecessaryInItself Thing Exists EssenceIncludesExistence.
Definition PossibleInItself : Thing -> Prop :=
  Division.PossibleInItself Thing Exists EssenceIncludesExistence.

(* The non-existence of x is possible: some world lacks x. *)
Definition NonExistencePossible (x : Thing) : Prop := exists w, ~ ExistsIn w x.

(* MP-007: what has existence from its essence exists in every world.  What
   it is guarantees that it is, wherever it is considered. *)
Definition MP007_EssentialExistenceCannotFail : Prop :=
  forall x, EssenceIncludesExistence x -> forall w, ExistsIn w x.

(* Step 2. *)
Theorem necessary_cannot_fail :
  MP007_EssentialExistenceCannotFail ->
  forall x, NecessaryInItself x -> ~ NonExistencePossible x.
Proof.
  intros M7 x [_ He] [w Hw]. exact (Hw (M7 x He w)).
Qed.

End Step2.

(* ------------------------------------------------------------------ *)
(* Checks.  Illustrations of logical possibility only; no claim about what
   exists.  Worlds are bool; the actual world is true. *)

(* 1. Countermodel without MP-007: a thing whose existence is from its
      essence, existing in the actual world but not in another.  It is
      necessary in itself, yet its non-existence is possible.  So MP-007 is
      needed. *)
Example without_MP007_necessary_could_fail :
  let EI := fun (w : bool) (_ : unit) => w = true in
  let Ess := fun (_ : unit) => True in
  NecessaryInItself unit bool true EI Ess tt /\ NonExistencePossible unit bool EI tt.
Proof.
  simpl. split.
  - split; [reflexivity | exact I].
  - exists false. discriminate.
Qed.

(* 2. Non-vacuity: MP-007 holds with one necessary thing, existing in every
      world, and one possible thing, which some world lacks. *)
Example mp007_allows_both :
  let EI := fun (w : bool) (x : bool) => x = true \/ w = true in
  let Ess := fun (x : bool) => x = true in
  MP007_EssentialExistenceCannotFail bool bool EI Ess /\
  NecessaryInItself bool bool true EI Ess true /\
  PossibleInItself bool bool true EI Ess false /\
  NonExistencePossible bool bool EI false.
Proof.
  unfold MP007_EssentialExistenceCannotFail. simpl.
  split; [| split; [| split]].
  - intros x Hx w. left. exact Hx.
  - split; [left; reflexivity | reflexivity].
  - split; [right; reflexivity | discriminate].
  - exists false. intros [H | H]; discriminate.
Qed.

(* 3. Necessary through another (wajib bi-ghayrihi): MP-007 does not force a
      possible thing ever to fail.  A thing possible in itself may exist in
      every world, necessitated by its cause, as in Ibn Sina's eternal
      world. *)
Example possible_may_never_fail :
  let EI := fun (_ : bool) (_ : bool) => True in
  let Ess := fun (x : bool) => x = true in
  MP007_EssentialExistenceCannotFail bool bool EI Ess /\
  PossibleInItself bool bool true EI Ess false /\
  ~ NonExistencePossible bool bool EI false.
Proof.
  unfold MP007_EssentialExistenceCannotFail. simpl.
  split; [| split].
  - intros. exact I.
  - split; [exact I | discriminate].
  - intros [w Hw]. exact (Hw I).
Qed.

Print Assumptions necessary_cannot_fail.
Print Assumptions without_MP007_necessary_could_fail.
Print Assumptions mp007_allows_both.
Print Assumptions possible_may_never_fail.