graph.v 3.96 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
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].
Robbert Krebbers's avatar
Robbert Krebbers committed
60
    apply set_equiv_spec_L; split; trivial.
61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
    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 _ {_ _}.