(* PR-011 (dalil al-kalima, its "if"): the universe is caused.

   The division.  Suppose the universe has no cause.  Considered in itself,
   the universe is then:
     case 1: wholly necessary -- excluded by observation (OP-006);
     case 2: necessary and possible in the same respect -- a contradiction
             (PR-006: nothing is both);
     case 3: necessary in one part and possible in another (a part may be
             physical or metaphysical) -- then the necessary part is what the
             argument is after, and the possible part needs a cause;
     case 4: wholly possible -- then it needs a cause, and dalil al-kalima's
             four premises take over.
   So at least something in the universe is possible, and by step 3 of dalil
   al-imkan (MP-008) it has a cause.

   Two definitions of "the universe":
   - the definition used here: the universe does not overlap with the
     necessary cause (no part of it is necessary).  Then case 3 cannot arise,
     and the universe as a whole is caused (with MP-010).
   - a broader definition (for example Spinoza's): the universe includes the
     necessary.  Then case 3 is possible, and what is caused is its possible
     part.  The difference is one of naming, not of substance: either way the
     necessary is reached.

   Rests on: PR-006 (the division), PR-008 (step 3, MP-008), PR-009 (MP-010),
   observational premise OP-006, and excluded middle.  No notion of time. *)

From Stdlib Require Import Classical.
Require PR004.NoRegressOfGiving PR006.Division PR008.PossibleRequiresMurajjih
        PR009.AggregateIsPossible.

Section Universe.

(* 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 PartOf : Thing -> Thing -> Prop.   (* PartOf p u : p is a part of u, physical or metaphysical *)
Variable Universe : Thing.

(* Reused definitions. *)
Definition NecessaryInItself := Division.NecessaryInItself Thing Exists EssenceIncludesExistence.
Definition PossibleInItself := Division.PossibleInItself Thing Exists EssenceIncludesExistence.
Definition ThroughAnother := NoRegressOfGiving.ThroughAnother Thing Gives.
Definition MP008 := PossibleRequiresMurajjih.MP008_NoPreponderanceWithoutPreponderator
                      Thing Exists EssenceIncludesExistence Gives.
Definition MP010 := AggregateIsPossible.MP010_NoNecessityFromPossibles
                      Thing EssenceIncludesExistence PartOf.

(* x is in the universe: x is the universe itself, or one of its parts. *)
Definition InUniverse (x : Thing) : Prop := x = Universe \/ PartOf x Universe.

(* The four cases, for a universe whose parts all exist. *)
Definition WhollyNecessary : Prop := forall x, InUniverse x -> NecessaryInItself x.
Definition WhollyPossible : Prop := forall x, InUniverse x -> PossibleInItself x.
Definition NecessaryAndPossibleInSameRespect : Prop :=
  exists x, InUniverse x /\ NecessaryInItself x /\ PossibleInItself x.
Definition Mixed : Prop :=
  (exists x, InUniverse x /\ NecessaryInItself x) /\ (exists y, InUniverse y /\ PossibleInItself y).

(* OP-006 (observation): at the very least, the universe is not wholly
   necessary -- something in it (or the universe itself) exists without having
   its existence from its own nature.
   OP-006 IS NEEDED FOR THE BROADER DEFINITION of the universe (one that may
   include the necessary, as in Spinoza).  Under that definition nothing but
   observation excludes case 1 (a wholly necessary universe); without OP-006
   nothing in the universe need be caused (see without_OP006_nothing_caused).
   Under OUR definition (the universe does not overlap with the necessary)
   OP-006 is not used: see universe_as_a_whole_is_caused, which instead needs
   OP-007 (the universe exists and has parts). *)
Definition OP006_NotWhollyNecessary : Prop :=
  exists x, InUniverse x /\ PossibleInItself x.

(* Case 2 is a contradiction (PR-006). *)
Theorem case2_impossible : ~ NecessaryAndPossibleInSameRespect.
Proof.
  intros [x [_ H]]. exact (Division.division_exclusive Thing Exists EssenceIncludesExistence x H).
Qed.

(* The division is exhaustive: if the universe and all its parts exist, it is
   wholly necessary (case 1), wholly possible (case 4), or mixed (case 3). *)
Theorem universe_division :
  (forall x, InUniverse x -> Exists x) ->
  WhollyNecessary \/ WhollyPossible \/ Mixed.
Proof.
  intro Hex.
  destruct (classic (exists y, InUniverse y /\ PossibleInItself y)) as [Hp | Hnp].
  - destruct (classic (exists x, InUniverse x /\ NecessaryInItself x)) as [Hn | Hnn].
    + right; right. split; assumption.
    + right; left. intros x Hx.
      destruct (Division.division_exhaustive Thing Exists EssenceIncludesExistence x (Hex x Hx))
        as [HN | HP]; [exfalso; apply Hnn; exists x; split; assumption | exact HP].
  - left. intros x Hx.
    destruct (Division.division_exhaustive Thing Exists EssenceIncludesExistence x (Hex x Hx))
      as [HN | HP]; [exact HN | exfalso; apply Hnp; exists x; split; assumption].
Qed.

(* The result for the BROADER definition (it holds under ours too): something
   in the universe is possible, and it is caused.  This is the theorem that
   needs OP-006. *)
Theorem something_in_universe_is_caused :
  MP008 -> OP006_NotWhollyNecessary ->
  exists x, InUniverse x /\ PossibleInItself x /\ ThroughAnother x.
Proof.
  intros M8 [x [Hin Hp]]. exists x. split; [exact Hin |]. split; [exact Hp |].
  exact (PossibleRequiresMurajjih.possible_requires_murajjih
           Thing Exists EssenceIncludesExistence Gives M8 x Hp).
Qed.

(* Our definition: the universe does not overlap with the necessary cause --
   none of its parts has its existence from its own nature. *)
Definition UniverseExcludesTheNecessary : Prop :=
  forall p, PartOf p Universe -> ~ EssenceIncludesExistence p.

(* Under our definition, case 3 cannot arise for the parts: no part is
   necessary. *)
Theorem narrow_no_necessary_part :
  UniverseExcludesTheNecessary -> ~ (exists p, PartOf p Universe /\ NecessaryInItself p).
Proof.
  intros Hnarrow [p [Hp [_ He]]]. exact (Hnarrow p Hp He).
Qed.

(* Under our definition, the universe as a whole is caused: it exists, it has
   parts, none of which is necessary, so by MP-010 it is itself possible, and
   by step 3 (MP-008) it has a cause.  This is C1 in the full sense.
   OP-006 is NOT used here: "not wholly necessary" follows from our
   definition.  Instead the observation OP-007 is used -- the universe exists
   and has parts -- which appears as the last two conditions. *)
Theorem universe_as_a_whole_is_caused :
  MP008 -> MP010 -> UniverseExcludesTheNecessary ->
  Exists Universe -> (exists p, PartOf p Universe) ->
  ThroughAnother Universe.
Proof.
  intros M8 M10 Hnarrow HexU Hparts.
  apply (PossibleRequiresMurajjih.possible_requires_murajjih
           Thing Exists EssenceIncludesExistence Gives M8 Universe).
  split; [exact HexU |]. exact (M10 Universe Hparts Hnarrow).
Qed.

End Universe.

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

Inductive Th := N | P | U.

(* 1. Our definition: the universe U has one part P, possible; N (outside U)
      is necessary and gives existence to U and P.  All premises hold, U is
      caused, and case 3 does not arise. *)
Example narrow_definition_model :
  let E := fun (_ : Th) => True in
  let Ess := fun (x : Th) => x = N in
  let G := fun (y x : Th) => y = N /\ x <> N in
  let Part := fun (p u : Th) => p = P /\ u = U in
  MP008 Th E Ess G /\ MP010 Th Ess Part /\ UniverseExcludesTheNecessary Th Ess Part U /\
  OP006_NotWhollyNecessary Th E Ess Part U /\ ThroughAnother Th G U.
Proof.
  intros E Ess G Part.
  unfold MP008, MP010, UniverseExcludesTheNecessary, OP006_NotWhollyNecessary, ThroughAnother,
         PossibleRequiresMurajjih.MP008_NoPreponderanceWithoutPreponderator,
         AggregateIsPossible.MP010_NoNecessityFromPossibles, NoRegressOfGiving.ThroughAnother,
         InUniverse, PossibleInItself, Division.PossibleInItself, E, Ess, G, Part.
  split; [| split; [| split; [| split]]].
  - intros [] _ Hn; try reflexivity; exfalso; apply Hn; exists N; (split; [reflexivity | discriminate]).
  - intros A [q [_ HA]] _. subst A. discriminate.
  - intros p [Hp _]. subst p. discriminate.
  - exists P. split; [right; split; reflexivity | split; [exact I | discriminate]].
  - exists N. split; [reflexivity | discriminate].
Qed.

(* 2. A broader definition (Spinoza's): the universe U includes a necessary
      part N and a possible part P; N gives existence to P.  Case 3 (mixed)
      holds, and the possible part is caused.  So under the broader
      definition case 3 is possible. *)
Example broad_definition_case3 :
  let E := fun (_ : Th) => True in
  let Ess := fun (x : Th) => x = N in
  let G := fun (y x : Th) => y = N /\ x = P in
  let Part := fun (p u : Th) => (p = N \/ p = P) /\ u = U in
  Mixed Th E Ess Part U /\ ThroughAnother Th G P.
Proof.
  intros E Ess G Part.
  unfold Mixed, ThroughAnother, NoRegressOfGiving.ThroughAnother, InUniverse,
         NecessaryInItself, PossibleInItself, Division.NecessaryInItself,
         Division.PossibleInItself, E, Ess, G, Part.
  split; [split |].
  - exists N. split; [right; split; [left; reflexivity | reflexivity] | split; [exact I | reflexivity]].
  - exists P. split; [right; split; [right; reflexivity | reflexivity] | split; [exact I | discriminate]].
  - exists N. split; reflexivity.
Qed.

(* 3. Countermodel without OP-006: a universe that is wholly necessary and
      uncaused.  MP-008 holds, and nothing in it is caused.  So the
      observation is needed. *)
Example without_OP006_nothing_caused :
  let E := fun (_ : unit) => True in
  let Ess := fun (_ : unit) => True in
  let G := fun (_ _ : unit) => False in
  let Part := fun (_ _ : unit) => False in
  MP008 unit E Ess G /\ WhollyNecessary unit E Ess Part tt /\
  ~ (exists x, InUniverse unit Part tt x /\ ThroughAnother unit G x).
Proof.
  intros E Ess G Part.
  unfold MP008, WhollyNecessary, ThroughAnother,
         PossibleRequiresMurajjih.MP008_NoPreponderanceWithoutPreponderator,
         NoRegressOfGiving.ThroughAnother, NecessaryInItself, Division.NecessaryInItself,
         E, Ess, G, Part.
  split; [| split].
  - intros x _ _. exact I.
  - intros x _. split; exact I.
  - intros [x [_ [y H]]]. exact H.
Qed.

(* 4. Countermodel without MP-008: something possible in the universe with no
      cause (a brute fact).  OP-006 holds, but nothing is caused.  So MP-008
      is needed. *)
Example without_MP008_possible_uncaused :
  let E := fun (_ : unit) => True in
  let Ess := fun (_ : unit) => False in
  let G := fun (_ _ : unit) => False in
  let Part := fun (_ _ : unit) => False in
  OP006_NotWhollyNecessary unit E Ess Part tt /\
  ~ (exists x, InUniverse unit Part tt x /\ ThroughAnother unit G x).
Proof.
  intros E Ess G Part.
  unfold OP006_NotWhollyNecessary, ThroughAnother, NoRegressOfGiving.ThroughAnother,
         InUniverse, PossibleInItself, Division.PossibleInItself, E, Ess, G, Part.
  split.
  - exists tt. split; [left; reflexivity | split; [exact I | intro H; exact H]].
  - intros [x [_ [y H]]]. exact H.
Qed.

Print Assumptions case2_impossible.
Print Assumptions universe_division.
Print Assumptions something_in_universe_is_caused.
Print Assumptions narrow_no_necessary_part.
Print Assumptions universe_as_a_whole_is_caused.
Print Assumptions narrow_definition_model.
Print Assumptions broad_definition_case3.
Print Assumptions without_OP006_nothing_caused.
Print Assumptions without_MP008_possible_uncaused.