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

From Stdlib Require Import PeanoNat Lia.
Require PR001.Exhaustiveness PR002.NoSelfCreation.

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.