From Stdlib Require Import Classical Relations.

Section Pilot.
(* Vocabulary.  Nothing is assumed about any of these. *)
Variable Thing : Type.
Variable Gives : Thing -> Thing -> Prop.     (* Gives y x : y gives existence to x *)
Variable Through : Thing -> Thing -> Prop.   (* Through x y : x has its existence through y *)
Variable Exists : Thing -> Prop.             (* x exists *)
Variable Ess : Thing -> Prop.                (* x's existence is from its own nature *)
Variable PartOf : Thing -> Thing -> Prop.    (* p is a part of u *)
Variable Universe : Thing.                   (* the universe *)

(* Definitions. *)
Definition DependsOn (x y : Thing) : Prop := Gives y x.            (* x depends on y *)
Definition ThroughAnother (x : Thing) : Prop := exists y, Gives y x.
Definition OfItself (x : Thing) : Prop := Exists x /\ ~ ThroughAnother x.
Definition Necessary (x : Thing) : Prop := Exists x /\ Ess x.
Definition Possible (x : Thing) : Prop := Exists x /\ ~ Ess x.
Definition InUniverse (x : Thing) : Prop := x = Universe \/ PartOf x Universe.

(* Approved postulates, written as definitions: a theorem uses one only when
   its statement lists it as a condition. *)
Definition MP001 : Prop := forall x y, Gives y x -> ~ Through y x.   (* a giver does not have its existence through what it gives existence to *)
Definition MP002 : Prop := forall x y, Gives y x -> Through x y.     (* the receiver has its existence through the giver *)
Definition MP003 : Prop := forall x y z, Through x y -> Through y z -> Through x z.  (* existence-through is inherited *)
Definition MP008 : Prop := forall x, Exists x -> ~ ThroughAnother x -> Ess x.       (* existence comes from one's nature or from a giver *)
Definition OP001 : Prop := forall x y, Gives y x -> OfItself y.      (* only what exists of itself gives existence *)
Definition OP006 : Prop := exists x, InUniverse x /\ Possible x.     (* the universe is not wholly necessary *)
Definition SP001 : Prop := exists x, Exists x.                       (* something exists *)

(* Added for the full test: aggregates, possible worlds, and their postulates. *)
Variable MemberOf : Thing -> Thing -> Prop.  (* p is a member of the aggregate a *)
Variable World : Type.
Variable ExistsIn : World -> Thing -> Prop.  (* x exists in world w *)
Definition Independent (x : Thing) : Prop := forall y, ~ DependsOn x y.
Definition NonExistencePossible (x : Thing) : Prop := exists w, ~ ExistsIn w x.
Definition AggregateOfPossibles (A : Thing) : Prop :=
  (forall p, p <> A -> (MemberOf p A <-> Possible p)) /\ ~ MemberOf A A.
Definition MP007 : Prop := forall x, Ess x -> forall w, ExistsIn w x.        (* existence from one's nature cannot fail *)
Definition MP009 : Prop := (exists p, Possible p) -> exists A, AggregateOfPossibles A /\ Exists A.  (* the aggregate of possibles exists *)
Definition MP010 : Prop := forall A, (exists p, MemberOf p A) ->
  (forall p, MemberOf p A -> ~ Ess p) -> ~ Ess A.                            (* possibles do not add up to a necessary *)
Definition MP011 : Prop := forall c A p, Gives c A -> MemberOf p A -> clos_trans Thing Gives c p.  (* giving to a whole gives to its members *)
Definition MP012 : Prop := forall y x, Gives y x -> Exists y.               (* a giver exists *)

Lemma imkan_s12_necessary_exists_L17 : MP002 -> MP003 -> forall a b, clos_trans Thing Gives a b -> Through b a.
Proof.
unfold MP002, MP003. intros A2 A3 a b H. induction H as [x y Hg | x y z H1 IH1 H2 IH2].
- apply A2. exact Hg.
- apply A3 with y.
  + exact IH2.
  + exact IH1.
Qed.

Lemma imkan_s12_necessary_exists_L25 : forall a b : Thing, Gives a b -> exists y, Gives y b /\ (y = a \/ clos_trans Thing Gives a y).
Proof.
intros; firstorder.
Qed.

Lemma imkan_s12_necessary_exists_L30 : forall a m b y : Thing, clos_trans Thing Gives a m -> Gives y b -> (y = m \/ clos_trans Thing Gives m y) -> (y = a \/ clos_trans Thing Gives a y).
Proof.
intros a m b y H1 H2 H3. destruct H3 as [E|H3].
- right. subst. exact H1.
- right. eapply t_trans; eauto.
Qed.

Lemma imkan_s12_necessary_exists_L24 : forall c, clos_trans Thing Gives c c -> exists y, Gives y c /\ (y = c \/ clos_trans Thing Gives c y).
Proof.
intros c H. cut (forall a b, clos_trans Thing Gives a b -> exists y, Gives y b /\ (y = a \/ clos_trans Thing Gives a y)).
- intro G. exact (G c c H).
- intros a b Hab. induction Hab as [a b Hg | a m b H1 IH1 H2 IH2].
  + exact (imkan_s12_necessary_exists_L25 a b Hg).
  + destruct IH2 as [y [Hy Hor]]. exists y. split; [exact Hy | exact (imkan_s12_necessary_exists_L30 a m b y H1 Hy Hor)].
Qed.

Lemma imkan_s12_necessary_exists_L12 : MP001 -> MP002 -> MP003 -> forall c, ~ clos_trans Thing Gives c c.
Proof.
intros H1 H2 H3 c Hc. destruct (imkan_s12_necessary_exists_L24 c Hc) as [y [Hg [->|Hy]]].
- exact (H1 _ _ Hg (H2 _ _ Hg)).
- exact (H1 _ _ Hg (imkan_s12_necessary_exists_L17 H2 H3 c y Hy)).
Qed.

Lemma imkan_s12_necessary_exists_L35 : MP001 -> MP002 -> MP008 -> MP009 -> MP012 -> SP001 -> ~ (exists n, Necessary n) -> exists c A, Gives c A /\ MemberOf c A.
Proof.
intros H1 H2 H8 H9 H12 S1 HN.
destruct S1 as [x Hx].
assert (HP: forall y, Exists y -> Possible y).
{ intros y Hy. split; [exact Hy|]. intro He. apply HN. exists y. split; assumption. }
assert (HT: forall y, Exists y -> ThroughAnother y).
{ intros y Hy. apply NNPP. intro Hn. apply HN. exists y. split; [exact Hy | apply H8; assumption]. }
destruct (H9 (ex_intro _ x (HP x Hx))) as [A [HAA HEA]].
destruct HAA as [HA _].
destruct (HT A HEA) as [c Hc].
exists c, A. split; [exact Hc|].
assert (Hne: c <> A).
{ intro e. subst c. exact (H1 _ _ Hc (H2 _ _ Hc)). }
apply (proj2 (HA c Hne)). apply HP. exact (H12 _ _ Hc).
Qed.

Lemma imkan_s12_necessary_exists_L6 : MP001 -> MP002 -> MP003 -> MP008 -> MP009 -> MP010 -> MP011 -> MP012 -> SP001 -> exists n, Necessary n.
Proof.
intros H1 H2 H3 H8 H9 H10 H11 H12 S1. apply NNPP. intro HN. destruct (imkan_s12_necessary_exists_L35 H1 H2 H8 H9 H12 S1 HN) as [c [A [G M]]]. exact (imkan_s12_necessary_exists_L12 H1 H2 H3 c (H11 c A c G M)).
Qed.

End Pilot.

Print Assumptions imkan_s12_necessary_exists_L6.