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

   All twelve steps and the conclusion, by proof (a) (the aggregate route,
   Ibn Sina) and proof (b) (the short route through OP-001).

   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 ImkanComplete.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-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-007: the necessary in itself cannot fail to exist
   ====================================================================== *)
Module NecessaryCannotFail.

(* PR-007 (dalil al-imkan, step 2): if an existent is necessary in itself, its
   non-existence is not possible.

   Rests on:
   - PR-006, reused for its definitions of "necessary in itself" and
     "possible in itself";
   - meaning postulate MP-007, stated below as an explicit condition.
   No axiom is used.  Nothing is assumed to exist.  No notion of time
   appears.

   Possibility is modelled with worlds (ways things could be): "the
   non-existence of x is possible" means some world lacks x; "x exists" means
   x exists in the actual world. *)


Section Step2.

(* Primitive vocabulary.  Nothing is assumed about any of these. *)
Variable Thing : Type.
Variable World : Type.
Variable actual : World.
Variable ExistsIn : World -> Thing -> Prop.
Variable EssenceIncludesExistence : Thing -> Prop.

Definition Exists (x : Thing) : Prop := ExistsIn actual x.

(* Reused from PR-006. *)
Definition NecessaryInItself : Thing -> Prop :=
  Division.NecessaryInItself Thing Exists EssenceIncludesExistence.
Definition PossibleInItself : Thing -> Prop :=
  Division.PossibleInItself Thing Exists EssenceIncludesExistence.

(* The non-existence of x is possible: some world lacks x. *)
Definition NonExistencePossible (x : Thing) : Prop := exists w, ~ ExistsIn w x.

(* MP-007: what has existence from its essence exists in every world.  What
   it is guarantees that it is, wherever it is considered. *)
Definition MP007_EssentialExistenceCannotFail : Prop :=
  forall x, EssenceIncludesExistence x -> forall w, ExistsIn w x.

(* Step 2. *)
Theorem necessary_cannot_fail :
  MP007_EssentialExistenceCannotFail ->
  forall x, NecessaryInItself x -> ~ NonExistencePossible x.
Proof.
  intros M7 x [_ He] [w Hw]. exact (Hw (M7 x He w)).
Qed.

End Step2.

(* ------------------------------------------------------------------ *)
(* Checks.  Illustrations of logical possibility only; no claim about what
   exists.  Worlds are bool; the actual world is true. *)

(* 1. Countermodel without MP-007: a thing whose existence is from its
      essence, existing in the actual world but not in another.  It is
      necessary in itself, yet its non-existence is possible.  So MP-007 is
      needed. *)
Example without_MP007_necessary_could_fail :
  let EI := fun (w : bool) (_ : unit) => w = true in
  let Ess := fun (_ : unit) => True in
  NecessaryInItself unit bool true EI Ess tt /\ NonExistencePossible unit bool EI tt.
Proof.
  simpl. split.
  - split; [reflexivity | exact I].
  - exists false. discriminate.
Qed.

(* 2. Non-vacuity: MP-007 holds with one necessary thing, existing in every
      world, and one possible thing, which some world lacks. *)
Example mp007_allows_both :
  let EI := fun (w : bool) (x : bool) => x = true \/ w = true in
  let Ess := fun (x : bool) => x = true in
  MP007_EssentialExistenceCannotFail bool bool EI Ess /\
  NecessaryInItself bool bool true EI Ess true /\
  PossibleInItself bool bool true EI Ess false /\
  NonExistencePossible bool bool EI false.
Proof.
  unfold MP007_EssentialExistenceCannotFail. simpl.
  split; [| split; [| split]].
  - intros x Hx w. left. exact Hx.
  - split; [left; reflexivity | reflexivity].
  - split; [right; reflexivity | discriminate].
  - exists false. intros [H | H]; discriminate.
Qed.

(* 3. Necessary through another (wajib bi-ghayrihi): MP-007 does not force a
      possible thing ever to fail.  A thing possible in itself may exist in
      every world, necessitated by its cause, as in Ibn Sina's eternal
      world. *)
Example possible_may_never_fail :
  let EI := fun (_ : bool) (_ : bool) => True in
  let Ess := fun (x : bool) => x = true in
  MP007_EssentialExistenceCannotFail bool bool EI Ess /\
  PossibleInItself bool bool true EI Ess false /\
  ~ NonExistencePossible bool bool EI false.
Proof.
  unfold MP007_EssentialExistenceCannotFail. simpl.
  split; [| split].
  - intros. exact I.
  - split; [exact I | discriminate].
  - intros [w Hw]. exact (Hw I).
Qed.

Print Assumptions necessary_cannot_fail.
Print Assumptions without_MP007_necessary_could_fail.
Print Assumptions mp007_allows_both.
Print Assumptions possible_may_never_fail.

End NecessaryCannotFail.

(* ======================================================================
   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-010: the cause of the aggregate is outside it and necessary
   ====================================================================== *)
Module CauseOutsideIsNecessary.

(* PR-010 (dalil al-imkan, steps 7 to 11).

   Step 7:  a sufficient cause of the existence of the entire aggregate must
            account for the existence of every constituent.  If that cause is
            itself a member, or a subset of its members considered
            collectively, it would have to account for its own existence,
            contrary to step 4.
   Step 8:  neither an individual possible, nor a subset of possibles, nor an
            aggregate composed entirely of possibles can cause its own
            existence.
   Step 9:  the existence of the aggregate therefore requires a cause outside
            the aggregate of possibles.
   Step 10: by the exhaustive division, an existing cause that is not
            possible in itself is necessary in itself.
   Step 11: the cause upon which the possible depends is therefore a
            Necessary Existent.

   Rests on:
   - PR-002 and PR-003 (no self-giving, no circle of giving), with MP-001,
     MP-002, MP-003;
   - PR-006 (the division), PR-008 (step 3) and PR-009 (steps 5 and 6), with
     MP-008, MP-009, MP-010;
   - meaning postulates MP-011 and MP-012, explicit conditions below;
   - excluded middle, only through PR-006 and PR-008.
   Nothing is assumed to exist.  No notion of time appears. *)


Section CauseOutside.

(* 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.     (* Gives y x : y gives existence to x *)
Variable Through : Thing -> Thing -> Prop.   (* Through x y : x has its existence through y *)
Variable MemberOf : Thing -> Thing -> Prop.  (* MemberOf p A : p is a member of the collection A *)

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

(* y gives existence to x, directly or through intermediaries. *)
Definition UltimatelyGives : Thing -> Thing -> Prop := clos_trans Thing Gives.

(* MP-011, whole to members: whatever gives existence to a collection gives
   existence to each of its members, directly or through intermediaries.
   The collection's existence is its members' existence. *)
Definition MP011_WholeToMembers : Prop :=
  forall c A p, Gives c A -> MemberOf p A -> UltimatelyGives c p.

(* MP-012, what does not exist cannot give: whatever gives existence exists. *)
Definition MP012_GiverExists : Prop :=
  forall y x, Gives y x -> Exists y.

(* A circle of giving is a circle of dependence (PR-003's form). *)
Lemma giving_circle_is_dependence_circle : forall c,
  UltimatelyGives c c -> NoCircularCreation.UltimatelyDependsOn Thing Gives c c.
Proof.
  intros c H. apply (proj1 (clos_trans_transp_permute Thing Gives c c)). exact H.
Qed.

(* Step 7 (member): the cause of a collection is not one of its members. *)
Theorem cause_is_not_a_member :
  MP001 -> MP002 -> MP003 -> MP011_WholeToMembers ->
  forall c A, Gives c A -> ~ MemberOf c A.
Proof.
  intros M1 M2 M3 M11 c A Hg Hm.
  exact (NoCircularCreation.no_circular_dependence Thing Gives Through M1 M2 M3 c
           (giving_circle_is_dependence_circle c (M11 c A c Hg Hm))).
Qed.

(* Step 7 (the aggregate itself): nothing gives existence to itself (PR-002). *)
Theorem aggregate_does_not_cause_itself :
  MP001 -> MP002 -> forall A, ~ Gives A A.
Proof.
  intros M1 M2 A. exact (NoSelfCreation.no_self_creation Thing Gives Through M1 M2 A).
Qed.

(* Step 7 (a subset): an existing sub-collection of possibles, other than the
   aggregate, cannot give existence to the aggregate. *)
Theorem subset_does_not_cause_aggregate :
  MP001 -> MP002 -> MP003 -> MP010 -> MP011_WholeToMembers ->
  forall A B, AggregateOfPossibles A -> B <> A -> Exists B ->
  (exists p, MemberOf p B) -> (forall p, MemberOf p B -> MemberOf p A) ->
  ~ Gives B A.
Proof.
  intros M1 M2 M3 M10 M11 A B HA Hne HexB Hsome Hsub Hg.
  assert (HB : PossibleInItself B).
  { split; [exact HexB |]. apply M10; [exact Hsome |].
    intros p Hp. destruct (AggregateIsPossible.members_are_possible
                             Thing Exists EssenceIncludesExistence MemberOf A HA p (Hsub p Hp)) as [_ H].
    exact H. }
  apply (cause_is_not_a_member M1 M2 M3 M11 B A Hg).
  exact (AggregateIsPossible.no_possible_outside Thing Exists EssenceIncludesExistence MemberOf
           A HA B Hne HB).
Qed.

(* Step 8: no individual possible, no sub-collection of possibles, and not
   the aggregate itself, gives the aggregate existence from within. *)
Theorem step8 :
  MP001 -> MP002 -> MP003 -> MP010 -> MP011_WholeToMembers ->
  forall A, AggregateOfPossibles A ->
    (forall x, ~ Gives x x) /\
    ~ Gives A A /\
    (forall c, MemberOf c A -> ~ Gives c A) /\
    (forall B, B <> A -> Exists B -> (exists p, MemberOf p B) ->
       (forall p, MemberOf p B -> MemberOf p A) -> ~ Gives B A).
Proof.
  intros M1 M2 M3 M10 M11 A HA. split; [| split; [| split]].
  - intro x. exact (NoSelfCreation.no_self_creation Thing Gives Through M1 M2 x).
  - exact (aggregate_does_not_cause_itself M1 M2 A).
  - intros c Hm Hg. exact (cause_is_not_a_member M1 M2 M3 M11 c A Hg Hm).
  - intros B. exact (subset_does_not_cause_aggregate M1 M2 M3 M10 M11 A B HA).
Qed.

(* Step 9: whatever gives the aggregate existence lies outside the
   aggregate: it is not a member, it is not the aggregate, and so it is not
   possible in itself. *)
Theorem cause_is_outside :
  MP001 -> MP002 -> MP003 -> MP011_WholeToMembers ->
  forall A c, AggregateOfPossibles A -> Gives c A ->
  ~ MemberOf c A /\ c <> A /\ ~ PossibleInItself c.
Proof.
  intros M1 M2 M3 M11 A c HA Hg.
  assert (Hnm : ~ MemberOf c A) by exact (cause_is_not_a_member M1 M2 M3 M11 c A Hg).
  assert (Hne : c <> A).
  { intro Heq. subst c. exact (aggregate_does_not_cause_itself M1 M2 A Hg). }
  split; [exact Hnm |]. split; [exact Hne |].
  intro Hp. apply Hnm.
  exact (AggregateIsPossible.no_possible_outside Thing Exists EssenceIncludesExistence MemberOf
           A HA c Hne Hp).
Qed.

(* Steps 10 and 11: that cause exists and is not possible, so by the
   division it is necessary in itself. *)
Theorem cause_is_necessary :
  MP001 -> MP002 -> MP003 -> MP011_WholeToMembers -> MP012_GiverExists ->
  forall A c, AggregateOfPossibles A -> Gives c A -> NecessaryInItself c.
Proof.
  intros M1 M2 M3 M11 M12 A c HA Hg.
  destruct (cause_is_outside M1 M2 M3 M11 A c HA Hg) as [_ [_ Hnp]].
  destruct (Division.division_exhaustive Thing Exists EssenceIncludesExistence c (M12 c A Hg))
    as [Hn | Hp].
  - exact Hn.
  - contradiction.
Qed.

(* Steps 6 to 11 together: if the aggregate exists and has a member, it has
   a cause, and every cause of it is a Necessary Existent outside it. *)
Theorem aggregate_has_necessary_cause :
  MP001 -> MP002 -> MP003 -> MP008 -> MP010 -> MP011_WholeToMembers -> MP012_GiverExists ->
  forall A, AggregateOfPossibles A -> Exists A ->
  (exists p, p <> A /\ PossibleInItself p) ->
  exists c, Gives c A /\ NecessaryInItself c /\ ~ MemberOf c A /\ c <> A.
Proof.
  intros M1 M2 M3 M8 M10 M11 M12 A HA HexA Hp.
  destruct (AggregateIsPossible.aggregate_requires_murajjih
              Thing Exists EssenceIncludesExistence Gives MemberOf M8 M10 A HA HexA Hp) as [c Hg].
  destruct (cause_is_outside M1 M2 M3 M11 A c HA Hg) as [Hnm [Hne _]].
  exists c. split; [exact Hg |]. split; [| split; assumption].
  exact (cause_is_necessary M1 M2 M3 M11 M12 A c HA Hg).
Qed.

End CauseOutside.

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

Definition Th := AggregateIsPossible.Th.
Definition N := AggregateIsPossible.N.
Definition P1 := AggregateIsPossible.P1.
Definition P2 := AggregateIsPossible.P2.
Definition Agg := AggregateIsPossible.Agg.
Definition Mem := AggregateIsPossible.Mem.
Definition EssN := AggregateIsPossible.EssN.

(* N gives existence to everything else; everything else has its existence
   through N. *)
Definition G1 (y x : Th) : Prop := y = N /\ x <> N.
Definition T1 (x y : Th) : Prop := x <> N /\ y = N.
Definition E1 (_ : Th) : Prop := True.

(* 1. Consistency and non-vacuity: every postulate used holds, Agg is the
      aggregate of P1 and P2, and N, its cause, is necessary. *)
Example all_hold_together :
  MP001 Th G1 T1 /\ MP002 Th G1 T1 /\ MP003 Th T1 /\ MP008 Th E1 EssN G1 /\
  MP010 Th EssN Mem /\ MP011_WholeToMembers Th G1 Mem /\ MP012_GiverExists Th E1 G1 /\
  AggregateOfPossibles Th E1 EssN Mem Agg /\ G1 N Agg /\ NecessaryInItself Th E1 EssN N.
Proof.
  unfold MP001, MP002, MP003, MP008, MP010, MP011_WholeToMembers, MP012_GiverExists,
         NoSelfCreation.MP001_Giver, NoSelfCreation.MP002_Receiver,
         NoCircularCreation.MP003_Inherited,
         PossibleRequiresMurajjih.MP008_NoPreponderanceWithoutPreponderator,
         NoRegressOfGiving.ThroughAnother, AggregateIsPossible.MP010_NoNecessityFromPossibles,
         UltimatelyGives, NecessaryInItself, Division.NecessaryInItself, G1, T1, E1.
  split; [| split; [| split; [| split; [| split; [| split; [| split; [| split; [| split]]]]]]]].
  - intros x y [Hy _] [HN _]. subst y. exact (HN eq_refl).
  - intros x y [Hy Hx]. split; assumption.
  - intros x y z [_ Hy] [Hy' _]. subst y. exfalso. exact (Hy' eq_refl).
  - intros x _ Hn. destruct x; try reflexivity; exfalso; apply Hn;
      exists N; (split; [reflexivity | discriminate]).
  - intros A [q [_ HA]] _. unfold EssN, AggregateIsPossible.EssN. subst A. discriminate.
  - intros c A p [Hc _] [[Hp|Hp] _]; subst c p; apply t_step; (split; [reflexivity | discriminate]).
  - intros y x _. exact I.
  - apply AggregateIsPossible.agg_is_aggregate.
    intro x. unfold AggregateIsPossible.EssN. split; [intro H; left; exact H | intros [H|[]]; exact H].
  - split; [reflexivity | discriminate].
  - split; [exact I | reflexivity].
Qed.

(* 2. Countermodel without MP-011: the aggregate is given existence by its
      own member P1 (P1 in turn by N).  Every other postulate used holds, but
      the cause of the aggregate is a member.  So MP-011 is needed. *)
Definition G2 (y x : Th) : Prop :=
  (y = P1 /\ x = Agg) \/ (y = N /\ (x = P1 \/ x = P2)).
Definition T2 (x y : Th) : Prop :=
  (x = Agg /\ (y = P1 \/ y = N)) \/ ((x = P1 \/ x = P2) /\ y = N).

Example without_MP011_cause_is_a_member :
  MP001 Th G2 T2 /\ MP002 Th G2 T2 /\ MP003 Th T2 /\ MP012_GiverExists Th E1 G2 /\
  G2 P1 Agg /\ Mem P1 Agg.
Proof.
  unfold MP001, MP002, MP003, MP012_GiverExists, NoSelfCreation.MP001_Giver,
         NoSelfCreation.MP002_Receiver, NoCircularCreation.MP003_Inherited, G2, T2, E1,
         Mem, AggregateIsPossible.Mem.
  split; [| split; [| split; [| split; [| split]]]].
  - intros x y Hg Ht. destruct x, y; simpl in *; unfold P1, P2, N, Agg in *;
      intuition discriminate.
  - intros x y Hg. destruct x, y; simpl in *; unfold P1, P2, N, Agg in *;
      intuition (first [discriminate | (left; split; auto) | (right; split; auto)]).
  - intros x y z H1 H2. destruct x, y, z; simpl in *; unfold P1, P2, N, Agg in *;
      intuition (first [discriminate | (left; split; auto) | (right; split; auto)]).
  - intros y x _. exact I.
  - left. split; reflexivity.
  - split; [left; reflexivity | reflexivity].
Qed.

(* 3. Countermodel without MP-012: the aggregate's giver N does not exist, so
      it is not a Necessary Existent.  So MP-012 is needed. *)
Definition E3 (x : Th) : Prop := x <> N.

Example without_MP012_cause_not_necessary :
  G1 N Agg /\ ~ NecessaryInItself Th E3 EssN N.
Proof.
  unfold NecessaryInItself, Division.NecessaryInItself, G1, E3.
  split; [split; [reflexivity | discriminate] |].
  intros [H _]. exact (H eq_refl).
Qed.

Print Assumptions giving_circle_is_dependence_circle.
Print Assumptions cause_is_not_a_member.
Print Assumptions aggregate_does_not_cause_itself.
Print Assumptions subset_does_not_cause_aggregate.
Print Assumptions step8.
Print Assumptions cause_is_outside.
Print Assumptions cause_is_necessary.
Print Assumptions aggregate_has_necessary_cause.
Print Assumptions all_hold_together.
Print Assumptions without_MP011_cause_is_a_member.
Print Assumptions without_MP012_cause_not_necessary.

End CauseOutsideIsNecessary.

(* ======================================================================
   Dalil al-imkan: step 12, the conclusion (proof a, the aggregate route)
   ====================================================================== *)
Module ImkanConclusion.

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

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

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


Section Conclusion.

(* Primitive vocabulary.  Nothing is assumed about any of these. *)
Variable Thing : Type.
Variable Exists : Thing -> Prop.
Variable EssenceIncludesExistence : Thing -> Prop.
Variable Gives : Thing -> Thing -> Prop.
Variable Through : Thing -> Thing -> Prop.
Variable MemberOf : Thing -> Thing -> Prop.

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

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

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

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

End Conclusion.

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

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

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

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

End ImkanConclusion.

(* ======================================================================
   Dalil al-imkan: proof (b), the short route through OP-001
   ====================================================================== *)
Module ImkanShortRoute.

(* Dalil al-imkan, proof (b): the short route through OP-001.

   Since something exists (SP-001), a Necessary Existent exists:
   - if the existent is necessary in itself, the conclusion holds at once;
   - if it is possible in itself, it has a giver (step 3, MP-008); by OP-001
     only what has existence of itself gives existence, so the giver exists
     with nothing giving it existence; by MP-008 its existence is then from
     its own nature, so it is necessary in itself.

   This route bypasses the aggregate (steps 5 to 9).  It shares its decisive
   premise, OP-001, with dalil al-kalima; proof (a) does not, which is why
   (a) is the primary proof and (b) the second.

   Rests on: PR-006 (step 1), PR-008 (step 3, MP-008), PR-004 (definitions,
   OP-001), SP-001, and excluded middle.  No notion of time appears. *)


Section Short.

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

(* Reused definitions. *)
Definition NecessaryInItself := Division.NecessaryInItself Thing Exists EssenceIncludesExistence.
Definition MP008 := PossibleRequiresMurajjih.MP008_NoPreponderanceWithoutPreponderator
                      Thing Exists EssenceIncludesExistence Gives.
Definition OP001 := NoRegressOfGiving.OP001_OnlySelfExistentGives Thing Gives Exists.
Definition SP001 : Prop := exists x, Exists x.

(* The giver of anything is necessary in itself (OP-001 and MP-008). *)
Lemma giver_is_necessary_in_itself :
  MP008 -> OP001 -> forall y x, Gives y x -> NecessaryInItself y.
Proof.
  intros M8 OP y x Hg. destruct (OP x y Hg) as [Hex Hn].
  split; [exact Hex | exact (M8 y Hex Hn)].
Qed.

(* Proof (b) of step 12: since something exists, a Necessary Existent
   exists. *)
Theorem necessary_existent_exists_short :
  MP008 -> OP001 -> SP001 -> exists n, NecessaryInItself n.
Proof.
  intros M8 OP [x Hx].
  destruct (Division.division_exhaustive Thing Exists EssenceIncludesExistence x Hx) as [Hn | Hp].
  - exists x. exact Hn.
  - destruct (PossibleRequiresMurajjih.possible_requires_murajjih
                Thing Exists EssenceIncludesExistence Gives M8 x Hp) as [y Hg].
    exists y. exact (giver_is_necessary_in_itself M8 OP y x Hg).
Qed.

End Short.

(* ------------------------------------------------------------------ *)
(* Checks.  Illustrations of logical possibility only. *)

(* 1. Consistency: MP-008, OP-001 and SP-001 hold together; a necessary
      thing (true) gives existence to a possible one (false). *)
Example premises_hold_together :
  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 bool E Ess G /\ OP001 bool E G /\ SP001 bool E.
Proof.
  intros E Ess G.
  unfold MP008, OP001, SP001, PossibleRequiresMurajjih.MP008_NoPreponderanceWithoutPreponderator,
         NoRegressOfGiving.OP001_OnlySelfExistentGives, NoRegressOfGiving.OfItself,
         NoRegressOfGiving.ThroughAnother, E, Ess, G.
  split; [| split].
  - intros [] _ Hn; [reflexivity |]. exfalso. apply Hn. exists true. split; reflexivity.
  - intros x y [Hy _]. subst y. split; [exact I |]. intros [z [_ H]]. discriminate.
  - exists true. exact I.
Qed.

(* 2. Countermodel without OP-001: numbers 0, 1, 2, ..., each possible and
      each given existence by the next.  MP-008 and SP-001 hold, but nothing
      is necessary.  So the short route needs OP-001. *)
Example without_OP001_no_necessary :
  let E := fun (_ : nat) => True in
  let Ess := fun (_ : nat) => False in
  let G := fun (y x : nat) => y = S x in
  MP008 nat E Ess G /\ SP001 nat E /\ ~ (exists n, NecessaryInItself nat E Ess n).
Proof.
  intros E Ess G.
  unfold MP008, SP001, NecessaryInItself, PossibleRequiresMurajjih.MP008_NoPreponderanceWithoutPreponderator,
         NoRegressOfGiving.ThroughAnother, Division.NecessaryInItself, E, Ess, G.
  split; [| split].
  - intros x _ Hn. exfalso. apply Hn. exists (S x). reflexivity.
  - exists 0. exact I.
  - intros [n [_ H]]. exact H.
Qed.

Print Assumptions giver_is_necessary_in_itself.
Print Assumptions necessary_existent_exists_short.
Print Assumptions premises_hold_together.
Print Assumptions without_OP001_no_necessary.

End ImkanShortRoute.