nmap.v 3.85 KB
Newer Older
1
(* Copyright (c) 2012-2017, Robbert Krebbers. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
2
3
4
(* This file is distributed under the terms of the BSD license. *)
(** This files extends the implementation of finite over [positive] to finite
maps whose keys range over Coq's data type of binary naturals [N]. *)
5
6
From iris.prelude Require Import pmap mapset.
From iris.prelude Require Export prelude fin_maps.
7
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
8
9
10
11
12
13
14
15

Local Open Scope N_scope.

Record Nmap (A : Type) : Type := NMap { Nmap_0 : option A; Nmap_pos : Pmap A }.
Arguments Nmap_0 {_} _.
Arguments Nmap_pos {_} _.
Arguments NMap {_} _ _.

16
Instance Nmap_eq_dec `{EqDecision A} : EqDecision (Nmap A).
Robbert Krebbers's avatar
Robbert Krebbers committed
17
Proof.
18
 refine (λ t1 t2,
Robbert Krebbers's avatar
Robbert Krebbers committed
19
20
  match t1, t2 with
  | NMap x t1, NMap y t2 => cast_if_and (decide (x = y)) (decide (t1 = t2))
21
  end); abstract congruence.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
Defined.
Instance Nempty {A} : Empty (Nmap A) := NMap None .
Global Opaque Nempty.
Instance Nlookup {A} : Lookup N A (Nmap A) := λ i t,
  match i with
  | N0 => Nmap_0 t
  | Npos p => Nmap_pos t !! p
  end.
Instance Npartial_alter {A} : PartialAlter N A (Nmap A) := λ f i t,
  match i, t with
  | N0, NMap o t => NMap (f o) t
  | Npos p, NMap o t => NMap o (partial_alter f p t)
  end.
Instance Nto_list {A} : FinMapToList N A (Nmap A) := λ t,
  match t with
  | NMap o t =>
     default [] o (λ x, [(0,x)]) ++ (prod_map Npos id <$> map_to_list t)
  end.
Instance Nomap: OMap Nmap := λ A B f t,
  match t with NMap o t => NMap (o = f) (omap f t) end.
Instance Nmerge: Merge Nmap := λ A B C f t1 t2,
  match t1, t2 with
  | NMap o1 t1, NMap o2 t2 => NMap (f o1 o2) (merge f t1 t2)
  end.
Instance Nfmap: FMap Nmap := λ A B f t,
  match t with NMap o t => NMap (f <$> o) (f <$> t) end.

Instance: FinMap N Nmap.
Proof.
  split.
52
  - intros ? [??] [??] H. f_equal; [apply (H 0)|].
Robbert Krebbers's avatar
Robbert Krebbers committed
53
    apply map_eq. intros i. apply (H (Npos i)).
54
55
56
  - by intros ? [|?].
  - intros ? f [? t] [|i]; simpl; [done |]. apply lookup_partial_alter.
  - intros ? f [? t] [|i] [|j]; simpl; try intuition congruence.
Robbert Krebbers's avatar
Robbert Krebbers committed
57
    intros. apply lookup_partial_alter_ne. congruence.
58
59
  - intros ??? [??] []; simpl. done. apply lookup_fmap.
  - intros ? [[x|] t]; unfold map_to_list; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
    + constructor.
61
62
      * rewrite elem_of_list_fmap. by intros [[??] [??]].
      * by apply (NoDup_fmap _), NoDup_map_to_list.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
    + apply (NoDup_fmap _), NoDup_map_to_list.
64
  - intros ? t i x. unfold map_to_list. split.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
    + destruct t as [[y|] t]; simpl.
66
      * rewrite elem_of_cons, elem_of_list_fmap.
67
        intros [? | [[??] [??]]]; simplify_eq/=; [done |].
Robbert Krebbers's avatar
Robbert Krebbers committed
68
        by apply elem_of_map_to_list.
69
      * rewrite elem_of_list_fmap; intros [[??] [??]]; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
70
71
        by apply elem_of_map_to_list.
    + destruct t as [[y|] t]; simpl.
72
      * rewrite elem_of_cons, elem_of_list_fmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
74
        destruct i as [|i]; simpl; [intuition congruence |].
        intros. right. exists (i, x). by rewrite elem_of_map_to_list.
75
      * rewrite elem_of_list_fmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
77
        destruct i as [|i]; simpl; [done |].
        intros. exists (i, x). by rewrite elem_of_map_to_list.
78
79
  - intros ?? f [??] [|?]; simpl; [done|]; apply (lookup_omap f).
  - intros ??? f ? [??] [??] [|?]; simpl; [done|]; apply (lookup_merge f).
Robbert Krebbers's avatar
Robbert Krebbers committed
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
Qed.

(** * Finite sets *)
(** We construct sets of [N]s satisfying extensional equality. *)
Notation Nset := (mapset Nmap).
Instance Nmap_dom {A} : Dom (Nmap A) Nset := mapset_dom.
Instance: FinMapDom N Nmap Nset := mapset_dom_spec.

(** * Fresh numbers *)
Definition Nfresh {A} (m : Nmap A) : N :=
  match m with NMap None _ => 0 | NMap _ m => Npos (Pfresh m) end.
Lemma Nfresh_fresh {A} (m : Nmap A) : m !! Nfresh m = None.
Proof. destruct m as [[]]. apply Pfresh_fresh. done. Qed. 

Instance Nset_fresh : Fresh N Nset := λ X,
  let (m) := X in Nfresh m.
Instance Nset_fresh_spec : FreshSpec N Nset.
Proof.
  split.
99
100
101
  - apply _.
  - intros X Y; rewrite <-elem_of_equiv_L. by intros ->.
  - unfold elem_of, mapset_elem_of, fresh; intros [m]; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
103
    by rewrite Nfresh_fresh.
Qed.