(* Dalil al-imkan, proof (b): the short route through OP-001.

   Since something exists (SP-001), a Necessary Existent exists:
   - if the existent is necessary in itself, the conclusion holds at once;
   - if it is possible in itself, it has a giver (step 3, MP-008); by OP-001
     only what has existence of itself gives existence, so the giver exists
     with nothing giving it existence; by MP-008 its existence is then from
     its own nature, so it is necessary in itself.

   This route bypasses the aggregate (steps 5 to 9).  It shares its decisive
   premise, OP-001, with dalil al-kalima; proof (a) does not, which is why
   (a) is the primary proof and (b) the second.

   Rests on: PR-006 (step 1), PR-008 (step 3, MP-008), PR-004 (definitions,
   OP-001), SP-001, and excluded middle.  No notion of time appears. *)

Require PR004.NoRegressOfGiving PR006.Division PR008.PossibleRequiresMurajjih.

Section Short.

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

(* Reused definitions. *)
Definition NecessaryInItself := Division.NecessaryInItself Thing Exists EssenceIncludesExistence.
Definition MP008 := PossibleRequiresMurajjih.MP008_NoPreponderanceWithoutPreponderator
                      Thing Exists EssenceIncludesExistence Gives.
Definition OP001 := NoRegressOfGiving.OP001_OnlySelfExistentGives Thing Gives Exists.
Definition SP001 : Prop := exists x, Exists x.

(* The giver of anything is necessary in itself (OP-001 and MP-008). *)
Lemma giver_is_necessary_in_itself :
  MP008 -> OP001 -> forall y x, Gives y x -> NecessaryInItself y.
Proof.
  intros M8 OP y x Hg. destruct (OP x y Hg) as [Hex Hn].
  split; [exact Hex | exact (M8 y Hex Hn)].
Qed.

(* Proof (b) of step 12: since something exists, a Necessary Existent
   exists. *)
Theorem necessary_existent_exists_short :
  MP008 -> OP001 -> SP001 -> exists n, NecessaryInItself n.
Proof.
  intros M8 OP [x Hx].
  destruct (Division.division_exhaustive Thing Exists EssenceIncludesExistence x Hx) as [Hn | Hp].
  - exists x. exact Hn.
  - destruct (PossibleRequiresMurajjih.possible_requires_murajjih
                Thing Exists EssenceIncludesExistence Gives M8 x Hp) as [y Hg].
    exists y. exact (giver_is_necessary_in_itself M8 OP y x Hg).
Qed.

End Short.

(* ------------------------------------------------------------------ *)
(* Checks.  Illustrations of logical possibility only. *)

(* 1. Consistency: MP-008, OP-001 and SP-001 hold together; a necessary
      thing (true) gives existence to a possible one (false). *)
Example premises_hold_together :
  let E := fun (_ : bool) => True in
  let Ess := fun (x : bool) => x = true in
  let G := fun (y x : bool) => y = true /\ x = false in
  MP008 bool E Ess G /\ OP001 bool E G /\ SP001 bool E.
Proof.
  intros E Ess G.
  unfold MP008, OP001, SP001, PossibleRequiresMurajjih.MP008_NoPreponderanceWithoutPreponderator,
         NoRegressOfGiving.OP001_OnlySelfExistentGives, NoRegressOfGiving.OfItself,
         NoRegressOfGiving.ThroughAnother, E, Ess, G.
  split; [| split].
  - intros [] _ Hn; [reflexivity |]. exfalso. apply Hn. exists true. split; reflexivity.
  - intros x y [Hy _]. subst y. split; [exact I |]. intros [z [_ H]]. discriminate.
  - exists true. exact I.
Qed.

(* 2. Countermodel without OP-001: numbers 0, 1, 2, ..., each possible and
      each given existence by the next.  MP-008 and SP-001 hold, but nothing
      is necessary.  So the short route needs OP-001. *)
Example without_OP001_no_necessary :
  let E := fun (_ : nat) => True in
  let Ess := fun (_ : nat) => False in
  let G := fun (y x : nat) => y = S x in
  MP008 nat E Ess G /\ SP001 nat E /\ ~ (exists n, NecessaryInItself nat E Ess n).
Proof.
  intros E Ess G.
  unfold MP008, SP001, NecessaryInItself, PossibleRequiresMurajjih.MP008_NoPreponderanceWithoutPreponderator,
         NoRegressOfGiving.ThroughAnother, Division.NecessaryInItself, E, Ess, G.
  split; [| split].
  - intros x _ Hn. exfalso. apply Hn. exists (S x). reflexivity.
  - exists 0. exact I.
  - intros [n [_ H]]. exact H.
Qed.

Print Assumptions giver_is_necessary_in_itself.
Print Assumptions necessary_existent_exists_short.
Print Assumptions premises_hold_together.
Print Assumptions without_OP001_no_necessary.