Library finmap

Require Import ZArith List Classical EqNat Permutation.
Require Import ssreflect ssrbool ssrnat ssrfun eqtype seq.

Require Import Arith_ext Lists_ext seq_ext.
Require Import order ordset ordset_pairs.

This file provides

a module type (MAP) for finite maps (equality is the Coq equality)
a functor (map) to instantiate finite maps between any ordered type and any eqtype
a functor (Map_prop) with some additional, derived properties
a functor (MapTac) with some tactics

Module Type MAP.

Parameter l : eqType.
Parameter ltl : l -> l -> bool.
Parameter v : eqType.

Parameter t : Type.
Parameter elts : t -> seq (l * v).
Parameter dom : t -> seq l.
Parameter dom_ord : forall h, OrderedSequence.ordered_fix _ ltl (dom h).
Parameter cdom : t -> seq v.
Parameter size_cdom_dom : forall h, size (cdom h) = size (dom h).
Parameter elts_dom : forall d, map (fun x => fst x) (elts d) = dom d.
Parameter elts_cdom : forall d, map (fun x => snd x) (elts d) = cdom d.
Parameter dom_cdom_heap : forall h1 h2, dom h1 = dom h2 -> cdom h1 = cdom h2 -> h1 = h2.

empty map

Parameter emp : t.
Parameter dom_emp : dom emp = [::].
Parameter dom_emp_inv : forall k, dom k = [::] -> k = emp.
Parameter cdom_emp : cdom emp = [::].
Parameter elts_emp : elts emp = [::].

singleton map

Parameter sing : l -> v -> t.
Parameter elts_sing : forall n w, elts (sing n w) = [:: (n, w)].
Parameter dom_sing : forall n z, dom (sing n z) = [:: n].
Parameter cdom_sing : forall n z, cdom (sing n z) = [:: z].

Parameter sing_inj : forall n v1 v2, sing n v1 = sing n v2 -> v1 = v2.

retrieve an element

Parameter get : l -> t -> option v.
Parameter get_Some_in : forall k n w, get n k = Some w -> (n, w) \in elts k.
Parameter get_None_notin : forall k n, get n k = None -> n \notin dom k.
Parameter get_Some_in_dom : forall k n z, get n k = Some z -> n \in dom k.
Parameter in_dom_get_Some : forall k n, n \in dom k -> exists z, get n k = Some z.
Parameter get_Some_in_cdom: forall k n z, get n k = Some z -> z \in cdom k.
Parameter get_emp : forall x, get x emp = None.
Parameter get_sing : forall n w, get n (sing n w) = Some w.
Parameter get_sing_inv : forall n w n' w', get n (sing n' w') = Some w -> n = n' /\ w = w'.

Parameter extensionality : forall h1 h2, (forall x, get x h1 = get x h2) -> h1 = h2.
Parameter permut_eq : forall h1 h2, Permutation (s2l (elts h1)) (s2l (elts h2)) -> h1 = h2.

update an entry

Parameter upd : l -> v -> t -> t.
Parameter upd_sing : forall n w w', upd n w' (sing n w) = sing n w'.
Parameter get_upd : forall x y z st, x <> y -> get x (upd y z st) = get x st.
Parameter upd_emp : forall l v, upd l v emp = emp.
Parameter upd_invariant : forall k p w, p \notin dom k -> upd p w k = k.
Parameter dom_upd_invariant : forall k n w, dom (upd n w k) = dom k.

disjointness

Parameter disj : t -> t -> Prop.
Notation "k '#' m" := (disj k m) (at level 79) : map_scope.
Local Open Scope map_scope.

Parameter disjE : forall h1 h2, (h1 # h2) = dis (dom h1) (dom h2).
Parameter disj_sym : forall h0 h1, h0 # h1 -> h1 # h0.
Parameter disj_emp_R : forall h, h # emp.
Parameter disj_emp_L : forall h, emp # h.
Parameter disj_sing : forall x y z z', x <> y -> (sing x z) # (sing y z').
Parameter disj_sing' : forall x y z z', (sing x z) # (sing y z') -> x <> y.
Parameter disj_sing_R : forall h n z, n \notin dom h -> h # sing n z.
Parameter disj_upd : forall n z h1 h2, h1 # h2 -> (upd n z h1) # h2.
Parameter disj_same_dom : forall k1 k2 k2', k1 # k2' -> dom k2 = dom k2' -> k1 # k2.

union

Parameter union : t -> t -> t.
Notation "k '+++' m" := (union k m) (at level 69) : map_scope.

Parameter union_emp_R : forall h1, h1 +++ emp = h1.
Parameter union_emp_L : forall h1, emp +++ h1 = h1.
Parameter union_com : forall h1 h2, h1 # h2 -> h1 +++ h2 = h2 +++ h1.
Parameter in_dom_union_L : forall x h1 h2, x \in dom h1 -> x \in dom (h1 +++ h2).
Parameter in_cdom_union_inv : forall t a b, t \in cdom (a +++ b) -> t \in cdom a \/ t \in cdom b.
Parameter in_dom_union_inv : forall t a b, t \in dom (a +++ b) -> t \in dom a \/ t \in dom b.
Parameter union_assoc : forall h1 h2 h3, h1 +++ (h2 +++ h3) = (h1 +++ h2) +++ h3.
Parameter get_union_sing_eq : forall x z st, get x (sing x z +++ st) = Some z.
Parameter get_union_sing_neq : forall x y z st, x <> y -> get x (sing y z +++ st) = get x st.
Parameter get_union_Some_inv : forall h1 h2 n z,
  get n (h1 +++ h2) = Some z -> get n h1 = Some z \/ get n h2 = Some z.
Parameter get_union_L : forall h1 h2, h1 # h2 -> forall n z, get n h1 = Some z -> get n (h1 +++ h2) = Some z.
Parameter get_union_R : forall h1 h2, h1 # h2 -> forall n z, get n h2 = Some z -> get n (h1 +++ h2) = Some z.
Parameter get_union_None_inv : forall h1 h2 n, get n (h1 +++ h2) = None -> get n h1 = None /\ get n h2 = None.
Parameter upd_union_L : forall h1 h2, h1 # h2 ->
  forall n z z1, get n h1 = Some z1 -> upd n z (h1 +++ h2) = (upd n z h1) +++ h2.
Parameter upd_union_R : forall h1 h2, h1 # h2 ->
  forall n z z2, get n h2 = Some z2 -> upd n z (h1 +++ h2) = h1 +++ (upd n z h2).
Parameter elts_union_sing : forall h n w,
  (forall m, m \in dom h -> ltl n m) -> elts (sing n w +++ h) = (n, w) :: elts h.
Parameter dom_union_sing : forall h n w,
  (forall m, m \in dom h -> ltl n m) -> dom (sing n w +++ h) = n :: dom h.
Parameter cdom_union_sing : forall k (a : l) b,
  (forall m, m \in dom k -> ltl a m) -> cdom (sing a b +++ k) = b :: cdom k.
Parameter cdom_union : forall h1 h2,
  (forall i j, i \in dom h1 -> j \in dom h2 -> ltl i j) ->
  cdom (h1 +++ h2) = cdom h1 ++ cdom h2.
Parameter dom_union : forall h1 h2,
  (forall i j, i \in dom h1 -> j \in dom h2 -> ltl i j) ->
  dom (h1 +++ h2) = dom h1 ++ dom h2.

Parameter Permutation_dom_union : forall h1 h2, h1 # h2 ->
  Permutation (s2l (dom (h1 +++ h2))) (s2l (dom h1) ++ s2l (dom h2)).
Parameter union_emp_inv : forall h1 h2, emp = h1 +++ h2 -> h1 = emp /\ h2 = emp.
Parameter union_inv : forall h0 h0' h1 h2, h0 +++ h1 = h0' +++ h2 -> dom h0 = dom h0' -> h1 # h0 -> h2 # h0' -> h0 = h0' /\ h1 = h2.

Parameter disj_union_R : forall h1 h2 h0, h0 # h1 -> h0 # h2 -> h0 # (h1 +++ h2).
Parameter disj_union_L : forall h1 h2 h0, h1 # h0 -> h2 # h0 -> (h1 +++ h2) # h0.
Parameter disj_union_inv : forall h1 h2 h0, h0 # (h1 +++ h2) -> h0 # h1 /\ h0 # h2.
Parameter dis_dom_union : forall h1 h2 l,
  dis l (dom (h1 +++ h2)) = dis l (dom h1) && dis l (dom h2).
Parameter elts_union_sing_Perm : forall l d x rx,
  Permutation l (s2l (elts d)) ->
  ~ In x (Lists_ext.uzip1 l) ->
  Permutation ((x, rx) :: l)%list (s2l (elts (union (sing x rx) d))).

delete several entries

Parameter difs : t -> seq l -> t.
Notation "k '[\m]' m" := (difs k m) (at level 69) : map_scope.

Parameter union_difs_L : forall h1 h2 k, dis (dom h2) k -> (h1 +++ h2) [\m ] k = (h1 [\m ] k) +++ h2.
Parameter difs_self : forall k, k [\m ] dom k = emp.

Parameter difs_upd : forall k n w d, n \in d -> (upd n w k) [\m ] d = k [\m ] d.
Parameter disj_difs : forall h1 h2, h1 # h2 -> forall d, h1 # h2 [\m ] d.
Parameter disj_difs' : forall h1 h2 d, inc (dom h1) d -> h1 # h2 [\m ] d.
Parameter get_difs : forall k x d, x \notin d -> get x (k [\m ] d) = get x k.
Parameter get_difs_None : forall k x d, x \in d -> get x (k [\m ] d) = None.
Parameter dom_difs_del : forall k d, dom (k [\m ] d) = del (fun x => x \in d) (dom k).

projection

Parameter proj : t -> seq l -> t.

Parameter proj_emp : forall l, proj emp l = emp.
Parameter proj_nil : forall k, proj k [::] = emp.
Parameter dom_proj_sing : forall k n, n \in dom k -> dom (proj k [:: n]) = [:: n].
Parameter inc_dom_proj : forall d k, inc (dom (proj k d)) d.
Parameter inc_dom_proj_dom : forall h d, inc (dom (proj h d)) (dom h).
Parameter dom_proj_exact : forall h d, OrderedSequence.ordered ltl d -> inc d (dom h) -> dom (proj h d) = d.
Parameter size_dom_proj_exact : forall h d, uniq d -> inc d (dom h) -> size (dom (proj h d)) = size d.
Parameter dom_proj_cons : forall k n d, n \notin dom k -> proj k (n :: d) = proj k d.
Parameter in_dom_proj : forall x d h, x \in d -> x \in dom h -> x \in dom (proj h d).
Parameter in_dom_proj_inter : forall k d m, m \in dom (proj k d) -> m \in dom k /\ m \in d.
Parameter proj_upd : forall d k p w, proj (upd p w k) d = upd p w (proj k d).
Parameter get_proj : forall d k n, n \in d -> get n (proj k d) = get n k.
Parameter get_proj_None : forall d k n, n \notin d -> get n (proj k d) = None.
Parameter disj_proj_emp : forall h1 h2, h1 # h2 -> proj h1 (dom h2) = emp.
Parameter disj_proj_same_dom : forall k1 k2 d1 d2, dom k1 = dom k2 -> proj k1 d1 # proj k1 d2 -> proj k2 d1 # proj k2 d2.
Parameter dis_disj_proj : forall k1 k2 d1 d2, dis d1 d2 -> proj k1 d1 # proj k2 d2.
Parameter disj_proj_L : forall h d k, h # k -> proj h d # k.
Parameter dom_dom_proj : forall h1 h2 d, dom h1 = dom h2 -> dom (proj h1 d) = dom (proj h2 d).
Parameter proj_itself : forall k, proj k (dom k) = k.

Parameter proj_union_L : forall h h1 h2, h # h2 -> proj (h1 +++ h2) (dom h) = proj h1 (dom h).
Parameter proj_union_R : forall h h', h # h' -> proj (h +++ h') (dom h') = h'.
Parameter proj_app : forall k d1 d2, proj k (d1 ++ d2) = proj k d1 +++ proj k d2.
Parameter proj_union_sing : forall k x y d, x \in d -> proj (sing x y +++ k) d = sing x y +++ proj k d.
Parameter proj_union_sing_notin : forall k x y d, x \notin d -> proj ((sing x y) +++ k) d = proj k d.
Parameter proj_dom_union : forall h h1 h2, h1 # h2 ->
  proj h (dom (h1 +++ h2)) = proj h (dom h1) +++ proj h (dom h2).
Parameter proj_difs : forall k d, k = proj k d +++ (k [\m ] d).
Parameter proj_difs_disj : forall k d d', inc d d' -> proj k d # k [\m ] d'.
Parameter proj_disj : forall k1 k2 k d, dom k1 = dom k2 -> proj k1 k # d -> proj k2 k # d.
Parameter cdom_proj : forall h l1 l2, dom h = l1 ++ l2 ->
  cdom (proj h l2) = drop (size l1) (cdom h).
Parameter cdom_difs : forall h l1 l2, dom h = l1 ++ l2 -> cdom (h [\m ] l2) = take (size l1) (cdom h).
Parameter app_proj_difs : forall h l1 l2, dom h = l1 ++ l2 ->
  proj h l1 = h [\m ] l2.
Parameter cdom_proj2 : forall h l1 l2, dom h = l1 ++ l2 ->
  cdom (proj h l1) = take (size l1) (cdom h).

inclusion

Parameter inclu : t -> t -> Prop.
Notation "k '[<=m]' m" := (inclu k m) (at level 69) : map_scope.
Parameter incluE : forall h k, k [<=m ] h <-> proj h (dom k) = k.
Parameter get_inclu : forall h1 h2,
  (forall n w, get n h1 = Some w -> get n h2 = Some w) -> h1 [<=m ] h2.
Parameter inclu_get : forall h1 h2, h1 [<=m ] h2 ->
  (forall n w, get n h1 = Some w -> get n h2 = Some w).
Parameter inclu_inc_dom : forall h1 h2, h1 [<=m ] h2 -> inc (dom h1) (dom h2).

Parameter inclu_union_L : forall h1 h2 k, h1 # h2 -> k [<=m ] h1 -> k [<=m ] (h1 +++ h2).
Parameter inclu_refl : forall k, k [<=m ] k.
Parameter proj_inclu : forall k h1 d, k [<=m ] (proj h1 d) -> k [<=m ] h1.
Parameter get_inclu_sing : forall h a b, get a h = Some b -> sing a b [<=m ] h.
Parameter proj_restrict : forall h1 h2 d, h1 [<=m ] h2 -> inc d (dom h1) -> proj h2 d = proj h1 d.
Parameter union_difs : forall h k d, k [<=m ] h -> dom k = d -> h = k +++ (h [\m ] d).
Parameter dom_union_difs : forall h k, inc (dom k) (dom h) -> dom h = dom (k +++ (h [\m ] dom k)).
Parameter inclu_proj : forall h d, proj h d [<=m ] h.
Parameter proj_dom_proj : forall k d, proj k (dom (proj k d)) = proj k d.
Parameter inclu_difs : forall h d, (h [\m ] d) [<=m ] h.

Parameter disj_proj_inclu : forall h d1 k, proj h d1 # k ->
  proj h d1 [<=m ] (h [\m ] (dom k)).
Parameter incl_proj2 : forall h1 h2 k, h1 [<=m ] k -> h2 [<=m ] k ->
  dom h1 = dom h2 -> h1 = h2.
Parameter disj_proj_app : forall h k d1 d2, h # (k [\m ] d1) ->
  h # (k [\m ] d2) -> h # (k [\m ] (d1 ++ d2)).

delete only one entry

Parameter dif : t -> l -> t.
Notation "k '---' l" := (dif k l) (at level 69) : map_scope.
Parameter dif_def : forall h n, h --- n = h [\m ] [:: n].

Parameter dif_sing: forall a b, (sing a b) --- a = emp.
Parameter dif_emp : forall p, emp --- p = emp.
Parameter dif_union: forall h1 h2 a, (h1 +++ h2) --- a = (h1 --- a) +++ (h2 --- a).
Parameter dif_disj: forall h a b, h # (sing a b) -> (h --- a) = h.
Parameter dif_disj': forall h1 h2 l, h1 # h2 -> (h1 --- l) # (h2 --- l).
Parameter get_dif : forall w st, get w (st --- w) = None.
Parameter get_dif' : forall st x y, x <> y -> get x (st --- y) = get x st.
Parameter proj_dif : forall k x d, x \in d -> proj (k --- x) d = (proj k d) --- x.

Require nodup.

Ltac Permutation_list_elts :=
  repeat
    match goal with
      | |- Permutation (List.cons (?x, ?rx) _) (seq_ext.s2l (elts (union (sing ?r ?rx) _))) =>
        apply elts_union_sing_Perm; last by unfold Lists_ext.uzip1; simpl List.map; nodup.Nodup_not_In
      | |- Permutation (List.cons (?x, ?rx) _) (seq_ext.s2l (elts (sing ?r ?rx))) =>
        rewrite -> elts_sing; simpl; by apply Permutation_refl
    end.

Ltac map_to_lst l :=
  match l with
    | union (sing ?r ?rx) ?tl =>
      let tl' := map_to_lst tl in
      constr:(List.cons (r, rx) tl')
    | sing ?r ?rx => constr:(List.cons (r, rx) List.nil)
  end.

Ltac From_cdom_to_list H :=
  match goal with
    |- context ctxt_id [seq_ext.s2l (cdom ?fima)] =>
      let fima_list := map_to_lst fima in
      let cdom_list := constr: (List.map (fun x => snd x) fima_list) in
      assert (H : Permutation cdom_list (seq_ext.s2l (cdom fima))) ; [
        apply Permutation_trans with (seq_ext.s2l (seq.map (fun x : l * v => snd x) (elts fima))) ; [
          rewrite <- seq_ext.map_s2l;
          apply Permutation_map ;
          by Permutation_list_elts
        |
          by rewrite -> elts_cdom; apply Permutation_refl ]
      |
        idtac ]
  end.

Ltac From_dom_to_list H :=
  match goal with
    |- context ctxt_id [seq_ext.s2l (dom ?fima)] =>
      let fima_list := map_to_lst fima in
      let dom_list := constr: (List.map (fun x => fst x) fima_list) in
      assert (H : Permutation dom_list (seq_ext.s2l (dom fima))) ; [
        apply Permutation_trans with (seq_ext.s2l (seq.map (fun x : l * v => fst x) (elts fima))) ; [
          rewrite <- seq_ext.map_s2l;
          apply Permutation_map ;
          by Permutation_list_elts
        |
          by rewrite -> elts_dom; apply Permutation_refl ]
      |
        idtac ]
  end.

Ltac Permutation_elts_elts :=
  match goal with
    |- Permutation (seq_ext.s2l (elts ?fima))
      (seq_ext.s2l (elts ?fima2)) =>
      let fima_list := map_to_lst fima in
      let fima_list2 := map_to_lst fima2 in
        apply Permutation_trans with fima_list ;
          [ apply Permutation_sym ;
            Permutation_list_elts
            |
            apply Permutation_trans with fima_list2 ;
              [ PermutProve
                |
                Permutation_list_elts
              ]
          ]
  end.

Ltac Equal_union :=
  match goal with
    | |- union _ _ = union _ _ =>
      apply permut_eq ;
      Permutation_elts_elts
  end.

End MAP.

Module Type EQTYPE.
  Variable A : eqType.
End EQTYPE.

Module map (X : ORDER) (E : EQTYPE) : MAP
  with Definition l := X.A
    with Definition v := E.A
      with Definition ltl := X.ltA.

Definition l := X.A.
Definition ltl := X.ltA.
Definition v := E.A.

Import OrderedSequence.

definition of maps

Inductive t' : Type := mk_t : forall k : seq (l * v), ordered X.ltA (unzip1 k) -> t'.
Definition t := t'.

Definition elts (k : t) := let (lst, _) := k in lst.
Definition prf (k : t) := let (l, v) as h return ordered X.ltA (unzip1 (elts h)) := k in v.

Lemma mk_t_pi : forall l1 (H1 : ordered X.ltA (unzip1 l1)) l2 (H2 : ordered X.ltA (unzip1 l2)),
  l1 = l2 -> mk_t l1 H1 = mk_t l2 H2.

Definition dom m := unzip1 (elts m).

Lemma dom_ord : forall h, OrderedSequence.ordered_fix _ ltl (dom h).

Definition cdom m := unzip2 (elts m).

Lemma size_cdom_dom : forall h, size (cdom h) = size (dom h).

Lemma elts_dom : forall d, map (fun x => fst x) (elts d) = dom d.

Lemma elts_cdom : forall d, map (fun x => snd x) (elts d) = cdom d.

Lemma dom_cdom_heap : forall h1 h2, dom h1 = dom h2 -> cdom h1 = cdom h2 -> h1 = h2.

Definition emp := mk_t [::] (ord_nil _ X.ltA).

Lemma dom_emp : dom emp = [::].

Lemma dom_emp_inv : forall k, dom k = [::] -> k = emp.

Lemma cdom_emp : cdom emp = [::].

Lemma elts_emp : elts emp = [::].

Lemma ordered_sing : forall n (v : v), ordered X.ltA (unzip1 [:: (n, v)]).

Definition sing n w := mk_t [:: (n, w)] (ordered_sing n w).

Lemma elts_sing : forall n w, elts (sing n w) = [:: (n, w)].

Lemma dom_sing : forall n z, dom (sing n z) = [:: n].

Lemma cdom_sing : forall n z, cdom (sing n z) = [:: z].

Lemma sing_inj : forall n v1 v2, sing n v1 = sing n v2 -> v1 = v2.

Definition get_seq (n : l) k : option v :=
  if ocamlfind (fun x => n == x.1) k is Some r then Some r.2 else None.

Lemma get_seq_cons : forall k a b, get_seq a ((a, b) :: k) = Some b.

Lemma get_seq_cons' : forall k a b n, a <> n -> get_seq n ((a, b) :: k) = get_seq n k.

Lemma get_seq_Some_in : forall k n w, get_seq n k = Some w -> (n, w) \in k.

Lemma get_seq_Some_in_unzip1 : forall k n z, get_seq n k = Some z -> n \in unzip1 k.

Lemma get_seq_Some_in_unzip2 : forall k n z, get_seq n k = Some z -> z \in unzip2 k.

Lemma in_get_seq_Some : forall k n, n \in unzip1 k -> exists z, get_seq n k = Some z.

Lemma ord_in_get_seq_Some : forall k n w, ordered X.ltA (unzip1 k) -> (n, w) \in k -> get_seq n k = Some w.

Lemma get_seq_None_notin : forall k n, get_seq n k = None -> ~ n \in unzip1 k.

Lemma notin_get_seq_None : forall k n, ~ n \in unzip1 k -> get_seq n k = None.

Definition get n k := get_seq n (elts k).

Lemma get_Some_in : forall k n w, get n k = Some w -> (n, w) \in elts k.

Lemma get_None_notin : forall k n, get n k = None -> n \notin dom k.

Lemma get_Some_in_dom : forall k n z, get n k = Some z -> n \in dom k.

Lemma in_unzip1_get_seq_Some : forall k n, n \in unzip1 k ->
  exists z, get_seq n k = Some z.

Lemma in_dom_get_Some : forall k n, n \in dom k -> exists z, get n k = Some z.

Lemma get_Some_in_cdom : forall k n z, get n k = Some z -> z \in cdom k.

Lemma get_emp : forall x, get x emp = None.

Lemma get_sing : forall n w, get n (sing n w) = Some w.

Lemma get_sing_inv : forall n w n' w', get n (sing n' w') = Some w -> n = n' /\ w = w'.

map equivalence

Definition equal h1 h2 := elts h1 = elts h2.
Notation "k '[=m]' m" := (equal k m) (at level 79) : map_scope.
Open Local Scope map_scope.

Lemma equal_eq : forall h1 h2, h1 [=m ] h2 -> h1 = h2.

Lemma eq_equal: forall h1 h2, h1 = h2 -> h1 [=m ] h2.

Ltac ord_pro := solve [apply X.ltA_trans | apply X.ltA_irr | apply X.ltA_total].

Lemma ext_helper : forall l1 l2,
  ordered X.ltA (unzip1 l1) -> ordered X.ltA (unzip1 l2) ->
  unzip1 l1 = unzip1 l2 ->
  (forall x, get_seq x l1 = get_seq x l2) ->
  l1 = l2.

Lemma extensionality_seq : forall l1 l2,
  ordered X.ltA (unzip1 l1) -> ordered X.ltA (unzip1 l2) ->
  (forall x, get_seq x l1 = get_seq x l2) -> l1 = l2.

Lemma extensionality: forall h1 h2, (forall x, get x h1 = get x h2) -> h1 = h2.

Lemma permut_eq : forall h1 h2,
  Permutation (seq_ext.s2l (elts h1)) (seq_ext.s2l (elts h2)) ->
  h1 = h2.

Fixpoint upd_seq (n : l) (w : v) (k : seq_eqType (prod_eqType l v)) { struct k } :=
  match k with
    | [::] => [::]
    | (h1, h2) :: tl => if n == h1 then (h1, w) :: tl else (h1, h2) :: upd_seq n w tl
  end.

Lemma unzip1_upd_seq : forall k n w, unzip1 (upd_seq n w k) = unzip1 k.

Lemma ocamlfind_upd_seq : forall k n w, n \in unzip1 k ->
  ocamlfind (fun x => n == x.1) (upd_seq n w k) = Some (n, w).

Lemma ocamlfind_upd_seq' : forall k n w n',
  n <> n' -> n \in unzip1 k ->
  ocamlfind (fun x => n' == x.1) (upd_seq n w k) = ocamlfind (fun x => n' == x.1) k.

Lemma in_unzip1_in_upd_seq : forall k n w, n \in unzip1 k -> (n, w) \in upd_seq n w k.

Lemma upd_seq_invariant : forall k n, ~ n \in unzip1 k -> forall z, upd_seq n z k = k.

Lemma in_upd_seq_inv : forall k n w x, x \in upd_seq n w k -> x = (n, w) \/ x \in k.

Lemma upd_seq_upd_seq_eq : forall k n w w', upd_seq n w (upd_seq n w' k) = upd_seq n w k.

Lemma upd_seq_upd_seq_neq : forall k n n', n <> n' -> n \in unzip1 k -> n' \in unzip1 k ->
  forall w w', upd_seq n w (upd_seq n' w' k) = upd_seq n' w' (upd_seq n w k).

Lemma get_seq_upd_seq : forall k x y z, x <> y -> get_seq x k = get_seq x (upd_seq y z k).

Lemma ordered_upd : forall k, ordered X.ltA (unzip1 k) -> forall n w, ordered X.ltA (unzip1 (upd_seq n w k)).

Definition upd n w k := mk_t (upd_seq n w (elts k)) (ordered_upd (elts k) (prf k) n w).

Lemma upd_sing : forall n w w', upd n w' (sing n w) = sing n w'.

Lemma get_upd : forall x y z st, x <> y -> get x (upd y z st) = get x st.

Lemma upd_emp : forall l v, upd l v emp = emp.

Lemma upd_invariant : forall k p w, p \notin dom k -> upd p w k = k.

Lemma unzip1_upd_seq_invariant : forall k n w, unzip1 (upd_seq n w k) = unzip1 k.

Lemma dom_upd_invariant : forall k n w, dom (upd n w k) = dom k.

Definition disj h1 h2 : Prop := dis (unzip1 (elts h1)) (unzip1 (elts h2)).
Notation "k '#' m" := (disj k m) (at level 79) : map_scope.

Lemma disjE : forall h1 h2, (h1 # h2) = dis (dom h1) (dom h2).

Lemma disj_sym : forall h1 h2, h1 # h2 -> h2 # h1.

Lemma disj_emp_R : forall h, h # emp.

Lemma disj_emp_L : forall h, emp # h.

Lemma disj_sing : forall x y z z', x <> y -> sing x z # sing y z'.

Lemma disj_sing' : forall x y z z', sing x z # sing y z' -> x <> y.

Lemma disj_sing_R : forall h n z, n \notin dom h -> h # sing n z.

Lemma disj_upd : forall n z h1 h2, h1 # h2 -> (upd n z h1) # h2.

Lemma disj_same_dom : forall k1 k2 k2', k1 # k2' -> dom k2 = dom k2' -> k1 # k2.

element addition

Import FinSetOfPairsForMap.

Definition add_seq n w k := if n \in unzip1 k then upd_seq n w k else add_map X.ltA n w k.

Lemma lb_add_seq : forall lst n m w, lb X.ltA n (unzip1 lst) -> X.ltA n m ->
  lb X.ltA n (unzip1 (add_seq m w lst)).

Lemma add_seq_lb: forall k a b, lb X.ltA a (unzip1 k) -> add_seq a b k = (a, b) :: k.

Lemma add_seq_ub : forall k a b, ub X.ltA a (unzip1 k) -> add_seq a b k = k ++ (a, b) :: nil.

Lemma ordered_add_seq : forall lst, ordered X.ltA (unzip1 lst) ->
  forall n w, ordered X.ltA (unzip1 (add_seq n w lst)).

Lemma in_add_seq : forall k a b, (a, b) \in add_seq a b k.

Lemma in_map_add_seq : forall {A:eqType} (f:l *v -> A) k a b, f (a, b) \in map f (add_seq a b k).

Lemma in_unzip1_add_seq_remains : forall k x a b, x \in unzip1 k -> x \in unzip1 (add_seq a b k).

Lemma in_add_seq_remains : forall k x a b, x \in k -> ~ a \in unzip1 k -> x \in add_seq a b k.

Lemma in_add_seq_inv : forall k x a b, x \in add_seq a b k -> x = (a, b) \/ x \in k.

Lemma in_map_add_seq_inv : forall {A:eqType} f k (x:A) a b, x \in map f (add_seq a b k) -> x = f (a, b) \/ x \in map f k.

Lemma get_seq_add_seq_eq : forall k n w, get_seq n (add_seq n w k) = Some w.

Lemma get_seq_add_seq_neq : forall k n w n' , n <> n' -> get_seq n' (add_seq n w k) = get_seq n' k.

Lemma upd_seq_add_map : forall k n w w', n \in unzip1 k = false ->
  upd_seq n w (add_map X.ltA n w' k) = add_map X.ltA n w k.

Lemma add_map_upd_seq : forall k n' w' n w, n' <> n -> n' \in unzip1 k -> n \in unzip1 k = false ->
  add_map X.ltA n w (upd_seq n' w' k) = upd_seq n' w' (add_map X.ltA n w k).

Lemma add_seq_add_seq_eq : forall k n w' w, add_seq n w (add_seq n w' k) = add_seq n w k.

Lemma add_seq_add_seq_neq : forall k n' w' n w, n' <> n ->
  add_seq n w (add_seq n' w' k) = add_seq n' w' (add_seq n w k).

Lemma upd_seq_is_add_seq : forall k n w, n \in unzip1 k -> upd_seq n w k = add_seq n w k.

Lemma upd_seq_add_seq : forall k n w w', upd_seq n w (add_seq n w' k) = add_seq n w k.

Lemma add_seq_upd_seq : forall k a b, add_seq a b (upd_seq a b k) = add_seq a b k.

Lemma upd_seq_add_seq_neq: forall k n n' w w', n' <> n ->
  upd_seq n w (add_seq n' w' k) = add_seq n' w' (upd_seq n w k).

Fixpoint app_seq (h1 h2:seq_eqType (prod_eqType l v)) {struct h1} : seq_eqType (prod_eqType l v) :=
  match h1 with
    | [::] => h2
    | (h, h') :: tl => add_seq h h' (app_seq tl h2)
  end.

Lemma lb_unzip1_app_seq : forall l1 l2 x,
  lb X.ltA x (unzip1 l1) -> lb X.ltA x (unzip1 l2) ->
  lb X.ltA x (unzip1 (app_seq l1 l2)).

Lemma ordered_app_seq : forall h1 h2,
  ordered X.ltA (unzip1 h1) -> ordered X.ltA (unzip1 h2) ->
  ordered X.ltA (unzip1 (app_seq h1 h2)).

Definition union h1 h2 := mk_t (app_seq (elts h1) (elts h2)) (ordered_app_seq _ _ (prf h1) (prf h2)).
Notation "k '+++' m" := (union k m) (at level 69) : map_scope.

Lemma app_seq_nil : forall k, ordered X.ltA (unzip1 k) -> app_seq k [::] = k.

Lemma union_emp_R : forall h, h +++ emp = h.

Lemma union_emp_L : forall h, emp +++ h = h.

Lemma app_seq_com : forall l1 l2, ordered X.ltA (unzip1 l1) -> ordered X.ltA (unzip1 l2) ->
  dis (unzip1 l1) (unzip1 l2) -> app_seq l1 l2 = app_seq l2 l1.

Lemma union_com : forall h1 h2, h1 # h2 -> h1 +++ h2 = h2 +++ h1.

Lemma in_unzip1_app_seq : forall l1 l2 n, n \in unzip1 l1 \/ n \in unzip1 l2 -> n \in unzip1 (app_seq l1 l2).

Lemma in_unzip1_app_seq_L : forall l1 n, n \in unzip1 l1 -> forall l2, n \in unzip1 (app_seq l1 l2).

Lemma in_unzip1_app_seq_R : forall l2 n, n \in unzip1 l2 -> forall l1, n \in unzip1 (app_seq l1 l2).

Lemma in_dom_union_L : forall x h1 h2, x \in dom h1 -> x \in dom (h1 +++ h2).

Lemma in_map_app_seq_inv : forall {A:eqType} (f:l *v->A) l1 l2 n, n \in map f (app_seq l1 l2) -> n \in map f l1 \/ n \in map f l2.

Lemma in_cdom_union_inv : forall t a b, t \in cdom (a +++ b) -> t \in cdom a \/ t \in cdom b.

Lemma in_dom_union_inv : forall t a b, t \in dom (a +++ b) -> t \in dom a \/ t \in dom b.

Lemma notin_unzip1_app_seq : forall l1 l2 x, ~ x \in unzip1 l1 -> ~ x \in unzip1 l2 -> ~ x \in (unzip1 (app_seq l1 l2)).

Lemma in_app_seq : forall l1 l2 n, ordered X.ltA (unzip1 l1) ->
  dis (unzip1 l1) (unzip1 l2) -> n \in l1 -> n \in app_seq l1 l2.

Lemma in_app_seq_inv : forall l1 l2 n, ordered X.ltA (unzip1 l1) ->
  dis (unzip1 l1) (unzip1 l2) -> n \in (app_seq l1 l2) -> n \in l1 \/ n \in l2.

Lemma upd_seq_app_seq : forall l1 l2 n z, n \in unzip1 l1 ->
  app_seq (upd_seq n z l1) l2 = upd_seq n z (app_seq l1 l2).

Lemma add_seq_app_seq: forall l1 l2 n w,
  add_seq n w (app_seq l1 l2) = app_seq (add_seq n w l1) l2.

Lemma add_seq_app_seq2 : forall l1 l2 n w, n \notin unzip1 l1 ->
  add_seq n w (app_seq l1 l2) = app_seq l1 (add_seq n w l2).

Lemma app_seq_upd_seq_upd_seq : forall l1 l2 a b,
  app_seq (upd_seq a b l1) (upd_seq a b l2) = upd_seq a b (app_seq l1 l2).

Lemma app_seq_add_seq_add_seq : forall l1 l2 a b,
  app_seq (add_seq a b l1) (add_seq a b l2) = add_seq a b (app_seq l1 l2).

Lemma union_assoc : forall h1 h2 h3, h1 +++ (h2 +++ h3) = (h1 +++ h2) +++ h3.

Lemma get_seq_app_seq_L : forall l1 l2 n z,
  get_seq n l1 = Some z -> get_seq n (app_seq l1 l2) = Some z.

Lemma get_seq_app_seq_R : forall l1 l2 n z,
   ordered X.ltA (unzip1 l1) -> ordered X.ltA (unzip1 l2) -> dis (unzip1 l1) (unzip1 l2) ->
   get_seq n l2 = Some z -> get_seq n (app_seq l1 l2) = Some z.

Lemma get_union_sing_eq : forall x z st, get x (sing x z +++ st) = Some z.

Lemma get_union_sing_neq : forall x y z st, x <> y -> get x (sing y z +++ st) = get x st.

Lemma get_union_Some_inv : forall h1 h2 n z,
  get n (h1 +++ h2) = Some z -> get n h1 = Some z \/ get n h2 = Some z.

Lemma get_union_L : forall h1 h2, h1 # h2 -> forall n z, get n h1 = Some z -> get n (h1 +++ h2) = Some z.

Lemma get_union_R : forall h1 h2, h1 # h2 -> forall n z, get n h2 = Some z -> get n (h1 +++ h2) = Some z.

Lemma get_union_None_inv : forall h1 h2 n, get n (h1 +++ h2) = None -> get n h1 = None /\ get n h2 = None.

Lemma upd_union_L : forall h1 h2, h1 # h2 -> forall n z z1, get n h1 = Some z1 ->
  upd n z (h1 +++ h2) = (upd n z h1) +++ h2.

Lemma upd_union_R : forall h1 h2, h1 # h2 -> forall n z z2, get n h2 = Some z2 ->
  upd n z (h1 +++ h2) = h1 +++ (upd n z h2).

Lemma elts_union_sing : forall h n w, (forall m, m \in dom h -> ltl n m) ->
  elts (sing n w +++ h) = (n, w) :: elts h.

Lemma dom_union_sing : forall h n w, (forall m, m \in dom h -> ltl n m) ->
  dom (sing n w +++ h) = n :: dom h.

Lemma cdom_union_sing : forall k (a : l) b, (forall m, m \in dom k -> ltl a m) ->
  cdom (sing a b +++ k) = b :: cdom k.

Lemma cdom_union : forall h1 h2,
  (forall i j, i \in dom h1 -> j \in dom h2 -> ltl i j) ->
  cdom (h1 +++ h2) = cdom h1 ++ cdom h2.

Lemma dom_union : forall h1 h2,
  (forall i j, i \in dom h1 -> j \in dom h2 -> X.ltA i j) ->
  dom (h1 +++ h2) = dom h1 ++ dom h2.

Lemma add_seq_Permutation : forall l a b, a \notin (unzip1 l) ->
  Permutation (s2l (add_seq a b l)) ((a, b) :: s2l l).

Lemma app_seq_Permutation : forall k l, ordered X.ltA (unzip1 k) ->
  dis (unzip1 k) (unzip1 l) -> Permutation (s2l (app_seq k l)) (s2l k ++ s2l l).

Lemma Permutation_dom_union : forall h1 h2, h1 # h2 ->
  Permutation (s2l (dom (h1 +++ h2))) (s2l (dom h1) ++ s2l (dom h2)).

Lemma app_seq_reg : forall h0 h0' h1 h2,
  ordered X.ltA (unzip1 h0) -> unzip1 h0 = unzip1 h0' ->
  ordered X.ltA (unzip1 h1) -> ordered X.ltA (unzip1 h2) ->
  app_seq h0 h1 = app_seq h0' h2 ->
  dis (unzip1 h1) (unzip1 h0) -> dis (unzip1 h2) (unzip1 h0') ->
  h0 = h0' /\ h1 = h2.

Lemma union_emp_inv : forall h1 h2, emp = h1 +++ h2 -> h1 = emp /\ h2 = emp.

Lemma union_inv : forall h0 h0' h1 h2,
  h0 +++ h1 = h0' +++ h2 -> dom h0 = dom h0' ->
  h1 # h0 -> h2 # h0' -> h0 = h0' /\ h1 = h2.

Lemma distributivity : forall h1 h2 h0, h0 # (h1 +++ h2) <-> h0 # h1 /\ h0 # h2.

Lemma disj_union_R : forall h1 h2 h0, h0 # h1 -> h0 # h2 -> h0 # (h1 +++ h2).

Lemma disj_union_L : forall h1 h2 h0, h1 # h0 -> h2 # h0 -> (h1 +++ h2) # h0.

Lemma disj_union_inv : forall h1 h2 h0, h0 # (h1 +++ h2) -> h0 # h1 /\ h0 # h2.

Lemma disj_add_map : forall h k n z,
  Lists_ext.disj k (List.map (@fst l v) (s2l ((n, z) :: h))) ->
  Lists_ext.disj k (List.map (@fst l v) (s2l (add_map X.ltA n z h))).

Lemma disj_app_app_seq : forall l1 l2 k,
  Lists_ext.disj k (List.map (@fst l v) (s2l l1) ++ List.map (@fst l v) (s2l l2)) ->
  Lists_ext.disj k (s2l (map (@fst l v) (app_seq l1 l2))).

Lemma dis_dom_union1 : forall h1 h2 l,
  dis l (dom h1) -> dis l (dom h2) -> dis l (dom (h1 +++ h2)).

Lemma dis_dom_union2 : forall h1 h2 l,
  dis l (dom (h1 +++ h2)) -> dis l (dom h1) /\ dis l (dom h2).

Lemma dis_dom_union : forall h1 h2 l,
  dis l (dom (h1 +++ h2)) = dis l (dom h1) && dis l (dom h2).

Lemma elts_union_sing_Perm' : forall d x rx, x \notin dom d ->
  Permutation (s2l ((x, rx) :: elts d)) (s2l (elts (union (sing x rx) d))).

Lemma elts_union_sing_Perm : forall l d x rx, Permutation l (s2l (elts d)) ->
  ~ In x (Lists_ext.uzip1 l) ->
  Permutation ((x, rx) :: l)%list (s2l (elts (union (sing x rx) d))).

deletion of several elements

Definition del_seq (d : seq l) (k : seq_eqType (prod_eqType l v)) := filter (fun x => ~~ (x.1 \in d)) k.

Lemma notin_unzip1_del_seq : forall l1 l2 x, x \in l1 -> x \notin unzip1 (del_seq l1 l2).

Lemma notin_unzip1_del_seq_app : forall l d1 d2 x,
  ~ x \in unzip1 (del_seq d1 l) -> ~ x \in unzip1 (del_seq d2 l) ->
  ~ x \in unzip1 (del_seq (d1 ++ d2) l).

Lemma del_seq_upd_seq : forall k d n w, n \in d -> del_seq d (upd_seq n w k) = del_seq d k.

Lemma del_seq_invariant : forall k ns, dis (unzip1 k) ns -> del_seq ns k = k.

Lemma ordered_del_seq : forall k, ordered X.ltA (unzip1 k) ->
  forall d, ordered X.ltA (unzip1 (del_seq d k)).

Definition difs h l := mk_t (del_seq l (elts h)) (ordered_del_seq (elts h) (prf h) l).
Notation "k '[\m]' m" := (difs k m) (at level 69) : map_scope.

Lemma filter_add_seq1 : forall k (Hk : ordered X.ltA (unzip1 k)) a b p,
  a \notin unzip1 k ->
  p a = true ->
  filter (fun x => p (fst x)) (add_seq a b k) =
  add_seq a b (filter (fun x => p (fst x)) k).

Lemma filter_add_seq2 : forall k (Hk : ordered X.ltA (unzip1 k)) a b p,
  a \in unzip1 k ->
  p a = true ->
  filter (fun x => p (fst x)) (add_seq a b k) =
  add_seq a b (filter (fun x => p (fst x)) k).

Lemma filter_add_seq : forall k (Hk : ordered X.ltA (unzip1 k)) a b p,
  p a = true ->
  filter (fun x => p (fst x)) (add_seq a b k) =
  add_seq a b (filter (fun x => p (fst x)) k).

Lemma filter_add_seq' : forall k (Hk : ordered X.ltA (unzip1 k)) a b p,
  p a = false ->
  filter (fun x => p (fst x)) (add_seq a b k) =
  filter (fun x => p (fst x)) k.

Lemma filter_app_seq : forall k1 (Hk1 : ordered X.ltA (unzip1 k1))
  k2 (Hk2 : ordered X.ltA (unzip1 k2)) (p : pred l),
  filter (fun x => p (fst x) ) (app_seq k1 k2) =
  app_seq (filter (fun x => p (fst x)) k1) (filter (fun x => p (fst x)) k2).

Lemma union_difs_L : forall h1 h2 k, dis (dom h2) k ->
  (h1 +++ h2) [\m ] k = (h1 [\m ] k) +++ h2.

Lemma difs_self : forall k, k [\m ] dom k = emp.

Lemma difs_upd : forall k n w d, n \in d -> difs (upd n w k) d = difs k d.

Lemma disj_difs : forall h1 h2, h1 # h2 -> forall d, h1 # h2 [\m ] d.

Lemma disj_difs' : forall h1 h2 d, inc (dom h1) d -> h1 # h2 [\m ] d.

Lemma get_seq_del_seq : forall k w d, w \in d -> get_seq w (del_seq d k) = None.

Lemma get_seq_del_seq' : forall k x d, x \notin d -> get_seq x (del_seq d k) = get_seq x k.

Lemma get_difs : forall k x d, x \notin d -> get x (k [\m ] d) = get x k.

Lemma get_difs_None : forall k x d, x \in d -> get x (k [\m ] d) = None.

Lemma dom_difs_del : forall k d, dom (k [\m ] d) = del (fun x => x \in d) (dom k).

projection

Definition
proj_seq (k : seq (l * v)) (d : seq l) : seq (l * v) := filter (fun x => x.1 \in d) k.

Lemma proj_seq_nil : forall d, proj_seq [::] d = [::].

Lemma proj_seq_nil' : forall k, proj_seq k [::] = [::].

Lemma proj_seq_cons : forall l2 h1 t1,
  h1 \notin (unzip1 l2) -> proj_seq l2 (cons h1 t1) = proj_seq l2 t1.

Lemma in_proj_seq_inv : forall d k x, x \in proj_seq k d -> x \in k.

Lemma get_seq_proj_seq_None : forall k d n, n \notin d -> get_seq n (proj_seq k d) = None.

Lemma get_seq_proj_seq : forall k d n, n \in d -> get_seq n (proj_seq k d) = get_seq n k.

Lemma dis_proj_seq : forall (l1 : seq_eqType (prod_eqType l v)) ( l2 : seq_eqType (prod_eqType l v)),
  dis (unzip1 l1) (unzip1 l2) -> proj_seq l1 (unzip1 l2) = [::].

Lemma ordered_proj_seq : forall k, ordered X.ltA (unzip1 k) ->
  forall d, ordered X.ltA (unzip1 (proj_seq k d)).

Definition proj k d : t := mk_t (proj_seq (elts k) d) (ordered_proj_seq _ (prf k) d).

Lemma proj_emp : forall k, proj emp k = emp.

Lemma proj_nil : forall k, proj k [::] = emp.

Lemma dom_proj_sing : forall k n, n \in dom k -> dom (proj k [:: n]) = [:: n].

Lemma inc_dom_proj : forall d k, inc (dom (proj k d)) d.

Lemma inc_dom_proj_dom : forall h d, inc (dom (proj h d)) (dom h).

Lemma dom_proj_exact' : forall k d, ordered X.ltA d -> inc d k ->
  ordered X.ltA k -> filter (mem d) k = d.

Lemma dom_proj_exact : forall h d, ordered X.ltA d -> inc d (dom h) -> dom (proj h d) = d.

Lemma size_dom_proj_exact' : forall (A : eqType) (k d : seq A),
  uniq k -> uniq d -> inc d k -> size (filter (mem d) k) = size d.

Lemma size_dom_proj_exact : forall h d, uniq d -> inc d (dom h) -> size (dom (proj h d)) = size d.

Lemma dom_proj_cons : forall k n d, n \notin dom k -> proj k (n :: d) = proj k d.

Lemma in_dom_proj : forall x d h, x \in d -> x \in dom h -> x \in dom (proj h d).

Lemma in_dom_proj_inter : forall k d m, m \in dom (proj k d) -> m \in dom k /\ m \in d.

Lemma filter_upd_seq : forall k p w P, P p = false ->
  filter (fun x : l * v => P (fst x)) (upd_seq p w k) =
  upd_seq p w (filter (fun x : l * v => P (fst x)) k).

Lemma filter_upd_seq' : forall k p w P, P p = true ->
  filter (fun x : l * v => P (fst x)) (upd_seq p w k) =
  upd_seq p w (filter (fun x : l * v => P (fst x)) k).

Lemma proj_upd_notin : forall d k p w, p \notin d -> proj (upd p w k) d = upd p w (proj k d).

Lemma proj_upd_in : forall d k p w, p \in d -> proj (upd p w k) d = upd p w (proj k d).

Lemma proj_upd : forall d k p w, proj (upd p w k) d = upd p w (proj k d).

Lemma get_proj : forall d k n, n \in d -> get n (proj k d) = get n k.

Lemma get_proj_None : forall d k n, n \notin d -> get n (proj k d) = None.

Lemma disj_proj_emp : forall h1 h2, h1 # h2 -> proj h1 (dom h2) = emp.

Lemma disj_proj_same_dom : forall k1 k2 d1 d2, dom k1 = dom k2 ->
  proj k1 d1 # proj k1 d2 ->
  proj k2 d1 # proj k2 d2.

Lemma dis_disj_proj : forall k1 k2 d1 d2, dis d1 d2 -> proj k1 d1 # proj k2 d2.

Lemma disj_proj_L : forall h d k, h # k -> proj h d # k.

Lemma dom_dom_proj : forall h1 h2 d, dom h1 = dom h2 -> dom (proj h1 d) = dom (proj h2 d).

Lemma filter_app_seq2 : forall (k : seq_eqType (prod_eqType l v)) (Hk : ordered X.ltA (unzip1 k))
  (r p q : pred l),
  (forall b, r b <-> p b \/ q b) ->
  filter (fun x : l * v => r x.1) k =
  app_seq (filter (fun x : l * v => p x.1) k) (filter (fun x : l * v => q x.1) k).

Lemma proj_seq_itself : forall k1, proj_seq k1 (unzip1 k1) = k1.

Lemma proj_itself : forall k, proj k (dom k) = k.

Lemma proj_seq_union_L : forall k1, ordered X.ltA (unzip1 k1) ->
  forall k2, ordered X.ltA (unzip1 k2) ->
  dis (unzip1 k1) (unzip1 k2) ->
  proj_seq (app_seq k1 k2) (map (fun x => fst x) k1) = k1.

Lemma proj_union_L : forall h h1 h2, h # h2 -> proj (h1 +++ h2) (dom h) = proj h1 (dom h).

Lemma proj_union_R : forall h h', h # h' -> proj (h +++ h') (dom h') = h'.

Lemma proj_app : forall k d1 d2, proj k (d1 ++ d2) = proj k d1 +++ proj k d2.

Lemma proj_union_sing : forall k x y d, x \in d ->
  proj (sing x y +++ k) d = sing x y +++ proj k d.

Lemma proj_union_sing_notin : forall k x y d, x \notin d ->
  proj (sing x y +++ k) d = proj k d.

Lemma proj_dom_union : forall h h1 h2, h1 # h2 ->
  proj h (dom (h1 +++ h2)) = proj h (dom h1) +++ proj h (dom h2).

Lemma proj_difs : forall k d, k = proj k d +++ (k [\m ] d).

Lemma proj_difs_disj : forall k d d', inc d d' -> proj k d # k [\m ] d'.

Lemma proj_disj : forall k1 k2 k d, dom k1 = dom k2 -> proj k1 k # d -> proj k2 k # d.

Definition continuous (A : Type) (def : A) (l : seq A) (ltA : A -> A -> bool) :=
  (forall i,
    0 <= i < size l ->
    ~ exists a, ltA (nth def l i) a /\ ltA a (nth def l i.+1))%nat.

Lemma map_filter_drop : forall k : seq (l * v), ordered X.ltA (unzip1 k) ->
  forall l1 l2, unzip1 k = l1 ++ l2 ->
    filter (fun x => x.1 \in l2) k = drop (size l1) k.

Lemma cdom_proj : forall h l1 l2, dom h = l1 ++ l2 ->
  cdom (proj h l2) = drop (size l1) (cdom h).

Lemma cdom_difs : forall h l1 l2, dom h = l1 ++ l2 -> cdom (h [\m ] l2) = take (size l1) (cdom h).

Lemma app_proj_difs : forall h l1 l2, dom h = l1 ++ l2 ->
  proj h l1 = h [\m ] l2.

Lemma cdom_proj2 : forall h l1 l2, dom h = l1 ++ l2 ->
  cdom (proj h l1) = take (size l1) (cdom h).

map inclusion

Definition inclu h1 h2 := proj h2 (dom h1) = h1.
Notation "k '[<=m]' m" := (inclu k m) (at level 69) : map_scope.

Lemma incluE : forall h k, k [<=m ] h <-> proj h (dom k) = k.

Lemma inc_seq_inclu' : forall (h1 : seq_eqType (prod_eqType l v))
  (Hh1 : ordered X.ltA (unzip1 h1))
  (h2 : seq_eqType (prod_eqType l v))
  (Hh2 : ordered X.ltA (unzip1 h2))
  (Hincl : forall (n : l) (w : v), get_seq n h1 = Some w -> get_seq n h2 = Some w),
  proj_seq h2 (unzip1 h1) = h1.

Lemma get_inclu : forall h1 h2,
  (forall n w, get n h1 = Some w -> get n h2 = Some w) -> h1 [<=m ] h2.

Lemma inclu_get : forall h1 h2, h1 [<=m ] h2 ->
  forall n w, get n h1 = Some w -> get n h2 = Some w.

Lemma inclu_inc : forall h1 h2, h1 [<=m ] h2 -> inc (elts h1) (elts h2).

Lemma inclu_inc_dom : forall h1 h2, h1 [<=m ] h2 -> inc (dom h1) (dom h2).

Lemma inclu_union_L : forall h1 h2 k, h1 # h2 -> k [<=m ] h1 ->
  k [<=m ] (h1 +++ h2).

Lemma inclu_refl : forall k, k [<=m ] k.

Lemma proj_inclu : forall k h1 d, k [<=m ] (proj h1 d) -> k [<=m ] h1.

Definition del_elt n k := del_seq [::n] k.

Lemma in_unzip1_del_elt : forall l0 x h1, x <> h1 ->
  x \in unzip1 l0 -> x \in unzip1 (del_elt h1 l0).

Lemma unzip1_add_seq_del_elt : forall l0 h1 h2,
  ordered X.ltA (unzip1 l0) ->
  h1 \in unzip1 l0 ->
  unzip1 l0 = unzip1 (add_seq h1 h2 (del_elt h1 l0)).

Lemma not_mem_dom_del_elt : forall k n, ~ n \in unzip1 k -> del_elt n k = k.

Lemma mem_dom_del_elt' : forall k n, n \in unzip1 (del_elt n k) = false.

Lemma del_seq_del_elt : forall k n ns, del_seq (n :: ns) k = del_seq ns (del_elt n k).

Lemma unzip1_app_seq_del_seq : forall k l,
  ordered X.ltA (unzip1 l) -> ordered X.ltA (unzip1 k) ->
  inc (unzip1 k) (unzip1 l) ->
  unzip1 l = unzip1 (app_seq k (del_seq (unzip1 k) l)).

Lemma add_seq_del_elt'' : forall (k : seq_eqType (prod_eqType X.A E.A)) n w,
  ordered X.ltA (unzip1 k) -> (n, w) \in k ->
  k = add_seq n w (del_elt n k).

Lemma ordered_del_elt : forall k, ordered X.ltA (unzip1 k) -> forall n, ordered X.ltA (unzip1 (del_elt n k)).

Lemma app_seq_del_seq : forall k l,
  ordered X.ltA (unzip1 l) -> ordered X.ltA (unzip1 k) ->
  inc k l -> l = app_seq k (del_seq (unzip1 k) l).

Lemma filter_app_seq' : forall k (Hk : ordered X.ltA (unzip1 k)) p,
  k = app_seq (filter (fun x => p (fst x)) k) (filter (fun x => ~~ p (fst x)) k).

Lemma app_seq_del_seq_proj_seq : forall k d,
  ordered X.ltA (unzip1 k) -> k = app_seq (del_seq d k) (proj_seq k d).

Lemma proj_seq_restrict' : forall (h2 : seq_eqType (prod_eqType l v))
  (Hh2 : ordered X.ltA (unzip1 h2)) (d d' : seq l),
  inc d d' -> proj_seq h2 d = proj_seq (proj_seq h2 d') d.

Lemma proj_restrict' : forall d d' h2, inc d d' -> proj h2 d = proj (proj h2 d') d.

Lemma proj_restrict : forall h1 h2 d, h1 [<=m ] h2 ->
  inc d (dom h1) -> proj h2 d = proj h1 d.

Lemma union_difs : forall h k d, k [<=m ] h -> dom k = d -> h = k +++ (h [\m ] d).

Lemma dom_union_difs : forall h k, inc (dom k) (dom h) -> dom h = dom (k +++ (h [\m ] dom k)).

Lemma get_inclu_sing : forall h a b, get a h = Some b -> sing a b [<=m ] h.

Lemma inclu_proj : forall k d, proj k d [<=m ] k.

Lemma proj_dom_proj : forall k d, proj k (dom (proj k d)) = proj k d.

Lemma proj_seq_del_seq : forall (k : seq (prod_eqType l v)) (Hk : ordered X.ltA (unzip1 k)) (d : seq l),
  proj_seq k (unzip1 (del_seq d k)) = del_seq d k.

Lemma proj_seq_del_seq2 : forall k x d, x \in d ->
  proj_seq (del_seq (cons x [::]) k) d = del_seq (cons x [::]) (proj_seq k d).

Lemma inclu_difs : forall h d, (h [\m ] d) [<=m ] h.

Lemma disj_proj_inclu : forall h d1 hh,
  proj h d1 # hh -> proj h d1 [<=m ] (h [\m ] (dom hh)).

Lemma incl_proj2 : forall h1 h2 k, h1 [<=m ] k -> h2 [<=m ] k -> dom h1 = dom h2 ->
  h1 = h2.

Lemma disj_proj_app : forall h k d1 d2, h # (k [\m ] d1) -> h # (k [\m ] d2) ->
  h # (k [\m ] (d1 ++ d2)).

Definition dif h l := h [\m ] [:: l].
Notation "k '---' m" := (dif k m) (at level 69) : map_scope.

Lemma dif_def : forall h n, h --- n = h [\m ] [:: n].

Lemma dif_sing : forall a b, sing a b --- a = emp.

Lemma dif_emp : forall p, emp --- p = emp.

Lemma mem_dom_del_elt : forall k n n', n <> n' -> n \in unzip1 (del_elt n' k) = (n \in unzip1 k).

Lemma del_elt_upd_seq : forall k n w, del_elt n (upd_seq n w k) = del_elt n k.

Lemma del_elt_upd_seq' : forall k n n' w, n <> n' -> del_elt n (upd_seq n' w k) = upd_seq n' w (del_elt n k).

Lemma add_seq_del_elt' : forall k n w, del_elt n (add_seq n w k) = del_elt n k.

Lemma add_seq_del_elt: forall lst n w n', ordered X.ltA (unzip1 lst) ->
  n' <> n -> add_seq n w (del_elt n' lst) = del_elt n' (add_seq n w lst).

Lemma get_seq_del_elt : forall w st, get_seq w (del_elt w st) = None.

Lemma get_seq_del_elt' : forall k x y, x <> y -> get_seq x (del_elt y k) = get_seq x k.

Lemma del_elt_app_seq : forall k m n, ordered X.ltA (unzip1 m) -> ordered X.ltA (unzip1 k) ->
  del_seq [:: n] (app_seq k m) = app_seq (del_seq [:: n] k) (del_seq [:: n] m).

Lemma dif_not_in_dom: forall h l, ~ l \in unzip1 (elts h) -> h --- l = h.

Lemma dif_union: forall h1 h2 a, (h1 +++ h2) --- a = (h1 --- a) +++ (h2 --- a).

Lemma dif_disj: forall h a b, h # sing a b -> h --- a = h.

Lemma dif_disj' : forall h1 h2 l, h1 # h2 -> h1 --- l # h2 --- l.

Lemma dis_dif : forall h k, k # (h [\m ] (unzip1 (elts k))).

Lemma get_dif : forall w st, get w (st --- w) = None.

Lemma get_dif' : forall st x y, x <> y -> get x (st --- y) = get x st.

Lemma proj_dif : forall k x d, x \in d -> proj (k --- x) d = (proj k d) --- x.

End map.

Additional, derived properties

Module Map_Prop (M : MAP).

Import M.
Local Open Scope map_scope.

Lemma emp_sing_dis : forall a b, M.emp <> M.sing a b.

Lemma get_exists_sing : forall h a b, M.get a h = Some b ->
  exists h', h = M.sing a b +++ h' /\ M.sing a b # h'.

Lemma proj_difs_disj_spec : forall k d, proj k d # k [\m ] d.

Lemma union_reg : forall h k l, h +++ k = h +++ l -> k # h -> l # h -> k = l.

Require Import nodup.

Lemma swap_heads : forall x rx y ry k,
  nodup (x :: y :: List.nil)%list ->
  M.sing x rx +++ (M.sing y ry +++ k) = M.sing y ry +++ (M.sing x rx +++ k).

Lemma app_inclu : forall h1 h2 h3 h4, h1 # h2 -> h3 # h4 ->
  h1 # h3 ->
  h1 +++ h2 = h3 +++ h4 ->
  h3 [<=m ] h2.

Lemma disj_comp : forall k1 h1 h2 k2, h1 # k1 -> h1 # h2 -> k1 # k2 ->
  k1 +++ k2 = h1 +++ h2 ->
  exists h', k1 # h' /\ h2 = h' +++ k1.

Fixpoint mk_finmap (lst : seq (l * v)) : t :=
  if lst is (hd1, hd2) :: tl then sing hd1 hd2 +++ mk_finmap tl else emp.

Lemma elts_mk_finmap : forall l, ordset.OrderedSequence.ordered M.ltl (unzip1 l) ->
  elts (mk_finmap l) = l.

Lemma size_dom_union : forall h1 h2, h1 # h2 ->
  size (dom (h1 +++ h2)) = (size (dom h1) + size (dom h2))%coq_nat.

Lemma size_dom_difs : forall k d, uniq d -> inc d (dom k) ->
  size (dom (k [\m ] d)) = (size (dom k) - size d)%coq_nat.

Lemma union_difs_L_old : forall h1 h2, h1 # h2 -> (h1 +++ h2)[\m ]dom h1 = h2.

Lemma inclu_union_L_old : forall h1 h2, h1 # h2 -> h1 [<=m ] (h1 +++ h2).

Lemma incl_dom_union : forall h1 h2, incl (s2l (dom h1)) (s2l (dom (h1 +++ h2))).

Lemma inclu_disj : forall h1 h2 k, h1 # h2 -> k [<=m ] h1 -> k # h2.

Lemma inclu_union : forall h h1 h2, h1 [<=m ] h -> h2 [<=m ] h -> (h1 +++ h2) [<=m ] h.

Lemma get_proj_Some_inv : forall d (k : t) (n : l) y,
  get n (proj k d) = Some y -> n \in d.

End Map_Prop.

Tactics for finite maps

Module Map_Tac (M : MAP).

Import M.
Local Open Scope map_scope.

Lemma disj_up : forall x x1 x2 x3, x = x1 +++ x3 -> x1 # x3 -> x # x2 -> x1 # x2.

Lemma disj_up' : forall x x1 x2 x3, x = x1 +++ x3 -> x1 # x3 -> x # x2 -> x3 # x2.

Ltac Disj :=
  match goal with
    | H: (?x1 +++ ?x2) # ?x |- _ =>
      let H1 := fresh in
      generalize (disj_union_inv x1 x2 x (disj_sym (x1 +++ x2) x H));
        intro H1; inversion_clear H1; clear H; Disj
    | H: ?x # (?x1 +++ ?x2) |- _ =>
      let H1 := fresh in
      generalize (disj_union_inv x1 x2 x H); intro H1; inversion_clear H1; clear H; Disj
    | |- (?x1 +++ ?x2) # ?x3 =>
      eapply disj_sym; apply disj_union_R; [ (Disj_simpl || Disj) | (Disj_simpl || Disj) ]
    | |- ?x3 # (?x1 +++ ?x2) =>
      apply disj_union_R; [ (Disj_simpl || Disj) | (Disj_simpl || Disj) ]
    | |- ?x1 # ?x2 => Disj_up
  end
with
  Disj_up := Disj_simpl || Disj_up_left || Disj_up_right
with
  Disj_up_left :=
  match goal with
    | H1: ?X1 = (?x1 +++ ?x1') |- ?x1 # ?x2 =>
      apply (disj_up X1 x1 x2 x1' H1); [(Disj_simpl || Disj) | (Disj_simpl || Disj)]
    | H1: ?X1 = (?x1 +++ ?x1') |- ?x1' # ?x2 =>
      apply (disj_up' X1 x1 x2 x1' H1) ; [(Disj_simpl || Disj) | (Disj_simpl || Disj)]
    | |- ?x1 # ?x2 => Disj_simpl
  end
with
  Disj_up_right :=
  match goal with
    | H1: ?X1 = (?x2 +++ ?x2') |- ?x1 # ?x2 =>
      apply disj_sym; apply (disj_up X1 x2 x1 x2' H1); [(Disj_simpl || Disj) | (Disj_simpl || Disj)]
    | H1: ?X1 = (?x2 +++ ?x2') |- ?x1 # ?x2' =>
      apply disj_sym; apply (disj_up' X1 x2 x1 x2' H1) ; [(Disj_simpl || Disj) | (Disj_simpl || Disj)]
    | |- ?x1 # ?x2 => Disj_simpl
  end
with
  Disj_simpl :=
  match goal with
    | H : ?x1 # ?x2 |- ?x1 # ?x2 => auto
    | H : ?x2 # ?x1 |- ?x1 # ?x2 => apply disj_sym; auto
    | |- ?x1 # emp => apply (disj_emp_R x1)
    | |- emp # ?x1 => apply disj_sym; apply (disj_emp_R x1)
    | |- sing ?l1 ?v1 # sing ?l2 ?v2 => eapply disj_sing; omega
  end.

Lemma Disj_test1 : forall h h1 h2, h # (h1 +++ h2) -> h # h2.

Lemma Disj_test2 : forall h h1 h2 h11 h12 h21 h22 h111 h112 h121 h122 h211 h212 h221 h222,
  h1 # h2 ->
  h11 # h12 ->
  h21 # h22 ->
  h111 # h112 ->
  h121 # h122 ->
  h211 # h212 ->
  h221 # h222 ->
  h = h1 +++ h2 ->
  h1 = h11 +++ h12 ->
  h2 = h21 +++ h22 ->
  h11 = h111 +++ h112 ->
  h12 = h121 +++ h122 ->
  h21 = h211 +++ h212 ->
  h22 = h221 +++ h222 ->
  (h112 +++ h221) # h222.

Lemma Equal_union_com: forall h1 h2 h3 h4, h1 # h2 ->
  h2 +++ h1 = h3 +++ h4 -> h1 +++ h2 = h3 +++ h4.

Lemma Equal_subst: forall X h1 h2, h1 = h2 -> X +++ h1 = X +++ h2.

Ltac Equal :=
  match goal with
    | |- (?h1 +++ ?h2) = (?h1 +++ ?h3) => apply (Equal_subst h1 h2 h3); Equal
    | |- ?h1 = ?h1 => auto
    | |- (emp +++ ?h1) = ?h2 => rewrite (union_emp_L h1); Equal
    | |- (?h1 +++ emp ) = ?h2 => rewrite (union_emp_R h1); Equal
    | |- ?h2 = (emp +++ ?h1) => rewrite (union_emp_L h1); Equal
    | |- ?h2 = (?h1 +++ emp ) => rewrite (union_emp_R h1); Equal
    | H: ?X = (?x1 +++ ?x2) |- (?X +++ ?x1') = (?Y +++ ?x2') => rewrite H ; Equal
    | H: ?Y = (?y1 +++ ?y2) |- (?X +++ ?x1') = (?Y +++ ?x2') => rewrite H ; Equal
    | H: ?X = (?x1 +++ ?x2) |- ?X = (?Y +++ ?x2') => rewrite H ; Equal
    | H: ?Y = (?y1 +++ ?y2) |- (?X +++ ?x1') = ?Y => rewrite H ; Equal
    | |- ((?h1 +++ ?h2) +++ ?h3) = ?X => rewrite -(union_assoc h1 h2 h3); [Equal]
    | |- ?X = ((?h1 +++ ?h2) +++ ?h3) => rewrite -(union_assoc h1 h2 h3); [Equal]
    | |- (?h1 +++ ?h2) = (?h3 +++ ?h4) => apply (Equal_union_com h1 h2 h3 h4); [Disj | Equal]
    | H1: ?h1 = ?h2 |- ?h1 = ?h3 => rewrite H1; Equal
    | H1: ?h1 = ?h2 |- ?h3 = ?h1 => rewrite H1; Equal
  end.

End Map_Tac.