Containers.v 2.44 KB
Newer Older
1
From Coq Require Import List.
2
From Coq Require Import ZArith.
3
From stdpp Require gmap.
4
From SmartContracts Require Import Monads.
5
From SmartContracts Require Import BoundedN.
6
7
Import ListNotations.

8
Notation FMap := gmap.gmap.
9

10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
Module FMap.
  Generalizable All Variables.
  Notation empty := stdpp.base.empty.
  Notation add := stdpp.base.insert.
  Notation find := stdpp.base.lookup.
  Definition mem `{base.Lookup K V M} (i : K) (m : M) :=
    match base.lookup i m with
    | Some _ => true
    | None => false
    end.

  Notation remove := stdpp.base.delete.
  Notation elements := fin_maps.map_to_list.
  Notation size := stdpp.base.size.
  Notation of_list := fin_maps.list_to_map.
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
  Notation union := stdpp.base.union.
  Notation alter := stdpp.base.alter.
  Notation partial_alter := stdpp.base.partial_alter.

  Section Theories.
    Context {K V : Type} `{countable.Countable K}.

    Proposition of_elements_eq (m : FMap K V) :
      of_list (elements m) = m.
    Proof. apply fin_maps.list_to_map_to_list. Qed.

    Lemma find_union_None (m1 m2 : FMap K V) (k : K) :
      find k m1 = None ->
      find k m2 = None ->
      find k (union m1 m2) = None.
    Proof.
      intros find1 find2.
      apply fin_maps.lookup_union_None; auto.
    Qed.
44

45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
    Lemma find_union_Some_l (m1 m2 : FMap K V) (k : K) (v : V) :
      find k m1 = Some v ->
      find k (union m1 m2) = Some v.
    Proof. apply fin_maps.lookup_union_Some_l. Qed.

    Lemma find_add (m : FMap K V) (k : K) (v : V) :
      find k (add k v m) = Some v.
    Proof. apply fin_maps.lookup_insert. Qed.

    Lemma find_add_ne (m : FMap K V) (k k' : K) (v : V) :
      k <> k' -> find k' (add k v m) = find k' m.
    Proof. apply fin_maps.lookup_insert_ne. Qed.

    Lemma find_partial_alter (m : FMap K V) f k :
      find k (partial_alter f k m) = f (find k m).
    Proof. apply fin_maps.lookup_partial_alter. Qed.

    Lemma find_partial_alter_ne (m : FMap K V) f k k' :
      k <> k' ->
      find k' (partial_alter f k m) = find k' m.
    Proof. apply fin_maps.lookup_partial_alter_ne. Qed.
  End Theories.
67
End FMap.
68

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
69
70
71
72
73
Hint Resolve
     FMap.find_union_None
     FMap.find_union_Some_l
     FMap.find_add
     FMap.find_add_ne : core.
74

75
76
77
78
79
Instance empty_set_eq_dec : stdpp.base.EqDecision Empty_set.
Proof. decidable.solve_decision. Defined.
Program Instance empty_set_countable : countable.Countable Empty_set :=
  {| countable.encode e := 1%positive; countable.decode d := None; |}.
Solve Obligations with contradiction.