(* Dalil al-kalima, unconditional: the "if the universe is caused" of the
   conclusion is discharged by PR-011.

   Rests on:
   - the kalima conclusion (KalimaConclusion.v), with its four premises
     PR-001 to PR-004 and MP-001, MP-002, MP-003, OP-001;
   - PR-011 (the universe is caused, by the division), with MP-008 and the
     observation OP-006 (and MP-010 for the whole-universe form);
   - excluded middle.
   No notion of time appears. *)

Require PR004.NoRegressOfGiving PR006.Division PR008.PossibleRequiresMurajjih
        PR009.AggregateIsPossible PR011.UniverseIsCaused KAL.KalimaConclusion.

Section Unconditional.

Variable Thing : Type.
Variable Exists : Thing -> Prop.
Variable EssenceIncludesExistence : Thing -> Prop.
Variable Gives : Thing -> Thing -> Prop.
Variable Through : Thing -> Thing -> Prop.
Variable PartOf : Thing -> Thing -> Prop.
Variable Universe : Thing.

Definition MP001 := KalimaConclusion.MP001 Thing Gives Through.
Definition MP002 := KalimaConclusion.MP002 Thing Gives Through.
Definition MP003 := KalimaConclusion.MP003 Thing Through.
Definition OP001 := KalimaConclusion.OP001 Thing Gives Exists.
Definition MP008 := UniverseIsCaused.MP008 Thing Exists EssenceIncludesExistence Gives.
Definition MP010 := UniverseIsCaused.MP010 Thing EssenceIncludesExistence PartOf.
Definition OP006 := UniverseIsCaused.OP006_NotWhollyNecessary Thing Exists EssenceIncludesExistence PartOf Universe.
Definition InUniverse := UniverseIsCaused.InUniverse Thing PartOf Universe.
Definition NecessaryInItself := Division.NecessaryInItself Thing Exists EssenceIncludesExistence.
Definition DependsOn := KalimaConclusion.DependsOn Thing Gives.

(* What kalima calls necessary (exists, nothing gives it existence) is, by
   MP-008, necessary in Ibn Sina's sense too (existence from its nature). *)
Lemma of_itself_is_necessary_in_itself :
  MP008 -> forall b, KalimaConclusion.Necessary Thing Gives Exists b -> NecessaryInItself b.
Proof.
  intros M8 b [Hex Hn]. split; [exact Hex |]. exact (M8 b Hex Hn).
Qed.

(* Kalima, unconditional, for the BROADER definition of the universe (it holds
   under ours too): something in the universe is caused, and it has a
   necessary first cause, beyond which there are no further causes.
   This form NEEDS OP-006 (the universe is not wholly necessary): under the
   broader definition only observation excludes a wholly necessary
   universe. *)
Theorem kalima_unconditional :
  MP001 -> MP002 -> MP003 -> OP001 -> MP008 -> OP006 ->
  exists x b, InUniverse x /\ Gives b x /\ Exists b /\ NecessaryInItself b /\
              Exhaustiveness.Independent Thing DependsOn b.
Proof.
  intros M1 M2 M3 OP M8 O6.
  destruct (UniverseIsCaused.something_in_universe_is_caused
              Thing Exists EssenceIncludesExistence Gives PartOf Universe M8 O6)
    as [x [Hin [_ Hcaused]]].
  destruct (KalimaConclusion.kalima_conclusion Thing Gives Through Exists x M1 M2 M3 OP Hcaused)
    as [b [Hg [Hex [Hnec [Hind _]]]]].
  exists x, b. split; [exact Hin |]. split; [exact Hg |]. split; [exact Hex |].
  split; [exact (of_itself_is_necessary_in_itself M8 b Hnec) | exact Hind].
Qed.

(* Kalima, unconditional for the universe as a whole (OUR definition: the
   universe does not overlap with the necessary cause): the universe itself
   has a necessary first cause.
   This form does NOT use OP-006; it uses OP-007 instead (the universe exists
   and has parts: the last two conditions). *)
Theorem kalima_unconditional_whole_universe :
  MP001 -> MP002 -> MP003 -> OP001 -> MP008 -> MP010 ->
  UniverseIsCaused.UniverseExcludesTheNecessary Thing EssenceIncludesExistence PartOf Universe ->
  Exists Universe -> (exists p, PartOf p Universe) ->
  exists b, Gives b Universe /\ Exists b /\ NecessaryInItself b /\
            Exhaustiveness.Independent Thing DependsOn b.
Proof.
  intros M1 M2 M3 OP M8 M10 Hnarrow HexU Hparts.
  pose proof (UniverseIsCaused.universe_as_a_whole_is_caused
                Thing Exists EssenceIncludesExistence Gives PartOf Universe M8 M10 Hnarrow HexU Hparts)
    as Hcaused.
  destruct (KalimaConclusion.kalima_conclusion Thing Gives Through Exists Universe M1 M2 M3 OP Hcaused)
    as [b [Hg [Hex [Hnec [Hind _]]]]].
  exists b. split; [exact Hg |]. split; [exact Hex |].
  split; [exact (of_itself_is_necessary_in_itself M8 b Hnec) | exact Hind].
Qed.

End Unconditional.

Print Assumptions of_itself_is_necessary_in_itself.
Print Assumptions kalima_unconditional.
Print Assumptions kalima_unconditional_whole_universe.