Library zoo.common.treemap

Require Import stdpp.gmap.

Require Import zoo.prelude.
Require Import zoo.options.

Section treemap ۰ rooted.
  Context {N} `{Countable N} {E : Type}.

  Implicit Type node root src dst : N.
  Implicit Type edge : E.
  Implicit Type path : list E.
  Implicit Type ϵ : N × E.
  Implicit Type tree : gmap N (N × E).

  Inductive treemap ۰ path tree dst : N → list E → Prop :=
    | treemap ۰ path ｰ nil :
        treemap ۰ path tree dst dst []
    | treemap ۰ path ｰ cons {node1} ϵ node2 edge path :
        tree !! node1 = Some ϵ →
        ϵ .1 = node2 →
        ϵ .2 = edge →
        treemap ۰ path tree dst node2 path →
        treemap ۰ path tree dst node1 (edge :: path).
  #[local] Hint Constructors treemap ۰ path : core.

  Definition treemap ۰ rooted tree root :=
    tree !! root = None ∧
      ∀ node,
      is_Some (tree !! node) →
        ∃ path,
        treemap ۰ path tree root node path.

  Definition treemap ۰ reroot tree root root' edge :=
    <[root := (root', edge )]> (delete root' tree ).

  Lemma treemap ۰ path ｰ app tree dst1 node path1 dst2 path2 :
    treemap ۰ path tree dst1 node path1 →
    treemap ۰ path tree dst2 dst1 path2 →
    treemap ۰ path tree dst2 node (path1 ++ path2).
  Lemma treemap ۰ path ｰ snoc {tree dst1 node path} ϵ dst2 edge :
    treemap ۰ path tree dst1 node path →
    tree !! dst1 = Some ϵ →
    ϵ .1 = dst2 →
    ϵ .2 = edge →
    treemap ۰ path tree dst2 node (path ++ [edge]).

  Lemma treemap ۰ path ｰ nil ｰ inv tree dst node :
    treemap ۰ path tree dst node [] →
    node = dst.
  Lemma treemap ۰ path ｰ cons ｰ inv tree dst node edge path :
    treemap ۰ path tree dst node (edge :: path) →
      ∃ node',
      tree !! node = Some (node', edge ) ∧
      treemap ۰ path tree dst node' path.
  Lemma treemap ۰ path ｰ app ｰ inv tree dst node path1 path2 :
    treemap ۰ path tree dst node (path1 ++ path2) →
      ∃ node',
      treemap ۰ path tree node' node path1 ∧
      treemap ۰ path tree dst node' path2.

  Lemma treemap ۰ path ｰ mono {tree dst node path} tree' :
    tree ##ₘ tree' →
    treemap ۰ path tree dst node path →
    treemap ۰ path (tree ∪ tree') dst node path.

  Lemma treemap ۰ rooted ｰ empty root :
    treemap ۰ rooted ∅ root.

  Lemma treemap ۰ rooted ｰ root tree root :
    treemap ۰ rooted tree root →
    tree !! root = None.

  Lemma treemap ۰ path ｰ is_nil tree root path :
    treemap ۰ rooted tree root →
    treemap ۰ path tree root root path →
    path = [].
  Lemma treemap ۰ path ｰ is_cons tree root node path :
    treemap ۰ rooted tree root →
    treemap ۰ path tree root node path →
    node ≠ root →
      ∃ node' edge path',
      path = edge :: path' ∧
      tree !! node = Some (node', edge ) ∧
      treemap ۰ path tree root node' path'.

  #[local] Lemma treemap ۰ path ｰ acyclic {tree root path} node ϵ node' :
    treemap ۰ rooted tree root →
    treemap ۰ path tree root node path →
    tree !! node = Some ϵ →
    ϵ .1 = node' →
    node ≠ node'.
  Lemma treemap ۰ rooted ｰ acyclic {tree root} node ϵ node' :
    treemap ۰ rooted tree root →
    tree !! node = Some ϵ →
    ϵ .1 = node' →
    node ≠ node'.

  Lemma treemap ۰ rooted ｰ path {tree root} node :
    treemap ۰ rooted tree root →
    is_Some (tree !! node) →
      ∃ path,
      treemap ۰ path tree root node path.

  Lemma treemap ۰ rooted ｰ lift {tree root} root' edge :
    treemap ۰ rooted tree root →
    tree !! root' = None →
    root ≠ root' →
    treemap ۰ rooted (<[root := (root', edge )]> tree) root'.

  Lemma treemap ｰ reroot ｰ path {tree root} root' ϵ edge dst node path :
    treemap ۰ rooted tree root →
    tree !! root' = Some ϵ →
    ϵ .1 = root →
    dst ≠ root →
    treemap ۰ path tree dst node path →
    treemap ۰ path (treemap ۰ reroot tree root root' edge) dst node path.
  Lemma treemap ｰ reroot ｰ path' {tree root} root' ϵ edge node path :
    treemap ۰ rooted tree root →
    tree !! root' = Some ϵ →
    ϵ .1 = root →
    treemap ۰ path tree root' node path →
    treemap ۰ path (treemap ۰ reroot tree root root' edge) root' node path.
  Lemma treemap ｰ reroot ｰ rooted {tree root} root' ϵ edge :
    treemap ۰ rooted tree root →
    tree !! root' = Some ϵ →
    ϵ .1 = root →
    treemap ۰ rooted (treemap ۰ reroot tree root root' edge) root'.
End treemap ۰ rooted.

#[global] Opaque treemap ۰ rooted.