(* Dalil al-kalima: the complete Rocq proof in one file.

   The four premises, the conclusion, and the proof that the universe is caused
   (PR-011), which removes the conclusion's "if".

   This file joins, unchanged apart from the lines noted below, the proofs of
   the premises and of the conclusion, so that the whole argument can be
   compiled in one step (for example in the Rocq tool at at.alkalam.org, or
   with:  rocq compile KalimaComplete.v ).

   Changes from the separate files: each file is wrapped in a Module of the
   same name, its standard-library imports are gathered here at the top, and
   its lines that load the other files ("Require PR0..." / "Require KAL...")
   are removed, because those files are already present above it.

   The only axiom anywhere is excluded middle ([classic]); every
   "Print Assumptions" line reports exactly what each result rests on. *)

From Stdlib Require Import Classical PeanoNat Lia Relations.

(* ======================================================================
   PR-001 (kalima premise 1): the four cases are exhaustive and exclusive, for chains
   ====================================================================== *)
Module Exhaustiveness.

(* Premise: every chain of dependence falls under exactly one of four cases:
   (1) self-dependence, (2) circularity, (3) infinite regress,
   (4) the chain ends at something that depends on nothing.

   Logical principle used, declared openly: the law of excluded middle
   (Stdlib Classical, axiom [classic]). Nothing else is assumed. *)


Section Cases.

(* Primitive vocabulary.  Nothing is assumed about either item: once the
   section closes, every theorem below holds for EVERY type of things and
   EVERY relation.  In particular, nothing is assumed to exist. *)
Variable Thing : Type.
Variable DependsOn : Thing -> Thing -> Prop.  (* x depends on y for its existence *)

(* Conditional definition: if x depends on nothing, x is called independent. *)
Definition Independent (x : Thing) : Prop := forall y, ~ DependsOn x y.

(* A chain is a sequence of positions; [None] means the chain has stopped. *)
Definition Chain := nat -> option Thing.

(* c is a maximal chain of dependence starting from u:
   - it starts at u;
   - each next item is something the previous item depends on;
   - once stopped, it stays stopped;
   - it stops only at something independent (it is never cut short). *)
Definition MaximalChainFrom (u : Thing) (c : Chain) : Prop :=
  c 0 = Some u /\
  (forall n x y, c n = Some x -> c (S n) = Some y -> DependsOn x y) /\
  (forall n, c n = None -> c (S n) = None) /\
  (forall n x, c n = Some x -> c (S n) = None -> Independent x).

(* Some item occurs twice in the chain. *)
Definition Repeats (c : Chain) : Prop :=
  exists i j x, i < j /\ c i = Some x /\ c j = Some x.

(* Case 1: some item is immediately followed by itself (x depends on x). *)
Definition SelfDependence (c : Chain) : Prop :=
  exists n x, c n = Some x /\ c (S n) = Some x.

(* Case 2: an item recurs, but never immediately. *)
Definition Circularity (c : Chain) : Prop :=
  Repeats c /\ ~ SelfDependence c.

(* Case 3: the chain never stops and no item recurs. *)
Definition InfiniteRegress (c : Chain) : Prop :=
  (forall n, c n <> None) /\ ~ Repeats c.

(* Case 4: the chain stops at an independent item, with no item recurring. *)
Definition EndsInIndependent (c : Chain) : Prop :=
  (exists n x, c n = Some x /\ c (S n) = None /\ Independent x) /\ ~ Repeats c.

(* Helper: a chain that starts with an item and later stops has a last item. *)
Lemma last_item : forall (c : Chain) (u : Thing) n,
  c 0 = Some u -> c n = None ->
  exists m x, c m = Some x /\ c (S m) = None.
Proof.
  intros c u n H0. induction n as [| k IH]; intros Hn.
  - congruence.
  - destruct (c k) as [x |] eqn:Hk.
    + exists k, x. split; assumption.
    + apply IH. reflexivity.
Qed.

(* Exhaustiveness: every maximal chain falls under at least one case. *)
Theorem four_cases_exhaustive : forall u c,
  MaximalChainFrom u c ->
  SelfDependence c \/ Circularity c \/ InfiniteRegress c \/ EndsInIndependent c.
Proof.
  intros u c [H0 [_ [_ Hstop]]].
  destruct (classic (Repeats c)) as [Hrep | Hnorep].
  - destruct (classic (SelfDependence c)) as [Hself | Hnoself].
    + left. exact Hself.
    + right; left. split; assumption.
  - destruct (classic (exists n, c n = None)) as [[n Hn] | Hnever].
    + destruct (last_item c u n H0 Hn) as [m [x [Hm HSm]]].
      right; right; right. split.
      * exists m, x. repeat split; try assumption. exact (Hstop m x Hm HSm).
      * exact Hnorep.
    + right; right; left. split.
      * intros n Hn. apply Hnever. exists n. exact Hn.
      * exact Hnorep.
Qed.

(* Exclusivity: no maximal chain falls under two cases. *)
Lemma self_repeats : forall c, SelfDependence c -> Repeats c.
Proof.
  intros c [n [x [H1 H2]]]. exists n, (S n), x. repeat split; try assumption. lia.
Qed.

Theorem four_cases_exclusive : forall c,
  (SelfDependence c -> ~ Circularity c /\ ~ InfiniteRegress c /\ ~ EndsInIndependent c) /\
  (Circularity c -> ~ InfiniteRegress c /\ ~ EndsInIndependent c) /\
  (InfiniteRegress c -> ~ EndsInIndependent c).
Proof.
  intro c. split; [| split].
  - intro Hs. split; [| split].
    + intros [_ Hns]. contradiction.
    + intros [_ Hnr]. exact (Hnr (self_repeats c Hs)).
    + intros [_ Hnr]. exact (Hnr (self_repeats c Hs)).
  - intros [Hr _]. split.
    + intros [_ Hnr]. contradiction.
    + intros [_ Hnr]. contradiction.
  - intros [Hnever _] [[n [x [_ [HSn _]]]] _]. exact (Hnever (S n) HSn).
Qed.

End Cases.

(* ------------------------------------------------------------------ *)
(* Non-vacuity: each case really occurs for some relation, so none of the
   four definitions is empty.  These are illustrations of logical
   possibility only; they make no claim about what exists. *)

(* Case 1: a single thing that depends on itself. *)
Example case1_occurs :
  let D := fun (_ _ : unit) => True in
  let c := fun (_ : nat) => Some tt in
  MaximalChainFrom unit D tt c /\ SelfDependence unit c.
Proof.
  simpl. split.
  - repeat split; intros; try discriminate; exact I.
  - exists 0, tt. split; reflexivity.
Qed.

(* Case 2: two things that depend on each other. *)
Example case2_occurs :
  let D := fun (x y : bool) => y = negb x in
  let c := fun (n : nat) => Some (Nat.odd n) in
  MaximalChainFrom bool D false c /\ Circularity bool c.
Proof.
  simpl. split.
  - repeat split.
    + intros n x y Hx Hy. injection Hx as <-. injection Hy as <-.
      rewrite Nat.odd_succ, <- Nat.negb_odd. reflexivity.
    + intros n H. discriminate.
    + intros n x _ H. discriminate.
  - split.
    + exists 0, 2, false. repeat split. lia.
    + intros [n [x [H1 H2]]]. injection H1 as H1. injection H2 as H2.
      rewrite Nat.odd_succ, <- Nat.negb_odd in H2. subst x.
      destruct (Nat.odd n); discriminate.
Qed.

(* Case 3: each number depends on the next, without end. *)
Example case3_occurs :
  let D := fun (x y : nat) => y = S x in
  let c := fun (n : nat) => Some n in
  MaximalChainFrom nat D 0 c /\ InfiniteRegress nat c.
Proof.
  simpl. split.
  - repeat split.
    + intros n x y Hx Hy. injection Hx as <-. injection Hy as <-. reflexivity.
    + intros n H. discriminate.
    + intros n x _ H. discriminate.
  - split.
    + intros n H. discriminate.
    + intros [i [j [x [Hij [Hi Hj]]]]]. injection Hi as Hi. injection Hj as Hj. lia.
Qed.

(* Case 4: one thing depends on a second, which depends on nothing. *)
Example case4_occurs :
  let D := fun (x y : bool) => x = false /\ y = true in
  let c := fun (n : nat) => match n with 0 => Some false | 1 => Some true | _ => None end in
  MaximalChainFrom bool D false c /\ EndsInIndependent bool D c.
Proof.
  simpl. split.
  - split; [reflexivity | split; [| split]].
    + intros [| [| n]] x y Hx Hy; simpl in *; try discriminate.
      injection Hx as <-. injection Hy as <-. split; reflexivity.
    + intros [| [| n]] H; simpl in *; try discriminate; reflexivity.
    + intros [| [| n]] x Hx Hn; simpl in *; try discriminate.
      injection Hx as <-. intros y [H _]. discriminate.
  - split.
    + exists 1, true. repeat split. intros y [H _]. discriminate.
    + intros [i [j [x [Hij [Hi Hj]]]]].
      destruct i as [| [| i]]; destruct j as [| [| j]]; simpl in *;
        try discriminate; try lia.
      injection Hi as <-. discriminate.
Qed.

Print Assumptions four_cases_exhaustive.
Print Assumptions four_cases_exclusive.
Print Assumptions case1_occurs.
Print Assumptions case2_occurs.
Print Assumptions case3_occurs.
Print Assumptions case4_occurs.

End Exhaustiveness.

(* ======================================================================
   PR-001, second form: the four cases without chains (as used by Leo-III)
   ====================================================================== *)
Module RelationalForms.

(* PR-001, second proof: the four cases stated in relational form (without
   chains), exactly as they are stated in the Leo-III files of dalil
   al-kalima (arguments/dalil-al-kalima/proofs/leo3-kalima/).

   Also proves that Leo-III's definition of "ultimately depends on" (the
   least transitive relation containing dependence, written as a
   higher-order formula) is equivalent to Rocq's clos_trans, which PR-003
   uses.  So the Leo-III premise 3 states exactly what PR-003 proves.

   Logical principle used: excluded middle (classic), in the exhaustiveness
   theorem only.  Nothing else is assumed.  Nothing is assumed to exist. *)


Section Relational.

(* Primitive vocabulary.  Nothing is assumed about either. *)
Variable Thing : Type.
Variable Gives : Thing -> Thing -> Prop.   (* Gives y x : y gives existence to x *)

(* The Leo-III definitions, transcribed. *)
Definition Dep (x y : Thing) : Prop := Gives y x.
Definition Independent (x : Thing) : Prop := forall y, ~ Dep x y.

(* Leo-III's "reach": x ultimately depends on y, written as a higher-order
   formula (true of every transitive relation containing Dep). *)
Definition Reach (x y : Thing) : Prop :=
  forall P : Thing -> Thing -> Prop,
    ((forall a b, Dep a b -> P a b) /\
     (forall a b c, P a b -> P b c -> P a c)) -> P x y.

Definition Case1 (x : Thing) : Prop :=
  exists y, (x = y \/ Reach x y) /\ Dep y y.
Definition Case2 (x : Thing) : Prop :=
  exists y, (x = y \/ Reach x y) /\ Reach y y /\ ~ Dep y y.
Definition Case3 (x : Thing) : Prop :=
  exists S : Thing -> Prop, S x /\ (forall a, S a -> exists b, S b /\ Dep a b).
Definition Case4 (x : Thing) : Prop :=
  Independent x \/ exists y, Reach x y /\ Independent y.

(* Leo-III's Reach coincides with Rocq's clos_trans (used in PR-003). *)
Theorem reach_iff_clos_trans : forall x y, Reach x y <-> clos_trans Thing Dep x y.
Proof.
  intros x y. split.
  - intro H. apply H. split.
    + intros a b Hab. apply t_step. exact Hab.
    + intros a b c H1 H2. apply t_trans with b; assumption.
  - intro H. induction H as [a b Hab | a b c _ IH1 _ IH2].
    + intros P [Hstep _]. exact (Hstep a b Hab).
    + intros P HP. destruct HP as [Hstep Htrans].
      apply Htrans with b; [apply IH1 | apply IH2]; split; assumption.
Qed.

(* Premise 1, relational form: every thing falls under at least one case. *)
Theorem four_cases_exhaustive_relational : forall x,
  Case1 x \/ Case2 x \/ Case3 x \/ Case4 x.
Proof.
  intro x.
  destruct (classic (Case4 x)) as [H4 | Hn4].
  - right; right; right. exact H4.
  - right; right; left.
    exists (fun z => z = x \/ Reach x z). split; [left; reflexivity |].
    intros a Ha.
    (* a is not independent, otherwise case 4 would hold *)
    assert (Hnind : ~ Independent a).
    { intro Hind. apply Hn4. destruct Ha as [Heq | Hr].
      - left. subst a. exact Hind.
      - right. exists a. split; assumption. }
    (* so a depends on some b *)
    destruct (not_all_not_ex Thing (fun b => Dep a b) Hnind) as [b Hab].
    exists b. split; [| exact Hab].
    right. destruct Ha as [Heq | Hr].
    + subst a. apply reach_iff_clos_trans. apply t_step. exact Hab.
    + apply reach_iff_clos_trans. apply t_trans with a.
      * exact (proj1 (reach_iff_clos_trans x a) Hr).
      * apply t_step. exact Hab.
Qed.

End Relational.

Print Assumptions reach_iff_clos_trans.
Print Assumptions four_cases_exhaustive_relational.

End RelationalForms.

(* ======================================================================
   PR-002: nothing gives existence to itself
   ====================================================================== *)
Module NoSelfCreation.

(* PR-002: Nothing gives existence to itself (self-creation is impossible).

   Rests on:
   - the law of non-contradiction, which is proved below from logic alone;
   - meaning postulates MP-001 and MP-002, which appear as explicit
     conditions of the theorem.
   No axiom is used.  Nothing is assumed to exist.  No notion of time appears:
   "has its existence through" means dependence in the order of being, not
   succession in time. *)

Section SelfCreation.

(* 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 *)

(* Link to the vocabulary of PR-001: x depends on y for its existence
   means y gives existence to x. *)
Definition DependsOn (x y : Thing) : Prop := Gives y x.

(* MP-001, "what lacks a thing cannot give it" (faqid al-shay' la yu'tih):
   whatever gives existence to x does not have its own existence through x. *)
Definition MP001_Giver : Prop := forall x y, Gives y x -> ~ Through y x.

(* MP-002, "receiving": whatever is given existence by y has its existence
   through y. *)
Definition MP002_Receiver : Prop := forall x y, Gives y x -> Through x y.

(* The law of non-contradiction: no statement is both true and not true.
   Proved from logic alone; it is a theorem here, not an axiom. *)
Theorem non_contradiction : forall P : Prop, ~ (P /\ ~ P).
Proof.
  intros P [Hp Hnp]. exact (Hnp Hp).
Qed.

(* Premise 2: nothing gives existence to itself. *)
Theorem no_self_creation :
  MP001_Giver -> MP002_Receiver -> forall x, ~ Gives x x.
Proof.
  intros M1 M2 x Hxx.
  apply (non_contradiction (Through x x)).
  split.
  - exact (M2 x x Hxx).
  - exact (M1 x x Hxx).
Qed.

(* The same, in the vocabulary of PR-001: nothing depends on itself. *)
Corollary no_self_dependence :
  MP001_Giver -> MP002_Receiver -> forall x, ~ DependsOn x x.
Proof.
  intros M1 M2 x. exact (no_self_creation M1 M2 x).
Qed.

End SelfCreation.

(* ------------------------------------------------------------------ *)
(* Checks.  These are illustrations of logical possibility only; they make
   no claim about what exists. *)

(* 1. Non-vacuity: both postulates can hold while giving really occurs.
      Two things: A (true) gives existence to B (false). *)
Example postulates_allow_giving :
  let G := fun (y x : bool) => y = true /\ x = false in
  let T := fun (x y : bool) => x = false /\ y = true in
  MP001_Giver bool G T /\ MP002_Receiver bool G T /\ G true false.
Proof.
  simpl. cbv delta [MP001_Giver MP002_Receiver]. split; [| split].
  - intros x y [Hy _] [HyF _]. subst y. discriminate.
  - intros x y [Hy Hx]. split; assumption.
  - split; reflexivity.
Qed.

(* 2. Countermodel without MP-001: one thing that gives existence to itself and
      has its existence through itself.  MP-002 holds; self-creation occurs. *)
Example without_MP001_self_creation_is_consistent :
  let G := fun (_ _ : unit) => True in
  let T := fun (_ _ : unit) => True in
  MP002_Receiver unit G T /\ G tt tt.
Proof.
  simpl. cbv delta [MP001_Giver MP002_Receiver]. split.
  - intros; exact I.
  - exact I.
Qed.

(* 3. Countermodel without MP-002: one thing that gives existence to itself but
      has its existence through nothing.  MP-001 holds; self-creation occurs. *)
Example without_MP002_self_creation_is_consistent :
  let G := fun (_ _ : unit) => True in
  let T := fun (_ _ : unit) => False in
  MP001_Giver unit G T /\ G tt tt.
Proof.
  simpl. cbv delta [MP001_Giver MP002_Receiver]. split.
  - intros x y _ H. exact H.
  - exact I.
Qed.

(* 4. Eternal-universe compatibility.  Time is introduced ONLY for this check
      and appears nowhere in the premise.  Both things exist at every moment
      (neither has a beginning), A gives existence to B, and both postulates
      hold.  So the postulates never require anything to have a beginning. *)
Example compatible_with_eternal_existence :
  let G := fun (y x : bool) => y = true /\ x = false in
  let T := fun (x y : bool) => x = false /\ y = true in
  let ExistsAt := fun (_ : bool) (_ : nat) => True in
  (forall t, ExistsAt true t /\ ExistsAt false t) /\
  MP001_Giver bool G T /\ MP002_Receiver bool G T /\ G true false.
Proof.
  simpl. cbv delta [MP001_Giver MP002_Receiver]. split; [| split; [| split]].
  - intros t. split; exact I.
  - intros x y [Hy _] [HyF _]. subst y. discriminate.
  - intros x y [Hy Hx]. split; assumption.
  - split; reflexivity.
Qed.

Print Assumptions non_contradiction.
Print Assumptions no_self_creation.
Print Assumptions no_self_dependence.
Print Assumptions postulates_allow_giving.
Print Assumptions without_MP001_self_creation_is_consistent.
Print Assumptions without_MP002_self_creation_is_consistent.
Print Assumptions compatible_with_eternal_existence.

End NoSelfCreation.

(* ======================================================================
   PR-003: no circle of dependence of any length
   ====================================================================== *)
Module NoCircularCreation.

(* PR-003: No circle of dependence of any length.  Nothing ultimately depends
   on itself, so no maximal chain of dependence (PR-001) contains a repeated
   thing: cases 1 and 2 of PR-001 are both eliminated.

   Rests on:
   - PR-001 (Exhaustiveness.v), reused for its chain definitions;
   - PR-002 (NoSelfCreation.v), reused for the one-step circle;
   - meaning postulates MP-001, MP-002 (from PR-002) and MP-003 (below),
     all as explicit conditions of the theorems.
   No axiom is used.  Nothing is assumed to exist.  No notion of time appears. *)


Section Circles.

(* Primitive vocabulary: the same as PR-002.  Nothing is assumed about it. *)
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 *)

(* Reused from PR-002: x depends on y means y gives existence to x. *)
Definition DependsOn : Thing -> Thing -> Prop := NoSelfCreation.DependsOn Thing Gives.

(* Reused meaning postulates from PR-002. *)
Definition MP001 : Prop := NoSelfCreation.MP001_Giver Thing Gives Through.
Definition MP002 : Prop := NoSelfCreation.MP002_Receiver Thing Gives Through.

(* MP-003, "existence through is inherited": if x has its existence through y,
   and y has its existence through z, then x has its existence through z. *)
Definition MP003_Inherited : Prop :=
  forall x y z, Through x y -> Through y z -> Through x z.

(* x ultimately depends on y: a chain of one or more steps of dependence.
   (clos_trans is the standard library's "one or more steps" of a relation.) *)
Definition UltimatelyDependsOn : Thing -> Thing -> Prop := clos_trans Thing DependsOn.

(* Step 1: ultimate dependence means having one's existence through. *)
Lemma ultimate_dependence_is_through :
  MP002 -> MP003_Inherited ->
  forall x y, UltimatelyDependsOn x y -> Through x y.
Proof.
  intros M2 M3 x y H. induction H as [x y Hxy | x y z _ IH1 _ IH2].
  - exact (M2 x y Hxy).
  - exact (M3 x y z IH1 IH2).
Qed.

(* Step 2 (premise 3): nothing ultimately depends on itself, however long
   the circle. *)
Theorem no_circular_dependence :
  MP001 -> MP002 -> MP003_Inherited ->
  forall x, ~ UltimatelyDependsOn x x.
Proof.
  intros M1 M2 M3 x Hc.
  apply clos_trans_t1n_iff in Hc.
  assert (Hgen : forall a b, clos_trans_1n Thing DependsOn a b -> a = b -> False).
  { intros a b H. destruct H as [b Hab | m b Ham Hmb]; intro Heq; subst b.
    - (* circle of one step: a gives existence to itself; excluded by PR-002 *)
      exact (NoSelfCreation.no_self_creation Thing Gives Through M1 M2 a Hab).
    - (* longer circle: a depends on m, and m ultimately depends on a *)
      apply clos_trans_t1n_iff in Hmb.
      pose proof (ultimate_dependence_is_through M2 M3 m a Hmb) as Hthrough.
      exact (M1 a m Ham Hthrough). }
  exact (Hgen x x Hc eq_refl).
Qed.

(* Step 3: link to the chains of PR-001.  Between two positions of a maximal
   chain, the earlier thing ultimately depends on the later one. *)
Lemma chain_segment : forall u c,
  Exhaustiveness.MaximalChainFrom Thing DependsOn u c ->
  forall i k a b, c i = Some a -> c (i + S k) = Some b -> UltimatelyDependsOn a b.
Proof.
  intros u c [_ [Hlink [Hstay _]]] i k.
  induction k as [| k IH]; intros a b Ha Hb.
  - apply t_step. rewrite Nat.add_1_r in Hb. exact (Hlink i a b Ha Hb).
  - destruct (c (i + S k)) as [m |] eqn:Hm.
    + apply t_trans with m.
      * exact (IH a m Ha eq_refl).
      * apply t_step. apply (Hlink (i + S k) m b Hm).
        rewrite <- Hb. f_equal. lia.
    + exfalso. pose proof (Hstay (i + S k) Hm) as Hn.
      replace (S (i + S k)) with (i + S (S k)) in Hn by lia. congruence.
Qed.

(* Step 4: no maximal chain contains any thing twice. *)
Theorem no_repetition_in_chains :
  MP001 -> MP002 -> MP003_Inherited ->
  forall u c, Exhaustiveness.MaximalChainFrom Thing DependsOn u c ->
  ~ Exhaustiveness.Repeats Thing c.
Proof.
  intros M1 M2 M3 u c Hc [i [j [x [Hij [Hi Hj]]]]].
  apply (no_circular_dependence M1 M2 M3 x).
  replace j with (i + S (j - i - 1)) in Hj by lia.
  exact (chain_segment u c Hc i (j - i - 1) x x Hi Hj).
Qed.

(* Step 5: cases 1 and 2 of PR-001 are eliminated. *)
Corollary cases_1_and_2_eliminated :
  MP001 -> MP002 -> MP003_Inherited ->
  forall u c, Exhaustiveness.MaximalChainFrom Thing DependsOn u c ->
  ~ Exhaustiveness.SelfDependence Thing c /\ ~ Exhaustiveness.Circularity Thing c.
Proof.
  intros M1 M2 M3 u c Hc. split.
  - intro Hs. exact (no_repetition_in_chains M1 M2 M3 u c Hc
                       (Exhaustiveness.self_repeats Thing c Hs)).
  - intros [Hr _]. exact (no_repetition_in_chains M1 M2 M3 u c Hc Hr).
Qed.

End Circles.

(* ------------------------------------------------------------------ *)
(* Checks.  Illustrations of logical possibility only; no claim about what
   exists.  Three things A, B, C. *)

Inductive Three := A | B | C.

(* A circle: B gives existence to A, C to B, A to C
   (A depends on B, B on C, C on A). *)
Definition CircleGives (y x : Three) : Prop :=
  match y, x with B, A | C, B | A, C => True | _, _ => False end.

(* A straight line: B gives existence to A, C to B. *)
Definition LineGives (y x : Three) : Prop :=
  match y, x with B, A | C, B => True | _, _ => False end.
(* In the line, A has its existence through B and C; B through C. *)
Definition LineThrough (x y : Three) : Prop :=
  match x, y with A, B | A, C | B, C => True | _, _ => False end.

(* 1. Non-vacuity: all three postulates hold while a real chain of giving
      of length two occurs. *)
Example postulates_allow_chains :
  MP001 Three LineGives LineThrough /\ MP002 Three LineGives LineThrough /\
  MP003_Inherited Three LineThrough /\ LineGives B A /\ LineGives C B.
Proof.
  unfold MP001, MP002, NoSelfCreation.MP001_Giver, NoSelfCreation.MP002_Receiver,
         MP003_Inherited.
  repeat split.
  - intros [] [] H1 H2; simpl in *; tauto.
  - intros [] [] H; simpl in *; tauto.
  - intros [] [] [] H1 H2; simpl in *; tauto.
Qed.

(* 2. Countermodel without MP-003: in the circle, let "through" hold only for
      the direct givers.  MP-001 and MP-002 hold, yet A ultimately depends
      on A. *)
Example without_MP003_a_circle_is_consistent :
  MP001 Three CircleGives (fun x y => CircleGives y x) /\
  MP002 Three CircleGives (fun x y => CircleGives y x) /\
  UltimatelyDependsOn Three CircleGives A A.
Proof.
  unfold MP001, MP002, NoSelfCreation.MP001_Giver, NoSelfCreation.MP002_Receiver.
  split; [| split].
  - intros [] [] H1 H2; simpl in *; tauto.
  - intros [] [] H; simpl in *; tauto.
  - apply t_trans with B; [apply t_step; exact I |].
    apply t_trans with C; apply t_step; exact I.
Qed.

(* 3. Countermodel without MP-001: in the circle, let everything have its
      existence through everything.  MP-002 and MP-003 hold, and the circle
      stands. *)
Example without_MP001_a_circle_is_consistent :
  MP002 Three CircleGives (fun _ _ => True) /\
  MP003_Inherited Three (fun _ _ => True) /\
  UltimatelyDependsOn Three CircleGives A A.
Proof.
  unfold MP002, NoSelfCreation.MP002_Receiver, MP003_Inherited.
  split; [| split].
  - intros; exact I.
  - intros; exact I.
  - apply t_trans with B; [apply t_step; exact I |].
    apply t_trans with C; apply t_step; exact I.
Qed.

(* 4. Countermodel without MP-002: in the circle, let nothing have its
      existence through anything.  MP-001 and MP-003 hold, and the circle
      stands. *)
Example without_MP002_a_circle_is_consistent :
  MP001 Three CircleGives (fun _ _ => False) /\
  MP003_Inherited Three (fun _ _ => False) /\
  UltimatelyDependsOn Three CircleGives A A.
Proof.
  unfold MP001, NoSelfCreation.MP001_Giver, MP003_Inherited.
  split; [| split].
  - intros x y _ H. exact H.
  - intros x y z H _. exact H.
  - apply t_trans with B; [apply t_step; exact I |].
    apply t_trans with C; apply t_step; exact I.
Qed.

Print Assumptions ultimate_dependence_is_through.
Print Assumptions no_circular_dependence.
Print Assumptions chain_segment.
Print Assumptions no_repetition_in_chains.
Print Assumptions cases_1_and_2_eliminated.
Print Assumptions postulates_allow_chains.
Print Assumptions without_MP003_a_circle_is_consistent.
Print Assumptions without_MP001_a_circle_is_consistent.
Print Assumptions without_MP002_a_circle_is_consistent.

End NoCircularCreation.

(* ======================================================================
   PR-004: no regress in the giving of existence
   ====================================================================== *)
Module NoRegressOfGiving.

(* PR-004: There is no regress in the giving of existence.  Whatever has its
   existence through another receives it from something that has existence of
   itself.  Proximate causes (which only transform what already exists) may
   form any structure, including an endless horizontal regress; the giving of
   existence may not.

   Rests on:
   - observational premise OP-001, stated below and used only as an explicit
     condition of the theorems;
   - PR-001 and PR-002, reused for chains and for DependsOn.
   No axiom is used.  Nothing is assumed to exist.  No notion of time
   appears. *)


Section Giving.

(* 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 Proximate : Thing -> Thing -> Prop.  (* Proximate y x : y is a proximate cause of x *)
Variable Exists : Thing -> Prop.              (* Exists x      : x actually exists *)

(* Conditional definitions. *)
(* x has its existence through another: something gives existence to x. *)
Definition ThroughAnother (x : Thing) : Prop := exists y, Gives y x.
(* x has existence of itself: x exists, and nothing gives existence to x. *)
Definition OfItself (x : Thing) : Prop := Exists x /\ ~ ThroughAnother x.

(* OP-001: only what has existence of itself can give existence.  Whatever has
   its existence through another can at most be a proximate cause.
   ([Proximate] is deliberately left unrestricted: proximate causation is not
   the giving of existence.) *)
Definition OP001_OnlySelfExistentGives : Prop :=
  forall x y, Gives y x -> OfItself y.

(* Premise 4: whatever has its existence through another receives it from
   something that has existence of itself. *)
Theorem giver_is_self_existent :
  OP001_OnlySelfExistentGives ->
  forall x, ThroughAnother x -> exists b, Gives b x /\ OfItself b.
Proof.
  intros OP x [y Hyx]. exists y. split; [exact Hyx | exact (OP x y Hyx)].
Qed.

(* No two-step giving: nothing that receives existence gives it onward. *)
Theorem no_two_step_giving :
  OP001_OnlySelfExistentGives ->
  forall x y z, Gives y x -> ~ Gives z y.
Proof.
  intros OP x y z Hyx Hzy. destruct (OP x y Hyx) as [_ Hnot].
  apply Hnot. exists z. exact Hzy.
Qed.

End Giving.

(* ------------------------------------------------------------------ *)
(* Link to PR-001: no chain of existence-giving is an infinite regress. *)

Section Chains.

Variable Thing : Type.
Variable Gives : Thing -> Thing -> Prop.
Variable Exists : Thing -> Prop.

Definition DependsOn : Thing -> Thing -> Prop := NoSelfCreation.DependsOn Thing Gives.

(* Every maximal chain of existence-giving stops by its third position: the
   thing's giver has existence of itself, so nothing lies beyond it. *)
Theorem giving_chain_stops :
  OP001_OnlySelfExistentGives Thing Gives Exists ->
  forall u c, Exhaustiveness.MaximalChainFrom Thing DependsOn u c ->
  c 2 = None.
Proof.
  intros OP u c [_ [Hlink [Hstay _]]].
  destruct (c 1) as [y |] eqn:H1.
  - destruct (c 2) as [z |] eqn:H2; [| reflexivity].
    exfalso. destruct (c 0) as [x |] eqn:H0.
    + apply (no_two_step_giving Thing Gives Exists OP x y z).
      * exact (Hlink 0 x y H0 H1).
      * exact (Hlink 1 y z H1 H2).
    + pose proof (Hstay 0 H0) as Hn. congruence.
  - exact (Hstay 1 H1).
Qed.

(* Hence case 3 of PR-001 (infinite regress) never occurs for existence-giving. *)
Corollary no_regress_of_giving :
  OP001_OnlySelfExistentGives Thing Gives Exists ->
  forall u c, Exhaustiveness.MaximalChainFrom Thing DependsOn u c ->
  ~ Exhaustiveness.InfiniteRegress Thing c.
Proof.
  intros OP u c Hc [Hnever _].
  exact (Hnever 2 (giving_chain_stops OP u c Hc)).
Qed.

End Chains.

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

(* 1. Countermodel: without OP-001, an infinite regress of existence-giving is
      consistent.  Numbers 0, 1, 2, ...: each is given existence by the next,
      and all exist. *)
Example without_OP001_regress_of_giving_is_consistent :
  let G := fun (y x : nat) => y = S x in
  let E := fun (_ : nat) => True in
  (forall n, G (S n) n) /\ (forall n, E n) /\
  ~ OP001_OnlySelfExistentGives nat G E.
Proof.
  simpl. split; [| split].
  - intro n. reflexivity.
  - intro n. exact I.
  - intro OP. destruct (OP 0 1 eq_refl) as [_ Hnot].
    apply Hnot. exists 2. reflexivity.
Qed.

(* 2. The rebuttal "then do we not exist?"  A base T (None) gives existence to
      every member of an endless horizontal chain 0, 1, 2, ... (Some n).  Each
      member is a proximate cause of the one before it.  OP-001 holds, and
      every member truly exists, has its existence through another, and is a
      real proximate cause.  So OP-001 denies only that dependent things GIVE
      existence, never that they exist or act. *)
Example dependent_things_exist_and_act :
  let G := fun (y x : option nat) => y = None /\ exists n, x = Some n in
  let P := fun (y x : option nat) => exists n, x = Some n /\ y = Some (S n) in
  let E := fun (_ : option nat) => True in
  OP001_OnlySelfExistentGives (option nat) G E /\
  OfItself (option nat) G E None /\
  (forall n, E (Some n) /\ ThroughAnother (option nat) G (Some n) /\
             P (Some (S n)) (Some n)).
Proof.
  simpl.
  assert (Hbase : OfItself (option nat) (fun y x => y = None /\ exists n, x = Some n)
                    (fun _ => True) None).
  { split; [exact I |]. intros [y [_ [n Hn]]]. discriminate. }
  split; [| split].
  - intros x y [Hy _]. subst y. exact Hbase.
  - exact Hbase.
  - intro n. split; [exact I | split].
    + exists None. split; [reflexivity | exists n; reflexivity].
    + exists n. split; reflexivity.
Qed.

(* 3. The recursion model, as proximate dependence: U(n) depends on U(n+1),
      without end and without a base.  "All exist" and "none exist" both fit
      the chain's links, so the proximate chain alone does not settle whether
      anything exists. *)
Example recursion_without_base_worlds_A_and_B :
  let link := fun (y x : nat) => y = S x in
  (forall x, True <-> exists y, link y x /\ True) /\
  (forall x, False <-> exists y, link y x /\ False).
Proof.
  simpl. split.
  - intro x. split; [intros _; exists (S x); split; [reflexivity | exact I] | intros _; exact I].
  - intro x. split; [intro H; contradiction | intros [y [_ H]]; exact H].
Qed.

(* 4. The recursion model with a base: U(0) ... U(k-1) each depend on the
      next, and U(k) is a base.  If the base exists, every world that fits the
      links has all of U(0) ... U(k) existing: only World A remains. *)
Example recursion_with_base_forces_world_A : forall (k : nat) (E : nat -> Prop),
  (forall x, x < k -> (E x <-> E (S x))) -> E k ->
  forall n, n <= k -> E n.
Proof.
  intros k E Hlink Hbase.
  assert (Hdown : forall d, d <= k -> E (k - d)).
  { induction d as [| d IH]; intros Hd.
    - rewrite Nat.sub_0_r. exact Hbase.
    - assert (Hm : k - S d < k) by lia.
      apply (proj2 (Hlink (k - S d) Hm)).
      replace (S (k - S d)) with (k - d) by lia. apply IH. lia. }
  intros n Hn. replace n with (k - (k - n)) by lia. apply Hdown. lia.
Qed.

Print Assumptions giver_is_self_existent.
Print Assumptions no_two_step_giving.
Print Assumptions giving_chain_stops.
Print Assumptions no_regress_of_giving.
Print Assumptions without_OP001_regress_of_giving_is_consistent.
Print Assumptions dependent_things_exist_and_act.
Print Assumptions recursion_without_base_worlds_A_and_B.
Print Assumptions recursion_with_base_forces_world_A.

End NoRegressOfGiving.

(* ======================================================================
   PR-006: every existent is necessary or possible in itself, not both
   ====================================================================== *)
Module Division.

(* PR-006 (dalil al-imkan, step 1): every existent is either necessary in
   itself (wajib al-wujud bi-dhatihi) or possible in itself (mumkin al-wujud
   bi-dhatihi), but not both.

   Definitions follow Ibn Sina: an existent is necessary in itself when its
   existence is from its essence, and possible in itself when it is not.
   Whether the possible needs a cause (its iḥtiyaj) is NOT part of the
   definition; it is a later step (step 3), to be proved.

   Logical principle used: excluded middle (classic), for exhaustiveness
   only.  Nothing else is assumed.  Nothing is assumed to exist.  No notion of
   time appears. *)


Section Div.

(* Primitive vocabulary.  Nothing is assumed about any of these. *)
Variable Thing : Type.
Variable Exists : Thing -> Prop.                    (* x exists *)
Variable EssenceIncludesExistence : Thing -> Prop.  (* x's existence is from its essence *)

(* Conditional definitions. *)
Definition NecessaryInItself (x : Thing) : Prop :=
  Exists x /\ EssenceIncludesExistence x.
Definition PossibleInItself (x : Thing) : Prop :=
  Exists x /\ ~ EssenceIncludesExistence x.

(* Step 1, exhaustive: every existent is necessary or possible in itself. *)
Theorem division_exhaustive : forall x,
  Exists x -> NecessaryInItself x \/ PossibleInItself x.
Proof.
  intros x Hx.
  destruct (classic (EssenceIncludesExistence x)) as [He | Hne].
  - left. split; assumption.
  - right. split; assumption.
Qed.

(* Step 1, exclusive: no existent is both. *)
Theorem division_exclusive : forall x,
  ~ (NecessaryInItself x /\ PossibleInItself x).
Proof.
  intros x [[_ He] [_ Hne]]. exact (Hne He).
Qed.

(* Step 1, as stated: every existent is one or the other, but not both. *)
Theorem division : forall x,
  Exists x ->
  (NecessaryInItself x \/ PossibleInItself x) /\
  ~ (NecessaryInItself x /\ PossibleInItself x).
Proof.
  intros x Hx. split.
  - exact (division_exhaustive x Hx).
  - exact (division_exclusive x).
Qed.

End Div.

(* ------------------------------------------------------------------ *)
(* Checks: both sides of the division really occur, so neither definition
   is empty.  Illustrations of logical possibility only. *)

(* A world with one necessary and one possible existent. *)
Example both_kinds_occur :
  let E := fun (_ : bool) => True in
  let Ess := fun (x : bool) => x = true in
  NecessaryInItself bool E Ess true /\ PossibleInItself bool E Ess false.
Proof.
  simpl. split.
  - split; [exact I | reflexivity].
  - split; [exact I | discriminate].
Qed.

Print Assumptions division_exhaustive.
Print Assumptions division_exclusive.
Print Assumptions division.
Print Assumptions both_kinds_occur.

End Division.

(* ======================================================================
   PR-008: the possible requires a murajjih
   ====================================================================== *)
Module PossibleRequiresMurajjih.

(* PR-008 (dalil al-imkan, step 3): if an existent is possible in itself, its
   existence and non-existence are both possible [in itself]; therefore its
   existence requires a determining cause (murajjih).

   (3a) the equipoise is definitional: under PR-006, "possible in itself"
        means that nothing in its essence secures its existence, while its
        existence is not ruled out (it exists).
   (3b) the need for a murajjih is substantive: it follows from meaning
        postulate MP-008, "no preponderance without a preponderator"
        (la tarjih bi-la murajjih).  This is Ibn Sina's thesis that the
        ground of need is possibility (illat al-ihtiyaj hiya al-imkan):
        nothing about time is used.

   Rests on:
   - PR-006 (definitions of necessary and possible in itself);
   - PR-004 (definition of "has its existence through another");
   - MP-008, an explicit condition of the theorem;
   - excluded middle (classic), in (3b) only.
   Nothing is assumed to exist.  No notion of time appears. *)


Section Step3.

(* Primitive vocabulary.  Nothing is assumed about any of these. *)
Variable Thing : Type.
Variable Exists : Thing -> Prop.                    (* x exists *)
Variable EssenceIncludesExistence : Thing -> Prop.  (* x's existence is from its essence *)
Variable Gives : Thing -> Thing -> Prop.            (* Gives y x : y gives existence to x *)

(* Reused definitions. *)
Definition PossibleInItself : Thing -> Prop :=
  Division.PossibleInItself Thing Exists EssenceIncludesExistence.
Definition ThroughAnother : Thing -> Prop :=
  NoRegressOfGiving.ThroughAnother Thing Gives.

(* MP-008, no preponderance without a preponderator: whatever exists, with
   nothing giving it existence, has its existence from its essence.  Existence
   comes either from what a thing is, or from something that gives it. *)
Definition MP008_NoPreponderanceWithoutPreponderator : Prop :=
  forall x, Exists x -> ~ ThroughAnother x -> EssenceIncludesExistence x.

(* (3a) Equipoise: for the possible in itself, nothing in its essence secures
   its existence, and its existence is not ruled out, since it exists. *)
Theorem possible_equipoise : forall x,
  PossibleInItself x -> ~ EssenceIncludesExistence x /\ Exists x.
Proof.
  intros x [Hx Hne]. split; assumption.
Qed.

(* (3b) Step 3: the possible in itself requires a murajjih. *)
Theorem possible_requires_murajjih :
  MP008_NoPreponderanceWithoutPreponderator ->
  forall x, PossibleInItself x -> ThroughAnother x.
Proof.
  intros M8 x [Hx Hne]. apply NNPP. intro Hn.
  exact (Hne (M8 x Hx Hn)).
Qed.

End Step3.

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

(* 1. Countermodel without MP-008 (the "brute fact"): a thing that exists,
      whose existence is not from its essence, and which nothing gives
      existence to.  It is possible in itself yet has no murajjih.  So MP-008
      is needed. *)
Example without_MP008_possible_without_cause :
  let E := fun (_ : unit) => True in
  let Ess := fun (_ : unit) => False in
  let G := fun (_ _ : unit) => False in
  PossibleInItself unit E Ess tt /\ ~ ThroughAnother unit G tt.
Proof.
  simpl. split.
  - split; [exact I | intro H; exact H].
  - intros [y H]. exact H.
Qed.

(* 2. Non-vacuity: MP-008 holds in a world with a necessary thing (true),
      whose existence is from its essence, giving existence to a possible
      thing (false). *)
Example mp008_allows_possibles :
  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_NoPreponderanceWithoutPreponderator bool E Ess G /\
  PossibleInItself bool E Ess false /\ ThroughAnother bool G false.
Proof.
  unfold MP008_NoPreponderanceWithoutPreponderator, ThroughAnother,
         NoRegressOfGiving.ThroughAnother.
  simpl. split; [| split].
  - intros [] _ Hn; [reflexivity |].
    exfalso. apply Hn. exists true. split; reflexivity.
  - split; [exact I | discriminate].
  - exists true. split; reflexivity.
Qed.

Print Assumptions possible_equipoise.
Print Assumptions possible_requires_murajjih.
Print Assumptions without_MP008_possible_without_cause.
Print Assumptions mp008_allows_possibles.

End PossibleRequiresMurajjih.

(* ======================================================================
   PR-009: the aggregate of possibles is itself possible
   ====================================================================== *)
Module AggregateIsPossible.

(* PR-009 (dalil al-imkan, steps 5 and 6).

   Step 5: consider the aggregate of all existing beings that are possible in
   themselves.  No possible lies outside it.
   Step 6: the aggregate, considered collectively, is itself possible in
   itself, and therefore requires a determining cause.

   Rests on:
   - PR-006 (definitions of necessary and possible in itself);
   - PR-008 (step 3: the possible requires a murajjih), with MP-008;
   - meaning postulates MP-009 and MP-010, explicit conditions below;
   - excluded middle, only through PR-008.
   Nothing is assumed to exist except as stated in the conditions.  No notion
   of time appears. *)


Section Aggregate.

(* 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 MemberOf : Thing -> Thing -> Prop.   (* MemberOf p A : p is a member of the collection A *)

(* Reused definitions. *)
Definition PossibleInItself : Thing -> Prop :=
  Division.PossibleInItself Thing Exists EssenceIncludesExistence.
Definition ThroughAnother : Thing -> Prop :=
  NoRegressOfGiving.ThroughAnother Thing Gives.
Definition MP008 : Prop :=
  PossibleRequiresMurajjih.MP008_NoPreponderanceWithoutPreponderator
    Thing Exists EssenceIncludesExistence Gives.

(* Step 5 (definition): A is the aggregate of all existing possibles when its
   members are exactly the existing possibles (other than the aggregate
   itself), and it is not a member of itself. *)
Definition AggregateOfPossibles (A : Thing) : Prop :=
  (forall p, p <> A -> (MemberOf p A <-> PossibleInItself p)) /\ ~ MemberOf A A.

(* Step 5: no possible, other than the aggregate itself, lies outside it. *)
Lemma no_possible_outside : forall A,
  AggregateOfPossibles A -> forall p, p <> A -> PossibleInItself p -> MemberOf p A.
Proof.
  intros A [HA _] p Hne Hp. exact (proj2 (HA p Hne) Hp).
Qed.

(* MP-009, the aggregate is a whole: if some possible exists, there is an
   existing aggregate of all existing possibles. *)
Definition MP009_AggregateExists : Prop :=
  (exists p, PossibleInItself p) -> exists A, AggregateOfPossibles A /\ Exists A.

(* MP-010, no necessity from possibles: a collection with members, all of
   whose members have existence not from their nature, does not have its
   existence from its own nature either. *)
Definition MP010_NoNecessityFromPossibles : Prop :=
  forall A, (exists p, MemberOf p A) ->
    (forall p, MemberOf p A -> ~ EssenceIncludesExistence p) ->
    ~ EssenceIncludesExistence A.

(* The members of the aggregate all have existence not from their nature. *)
Lemma members_are_possible : forall A,
  AggregateOfPossibles A -> forall p, MemberOf p A -> PossibleInItself p.
Proof.
  intros A [HA Hnot] p Hm.
  assert (Hne : p <> A). { intro Heq. subst p. exact (Hnot Hm). }
  exact (proj1 (HA p Hne) Hm).
Qed.

(* Step 6, first part: if some possible other than the aggregate exists, the
   aggregate is itself possible in itself. *)
Theorem aggregate_is_possible :
  MP010_NoNecessityFromPossibles ->
  forall A, AggregateOfPossibles A -> Exists A ->
  (exists p, p <> A /\ PossibleInItself p) ->
  PossibleInItself A.
Proof.
  intros M10 A HA HexA [p [Hne Hp]]. split; [exact HexA |].
  apply M10.
  - exists p. exact (no_possible_outside A HA p Hne Hp).
  - intros q Hq. destruct (members_are_possible A HA q Hq) as [_ Hnq]. exact Hnq.
Qed.

(* Step 6, second part: therefore the aggregate requires a murajjih (by PR-008). *)
Theorem aggregate_requires_murajjih :
  MP008 -> MP010_NoNecessityFromPossibles ->
  forall A, AggregateOfPossibles A -> Exists A ->
  (exists p, p <> A /\ PossibleInItself p) ->
  ThroughAnother A.
Proof.
  intros M8 M10 A HA HexA Hp.
  exact (PossibleRequiresMurajjih.possible_requires_murajjih
           Thing Exists EssenceIncludesExistence Gives M8 A
           (aggregate_is_possible M10 A HA HexA Hp)).
Qed.

(* Steps 5 and 6 together, from MP-009: if some possible exists, there is an
   existing aggregate of all possibles, it is possible in itself, and it
   requires a murajjih. *)
Theorem steps_5_and_6 :
  MP008 -> MP009_AggregateExists -> MP010_NoNecessityFromPossibles ->
  forall p, PossibleInItself p ->
  exists A, AggregateOfPossibles A /\ Exists A /\
    ((exists q, q <> A /\ PossibleInItself q) ->
     PossibleInItself A /\ ThroughAnother A).
Proof.
  intros M8 M9 M10 p Hp.
  destruct (M9 (ex_intro _ p Hp)) as [A [HA HexA]].
  exists A. split; [exact HA |]. split; [exact HexA |].
  intro Hq. split.
  - exact (aggregate_is_possible M10 A HA HexA Hq).
  - exact (aggregate_requires_murajjih M8 M10 A HA HexA Hq).
Qed.

End Aggregate.

(* ------------------------------------------------------------------ *)
(* Checks.  Illustrations of logical possibility only; no claim about what
   exists.  Things: a necessary N, two possibles P1 and P2, their aggregate
   Agg. *)

Inductive Th := N | P1 | P2 | Agg.

Definition Mem (p a : Th) : Prop := (p = P1 \/ p = P2) /\ a = Agg.
Definition EssN (x : Th) : Prop := x = N.
Definition GivN (y x : Th) : Prop := y = N /\ x <> N.

(* The aggregate facts for Agg, when Ess picks out exactly the given things. *)
Lemma agg_is_aggregate : forall Ess : Th -> Prop,
  (forall x, Ess x <-> x = N \/ False) ->
  AggregateOfPossibles Th (fun _ => True) Ess Mem Agg.
Proof.
  intros Ess HEss. unfold AggregateOfPossibles, PossibleInItself, Division.PossibleInItself, Mem.
  split.
  - intros q Hne. split.
    + intros [[H|H] _]; subst q; split; try exact I; intro He;
        destruct (proj1 (HEss _) He) as [He'|[]]; discriminate.
    + intros [_ Hn]. destruct q.
      * exfalso. apply Hn. apply (proj2 (HEss N)). left. reflexivity.
      * split; [left; reflexivity | reflexivity].
      * split; [right; reflexivity | reflexivity].
      * exfalso. apply Hne. reflexivity.
  - intros [[H|H] _]; discriminate.
Qed.

(* 1. Consistency and non-vacuity: MP-008, MP-009 and MP-010 all hold; Agg is
      the aggregate of all possibles, it is possible in itself, and N gives
      it existence. *)
Example all_hold_together :
  let E := fun (_ : Th) => True in
  MP008 Th E EssN GivN /\
  MP009_AggregateExists Th E EssN Mem /\
  MP010_NoNecessityFromPossibles Th EssN Mem /\
  AggregateOfPossibles Th E EssN Mem Agg /\
  PossibleInItself Th E EssN Agg /\ ThroughAnother Th GivN Agg.
Proof.
  intro E.
  assert (HEss : forall x, EssN x <-> x = N \/ False).
  { intro x. unfold EssN. split; [intro H; left; exact H | intros [H|[]]; exact H]. }
  pose proof (agg_is_aggregate EssN HEss) as Hagg.
  split; [| split; [| split; [| split; [| split]]]].
  - unfold MP008, PossibleRequiresMurajjih.MP008_NoPreponderanceWithoutPreponderator,
           NoRegressOfGiving.ThroughAnother, EssN, GivN.
    intros x _ Hn. destruct x; try reflexivity; exfalso; apply Hn;
      exists N; (split; [reflexivity | discriminate]).
  - intros _. exists Agg. split; [exact Hagg | exact I].
  - unfold MP010_NoNecessityFromPossibles, Mem, EssN.
    intros A [q [_ HA]] _. subst A. discriminate.
  - exact Hagg.
  - unfold PossibleInItself, Division.PossibleInItself, EssN. split; [exact I | discriminate].
  - unfold ThroughAnother, NoRegressOfGiving.ThroughAnother, GivN.
    exists N. split; [reflexivity | discriminate].
Qed.

(* 2. Countermodel without MP-010: the aggregate of possibles has its
      existence from its own nature, so it is necessary, not possible.  So
      MP-010 is needed. *)
Example without_MP010_aggregate_not_possible :
  let E := fun (_ : Th) => True in
  let Ess := fun (x : Th) => x = N \/ x = Agg in
  AggregateOfPossibles Th E Ess Mem Agg /\ ~ PossibleInItself Th E Ess Agg.
Proof.
  intros E Ess. unfold AggregateOfPossibles, PossibleInItself, Division.PossibleInItself, Mem, Ess, E.
  split; [split |].
  - intros q Hne. split.
    + intros [[H|H] _]; subst q; split; try exact I; intros [H'|H']; discriminate.
    + intros [_ Hn]. destruct q.
      * exfalso. apply Hn. left. reflexivity.
      * split; [left; reflexivity | reflexivity].
      * split; [right; reflexivity | reflexivity].
      * exfalso. apply Hne. reflexivity.
  - intros [[H|H] _]; discriminate.
  - intros [_ H]. apply H. right. reflexivity.
Qed.

(* 3. Countermodel without MP-009: possibles exist, but nothing is their
      aggregate (no collection has members).  So MP-009 is needed. *)
Example without_MP009_no_aggregate :
  let E := fun (_ : Th) => True in
  let NoMem := fun (_ _ : Th) => False in
  PossibleInItself Th E EssN P1 /\
  ~ (exists A, AggregateOfPossibles Th E EssN NoMem A).
Proof.
  intros E NoMem. unfold AggregateOfPossibles, PossibleInItself, Division.PossibleInItself, EssN, E, NoMem.
  split.
  - split; [exact I | discriminate].
  - intros [A [HA _]].
    assert (HP1 : True /\ P1 <> N) by (split; [exact I | discriminate]).
    assert (HP2 : True /\ P2 <> N) by (split; [exact I | discriminate]).
    destruct A.
    + exact (proj2 (HA P1 ltac:(discriminate)) HP1).
    + exact (proj2 (HA P2 ltac:(discriminate)) HP2).
    + exact (proj2 (HA P1 ltac:(discriminate)) HP1).
    + exact (proj2 (HA P1 ltac:(discriminate)) HP1).
Qed.

Print Assumptions no_possible_outside.
Print Assumptions members_are_possible.
Print Assumptions aggregate_is_possible.
Print Assumptions aggregate_requires_murajjih.
Print Assumptions steps_5_and_6.
Print Assumptions agg_is_aggregate.
Print Assumptions all_hold_together.
Print Assumptions without_MP010_aggregate_not_possible.
Print Assumptions without_MP009_no_aggregate.

End AggregateIsPossible.

(* ======================================================================
   PR-011: the universe is caused (the division)
   ====================================================================== *)
Module UniverseIsCaused.

(* 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. *)


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.

End UniverseIsCaused.

(* ======================================================================
   Dalil al-kalima: the conclusion (conditional form)
   ====================================================================== *)
Module KalimaConclusion.

(* 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. *)


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.

End KalimaConclusion.

(* ======================================================================
   Dalil al-kalima: the conclusion without its "if"
   ====================================================================== *)
Module KalimaUnconditional.

(* 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. *)


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.

End KalimaUnconditional.