graph.v 3.96 KB
 Amin Timany committed Dec 15, 2017 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 committed Feb 20, 2019 60 `````` apply set_equiv_spec_L; split; trivial. `````` Amin Timany committed Dec 15, 2017 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 _ {_ _}.``````