(* Dalil al-imkan, step 12 (the conclusion): since something exists, a
   Necessary Existent exists.  Ibn Sina's starting point (al-Isharat,
   namat 4): "there is no doubt that there is existence".  Take any existent:
   if it is necessary, the conclusion holds at once; if it is possible, the
   aggregate argument (steps 5 to 11) shows a Necessary Existent.

   Proof (a), the Avicennan route through the aggregate.

   Rests on:
   - PR-002 and PR-003 (with MP-001, MP-002, MP-003);
   - PR-006 (step 1, the division);
   - PR-008 (step 3, with MP-008);
   - PR-009 (steps 5 and 6, with MP-009, MP-010);
   - PR-010 (steps 7 to 11, with MP-011, MP-012);
   - self-evident premise SP-001 (something exists);
   - excluded middle.
   All postulates enter as explicit conditions of the theorem.  No notion of
   time appears. *)

From Stdlib Require Import Classical.
Require PR002.NoSelfCreation PR003.NoCircularCreation PR004.NoRegressOfGiving
        PR006.Division PR008.PossibleRequiresMurajjih PR009.AggregateIsPossible
        PR010.CauseOutsideIsNecessary.

Section Conclusion.

(* 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.
Variable Through : Thing -> Thing -> Prop.
Variable MemberOf : Thing -> Thing -> Prop.

(* Reused definitions. *)
Definition NecessaryInItself := Division.NecessaryInItself Thing Exists EssenceIncludesExistence.
Definition PossibleInItself := Division.PossibleInItself Thing Exists EssenceIncludesExistence.
Definition MP001 := NoSelfCreation.MP001_Giver Thing Gives Through.
Definition MP002 := NoSelfCreation.MP002_Receiver Thing Gives Through.
Definition MP003 := NoCircularCreation.MP003_Inherited Thing Through.
Definition MP008 := PossibleRequiresMurajjih.MP008_NoPreponderanceWithoutPreponderator
                      Thing Exists EssenceIncludesExistence Gives.
Definition MP009 := AggregateIsPossible.MP009_AggregateExists
                      Thing Exists EssenceIncludesExistence MemberOf.
Definition MP010 := AggregateIsPossible.MP010_NoNecessityFromPossibles
                      Thing EssenceIncludesExistence MemberOf.
Definition MP011 := CauseOutsideIsNecessary.MP011_WholeToMembers Thing Gives MemberOf.
Definition MP012 := CauseOutsideIsNecessary.MP012_GiverExists Thing Exists Gives.

(* SP-001 (self-evident): something exists. *)
Definition SP001_SomethingExists : Prop := exists x, Exists x.

(* The possible case: if some possible thing exists, a Necessary Existent
   exists.  Moreover, if the aggregate of possibles has a member, a
   Necessary Existent outside it gives it existence. *)
Lemma necessary_existent_from_a_possible :
  MP001 -> MP002 -> MP003 -> MP008 -> MP009 -> MP010 -> MP011 -> MP012 ->
  (exists p, PossibleInItself p) ->
  exists n, NecessaryInItself n.
Proof.
  intros M1 M2 M3 M8 M9 M10 M11 M12 [p Hp].
  destruct (M9 (ex_intro _ p Hp)) as [A [HA HexA]].
  destruct (classic (exists q, q <> A /\ PossibleInItself q)) as [Hq | Hnq].
  - (* the aggregate has a member: steps 6 to 11 *)
    destruct (CauseOutsideIsNecessary.aggregate_has_necessary_cause
                Thing Exists EssenceIncludesExistence Gives Through MemberOf
                M1 M2 M3 M8 M10 M11 M12 A HA HexA Hq) as [c [_ [Hc _]]].
    exists c. exact Hc.
  - (* the only possible thing is the aggregate itself: by step 3 it has a
       giver c; c is not possible (it is not the aggregate, by PR-002, and no
       other possible exists), and c exists (MP-012), so c is necessary *)
    assert (HpA : PossibleInItself A).
    { destruct (classic (p = A)) as [Heq | Hne].
      - subst p. exact Hp.
      - exfalso. apply Hnq. exists p. split; assumption. }
    destruct (PossibleRequiresMurajjih.possible_requires_murajjih
                Thing Exists EssenceIncludesExistence Gives M8 A HpA) as [c Hg].
    exists c.
    destruct (Division.division_exhaustive Thing Exists EssenceIncludesExistence c (M12 c A Hg))
      as [Hn | Hpc]; [exact Hn |].
    exfalso. destruct (classic (c = A)) as [Heq | Hne].
    + subst c. exact (NoSelfCreation.no_self_creation Thing Gives Through M1 M2 A Hg).
    + apply Hnq. exists c. split; assumption.
Qed.

(* Step 12: since something exists, a Necessary Existent exists.  Ibn Sina's
   case split: the existent is necessary (done) or possible (the lemma). *)
Theorem necessary_existent_exists :
  MP001 -> MP002 -> MP003 -> MP008 -> MP009 -> MP010 -> MP011 -> MP012 ->
  SP001_SomethingExists ->
  exists n, NecessaryInItself n.
Proof.
  intros M1 M2 M3 M8 M9 M10 M11 M12 [x Hx].
  destruct (Division.division_exhaustive Thing Exists EssenceIncludesExistence x Hx)
    as [Hn | Hp].
  - exists x. exact Hn.
  - exact (necessary_existent_from_a_possible M1 M2 M3 M8 M9 M10 M11 M12 (ex_intro _ x Hp)).
Qed.

End Conclusion.

(* ------------------------------------------------------------------ *)
(* Checks.  Illustrations of logical possibility only; no claim about what
   exists. *)

(* 1. Consistency and non-vacuity: every postulate and SP-001 hold together
      (the model of PR-010: a necessary N, possibles P1 and P2, their
      aggregate Agg), and N is a Necessary Existent. *)
Example all_premises_hold_together :
  let Th := CauseOutsideIsNecessary.Th in
  let E := CauseOutsideIsNecessary.E1 in
  let G := CauseOutsideIsNecessary.G1 in
  let T := CauseOutsideIsNecessary.T1 in
  let Ess := CauseOutsideIsNecessary.EssN in
  let Mem := CauseOutsideIsNecessary.Mem in
  MP001 Th G T /\ MP002 Th G T /\ MP003 Th T /\ MP008 Th E Ess G /\
  MP009 Th E Ess Mem /\ MP010 Th Ess Mem /\ MP011 Th G Mem /\ MP012 Th E G /\
  SP001_SomethingExists Th E /\ NecessaryInItself Th E Ess CauseOutsideIsNecessary.N.
Proof.
  intros Th E G T Ess Mem.
  destruct CauseOutsideIsNecessary.all_hold_together
    as [H1 [H2 [H3 [H8 [H10 [H11 [H12 [HA [_ HN]]]]]]]]].
  split; [exact H1 |]. split; [exact H2 |]. split; [exact H3 |]. split; [exact H8 |].
  split; [intros _; exists AggregateIsPossible.Agg; split; [exact HA | exact I] |].
  split; [exact H10 |]. split; [exact H11 |]. split; [exact H12 |].
  split; [| exact HN].
  exists AggregateIsPossible.P1. exact I.
Qed.

(* 2. Countermodel without SP-001: nothing exists.  Every postulate holds,
      and there is no Necessary Existent.  So the existence claim comes only
      from SP-001; the postulates alone assert nothing about existence. *)
Example without_SP001_no_necessary_existent :
  let E := fun (_ : unit) => False in
  let Ess := fun (_ : unit) => False in
  let G := fun (_ _ : unit) => False in
  let T := fun (_ _ : unit) => False in
  let Mem := fun (_ _ : unit) => False in
  MP001 unit G T /\ MP002 unit G T /\ MP003 unit T /\ MP008 unit E Ess G /\
  MP009 unit E Ess Mem /\ MP010 unit Ess Mem /\ MP011 unit G Mem /\ MP012 unit E G /\
  ~ (exists n, NecessaryInItself unit E Ess n).
Proof.
  intros E Ess G T Mem.
  unfold MP001, MP002, MP003, MP008, MP009, MP010, MP011, MP012,
         NoSelfCreation.MP001_Giver, NoSelfCreation.MP002_Receiver,
         NoCircularCreation.MP003_Inherited,
         PossibleRequiresMurajjih.MP008_NoPreponderanceWithoutPreponderator,
         AggregateIsPossible.MP009_AggregateExists, AggregateIsPossible.MP010_NoNecessityFromPossibles,
         CauseOutsideIsNecessary.MP011_WholeToMembers, CauseOutsideIsNecessary.MP012_GiverExists,
         NecessaryInItself, Division.NecessaryInItself, Division.PossibleInItself,
         AggregateIsPossible.PossibleInItself, E, Ess, G, T, Mem.
  split; [| split; [| split; [| split; [| split; [| split; [| split; [| split]]]]]]].
  - intros x y H. contradiction.
  - intros x y H. contradiction.
  - intros x y z H. contradiction.
  - intros x H. contradiction.
  - intros [p [H _]]. contradiction.
  - intros A [p H]. contradiction.
  - intros c A p H. contradiction.
  - intros y x H. contradiction.
  - intros [n [H _]]. exact H.
Qed.

Print Assumptions necessary_existent_from_a_possible.
Print Assumptions necessary_existent_exists.
Print Assumptions all_premises_hold_together.
Print Assumptions without_SP001_no_necessary_existent.