From Stdlib Require Import Classical Relations.
From Hammer Require Import Hammer Tactics.

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

Set Hammer ATPLimit 20.
Set Hammer ReconstrLimit 10.

Lemma imkan_s9_cause_outside_L1 : MP002 -> MP003 -> forall a b, clos_trans Thing Gives a b -> Through b a.
Proof.
intros; match goal with H : clos_trans _ _ _ _ |- _ => induction H end; firstorder eauto.
Qed.

Lemma imkan_s9_cause_outside_L2 : forall a b, clos_trans Thing Gives a b -> clos_trans_1n Thing Gives a b.
Proof.
intros; srun (eauto) use: clos_trans_t1n unfold: relation.
Qed.

Lemma imkan_s9_cause_outside_L3 : forall a b, clos_trans_1n Thing Gives a b -> (Gives a b \/ exists z, Gives a z /\ clos_trans_1n Thing Gives z b).
Proof.
intros; match goal with H : clos_trans_1n _ _ _ _ |- _ => induction H end; firstorder eauto.
Qed.

Lemma imkan_s9_cause_outside_L4 : forall a b, Gives a b -> clos_refl_trans Thing Gives a b.
Proof.
intros; sauto lq: on.
Qed.

Lemma imkan_s9_cause_outside_L5 : forall a b c, Gives a b -> clos_refl_trans Thing Gives b c -> clos_refl_trans Thing Gives a c.
Proof.
intros; sauto lq: on.
Qed.

Lemma imkan_s9_cause_outside_L6 : forall a b, clos_trans_1n Thing Gives a b -> clos_refl_trans Thing Gives a b.
Proof.
intros; srun (eauto) use: imkan_s9_cause_outside_L4, clos_t1n_trans, clos_rt_t, imkan_s9_cause_outside_L3, clos_t_clos_rt unfold: relation, inclusion.
Qed.

Lemma imkan_s9_cause_outside_L7 : forall a b, clos_trans Thing Gives a b -> clos_refl_trans Thing Gives a b.
Proof.
pose proof imkan_s9_cause_outside_L4 as sub1. pose proof imkan_s9_cause_outside_L5 as sub2. pose proof imkan_s9_cause_outside_L6 as sub3. intros; srun (eauto) use: imkan_s9_cause_outside_L2.
Qed.

Lemma imkan_s9_cause_outside_L8 : forall a b c, (exists z, Gives a z /\ clos_refl_trans Thing Gives z b) -> clos_refl_trans Thing Gives b c -> exists z, Gives a z /\ clos_refl_trans Thing Gives z c.
Proof.
intros; sauto lq: on.
Qed.

Lemma imkan_s9_cause_outside_L9 : forall a b, Gives a b -> exists z, Gives a z /\ clos_refl_trans Thing Gives z b.
Proof.
intros; sfirstorder.
Qed.

Lemma imkan_s9_cause_outside_L10 : forall x, clos_trans Thing Gives x x -> exists z, Gives x z /\ clos_refl_trans Thing Gives z x.
Proof.
pose proof imkan_s9_cause_outside_L7 as sub1. pose proof imkan_s9_cause_outside_L8 as sub2. pose proof imkan_s9_cause_outside_L9 as sub3. unfold MP001, MP002, MP003, MP007, MP008, MP009, MP010, MP011, MP012, OP001, OP006, SP001, OfItself, ThroughAnother, Necessary, Possible, InUniverse, DependsOn, Independent, NonExistencePossible, AggregateOfPossibles in *; intros; qauto use: imkan_s9_cause_outside_L2, imkan_s9_cause_outside_L3, clos_t1n_trans unfold: relation.
Qed.

Lemma imkan_s9_cause_outside_L11 : forall a b, clos_refl_trans Thing Gives a b -> forall c, Gives b c -> clos_trans Thing Gives a c \/ a = c \/ False.
Proof.
intros; srun (eauto) use: clos_rt_t, t_step unfold: relation.
Qed.

Lemma imkan_s9_cause_outside_L12 : forall a b, clos_refl_trans Thing Gives a b -> a = b \/ (exists z, clos_refl_trans Thing Gives a z /\ Gives z b).
Proof.
intros; qauto use: clos_rt_rtn1, clos_rt_rtn1_iff unfold: relation inv: clos_refl_trans_n1, clos_refl_trans.
Qed.

Lemma imkan_s9_cause_outside_L13 : forall a b, (exists z, clos_refl_trans Thing Gives a z /\ Gives z b) -> clos_trans Thing Gives a b.
Proof.
unfold MP001, MP002, MP003, MP007, MP008, MP009, MP010, MP011, MP012, OP001, OP006, SP001, OfItself, ThroughAnother, Necessary, Possible, InUniverse, DependsOn, Independent, NonExistencePossible, AggregateOfPossibles in *; intros; hauto lq: on use: clos_rt_t, imkan_s9_cause_outside_L11, t_step unfold: relation.
Qed.

Lemma imkan_s9_cause_outside_L14 : forall a b, clos_refl_trans Thing Gives a b -> a = b \/ clos_trans Thing Gives a b.
Proof.
pose proof imkan_s9_cause_outside_L11 as sub1. pose proof imkan_s9_cause_outside_L12 as sub2. pose proof imkan_s9_cause_outside_L13 as sub3. intros; hauto.
Qed.

Lemma imkan_s9_cause_outside_L15 : MP002 -> MP003 -> forall a b, clos_refl_trans Thing Gives a b -> a = b \/ Through b a.
Proof.
pose proof imkan_s9_cause_outside_L14 as sub1. pose proof imkan_s9_cause_outside_L1 as sub2. intros; firstorder.
Qed.

Lemma imkan_s9_cause_outside_L16 : MP001 -> MP002 -> forall x z, Gives x z -> ~ (x = z \/ Through x z).
Proof.
intros; hauto lq: on unfold: MP001, MP002.
Qed.

Lemma imkan_s9_cause_outside_L17 : MP001 -> MP002 -> MP003 -> forall x, ~ clos_trans Thing Gives x x.
Proof.
pose proof imkan_s9_cause_outside_L10 as sub1. pose proof imkan_s9_cause_outside_L15 as sub2. pose proof imkan_s9_cause_outside_L16 as sub3. intros; hcrush use: imkan_s9_cause_outside_L1 unfold: MP001.
Qed.

Lemma imkan_s9_cause_outside_L18 : MP001 -> MP002 -> forall A, ~ Gives A A.
Proof.
intros; firstorder.
Qed.

Lemma imkan_s9_cause_outside_L19 : forall A c, AggregateOfPossibles A -> c <> A -> ~ MemberOf c A -> ~ Possible c.
Proof.
intros; firstorder.
Qed.

Lemma imkan_s9_cause_outside_L20 : MP001 -> MP002 -> MP003 -> MP011 -> forall A c, AggregateOfPossibles A -> Gives c A -> ~ MemberOf c A /\ c <> A /\ ~ Possible c.
Proof.
pose proof imkan_s9_cause_outside_L1 as sub1. pose proof imkan_s9_cause_outside_L17 as sub2. pose proof imkan_s9_cause_outside_L18 as sub3. pose proof imkan_s9_cause_outside_L19 as sub4. intros; qauto unfold: MP011, MP001, AggregateOfPossibles, MP002.
Qed.

End Pilot.

Print Assumptions imkan_s9_cause_outside_L20.