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

Require PR006.Division PR004.NoRegressOfGiving PR008.PossibleRequiresMurajjih.

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.