(* PR-003: No circle of dependence of any length.  Nothing ultimately depends
   on itself, so no maximal chain of dependence (PR-001) contains a repeated
   thing: cases 1 and 2 of PR-001 are both eliminated.

   Rests on:
   - PR-001 (Exhaustiveness.v), reused for its chain definitions;
   - PR-002 (NoSelfCreation.v), reused for the one-step circle;
   - meaning postulates MP-001, MP-002 (from PR-002) and MP-003 (below),
     all as explicit conditions of the theorems.
   No axiom is used.  Nothing is assumed to exist.  No notion of time appears. *)

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

Section Circles.

(* Primitive vocabulary: the same as PR-002.  Nothing is assumed about it. *)
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 *)

(* Reused from PR-002: x depends on y means y gives existence to x. *)
Definition DependsOn : Thing -> Thing -> Prop := NoSelfCreation.DependsOn Thing Gives.

(* Reused meaning postulates from PR-002. *)
Definition MP001 : Prop := NoSelfCreation.MP001_Giver Thing Gives Through.
Definition MP002 : Prop := NoSelfCreation.MP002_Receiver Thing Gives Through.

(* MP-003, "existence through is inherited": if x has its existence through y,
   and y has its existence through z, then x has its existence through z. *)
Definition MP003_Inherited : Prop :=
  forall x y z, Through x y -> Through y z -> Through x z.

(* x ultimately depends on y: a chain of one or more steps of dependence.
   (clos_trans is the standard library's "one or more steps" of a relation.) *)
Definition UltimatelyDependsOn : Thing -> Thing -> Prop := clos_trans Thing DependsOn.

(* Step 1: ultimate dependence means having one's existence through. *)
Lemma ultimate_dependence_is_through :
  MP002 -> MP003_Inherited ->
  forall x y, UltimatelyDependsOn x y -> Through x y.
Proof.
  intros M2 M3 x y H. induction H as [x y Hxy | x y z _ IH1 _ IH2].
  - exact (M2 x y Hxy).
  - exact (M3 x y z IH1 IH2).
Qed.

(* Step 2 (premise 3): nothing ultimately depends on itself, however long
   the circle. *)
Theorem no_circular_dependence :
  MP001 -> MP002 -> MP003_Inherited ->
  forall x, ~ UltimatelyDependsOn x x.
Proof.
  intros M1 M2 M3 x Hc.
  apply clos_trans_t1n_iff in Hc.
  assert (Hgen : forall a b, clos_trans_1n Thing DependsOn a b -> a = b -> False).
  { intros a b H. destruct H as [b Hab | m b Ham Hmb]; intro Heq; subst b.
    - (* circle of one step: a gives existence to itself; excluded by PR-002 *)
      exact (NoSelfCreation.no_self_creation Thing Gives Through M1 M2 a Hab).
    - (* longer circle: a depends on m, and m ultimately depends on a *)
      apply clos_trans_t1n_iff in Hmb.
      pose proof (ultimate_dependence_is_through M2 M3 m a Hmb) as Hthrough.
      exact (M1 a m Ham Hthrough). }
  exact (Hgen x x Hc eq_refl).
Qed.

(* Step 3: link to the chains of PR-001.  Between two positions of a maximal
   chain, the earlier thing ultimately depends on the later one. *)
Lemma chain_segment : forall u c,
  Exhaustiveness.MaximalChainFrom Thing DependsOn u c ->
  forall i k a b, c i = Some a -> c (i + S k) = Some b -> UltimatelyDependsOn a b.
Proof.
  intros u c [_ [Hlink [Hstay _]]] i k.
  induction k as [| k IH]; intros a b Ha Hb.
  - apply t_step. rewrite Nat.add_1_r in Hb. exact (Hlink i a b Ha Hb).
  - destruct (c (i + S k)) as [m |] eqn:Hm.
    + apply t_trans with m.
      * exact (IH a m Ha eq_refl).
      * apply t_step. apply (Hlink (i + S k) m b Hm).
        rewrite <- Hb. f_equal. lia.
    + exfalso. pose proof (Hstay (i + S k) Hm) as Hn.
      replace (S (i + S k)) with (i + S (S k)) in Hn by lia. congruence.
Qed.

(* Step 4: no maximal chain contains any thing twice. *)
Theorem no_repetition_in_chains :
  MP001 -> MP002 -> MP003_Inherited ->
  forall u c, Exhaustiveness.MaximalChainFrom Thing DependsOn u c ->
  ~ Exhaustiveness.Repeats Thing c.
Proof.
  intros M1 M2 M3 u c Hc [i [j [x [Hij [Hi Hj]]]]].
  apply (no_circular_dependence M1 M2 M3 x).
  replace j with (i + S (j - i - 1)) in Hj by lia.
  exact (chain_segment u c Hc i (j - i - 1) x x Hi Hj).
Qed.

(* Step 5: cases 1 and 2 of PR-001 are eliminated. *)
Corollary cases_1_and_2_eliminated :
  MP001 -> MP002 -> MP003_Inherited ->
  forall u c, Exhaustiveness.MaximalChainFrom Thing DependsOn u c ->
  ~ Exhaustiveness.SelfDependence Thing c /\ ~ Exhaustiveness.Circularity Thing c.
Proof.
  intros M1 M2 M3 u c Hc. split.
  - intro Hs. exact (no_repetition_in_chains M1 M2 M3 u c Hc
                       (Exhaustiveness.self_repeats Thing c Hs)).
  - intros [Hr _]. exact (no_repetition_in_chains M1 M2 M3 u c Hc Hr).
Qed.

End Circles.

(* ------------------------------------------------------------------ *)
(* Checks.  Illustrations of logical possibility only; no claim about what
   exists.  Three things A, B, C. *)

Inductive Three := A | B | C.

(* A circle: B gives existence to A, C to B, A to C
   (A depends on B, B on C, C on A). *)
Definition CircleGives (y x : Three) : Prop :=
  match y, x with B, A | C, B | A, C => True | _, _ => False end.

(* A straight line: B gives existence to A, C to B. *)
Definition LineGives (y x : Three) : Prop :=
  match y, x with B, A | C, B => True | _, _ => False end.
(* In the line, A has its existence through B and C; B through C. *)
Definition LineThrough (x y : Three) : Prop :=
  match x, y with A, B | A, C | B, C => True | _, _ => False end.

(* 1. Non-vacuity: all three postulates hold while a real chain of giving
      of length two occurs. *)
Example postulates_allow_chains :
  MP001 Three LineGives LineThrough /\ MP002 Three LineGives LineThrough /\
  MP003_Inherited Three LineThrough /\ LineGives B A /\ LineGives C B.
Proof.
  unfold MP001, MP002, NoSelfCreation.MP001_Giver, NoSelfCreation.MP002_Receiver,
         MP003_Inherited.
  repeat split.
  - intros [] [] H1 H2; simpl in *; tauto.
  - intros [] [] H; simpl in *; tauto.
  - intros [] [] [] H1 H2; simpl in *; tauto.
Qed.

(* 2. Countermodel without MP-003: in the circle, let "through" hold only for
      the direct givers.  MP-001 and MP-002 hold, yet A ultimately depends
      on A. *)
Example without_MP003_a_circle_is_consistent :
  MP001 Three CircleGives (fun x y => CircleGives y x) /\
  MP002 Three CircleGives (fun x y => CircleGives y x) /\
  UltimatelyDependsOn Three CircleGives A A.
Proof.
  unfold MP001, MP002, NoSelfCreation.MP001_Giver, NoSelfCreation.MP002_Receiver.
  split; [| split].
  - intros [] [] H1 H2; simpl in *; tauto.
  - intros [] [] H; simpl in *; tauto.
  - apply t_trans with B; [apply t_step; exact I |].
    apply t_trans with C; apply t_step; exact I.
Qed.

(* 3. Countermodel without MP-001: in the circle, let everything have its
      existence through everything.  MP-002 and MP-003 hold, and the circle
      stands. *)
Example without_MP001_a_circle_is_consistent :
  MP002 Three CircleGives (fun _ _ => True) /\
  MP003_Inherited Three (fun _ _ => True) /\
  UltimatelyDependsOn Three CircleGives A A.
Proof.
  unfold MP002, NoSelfCreation.MP002_Receiver, MP003_Inherited.
  split; [| split].
  - intros; exact I.
  - intros; exact I.
  - apply t_trans with B; [apply t_step; exact I |].
    apply t_trans with C; apply t_step; exact I.
Qed.

(* 4. Countermodel without MP-002: in the circle, let nothing have its
      existence through anything.  MP-001 and MP-003 hold, and the circle
      stands. *)
Example without_MP002_a_circle_is_consistent :
  MP001 Three CircleGives (fun _ _ => False) /\
  MP003_Inherited Three (fun _ _ => False) /\
  UltimatelyDependsOn Three CircleGives A A.
Proof.
  unfold MP001, NoSelfCreation.MP001_Giver, MP003_Inherited.
  split; [| split].
  - intros x y _ H. exact H.
  - intros x y z H _. exact H.
  - apply t_trans with B; [apply t_step; exact I |].
    apply t_trans with C; apply t_step; exact I.
Qed.

Print Assumptions ultimate_dependence_is_through.
Print Assumptions no_circular_dependence.
Print Assumptions chain_segment.
Print Assumptions no_repetition_in_chains.
Print Assumptions cases_1_and_2_eliminated.
Print Assumptions postulates_allow_chains.
Print Assumptions without_MP003_a_circle_is_consistent.
Print Assumptions without_MP001_a_circle_is_consistent.
Print Assumptions without_MP002_a_circle_is_consistent.