zmap.v 4.07 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* 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 [Z]. *)
5 6
From iris.prelude Require Import pmap mapset.
From iris.prelude Require Export prelude fin_maps.
Robbert Krebbers's avatar
Robbert Krebbers committed
7 8 9 10 11 12 13 14 15
Local Open Scope Z_scope.

Record Zmap (A : Type) : Type :=
  ZMap { Zmap_0 : option A; Zmap_pos : Pmap A; Zmap_neg : Pmap A }.
Arguments Zmap_0 {_} _.
Arguments Zmap_pos {_} _.
Arguments Zmap_neg {_} _.
Arguments ZMap {_} _ _ _.

16
Instance Zmap_eq_dec `{EqDecision A} : EqDecision (Zmap A).
Robbert Krebbers's avatar
Robbert Krebbers committed
17
Proof.
18
 refine (λ t1 t2,
Robbert Krebbers's avatar
Robbert Krebbers committed
19 20 21
  match t1, t2 with
  | ZMap x t1 t1', ZMap y t2 t2' =>
     cast_if_and3 (decide (x = y)) (decide (t1 = t2)) (decide (t1' = t2'))
22
  end); abstract congruence.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 52 53
Defined.
Instance Zempty {A} : Empty (Zmap A) := ZMap None  .
Instance Zlookup {A} : Lookup Z A (Zmap A) := λ i t,
  match i with
  | Z0 => Zmap_0 t | Zpos p => Zmap_pos t !! p | Zneg p => Zmap_neg t !! p
  end.
Instance Zpartial_alter {A} : PartialAlter Z A (Zmap A) := λ f i t,
  match i, t with
  | Z0, ZMap o t t' => ZMap (f o) t t'
  | Zpos p, ZMap o t t' => ZMap o (partial_alter f p t) t'
  | Zneg p, ZMap o t t' => ZMap o t (partial_alter f p t')
  end.
Instance Zto_list {A} : FinMapToList Z A (Zmap A) := λ t,
  match t with
  | ZMap o t t' => default [] o (λ x, [(0,x)]) ++
     (prod_map Zpos id <$> map_to_list t) ++
     (prod_map Zneg id <$> map_to_list t')
  end.
Instance Zomap: OMap Zmap := λ A B f t,
  match t with ZMap o t t' => ZMap (o = f) (omap f t) (omap f t') end.
Instance Zmerge: Merge Zmap := λ A B C f t1 t2,
  match t1, t2 with
  | ZMap o1 t1 t1', ZMap o2 t2 t2' =>
     ZMap (f o1 o2) (merge f t1 t2) (merge f t1' t2')
  end.
Instance Nfmap: FMap Zmap := λ A B f t,
  match t with ZMap o t t' => ZMap (f <$> o) (f <$> t) (f <$> t') end.

Instance: FinMap Z Zmap.
Proof.
  split.
54
  - intros ? [??] [??] H. f_equal.
Robbert Krebbers's avatar
Robbert Krebbers committed
55 56 57
    + apply (H 0).
    + apply map_eq. intros i. apply (H (Zpos i)).
    + apply map_eq. intros i. apply (H (Zneg i)).
58 59 60
  - by intros ? [].
  - intros ? f [] [|?|?]; simpl; [done| |]; apply lookup_partial_alter.
  - intros ? f [] [|?|?] [|?|?]; simpl; intuition congruence ||
Robbert Krebbers's avatar
Robbert Krebbers committed
61
      intros; apply lookup_partial_alter_ne; congruence.
62 63
  - intros ??? [??] []; simpl; [done| |]; apply lookup_fmap.
  - intros ? [o t t']; unfold map_to_list; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
64 65
    assert (NoDup ((prod_map Z.pos id <$> map_to_list t) ++
      prod_map Z.neg id <$> map_to_list t')).
66
    { apply NoDup_app; split_and?.
Robbert Krebbers's avatar
Robbert Krebbers committed
67 68 69 70 71
      - apply (NoDup_fmap_2 _), NoDup_map_to_list.
      - intro. rewrite !elem_of_list_fmap. naive_solver.
      - apply (NoDup_fmap_2 _), NoDup_map_to_list. }
    destruct o; simpl; auto. constructor; auto.
    rewrite elem_of_app, !elem_of_list_fmap. naive_solver.
72
  - intros ? t i x. unfold map_to_list. split.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
    + destruct t as [[y|] t t']; simpl.
74
      * rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap.
75
        intros [?|[[[??][??]]|[[??][??]]]]; simplify_eq/=; [done| |];
Robbert Krebbers's avatar
Robbert Krebbers committed
76
          by apply elem_of_map_to_list.
77
      * rewrite elem_of_app, !elem_of_list_fmap. intros [[[??][??]]|[[??][??]]];
78
          simplify_eq/=; by apply elem_of_map_to_list.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
    + destruct t as [[y|] t t']; simpl.
80
      * rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
81 82 83
        destruct i as [|i|i]; simpl; [intuition congruence| |].
        { right; left. exists (i, x). by rewrite elem_of_map_to_list. }
        right; right. exists (i, x). by rewrite elem_of_map_to_list.
84
      * rewrite elem_of_app, !elem_of_list_fmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
85 86 87
        destruct i as [|i|i]; simpl; [done| |].
        { left; exists (i, x). by rewrite elem_of_map_to_list. }
        right; exists (i, x). by rewrite elem_of_map_to_list.
88 89
  - intros ?? f [??] [|?|?]; simpl; [done| |]; apply (lookup_omap f).
  - intros ??? f ? [??] [??] [|?|?]; simpl; [done| |]; apply (lookup_merge f).
Robbert Krebbers's avatar
Robbert Krebbers committed
90 91 92 93 94 95 96
Qed.

(** * Finite sets *)
(** We construct sets of [Z]s satisfying extensional equality. *)
Notation Zset := (mapset Zmap).
Instance Zmap_dom {A} : Dom (Zmap A) Zset := mapset_dom.
Instance: FinMapDom Z Zmap Zset := mapset_dom_spec.