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

From Stdlib Require Import Relations.
Require PR002.NoSelfCreation PR003.NoCircularCreation PR004.NoRegressOfGiving
        PR006.Division PR008.PossibleRequiresMurajjih PR009.AggregateIsPossible.

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.