Require Import Relations Recdef.

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Require Import choice fintype finfun finset path fingraph bigop.

Require Import edone bcase fset.
Require Import base.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

Infrastructure

Termination and Transitive Closure

Inductive sn (X : Type) (R : X -> X -> Prop) (x : X) : Prop :=
  SN : (forall y, R x y -> sn R y) -> sn R x.

Inductive star (X : Type) (R : X -> X -> Prop) (x : X) : X -> Prop :=
| Star0 : star R x x
| StarL y z : R x z -> star R z y -> star R x y.

Definition terminates X (e : X -> X -> Prop) := forall x, sn e x.

Section SeqSubConnect.
  Variable (T : choiceType) (xs : seq T) (e : rel T).
  Hypothesis sub_closed : forall x y, e x y -> x \in xs -> y \in xs.

  Definition restrict := [rel x y : seq_sub xs | e (val x) (val y)].

  Lemma sn_restrict x (Hx : x \in xs) : sn e x -> sn [eta restrict ] (SeqSub x Hx).
  Proof.
    move => S. elim: S Hx => {x} x _ IH Hx.
    apply: SN => [[y Hy]] /= ?. exact: IH.
  Qed.

  Lemma connect_restrict x y (Hx : x \in xs) (Hy : y \in xs) :
    star e x y -> connect restrict (SeqSub x Hx) (SeqSub y Hy).
  Proof.
    move => H. elim: H Hx Hy => {x y} [x Hx Hy|x z y xy _ IH Hx Hz].
    - by rewrite (bool_irrelevance Hx Hy) connect0.
    - exact: connect_trans (connect1 _) (IH (sub_closed xy Hx) Hz).
  Qed.
End SeqSubConnect.

Finite Rooted Labeled Graphs

Record graph (L : Type) :=
  Graph { vertex :> finType ; edge : rel vertex ; label : vertex -> L }.

Record rGraph (L : Type) := RGraph {
    graph_of :> graph L ;
    root : graph_of ;
    rootP x : connect (@edge _ graph_of) root x }.

Section GraphTheory.
  Variables (L : choiceType) (p : L -> {fset L } -> bool).
  Implicit Types (G : graph L) (rG : rGraph L).

  Definition erel G := (@edge _ G).
  Implicit Arguments erel [].
  Definition glocal G := [forall x : G , p (label x) [fset (label y) | y <- fset (edge x)]].
  Definition respects e G := [forall x : G , forall y : G , edge x y ==> e (label x) (label y)].

  Definition leaf G (x:G) := ~~ [exists y, edge x y].
End GraphTheory.
Arguments erel [L] G _ _.

Finitely Branching Trees and Conversion to Rooted Dags

Inductive tree X := Tree of X & seq (tree X).

Due to the nested recursion in tree the automatically generated induction principle is next to useless and we derive our own

Lemma tree_rect' X (P : tree X -> Type) (Ps : seq (tree X) -> Type) :
  Ps [::] ->
  (forall t ts, P t -> Ps ts -> Ps (t ::ts)) ->
  (forall x ts, Ps ts -> P (Tree x ts)) ->
  forall t , P t.
Proof.
  move => P'nil P'cons Pcons. fix 1. case => t ts.
  apply : Pcons. elim : ts => [|t' tr]. apply : P'nil.
  apply : P'cons. apply tree_rect'.
Qed.

The type of trees over a countable type is itself a countable type. In particular this allows for a simpler induction principle

Section TreeCountType.
  Variable (T : countType).

  Fixpoint tpickle (t : tree T) : GenTree.tree unit :=
    let: Tree x ts := t in GenTree.Node (pickle x) (map tpickle ts).

  Fixpoint tunpickle (t : GenTree.tree unit) : option (tree T) :=
    if t isn't GenTree.Node n ts then None else
      obind (fun x => Some (Tree x (pmap tunpickle ts))) (unpickle n).

  Lemma tpickleK : pcancel tpickle tunpickle.
  Proof.
    pose pmapK ts := pmap tunpickle [seq tpickle i | i <- ts ] = ts.
    apply: (tree_rect' (Ps := pmapK)) => //= [t ts IH tsK|x ts tsK].
    - by rewrite /pmapK /= IH tsK.
    - by rewrite pickleK /= tsK.
  Qed.

  Definition tree_countMixin := PcanCountMixin tpickleK.
  Canonical tree_eqType := EqType (tree T) (Countable.EqMixin tree_countMixin).
  Canonical tree_choiceType := ChoiceType (tree T) (PcanChoiceMixin tpickleK).
  Canonical tree_countType := CountType (tree T) tree_countMixin.

  Lemma simple_tree_rect (P : tree T -> Type) :
   (forall x xs , (forall y , y \in xs -> P y) -> P (Tree x xs)) -> forall t , P t.
  Proof.
    move => ?. apply: (tree_rect' (Ps := fun xs => forall y , y \in xs -> P y)) => //.
    move => t ts Pt H y. rewrite in_cons. case/orS => //. by move/eqP ->. apply: H.
  Qed.
End TreeCountType.

We convert trees to rooted dags in a way that preserves all local properties. Here, local means that the property relates the label of some node to the set of labels on the immediate children. We begin by defining the parent-child relation on trees

Section TreeRel.
  Variables (L : countType).
  Implicit Types (s t u : tree L) (p : L -> {fset L } -> bool) (e : rel L).

  Definition rlab t := let: Tree l _ := t in l.

  Fixpoint subtrees (t : tree L) :=
    t :: let: Tree x ts := t in flatten (map subtrees ts).

  Lemma subtrees_refl t : t \in subtrees t.
  Proof. case: t => x ts. exact: mem_head. Qed.
  Hint Resolve subtrees_refl.

  Lemma subtrees1 x t ts : t \in ts -> t \in subtrees (Tree x ts).
  Proof.
    move => in_ts. rewrite unfold_in /= [X in _ || X](_ : is_true _ ) //=.
    apply/flattenP. exists (subtrees t) => //. exact: map_f.
  Qed.

  Lemma subtrees_trans u s t : s \in subtrees u -> u \in subtrees t -> s \in subtrees t.
  Proof.
    move: t s u. apply: simple_tree_rect => x ts IH s t H2 H1.
    rewrite /= inE in H1. case/predU1P : H1 H2 => [->//|].
    case/flattenP => xs /mapP [y Hy ->] H1 H2. move: (IH _ Hy) => stc_y.
    rewrite /= inE. rightb;apply/flattenP.
    exists (subtrees y); [exact: map_f| exact: stc_y H1].
  Qed.

  Definition tree_rel := [rel s t : tree L | let: Tree _ ts := s in t \in ts].

  Lemma tree_rooted s t : s \in subtrees t -> star [eta tree_rel ] t s.
  Proof.
    move: t s. apply: simple_tree_rect => t ts IH s.
    rewrite /= in_cons. case/predU1P => [->|]; first exact: Star0.
    case/flattenP => xs /mapP [u Hu ->] sub_u. exact: StarL (IH _ Hu _ sub_u).
  Qed.

  Lemma tree_rel_sn t : sn [eta tree_rel ] t.
  Proof. move: t. apply: simple_tree_rect => x ts IH /=. exact: SN. Qed.

  Definition tlocal p :=
    fix tlocal t := let: Tree l ts := t in all tlocal ts && p l (set_of (map rlab ts)).

  Lemma tlocal_sub p s t : s \in subtrees t -> tlocal p t -> tlocal p s.
  Proof.
    move/tree_rooted. elim => {s t} // [[a ts]] y z /= in_ts _ IH.
    case/andP => /allP /(_ _ in_ts). by auto.
  Qed.

  Definition trespects e t := tlocal (fun l ls => all (e l) ls) t.

  Lemma trespects_leaf e l : trespects e (Tree l [::]).
  Proof. apply/allP => ? /=. by rewrite set_ofE. Qed.

  Lemma tlocalE p (l : L) ts :
    tlocal p (Tree l ts) = all (tlocal p) ts && p l (set_of [seq rlab i | i <- ts ]).
  Proof. done. Qed.

  Lemma trespectsE e (l : L) ts :
    trespects e (Tree l ts) = [all t in ts , trespects e t] && [all l' in [seq rlab t | t <- ts ] , e l l'].
  Proof.
    rewrite /trespects /=. apply: andb_id2l => _.
    apply/allP/allP; move => H ? H';apply H; by rewrite set_ofE in H' *.
  Qed.

End TreeRel.

The conversion from trees to graphs uses the subtress as nodes and the (suitable restriced) parent child relation for edges

Section GraphOf.
  Local Arguments SeqSub [T s ssval] ssvalP.
  Unset Printing Records.

  Variables (L : countType) (t : tree L).
  Implicit Types (p : L -> {fset L } -> bool) (e : rel L).

  Definition graph_of_type := seq_sub (subtrees t).
  Definition graph_of_label (x : graph_of_type) := rlab (val x).
  Definition graph_of_rel : rel graph_of_type := restrict (subtrees t) (tree_rel _).

  Definition graph_of_root := SeqSub (subtrees_refl t).

  Lemma graph_of_rootP y : connect graph_of_rel graph_of_root y.
  Proof.
    case: y => u Hu. apply: connect_restrict; last exact: tree_rooted.
    case => a ts y /= H. apply: subtrees_trans. exact: subtrees1.
  Qed.

  Definition graph_of_tree := Graph graph_of_rel graph_of_label.

  Definition rgraph_of := @RGraph _ graph_of_tree _ graph_of_rootP.

  Lemma rgraph_of_local p : tlocal p t -> glocal p rgraph_of.
  Proof.
    move => t_loc. apply/forallP => [[s in_sub]] /=.
    rewrite /graph_of_label /graph_of_rel /=. move: (tlocal_sub in_sub t_loc).
    case: s in_sub => x ts in_t /= /andP[_]. congr p.
    apply: fset_ext => a. rewrite set_ofE. apply/mapP/fimsetP.
    - case => t' in_ts ->.
      have Ht': t' \in subtrees t. apply: subtrees_trans in_t. exact: subtrees1.
      exists (SeqSub Ht') => //. by rewrite inE in_fsetT.
    - case => [[s sub_t] H ->]. rewrite inE in_fsetT /= in H. by exists s.
  Qed.

  Lemma rgraph_of_acyclic : terminates (erel rgraph_of).
  Proof. case => x Hx. apply: sn_restrict. exact: tree_rel_sn. Qed.

  Lemma rgraph_of_respects e : trespects e t -> respects e (rgraph_of).
  Proof.
    move/rgraph_of_local => gl. apply/forallP => x. apply/forall_inP => y xy.
    move/allP: (forallP gl x) => /(_ (label y)). apply. apply: in_fimset. by rewrite fsetE.
  Qed.

End GraphOf.

Arguments existT [A] [P] x _.

Disjoint Union of finite graphs

Section Disjoint.
  Variables (L : Type) (I:finType) (G : I -> graph L).

  Definition lift_edge (x y : {i : I & G i}) :=
    (tag x == tag y ) && edge (tagged x) (tagged_as x y).

  Lemma lift_eq (i : I) (x y : G i) :
    lift_edge (existT i x) (existT i y) = edge x y.
  Proof. by rewrite /lift_edge /= eqxx tagged_asE. Qed.

  Lemma lift_eqn (ix iy : I) (x : G ix) (y : G iy) :
    ix != iy -> lift_edge (existT ix x) (existT iy y) = false.
  Proof. by rewrite /lift_edge /= => /negbTE ->. Qed.

  Lemma liftE (i j : I) (x : G i) (y : G j) :
    lift_edge (existT i x) (existT j y) -> j = i.
  Proof. by case/andP => /= /eqP. Qed.

  Lemma lift_connect (i : I) (x y : G i) :
    connect (@edge _ (G i)) x y -> connect lift_edge (existT i x) (existT i y).
  Proof. case/connectP => p.
    elim: p x y => /= [x y _ ->|z p IHp x y /andP [? ?] ?]; first exact: connect0.
    apply: (@connect_trans _ _ (existT i z)); last exact: IHp.
    by rewrite connect1 // lift_eq.
  Qed.
End Disjoint.