From 4cda26dd8d42e6dee7ebeacbb71b3f3d37d54c98 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Wed, 10 Oct 2012 11:35:41 +0200 Subject: [PATCH] Various minor changes. * Introduce a type class and notation for disjointness. * Define unions of finite maps (a lot of theory has still to be moved from memory to fin_maps). * Prove the Hoare rule for function calls with arguments. * Prove the Hoare rule to add sets of functions. * Some additional theory on lifting of assertions. --- theories/base.v | 7 +++++++ theories/fin_maps.v | 44 +++++++++++++++++++++++++++++++++----------- 2 files changed, 40 insertions(+), 11 deletions(-) diff --git a/theories/base.v b/theories/base.v index 7ce783d..38fdebf 100644 --- a/theories/base.v +++ b/theories/base.v @@ -160,6 +160,13 @@ Notation "(∉)" := (λ x X, x ∉ X) (only parsing) : C_scope. Notation "( x ∉)" := (λ X, x ∉ X) (only parsing) : C_scope. Notation "(∉ X )" := (λ x, x ∉ X) (only parsing) : C_scope. +Class Disjoint A := disjoint : A → A → Prop. +Instance: Params (@disjoint) 2. +Infix "⊥" := disjoint (at level 70) : C_scope. +Notation "(⊥)" := disjoint (only parsing) : C_scope. +Notation "( X ⊥)" := (disjoint X) (only parsing) : C_scope. +Notation "(⊥ X )" := (λ Y, disjoint Y X) (only parsing) : C_scope. + (** ** Operations on maps *) (** In this section we define operational type classes for the operations on maps. In the file [fin_maps] we will axiomatize finite maps. diff --git a/theories/fin_maps.v b/theories/fin_maps.v index d2d0113..073b46b 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -54,13 +54,23 @@ Instance finmap_singleton `{PartialAlter K M} {A} Definition list_to_map `{Insert K M} {A} `{Empty (M A)} (l : list (K * A)) : M A := insert_list l ∅. -Instance finmap_union `{Merge M} : UnionWith M := λ A f, +Instance finmap_union_with `{Merge M} : UnionWith M := λ A f, merge (union_with f). -Instance finmap_intersection `{Merge M} : IntersectionWith M := λ A f, +Instance finmap_intersection_with `{Merge M} : IntersectionWith M := λ A f, merge (intersection_with f). -Instance finmap_difference `{Merge M} : DifferenceWith M := λ A f, +Instance finmap_difference_with `{Merge M} : DifferenceWith M := λ A f, merge (difference_with f). +(** Two finite maps are disjoint if they do not have overlapping cells. *) +Instance finmap_disjoint `{Lookup K M} {A} : Disjoint (M A) := λ m1 m2, + ∀ i, m1 !! i = None ∨ m2 !! i = None. + +(** The union of two finite maps only has a meaningful definition for maps +that are disjoint. However, as working with partial functions is inconvenient +in Coq, we define the union as a total function. In case both finite maps +have a value at the same index, we take the value of the first map. *) +Instance finmap_union `{Merge M} {A} : Union (M A) := union_with (λ x _ , x). + (** * General theorems *) Section finmap. Context `{FinMap K M} `{∀ i j : K, Decision (i = j)} {A : Type}. @@ -385,30 +395,30 @@ End merge. Section union_intersection. Context (f : A → A → A). - Lemma finmap_union_merge m1 m2 i x y : + Lemma finmap_union_with_merge m1 m2 i x y : m1 !! i = Some x → m2 !! i = Some y → union_with f m1 m2 !! i = Some (f x y). Proof. - intros Hx Hy. unfold union_with, finmap_union. + intros Hx Hy. unfold union_with, finmap_union_with. now rewrite (merge_spec _), Hx, Hy. Qed. - Lemma finmap_union_l m1 m2 i x : + Lemma finmap_union_with_l m1 m2 i x : m1 !! i = Some x → m2 !! i = None → union_with f m1 m2 !! i = Some x. Proof. - intros Hx Hy. unfold union_with, finmap_union. + intros Hx Hy. unfold union_with, finmap_union_with. now rewrite (merge_spec _), Hx, Hy. Qed. - Lemma finmap_union_r m1 m2 i y : + Lemma finmap_union_with_r m1 m2 i y : m1 !! i = None → m2 !! i = Some y → union_with f m1 m2 !! i = Some y. Proof. - intros Hx Hy. unfold union_with, finmap_union. + intros Hx Hy. unfold union_with, finmap_union_with. now rewrite (merge_spec _), Hx, Hy. Qed. - Lemma finmap_union_None m1 m2 i : + Lemma finmap_union_with_None m1 m2 i : union_with f m1 m2 !! i = None ↔ m1 !! i = None ∧ m2 !! i = None. Proof. - unfold union_with, finmap_union. rewrite (merge_spec _). + unfold union_with, finmap_union_with. rewrite (merge_spec _). destruct (m1 !! i), (m2 !! i); compute; intuition congruence. Qed. @@ -421,6 +431,18 @@ Section union_intersection. Global Instance: Idempotent (=) f → Idempotent (=) (union_with f : M A → M A → M A) := _. End union_intersection. + +Lemma finmap_union_Some (m1 m2 : M A) i x : + (m1 ∪ m2) !! i = Some x ↔ + m1 !! i = Some x ∨ (m1 !! i = None ∧ m2 !! i = Some x). +Proof. + unfold union, finmap_union, union_with, finmap_union_with. + rewrite (merge_spec _). + destruct (m1 !! i), (m2 !! i); compute; try intuition congruence. +Qed. +Lemma finmap_union_None (m1 m2 : M A) b : + (m1 ∪ m2) !! b = None ↔ m1 !! b = None ∧ m2 !! b = None. +Proof. apply finmap_union_with_None. Qed. End finmap. (** * The finite map tactic *) -- 2.24.1