(* Premise: every chain of dependence falls under exactly one of four cases:
   (1) self-dependence, (2) circularity, (3) infinite regress,
   (4) the chain ends at something that depends on nothing.

   Logical principle used, declared openly: the law of excluded middle
   (Stdlib Classical, axiom [classic]). Nothing else is assumed. *)

From Stdlib Require Import Classical PeanoNat Lia.

Section Cases.

(* Primitive vocabulary.  Nothing is assumed about either item: once the
   section closes, every theorem below holds for EVERY type of things and
   EVERY relation.  In particular, nothing is assumed to exist. *)
Variable Thing : Type.
Variable DependsOn : Thing -> Thing -> Prop.  (* x depends on y for its existence *)

(* Conditional definition: if x depends on nothing, x is called independent. *)
Definition Independent (x : Thing) : Prop := forall y, ~ DependsOn x y.

(* A chain is a sequence of positions; [None] means the chain has stopped. *)
Definition Chain := nat -> option Thing.

(* c is a maximal chain of dependence starting from u:
   - it starts at u;
   - each next item is something the previous item depends on;
   - once stopped, it stays stopped;
   - it stops only at something independent (it is never cut short). *)
Definition MaximalChainFrom (u : Thing) (c : Chain) : Prop :=
  c 0 = Some u /\
  (forall n x y, c n = Some x -> c (S n) = Some y -> DependsOn x y) /\
  (forall n, c n = None -> c (S n) = None) /\
  (forall n x, c n = Some x -> c (S n) = None -> Independent x).

(* Some item occurs twice in the chain. *)
Definition Repeats (c : Chain) : Prop :=
  exists i j x, i < j /\ c i = Some x /\ c j = Some x.

(* Case 1: some item is immediately followed by itself (x depends on x). *)
Definition SelfDependence (c : Chain) : Prop :=
  exists n x, c n = Some x /\ c (S n) = Some x.

(* Case 2: an item recurs, but never immediately. *)
Definition Circularity (c : Chain) : Prop :=
  Repeats c /\ ~ SelfDependence c.

(* Case 3: the chain never stops and no item recurs. *)
Definition InfiniteRegress (c : Chain) : Prop :=
  (forall n, c n <> None) /\ ~ Repeats c.

(* Case 4: the chain stops at an independent item, with no item recurring. *)
Definition EndsInIndependent (c : Chain) : Prop :=
  (exists n x, c n = Some x /\ c (S n) = None /\ Independent x) /\ ~ Repeats c.

(* Helper: a chain that starts with an item and later stops has a last item. *)
Lemma last_item : forall (c : Chain) (u : Thing) n,
  c 0 = Some u -> c n = None ->
  exists m x, c m = Some x /\ c (S m) = None.
Proof.
  intros c u n H0. induction n as [| k IH]; intros Hn.
  - congruence.
  - destruct (c k) as [x |] eqn:Hk.
    + exists k, x. split; assumption.
    + apply IH. reflexivity.
Qed.

(* Exhaustiveness: every maximal chain falls under at least one case. *)
Theorem four_cases_exhaustive : forall u c,
  MaximalChainFrom u c ->
  SelfDependence c \/ Circularity c \/ InfiniteRegress c \/ EndsInIndependent c.
Proof.
  intros u c [H0 [_ [_ Hstop]]].
  destruct (classic (Repeats c)) as [Hrep | Hnorep].
  - destruct (classic (SelfDependence c)) as [Hself | Hnoself].
    + left. exact Hself.
    + right; left. split; assumption.
  - destruct (classic (exists n, c n = None)) as [[n Hn] | Hnever].
    + destruct (last_item c u n H0 Hn) as [m [x [Hm HSm]]].
      right; right; right. split.
      * exists m, x. repeat split; try assumption. exact (Hstop m x Hm HSm).
      * exact Hnorep.
    + right; right; left. split.
      * intros n Hn. apply Hnever. exists n. exact Hn.
      * exact Hnorep.
Qed.

(* Exclusivity: no maximal chain falls under two cases. *)
Lemma self_repeats : forall c, SelfDependence c -> Repeats c.
Proof.
  intros c [n [x [H1 H2]]]. exists n, (S n), x. repeat split; try assumption. lia.
Qed.

Theorem four_cases_exclusive : forall c,
  (SelfDependence c -> ~ Circularity c /\ ~ InfiniteRegress c /\ ~ EndsInIndependent c) /\
  (Circularity c -> ~ InfiniteRegress c /\ ~ EndsInIndependent c) /\
  (InfiniteRegress c -> ~ EndsInIndependent c).
Proof.
  intro c. split; [| split].
  - intro Hs. split; [| split].
    + intros [_ Hns]. contradiction.
    + intros [_ Hnr]. exact (Hnr (self_repeats c Hs)).
    + intros [_ Hnr]. exact (Hnr (self_repeats c Hs)).
  - intros [Hr _]. split.
    + intros [_ Hnr]. contradiction.
    + intros [_ Hnr]. contradiction.
  - intros [Hnever _] [[n [x [_ [HSn _]]]] _]. exact (Hnever (S n) HSn).
Qed.

End Cases.

(* ------------------------------------------------------------------ *)
(* Non-vacuity: each case really occurs for some relation, so none of the
   four definitions is empty.  These are illustrations of logical
   possibility only; they make no claim about what exists. *)

(* Case 1: a single thing that depends on itself. *)
Example case1_occurs :
  let D := fun (_ _ : unit) => True in
  let c := fun (_ : nat) => Some tt in
  MaximalChainFrom unit D tt c /\ SelfDependence unit c.
Proof.
  simpl. split.
  - repeat split; intros; try discriminate; exact I.
  - exists 0, tt. split; reflexivity.
Qed.

(* Case 2: two things that depend on each other. *)
Example case2_occurs :
  let D := fun (x y : bool) => y = negb x in
  let c := fun (n : nat) => Some (Nat.odd n) in
  MaximalChainFrom bool D false c /\ Circularity bool c.
Proof.
  simpl. split.
  - repeat split.
    + intros n x y Hx Hy. injection Hx as <-. injection Hy as <-.
      rewrite Nat.odd_succ, <- Nat.negb_odd. reflexivity.
    + intros n H. discriminate.
    + intros n x _ H. discriminate.
  - split.
    + exists 0, 2, false. repeat split. lia.
    + intros [n [x [H1 H2]]]. injection H1 as H1. injection H2 as H2.
      rewrite Nat.odd_succ, <- Nat.negb_odd in H2. subst x.
      destruct (Nat.odd n); discriminate.
Qed.

(* Case 3: each number depends on the next, without end. *)
Example case3_occurs :
  let D := fun (x y : nat) => y = S x in
  let c := fun (n : nat) => Some n in
  MaximalChainFrom nat D 0 c /\ InfiniteRegress nat c.
Proof.
  simpl. split.
  - repeat split.
    + intros n x y Hx Hy. injection Hx as <-. injection Hy as <-. reflexivity.
    + intros n H. discriminate.
    + intros n x _ H. discriminate.
  - split.
    + intros n H. discriminate.
    + intros [i [j [x [Hij [Hi Hj]]]]]. injection Hi as Hi. injection Hj as Hj. lia.
Qed.

(* Case 4: one thing depends on a second, which depends on nothing. *)
Example case4_occurs :
  let D := fun (x y : bool) => x = false /\ y = true in
  let c := fun (n : nat) => match n with 0 => Some false | 1 => Some true | _ => None end in
  MaximalChainFrom bool D false c /\ EndsInIndependent bool D c.
Proof.
  simpl. split.
  - split; [reflexivity | split; [| split]].
    + intros [| [| n]] x y Hx Hy; simpl in *; try discriminate.
      injection Hx as <-. injection Hy as <-. split; reflexivity.
    + intros [| [| n]] H; simpl in *; try discriminate; reflexivity.
    + intros [| [| n]] x Hx Hn; simpl in *; try discriminate.
      injection Hx as <-. intros y [H _]. discriminate.
  - split.
    + exists 1, true. repeat split. intros y [H _]. discriminate.
    + intros [i [j [x [Hij [Hi Hj]]]]].
      destruct i as [| [| i]]; destruct j as [| [| j]]; simpl in *;
        try discriminate; try lia.
      injection Hi as <-. discriminate.
Qed.

Print Assumptions four_cases_exhaustive.
Print Assumptions four_cases_exclusive.
Print Assumptions case1_occurs.
Print Assumptions case2_occurs.
Print Assumptions case3_occurs.
Print Assumptions case4_occurs.