From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import ZArith.
From Coq Require Import Bool.
From Coq Require Import Lia.

From Padec Require Import SetoidUtil.
From Padec Require Import RelationA.
From Padec Require Import All_In.
From Padec Require Import WellfoundedUtil.
From Padec Require Import Graph_Diameter.
From Padec Require Import ListUtils.

Open Scope nat_scope.
Open Scope signature_scope.
Set Implicit Arguments.

Section DAG.

  Context {A} `{SA: Setoid A} {DA: Decider (equiv (A:=A))}.

  Variable (D: relation A) (D_compat: Proper pequiv D)
           (D_dec: Decider D).

  Definition is_dag: Prop :=
    (forall x, ~ transitive_closure D x x).

  Definition is_root x: Prop := forall y, ~ D x y.

  Notation is_simple := (is_simple (DA := DA)).
  Notation is_simple_b := (is_simple_b (DA := DA)).

  Variable (all: list A) (all_here: forall a, InA equiv a all).

  Variable (one: A).

  Lemma exists_root_in_dag: is_dag -> exists x, is_root x.

  Lemma unique_root_in_connected_dag:
    is_dag -> is_connected D ->
    forall r1 r2, is_root r1 -> is_root r2 -> r1 == r2.

  Lemma chain_flip_nil:
    forall x y, chain D x nil y -> chain (flip D) y nil x.

  Lemma chain_flip:
    forall (R: relation A) (rc: Proper pequiv R),
    forall p x y yy, RelationA.chain R x (p ++ yy :: nil) y ->
                     RelationA.chain (flip R) y (rev (x :: p)) x.

  Lemma path_to_root_in_dag:
    is_dag ->
    forall x, exists p r, is_root r /\ (r == x \/
                                        is_path D x p r).

  Lemma is_path_app:
    forall p p' x y a, is_path D x (p ++ a :: p') y <->
                       is_path D x p a /\ is_path D a p' y.

  Lemma is_simple_witness:
    forall p, is_simple_b p = false -> exists x l l' l'',
        p == l ++ x :: l' ++ x :: l''.

  Lemma eqlistA_app_end:
    forall l l' x y,
      l ++ x :: nil == l' ++ y :: nil -> x == y /\ l == l'.

  Lemma is_path_simple_in_dag:
    is_dag ->
    forall p x y, is_path D x p y ->
                  is_simple (x :: p ++ y :: nil).

  Lemma no_cycle_in_dag:
    is_dag -> forall x p, ~ is_path D x p x.

  Lemma get_parent: is_dag -> forall n, ~ is_root n -> exists m, D n m.
  Lemma WF_par: is_dag -> well_founded D.

  Lemma WF_child: is_dag -> well_founded (flip D).

End DAG.

Section Tree.

  Context {A} `{SA: Setoid A} {DA: Decider (equiv (A:=A))}.

  Variable (all: list A) (all_here: forall a, InA equiv a all).

  Variable (T: relation A) (T_compat: Proper pequiv T) (T_dec: Decider T).

  Variable (Root: A).

  Definition single_parent: Prop :=
    forall x y1 y2, T x y1 -> T x y2 -> y1 == y2.

  Definition all_path_to_root: Prop :=
    forall x, ~ x == Root -> exists p, is_path T x p Root.

  Definition is_tree: Prop :=
    is_dag T /\ single_parent /\ all_path_to_root.

  Lemma no_path_from_root:
    is_root T Root -> forall x p, ~ is_path T Root p x.

  Lemma Root_is_root:
    is_dag T -> all_path_to_root ->
    forall p, p == Root <-> is_root T p.

  Lemma Root_is_root':
    is_dag T -> all_path_to_root -> is_root T Root.

  Lemma is_root_unique:
    is_dag T -> all_path_to_root ->
    forall r, is_root T r -> r == Root.

  Lemma is_spanning_build_path:
    all_path_to_root -> forall n, ~ n == Root ->
                                  {p | is_path T n p Root }.

  Lemma is_path_unique_in_tree:
    is_dag T -> single_parent ->
    forall x y p1 p2, is_path T x p1 y -> is_path T x p2 y ->
                      p1 == p2.

  Lemma is_path_dist_in_tree:
    is_dag T -> single_parent ->
    forall p x y, is_path T x p y ->
                  forall d, S (length p) = d <-> is_dist T x y d.

  Definition is_leaf x := forall y, ~ T y x.

  Instance is_leaf_compat: Proper pequiv is_leaf.


  Lemma is_leaf_dec: forall x, {is_leaf x}+{~ is_leaf x}.

  Definition children x :=
    filter (fun y => if T_dec y x then true else false) all.

  Instance fun_T_dec_compat:
    Proper fequiv
           (fun x y => if T_dec y x then true else false).

  Instance children_compat: Proper pequiv children.

  Lemma children_prop:
    forall x y, InA equiv y (children x) <-> T y x.

  Lemma is_leaf_no_children:
    forall x, is_leaf x <-> children x = nil.

  Definition in_subtree r x :=
    r == x \/ exists p, is_path T x p r.

  Lemma in_subtree_dec: forall r x, {in_subtree r x}+{~ in_subtree r x}.

  Instance in_subtree_compat: Proper pequiv in_subtree.

  Definition subtree_elements (x: A): list A :=
    filter (fun l => if in_subtree_dec x l then true else false) all.

  Instance subtree_elements_compat: Proper pequiv subtree_elements.

End Tree.

Section SpanningTree.
  Context {A} `{SA: Setoid A} {DA: Decider (equiv (A:=A))}.

  Variable (all: list A) (all_here: forall a, InA equiv a all).

  Variable (T: relation A) (T_compat: Proper pequiv T) (T_dec: Decider T).

  Variable (G: relation A) (G_compat: Proper pequiv G) (G_dec: Decider G).

  Variable (Root: A).

  Definition is_spanning_tree: Prop :=
    is_subgraph T G /\ is_tree T Root.

  Definition is_BFS: Prop :=
    forall x d, is_dist T x Root d -> is_dist G x Root d.

End SpanningTree.

Section Compat.

  Context {A} `{SA: Setoid A}.

  Instance single_parent_compat:
    Proper pequiv (single_parent (A := A)).

  Instance all_path_to_root_compat:
    Proper pequiv (all_path_to_root (A := A)).

  Instance is_dag_compat:
    Proper pequiv (is_dag (A := A)).

  Instance is_tree_compat:
    Proper pequiv (is_tree (A := A)).

  Instance is_spanning_tree_compat:
    Proper pequiv (is_spanning_tree (A := A)).

  Instance is_root_compat: Proper pequiv (is_root (A := A)).

  Instance is_BFS_compat: Proper pequiv (is_BFS (A := A)).

End Compat.

Section Dec_finite.

  Context {A} `{SA: Setoid A} {DA: Decider (equiv (A:=A))}.
  Variable (all_A: list A)
           (all_A_prop: forall a, InA equiv a all_A).

  Lemma is_root_dec:
    forall p (r: A),
      Proper pequiv p -> (forall x, {p r x} + {~ p r x}) ->
      {is_root p r} + {~ is_root p r}.

  Lemma is_dag_dec:
    forall (G: relation A),
      Proper pequiv G -> (forall x y, {G x y} + {~G x y}) ->
      {is_dag G} + {~is_dag G}.

  Lemma single_parent_dec:
    forall (G: relation A),
      Proper pequiv G -> (forall x y, {G x y} + {~G x y}) ->
      {single_parent G} + {~single_parent G}.

  Lemma all_path_to_root_dec:
    forall (G: relation A) (Root: A),
      Proper pequiv G -> (forall x y, {G x y} + {~G x y}) ->
      {all_path_to_root G Root} + {~ all_path_to_root G Root}.

  Lemma is_tree_dec:
    forall (G: relation A) (Root: A),
      Proper pequiv G -> (forall x y, {G x y} + {~G x y}) ->
      {is_tree G Root} + {~ is_tree G Root}.

  Lemma is_spanning_tree_dec:
    forall (G G': relation A),
      Proper pequiv G -> (forall x y, {G x y} + {~G x y}) ->
      Proper pequiv G' -> (forall x y, {G' x y} + {~G' x y}) ->
      forall p, {is_spanning_tree G G' p} + {~ is_spanning_tree G G' p}.

  Lemma is_BFS_dec:
    forall (G G': relation A),
      Proper pequiv G -> (forall x y, {G x y} + {~G x y}) ->
      Proper pequiv G' -> (forall x y, {G' x y} + {~G' x y}) ->
      forall p, {is_BFS G' G p} + { ~ is_BFS G' G p}.

End Dec_finite.

Section Height.

  Context {A} `{SA: Setoid A} {DA: Decider (equiv (A:=A))}.

  Variable (all: list A) (all_here: forall a, InA equiv a all).

  Variable (T: relation A) (T_compat: Proper pequiv T) (T_dec: Decider T).

  Variable (Root: A) (IT: is_tree T Root).

  Definition is_height (a: A) (h: nat): Prop :=
    (is_leaf T a /\ h = 0) \/
    (forall b p, is_path T b p a -> h >= S (length p)) /\
    exists b p, is_path T b p a /\ h = S (length p).

  Definition max_list' (a: nat) (l: list nat): nat :=
    fold_right max a l.

  Global Instance max_list'_compat: Proper pequiv max_list'.

  Lemma max_list'_prop:
    forall a l m, max_list' a l = m <->
                  InA equiv m (a :: l) /\
                  forall x, InA equiv x (a :: l) -> m >= x.

  Definition height: nat :=
    compute_diameter' all_here T_compat T_dec Root (DA := DA).

End Height.

Close Scope signature_scope.
Close Scope nat_scope.
Unset Implicit Arguments.