Merge pull request #3 from libtx/avl

Add an instance for FMapAVL

Author: k32

Makefile

@@ -14,7 +14,7 @@ CoqMakefile: Makefile _CoqProject
 invoke-coqmakefile: CoqMakefile
 	$(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))
 
-.PHONY: invoke-coqmakefile record-update $(KNOWNFILES)
+.PHONY: invoke-coqmakefile $(KNOWNFILES)
 
 ####################################################################
 ##                      Your targets here                         ##

README.org

@@ -14,4 +14,5 @@ This repository contains:
 - Some theorems related to Wlog equivalence
 
 Instances:
-- =LibTx.Storage.Instances.List=
+- =LibTx.Storage.Instances.List=: pure storage instance based on flat lists
+- =LibTx.Storage.Instances.AVL=: pure storage instance based on AVL-tree (wrapper over =FMapAVL= from the standard library)

_CoqProject

@@ -4,3 +4,4 @@ theories/Storage/Tactics.v
 theories/Storage/Properties.v
 theories/Storage.v
 theories/Storage/Instances/List.v
+theories/Storage/Instances/AVL.v

coq-libtx-storage.opam

@@ -5,7 +5,7 @@ homepage: "https://github.com/libtx/Storage"
 dev-repo: "git+https://github.com/libtx/Storage.git"
 license: "GPL3"
 maintainer: "noreply@example.com"
-synopsis: "Formal model of storage backend"
+synopsis: "Axiomatic abstraction of storage container"
 description: """
 """
 
@@ -14,14 +14,12 @@ build: [
 ]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.19") | (= "dev")}
-  "coq-record-update" {(>= "0.3" & < "0.4~")}
+  "coq" {(>= "8.19")}
   "coq-hammer"
 ]
 
 tags: [
-  "keyword:program verification"
-  "keyword:distributed algorithms"
+  "keyword:containers"
 ]
 authors: [
   "k32"

theories/Storage/Classes.v

@@ -1,7 +1,7 @@
 From Coq Require Import
-     List
-     Classes.EquivDec
-     Classes.SetoidClass.
+  List
+  Classes.EquivDec
+  Classes.SetoidClass.
 
 Section defns.
   Context {K V : Type}.

theories/Storage/Instances/AVL.v

@@ -0,0 +1,99 @@
+From Coq Require Import
+  FMapInterface
+  FMapAVL
+  OrderedType
+  OrderedTypeEx
+  ZArith.
+
+Require Import Classes.
+
+Module Type Make (E : OrderedType).
+  Include FMapAVL.Make E.
+
+  Parameter dec_eq_is_eq : forall a b, E.eq a b <-> a = b.
+
+  Lemma fmap_new_empty {ValT : Type} k : find k (@empty ValT) = None.
+  Proof.
+    remember (find k (empty ValT)) as maybe_v.
+    destruct maybe_v as [v|].
+    - exfalso.
+      specialize (@empty_1 ValT k v) as H.
+      symmetry in Heqmaybe_v. now apply find_2 in Heqmaybe_v.
+    - reflexivity.
+  Qed.
+
+  Lemma fmap_keep {ValT : Type} s k (v : ValT) : find k (add k v s) = Some v.
+  Proof.
+    specialize (@add_1 ValT s k k v (E.eq_refl k)) as H.
+    now apply find_1.
+  Qed.
+
+  Lemma fmap_distinct {ValT : Type} s k1 k2 (v2 : ValT) :
+    k1 <> k2 ->
+    find k1 s = find k1 (add k2 v2 s).
+  Proof.
+    intros Hk.
+    assert (Hk' : ~E.eq k2 k1). {
+      intros Habsurd.
+      apply not_eq_sym in Hk.
+      now apply dec_eq_is_eq in Habsurd.
+    }
+    apply Raw.Proofs.find_find.
+    intros v. split.
+    - intros H.
+      apply find_1.
+      apply find_2 in H.
+      now apply add_2.
+    - intros H.
+      apply find_1.
+      apply find_2 in H.
+      eapply add_3; eauto.
+  Qed.
+
+  Lemma fmap_delete_keep {ValT : Type} s k:
+      @find ValT k (remove k s) = None.
+  Proof.
+    specialize (@remove_1 ValT s k k (E.eq_refl k)) as H.
+    remember (remove (elt:=ValT) k s) as s'.
+    unfold find, remove, In in H.
+    destruct s' as [s' bst'].
+    apply Raw.Proofs.not_find_iff.
+    - assumption.
+    - now rewrite Raw.Proofs.In_alt in H.
+  Qed.
+
+  Lemma fmap_delete_distinct {ValT : Type} (s : t ValT) k1 k2 :
+    k1 <> k2 ->
+    find k1 s = find k1 (remove k2 s).
+  Proof.
+    intros Hk.
+    assert (Hk' : ~E.eq k2 k1). {
+      intros Habsurd.
+      apply not_eq_sym in Hk.
+      now apply dec_eq_is_eq in Habsurd.
+    }
+    apply Raw.Proofs.find_find.
+    intros v1. split.
+    - intros H.
+      apply find_1.
+      apply find_2 in H.
+      now apply remove_2.
+    - intros H.
+      apply find_1.
+      apply find_2 in H.
+      eapply remove_3; eauto.
+  Qed.
+
+  Global Instance fmapStorage {Val : Type} : @Storage E.t Val (t Val) :=
+    {|
+      new := @empty Val;
+      get := @find Val;
+      put := @add Val;
+      delete := @remove Val;
+      new_empty := @fmap_new_empty Val;
+      keep := @fmap_keep Val;
+      distinct := @fmap_distinct Val;
+      delete_keep := @fmap_delete_keep Val;
+      delete_distinct := @fmap_delete_distinct Val;
+    |}.
+End Make.