(* Dalil al-kalima: the conclusion.

   The argument's conclusion is conditional, exactly as the argument states
   it: IF the existence of the universe requires a cause, then every chain of
   existence-giving from the universe ends in something that depends on
   nothing (self-creation, circular creation and infinite regress being
   impossible), and there is a necessary first cause, beyond which there are
   no further causes, which gives existence to the universe.

   Rests only on the argument's four premises:
   - PR-001: the four cases are exhaustive (uses excluded middle);
   - PR-002 and PR-003: self-creation and circular creation are impossible
     (MP-001, MP-002, MP-003);
   - PR-004: an infinite regress of existence-giving is impossible (OP-001).
   Whether the universe's existence does require a cause is a separate
   question, not part of this argument; it is the antecedent of the
   conclusion.

   The universe is a section variable: once the section closes, the theorems
   hold for EVERY thing taken as "the universe".  Nothing is assumed to
   exist.  No notion of time appears. *)

Require PR001.Exhaustiveness PR002.NoSelfCreation PR003.NoCircularCreation
        PR004.NoRegressOfGiving.

Section Conclusion.

(* Primitive vocabulary.  Nothing is assumed about any of these. *)
Variable Thing : Type.
Variable Gives : Thing -> Thing -> Prop.    (* Gives y x   : y gives existence to x *)
Variable Through : Thing -> Thing -> Prop.  (* Through x y : x has its existence through y *)
Variable Exists : Thing -> Prop.            (* Exists x    : x actually exists *)
Variable Universe : Thing.                  (* the thing whose existence is explained *)

(* Reused definitions. *)
Definition DependsOn : Thing -> Thing -> Prop := NoSelfCreation.DependsOn Thing Gives.
Definition MP001 := NoCircularCreation.MP001 Thing Gives Through.
Definition MP002 := NoCircularCreation.MP002 Thing Gives Through.
Definition MP003 := NoCircularCreation.MP003_Inherited Thing Through.
Definition OP001 := NoRegressOfGiving.OP001_OnlySelfExistentGives Thing Gives Exists.

(* The antecedent of the conclusion: the existence of the universe requires a
   cause, i.e. the universe has its existence through another. *)
Definition UniverseIsCaused : Prop :=
  NoRegressOfGiving.ThroughAnother Thing Gives Universe.

(* Conditional definition: x is necessary if its existence belongs to it of
   itself -- x exists and nothing gives it existence -- so there is no giver
   who could withhold it.  (The classical wajib al-wujud li-dhatihi.) *)
Definition Necessary (x : Thing) : Prop := NoRegressOfGiving.OfItself Thing Gives Exists x.

(* Step 1: of the four cases, only case 4 remains.  Every maximal chain of
   existence-giving from the universe ends in something that depends on
   nothing. *)
Theorem only_case_4_remains :
  MP001 -> MP002 -> MP003 -> OP001 ->
  forall c, Exhaustiveness.MaximalChainFrom Thing DependsOn Universe c ->
  Exhaustiveness.EndsInIndependent Thing DependsOn c.
Proof.
  intros M1 M2 M3 OP c Hc.
  destruct (Exhaustiveness.four_cases_exhaustive Thing DependsOn Universe c Hc)
    as [H1 | [H2 | [H3 | H4]]].
  - (* case 1, self-creation: impossible by PR-003 (which includes PR-002) *)
    exfalso. exact (proj1 (NoCircularCreation.cases_1_and_2_eliminated
                             Thing Gives Through M1 M2 M3 Universe c Hc) H1).
  - (* case 2, circular creation: impossible by PR-003 *)
    exfalso. exact (proj2 (NoCircularCreation.cases_1_and_2_eliminated
                             Thing Gives Through M1 M2 M3 Universe c Hc) H2).
  - (* case 3, infinite regress: impossible by PR-004 *)
    exfalso. exact (NoRegressOfGiving.no_regress_of_giving
                      Thing Gives Exists OP Universe c Hc H3).
  - (* case 4: the chain ends in something independent *)
    exact H4.
Qed.

(* Step 2, the conclusion: if the universe is caused, there is a
   necessary first cause b, beyond which there are no further causes, that
   gives existence to the universe; and a maximal chain from the universe
   really exists and ends at b. *)
Theorem kalima_conclusion :
  MP001 -> MP002 -> MP003 -> OP001 ->
  UniverseIsCaused ->
  exists b,
    Gives b Universe /\
    Exists b /\
    Necessary b /\
    Exhaustiveness.Independent Thing DependsOn b /\
    exists c,
      Exhaustiveness.MaximalChainFrom Thing DependsOn Universe c /\
      c 1 = Some b /\
      Exhaustiveness.EndsInIndependent Thing DependsOn c.
Proof.
  intros M1 M2 M3 OP [b Hb].
  destruct (OP Universe b Hb) as [Hex Hnot].
  assert (Hind : Exhaustiveness.Independent Thing DependsOn b).
  { intros y Hy. apply Hnot. exists y. exact Hy. }
  exists b. split; [exact Hb |]. split; [exact Hex |].
  split; [split; assumption |]. split; [exact Hind |].
  (* The chain: the universe, then b, then stop. *)
  pose (c := fun n : nat => match n with 0 => Some Universe | 1 => Some b | _ => None end).
  assert (Hc : Exhaustiveness.MaximalChainFrom Thing DependsOn Universe c).
  { split; [reflexivity |]. split; [| split].
    - intros [| [| n]] x y Hx Hy; simpl in *; try discriminate.
      injection Hx as <-. injection Hy as <-. exact Hb.
    - intros [| [| n]] H; simpl in *; try discriminate; reflexivity.
    - intros [| [| n]] x Hx Hn; simpl in *; try discriminate.
      injection Hx as <-. exact Hind. }
  exists c. split; [exact Hc |]. split; [reflexivity |].
  exact (only_case_4_remains M1 M2 M3 OP c Hc).
Qed.

End Conclusion.

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

(* 1. Consistency and non-vacuity: every premise holds, and the universe is
      caused.
      Two things: a base (true) gives existence to the universe (false). *)
Example all_premises_hold_together :
  let G := fun (y x : bool) => y = true /\ x = false in
  let T := fun (x y : bool) => x = false /\ y = true in
  let E := fun (_ : bool) => True in
  MP001 bool G T /\ MP002 bool G T /\ MP003 bool T /\ OP001 bool G E /\
  UniverseIsCaused bool G false.
Proof.
  unfold MP001, MP002, MP003, OP001, UniverseIsCaused,
         NoCircularCreation.MP001, NoCircularCreation.MP002,
         NoSelfCreation.MP001_Giver, NoSelfCreation.MP002_Receiver,
         NoCircularCreation.MP003_Inherited,
         NoRegressOfGiving.OP001_OnlySelfExistentGives,
         NoRegressOfGiving.OfItself, NoRegressOfGiving.ThroughAnother.
  simpl. split; [| split; [| split; [| split]]].
  - intros x y [Hy _] [HyF _]. subst y. discriminate.
  - intros x y [Hy Hx]. split; assumption.
  - intros x y z [_ Hy] [Hy' _]. subst y. discriminate.
  - intros x y [Hy _]. subst y. split; [exact I |]. intros [z [_ Hbad]]. discriminate.
  - exists true. split; reflexivity.
Qed.

(* 2. The "if" matters: for a universe that nothing gives existence to, all
      premises hold but nothing gives it existence.  So the conclusion is
      conditional, as the argument states. *)
Example uncaused_universe_no_first_cause_follows :
  let G := fun (_ _ : unit) => False in
  let T := fun (_ _ : unit) => False in
  let E := fun (_ : unit) => True in
  MP001 unit G T /\ MP002 unit G T /\ MP003 unit T /\ OP001 unit G E /\
  ~ (exists b, G b tt).
Proof.
  unfold MP001, MP002, MP003, OP001,
         NoCircularCreation.MP001, NoCircularCreation.MP002,
         NoSelfCreation.MP001_Giver, NoSelfCreation.MP002_Receiver,
         NoCircularCreation.MP003_Inherited,
         NoRegressOfGiving.OP001_OnlySelfExistentGives.
  simpl. split; [| split; [| split; [| split]]].
  - intros x y H. contradiction.
  - intros x y H. contradiction.
  - intros x y z H. contradiction.
  - intros x y H. contradiction.
  - intros [b H]. exact H.
Qed.

(* 3. Without OP-001 the conclusion fails: numbers 0, 1, 2, ..., each given
      existence by the next (0 is the "universe").  MP-001 to MP-003
      hold and the universe is caused, but no giver of it is necessary. *)
Example without_OP001_no_necessary_cause_follows :
  let G := fun (y x : nat) => y = S x in
  let T := fun (x y : nat) => x < y in
  let E := fun (_ : nat) => True in
  MP001 nat G T /\ MP002 nat G T /\ MP003 nat T /\
  UniverseIsCaused nat G 0 /\
  ~ (exists b, G b 0 /\ Necessary nat G E b).
Proof.
  unfold MP001, MP002, MP003, UniverseIsCaused, Necessary,
         NoCircularCreation.MP001, NoCircularCreation.MP002,
         NoSelfCreation.MP001_Giver, NoSelfCreation.MP002_Receiver,
         NoCircularCreation.MP003_Inherited,
         NoRegressOfGiving.OfItself, NoRegressOfGiving.ThroughAnother.
  simpl. split; [| split; [| split; [| split]]].
  - intros x y Hy Hlt. subst y. exact (PeanoNat.Nat.lt_irrefl _ (PeanoNat.Nat.lt_trans _ _ _ Hlt (PeanoNat.Nat.lt_succ_diag_r x))).
  - intros x y Hy. subst y. exact (PeanoNat.Nat.lt_succ_diag_r x).
  - intros x y z H1 H2. exact (PeanoNat.Nat.lt_trans _ _ _ H1 H2).
  - exists 1. reflexivity.
  - intros [b [Hb [_ Hnot]]]. subst b. apply Hnot. exists 2. reflexivity.
Qed.

Print Assumptions only_case_4_remains.
Print Assumptions kalima_conclusion.
Print Assumptions all_premises_hold_together.
Print Assumptions uncaused_universe_no_first_cause_follows.
Print Assumptions without_OP001_no_necessary_cause_follows.