Require Export HFS.Operations.

Section TransitiveClosure.
  Variable X : HF.
  Implicit Types x y z a u : X.

  Definition TC x u := forall z, z el u <-> forall y, trans y -> x <<= y -> z el y.

  Fact TC_trans x u :
    TC x u -> trans u.
  Proof.
    intros A y B a C. apply A. intros b D E.
    enough (y el b) by hfs. now apply A.
  Qed.

  Fact TC_incl x u :
    TC x u -> x <<= u.
  Proof.
    intros A y B. apply A. auto.
  Qed.

  Fact TC_fun x y y' :
    TC x y -> TC x y' -> y = y'.
  Proof.
    intros A B. extensio as z. split; intros C.
    - apply B. intros u D E. now apply A.
    - apply A. intros u D E. now apply B.
  Qed.

  Lemma TC_empty :
    TC 0 0.
  Proof.
     intros z. split. hfs.
     intros A. apply A; hfs.
  Qed.

  Lemma TC_adj a x u v :
    TC a u -> TC x v -> TC (a@x) (a @ (bun u v)).
  Proof.
    intros A B z. split.
    - rewrite adj_el, bun_el. intros [-> |[C|C]] y D E.
      + hfs.
      + apply A; hfs.
      + apply B; try hfs.
    - intros C. apply C.
      + intros b [-> |[D|D] % bun_el] % adj_el c E; rewrite adj_el, bun_el.
        * generalize (TC_incl A). hfs.
        * generalize (TC_trans A). hfs.
        * generalize (TC_trans B). hfs.
      + intros b; rewrite !adj_el, bun_el. intros [-> |D].
        * now auto.
        * generalize (TC_trans B), (TC_incl B). hfs.
  Qed.

  Lemma tc' x :
    Sigma u, TC x u.
  Proof.
    hf_induction x.
    - eauto using TC_empty.
    - intros a x (u&A) (v&B). eauto using TC_adj.
  Qed.

  Definition tc x := projT1 (tc' x).

  Fact TC_tc x :
    TC x (tc x).
  Proof.
    unfold tc. destruct (tc' x) as (u&A). apply A.
  Qed.

  Theorem tc_el x z :
    z el tc x <-> forall y, trans y -> x <<= y -> z el y.
  Proof.
    apply TC_tc.
  Qed.

  Fact tc_trans x:
    trans (tc x).
  Proof.
    eapply TC_trans, TC_tc.
  Qed.

  Fact tc_incl x:
    x <<= tc x.
  Proof.
    eapply TC_incl, TC_tc.
  Qed.

  Fact tc_least x y :
    trans y -> x <<= y -> tc x <<= y.
  Proof.
    intros A B z C % tc_el; eauto.
  Qed.

  Fact tcE_eq :
    tc 0 = 0.
  Proof.
    apply TC_fun with (x:=0). apply TC_tc. apply TC_empty.
  Qed.

  Fact tcA_eq a x:
    tc (a@x) = a @ (bun (tc a) (tc x)).
  Proof.
    apply TC_fun with (x := a@x). apply TC_tc.
    apply TC_adj; apply TC_tc.
  Qed.

  Inductive tel x y : Prop :=
  | telI : x el y -> x < y
  | telT z : x < z -> z < y -> x < y
  where "x '<' y" := (tel x y).

  Fact tel_inv x y :
    x < y <-> x el y \/ exists z, x < z /\ z el y.
  Proof.
    split.
    - induction 1 as [x z A|x y z A _ _ IHB].
      + auto.
      + destruct IHB as [C|(u&C&D)]; eauto using tel.
    - intros [A|(z&A&B)]; eauto using tel.
  Qed.

  Fact tel_adjL z a x :
    z < a -> z < a @ x.
  Proof.
    intros A. apply telT with (z:=a). exact A. apply telI. hfs.
  Qed.

  Fact tel_adjR z a x :
    z < x -> z < a @ x.
  Proof.
    intros [A|(u&A&B)] % tel_inv.
    - apply telI. hfs.
    - apply telT with (z:=u). exact A. apply telI. hfs.
  Qed.

  Theorem tel_TC x y :
    x < y <-> x el tc y.
  Proof.
    split; intros A.
    - apply tc_el. intros u B C. revert u B C.
      induction A as [x z A|x y z _ IHA _ IHB].
      + hfs.
      + intros u C D. specialize (IHB u C D). apply IHA; hfs.
    - revert A. hf_induction y.
      + rewrite tcE_eq. hfs.
      + intros a y IHa IHy.
        rewrite tcA_eq, adj_el, bun_el. intros [-> |[A|A]].
        * apply telI. hfs.
        * auto using tel_adjL.
        * auto using tel_adjR.
  Qed.

  Corollary tel_dec x y :
    dec (x < y).
  Proof.
    apply (dec_trans (x el tc y)).
    - symmetry. apply tel_TC.
    - auto.
  Qed.

End TransitiveClosure.