(* PR-001, second proof: the four cases stated in relational form (without
   chains), exactly as they are stated in the Leo-III files of dalil
   al-kalima (arguments/dalil-al-kalima/proofs/leo3-kalima/).

   Also proves that Leo-III's definition of "ultimately depends on" (the
   least transitive relation containing dependence, written as a
   higher-order formula) is equivalent to Rocq's clos_trans, which PR-003
   uses.  So the Leo-III premise 3 states exactly what PR-003 proves.

   Logical principle used: excluded middle (classic), in the exhaustiveness
   theorem only.  Nothing else is assumed.  Nothing is assumed to exist. *)

From Stdlib Require Import Classical Relations.

Section Relational.

(* Primitive vocabulary.  Nothing is assumed about either. *)
Variable Thing : Type.
Variable Gives : Thing -> Thing -> Prop.   (* Gives y x : y gives existence to x *)

(* The Leo-III definitions, transcribed. *)
Definition Dep (x y : Thing) : Prop := Gives y x.
Definition Independent (x : Thing) : Prop := forall y, ~ Dep x y.

(* Leo-III's "reach": x ultimately depends on y, written as a higher-order
   formula (true of every transitive relation containing Dep). *)
Definition Reach (x y : Thing) : Prop :=
  forall P : Thing -> Thing -> Prop,
    ((forall a b, Dep a b -> P a b) /\
     (forall a b c, P a b -> P b c -> P a c)) -> P x y.

Definition Case1 (x : Thing) : Prop :=
  exists y, (x = y \/ Reach x y) /\ Dep y y.
Definition Case2 (x : Thing) : Prop :=
  exists y, (x = y \/ Reach x y) /\ Reach y y /\ ~ Dep y y.
Definition Case3 (x : Thing) : Prop :=
  exists S : Thing -> Prop, S x /\ (forall a, S a -> exists b, S b /\ Dep a b).
Definition Case4 (x : Thing) : Prop :=
  Independent x \/ exists y, Reach x y /\ Independent y.

(* Leo-III's Reach coincides with Rocq's clos_trans (used in PR-003). *)
Theorem reach_iff_clos_trans : forall x y, Reach x y <-> clos_trans Thing Dep x y.
Proof.
  intros x y. split.
  - intro H. apply H. split.
    + intros a b Hab. apply t_step. exact Hab.
    + intros a b c H1 H2. apply t_trans with b; assumption.
  - intro H. induction H as [a b Hab | a b c _ IH1 _ IH2].
    + intros P [Hstep _]. exact (Hstep a b Hab).
    + intros P HP. destruct HP as [Hstep Htrans].
      apply Htrans with b; [apply IH1 | apply IH2]; split; assumption.
Qed.

(* Premise 1, relational form: every thing falls under at least one case. *)
Theorem four_cases_exhaustive_relational : forall x,
  Case1 x \/ Case2 x \/ Case3 x \/ Case4 x.
Proof.
  intro x.
  destruct (classic (Case4 x)) as [H4 | Hn4].
  - right; right; right. exact H4.
  - right; right; left.
    exists (fun z => z = x \/ Reach x z). split; [left; reflexivity |].
    intros a Ha.
    (* a is not independent, otherwise case 4 would hold *)
    assert (Hnind : ~ Independent a).
    { intro Hind. apply Hn4. destruct Ha as [Heq | Hr].
      - left. subst a. exact Hind.
      - right. exists a. split; assumption. }
    (* so a depends on some b *)
    destruct (not_all_not_ex Thing (fun b => Dep a b) Hnind) as [b Hab].
    exists b. split; [| exact Hab].
    right. destruct Ha as [Heq | Hr].
    + subst a. apply reach_iff_clos_trans. apply t_step. exact Hab.
    + apply reach_iff_clos_trans. apply t_trans with a.
      * exact (proj1 (reach_iff_clos_trans x a) Hr).
      * apply t_step. exact Hab.
Qed.

End Relational.

Print Assumptions reach_iff_clos_trans.
Print Assumptions four_cases_exhaustive_relational.