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.