Library zoo.common.treemap

From stdpp Require Import
  gmap.

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

Section treemap_rooted.
  Context {N} `{Countable N} {E : Type}.

  Implicit Types node root src dst : N.
  Implicit Types edge : E.
  Implicit Types path : list E.
  Implicit Types ϵ : N × E.
  Implicit Types 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.