Add the spanning tree algorithm.

This closes #3 (closed).

theories/spanning_tree/graph.v

+From iris.algebra Require Import base gmap.
+From stdpp Require Import gmap mapset.
+
+Section Graphs.
+  Context {T : Type} {HD : EqDecision T} {HC : @Countable T HD}.
+
+  Definition graph := gmap T (option T * option T).
+
+  Identity Coercion graph_to_gmap : graph >-> gmap.
+
+  Definition get_left (g : graph) x : option T := g !! x ≫= fst.
+  Definition get_right (g : graph) x : option T := g !! x ≫= snd.
+
+  Definition strict_sub_child (ch ch' : option T) :=
+    match ch, ch' with
+    | Some c, Some c' => c = c'
+    | Some c, None => True
+    | None, Some _ => False
+    | None, None => True
+    end.
+
+  Definition strict_sub_children (ch ch' : option T * option T) : Prop :=
+    strict_sub_child (ch.1) (ch'.1) ∧ strict_sub_child (ch.2) (ch'.2).
+
+  Definition strict_subgraph (g g' : graph) : Prop :=
+    ∀ x, strict_sub_children (get_left g x, get_right g x)
+           (get_left g' x, get_right g' x).
+
+(* A path is a list of booleans true for left child and false for the right *)
+(* The empty list is the identity trace (from x to x). *)
+  Definition path := list bool.
+
+  Identity Coercion path_to_list : path >-> list.
+
+  Inductive valid_path (g : graph) (x y : T) : path → Prop :=
+  | valid_path_E : x ∈ dom (gset _) g → x = y → valid_path g x y []
+  | valid_path_l (xl : T) p : get_left g x = Some xl → valid_path g xl y p →
+      valid_path g x y (true :: p)
+  | valid_path_r (xr : T) p : get_right g x = Some xr → valid_path g xr y p →
+      valid_path g x y (false :: p).
+
+  Definition connected (g : graph) (x : T) :=
+    ∀ z, z ∈ dom (gset _) g → ∃ p, valid_path g x z p.
+
+  Definition front (g : graph) (t t' : gset T) := t ⊆ dom (gset _) g ∧
+    ∀ x v, x ∈ t → (get_left g x = Some v) ∨ (get_right g x = Some v) →
+       v ∈ t'.
+
+  Definition maximal (g : graph) := front g (dom (gset _) g) (dom (gset _) g).
+
+  Definition tree (g : graph) (x : T) :=
+    ∀ z, z ∈ dom (gset _) g → exists !p, valid_path g x z p.
+
+  (* graph facts *)
+
+  Lemma front_t_t_dom g z t :
+    z ∈ t → connected g z → front g t t → t = dom (gset _) g.
+  Proof.
+    intros Hz Hc [Hsb Hdt].
+    apply collection_equiv_spec_L; split; trivial.
+    apply elem_of_subseteq => x Hx. destruct (Hc x Hx) as [p pv].
+    clear Hc Hx; revert z Hz pv.
+    induction p => z Hz pv.
+    - by inversion pv; subst.
+    - inversion pv as [|? ? Hpv1 Hpv2 Hpv3|? ? Hpv1 Hpv2 Hpv3]; subst.
+      + eapply IHp; [eapply Hdt|apply Hpv2]; eauto.
+      + eapply IHp; [eapply Hdt|apply Hpv2]; eauto.
+  Qed.
+
+  Lemma front_mono g t t' s : front g t t' → t' ⊆ s → front g t s.
+  Proof. intros [Htd Hf] Hts; split; eauto. Qed.
+
+  Lemma front_empty g : front g ∅ ∅.
+  Proof. split; auto. intros ? Hcn; inversion Hcn. Qed.
+
+  Lemma strict_sub_children_refl v : strict_sub_children v v.
+  Proof. by destruct v as [[] []]. Qed.
+
+  Lemma strict_sub_children_trans v1 v2 v3 : strict_sub_children v1 v2 →
+    strict_sub_children v2 v3 → strict_sub_children v1 v3.
+  Proof.
+   destruct v1 as [[] []]; destruct v2 as [[] []];
+   destruct v3 as [[] []]; cbv; by intuition subst.
+  Qed.
+
+  Lemma strict_sub_children_None v : strict_sub_children v (None, None).
+  Proof. by destruct v as[[] []]. Qed.
+
+  Lemma strict_subgraph_empty g : strict_subgraph g ∅.
+  Proof.
+    intros i.
+    rewrite /get_left /get_right /strict_sub_child lookup_empty //=.
+    by destruct (g !! i) as [[[] []]|].
+  Qed.
+
+  Lemma get_left_dom g x y : get_left g x = Some y → x ∈ dom (gset _) g.
+  Proof.
+    rewrite /get_left elem_of_dom. case _ : (g !! x); inversion 1; eauto.
+  Qed.
+
+  Lemma get_right_dom g x y : get_right g x = Some y → x ∈ dom (gset _) g.
+  Proof.
+    rewrite /get_right elem_of_dom. case _ : (g !! x); inversion 1; eauto.
+  Qed.
+
+  Lemma path_start g x y p : valid_path g x y p → x ∈ dom (gset _) g.
+  Proof. inversion 1; subst; eauto using get_left_dom, get_right_dom. Qed.
+
+  Lemma path_end g x y p : valid_path g x y p → y ∈ dom (gset _) g.
+  Proof. induction 1; subst; eauto. Qed.
+
+End Graphs.
+
+Arguments graph _ {_ _}.
\ No newline at end of file