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.
Import Prenex Implicits.
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.
Import Prenex Implicits.
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).
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).
End SeqSubConnect.
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.
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.
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.
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.
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.
Hint Resolve subtrees_refl.
Lemma subtrees1 x t ts : t \in ts -> t \in subtrees (Tree x ts).
Lemma subtrees_trans u s t : s \in subtrees u -> u \in subtrees t -> s \in subtrees t.
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.
Lemma tree_rel_sn t : sn [eta tree_rel] t.
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.
Definition trespects e t := tlocal (fun l ls => all (e l) ls) t.
Lemma trespects_leaf e l : trespects e (Tree l [::]).
Lemma tlocalE p (l : L) ts :
tlocal p (Tree l ts) = all (tlocal p) ts && p l (set_of [seq rlab i | i <- ts]).
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'].
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
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.
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.
Lemma rgraph_of_acyclic : terminates (erel rgraph_of).
Lemma rgraph_of_respects e : trespects e t -> respects e (rgraph_of).
End GraphOf.
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.
Lemma lift_eqn (ix iy : I) (x : G ix) (y : G iy) :
ix != iy -> lift_edge (existT ix x) (existT iy y) = false.
Lemma liftE (i j : I) (x : G i) (y : G j) :
lift_edge (existT i x) (existT j y) -> j = i.
Lemma lift_connect (i : I) (x y : G i) :
connect (@edge _ (G i)) x y -> connect lift_edge (existT i x) (existT i y).
End Disjoint.