(*
 * Vericert: Verified high-level synthesis.
 * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
 *
 * This program is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program.  If not, see <https://www.gnu.org/licenses/>.
 *)

From vericert Require Import Vericertlib ValueInt.
From compcert Require Import Maps.

Definition reg := positive.

Module AssocMap := Maps.PTree.

Module AssocMapExt.
  Import AssocMap.

  Hint Resolve elements_correct elements_complete
       elements_keys_norepet : assocmap.
  Hint Resolve gso gss : assocmap.

  Section Operations.

    Variable A : Type.

    Definition get_default (a : A) (k : reg) (m : t A) : A :=
      match get k m with
      | None => a
      | Some v => v
      end.

    Fixpoint merge (m1 m2 : t A) : t A :=
      match m1, m2 with
      | Node l1 (Some a) r1, Node l2 _ r2 => Node (merge l1 l2) (Some a) (merge r1 r2)
      | Node l1 None r1, Node l2 o r2 => Node (merge l1 l2) o (merge r1 r2)
      | Leaf, _ => m2
      | _, _ => m1
      end.

    Lemma merge_base_1 :
      forall am,
      merge (empty A) am = am.
A:Type
forall am : t A, merge (empty A) am = am
    Proof.
A:Type
forall am : t A, merge (empty A) am = am auto. Qed.
    Hint Resolve merge_base_1 : assocmap.

    Lemma merge_base_2 :
      forall am,
      merge am (empty A) = am.
A:Type
forall am : t A, merge am (empty A) = am
    Proof.
A:Type
forall am : t A, merge am (empty A) = am
      unfold merge.
A:Type
forall am : t A,
(fix merge (m1 m2 : t A) {struct m1} : t A :=
   match m1 with
   | Leaf => m2
   | Node l1 (Some a) r1 =>
       match m2 with
       | Leaf => m1
       | Node l2 _ r2 =>
           Node (merge l1 l2) (Some a) (merge r1 r2)
       end
   | Node l1 None r1 =>
       match m2 with
       | Leaf => m1
       | Node l2 o r2 =>
           Node (merge l1 l2) o (merge r1 r2)
       end
   end) am (empty A) = am
      destruct am; trivial.
A:Type
am1:tree A
o:option A
am2:tree A
match o with
| Some a =>
    match empty A with
    | Leaf => Node am1 o am2
    | Node l2 _ r2 =>
        Node
          ((fix merge (m1 m2 : t A) {struct m1} :
                t A :=
              match m1 with
              | Leaf => m2
              | Node l1 (Some a0) r1 =>
                  match m2 with
                  | Leaf => m1
                  | Node l3 _ r3 =>
                      Node (merge l1 l3) (Some a0)
                        (merge r1 r3)
                  end
              | Node l1 None r1 =>
                  match m2 with
                  | Leaf => m1
                  | Node l3 o1 r3 =>
                      Node (merge l1 l3) o1
                        (merge r1 r3)
                  end
              end) am1 l2) (Some a)
          ((fix merge (m1 m2 : t A) {struct m1} :
                t A :=
              match m1 with
              | Leaf => m2
              | Node l1 (Some a0) r1 =>
                  match m2 with
                  | Leaf => m1
                  | Node l3 _ r3 =>
                      Node (merge l1 l3) (Some a0)
                        (merge r1 r3)
                  end
              | Node l1 None r1 =>
                  match m2 with
                  | Leaf => m1
                  | Node l3 o1 r3 =>
                      Node (merge l1 l3) o1
                        (merge r1 r3)
                  end
              end) am2 r2)
    end
| None =>
    match empty A with
    | Leaf => Node am1 o am2
    | Node l2 o r2 =>
        Node
          ((fix merge (m1 m2 : t A) {struct m1} :
                t A :=
              match m1 with
              | Leaf => m2
              | Node l1 (Some a) r1 =>
                  match m2 with
                  | Leaf => m1
                  | Node l3 _ r3 =>
                      Node (merge l1 l3) (Some a)
                        (merge r1 r3)
                  end
              | Node l1 None r1 =>
                  match m2 with
                  | Leaf => m1
                  | Node l3 o1 r3 =>
                      Node (merge l1 l3) o1
                        (merge r1 r3)
                  end
              end) am1 l2) o
          ((fix merge (m1 m2 : t A) {struct m1} :
                t A :=
              match m1 with
              | Leaf => m2
              | Node l1 (Some a) r1 =>
                  match m2 with
                  | Leaf => m1
                  | Node l3 _ r3 =>
                      Node (merge l1 l3) (Some a)
                        (merge r1 r3)
                  end
              | Node l1 None r1 =>
                  match m2 with
                  | Leaf => m1
                  | Node l3 o1 r3 =>
                      Node (merge l1 l3) o1
                        (merge r1 r3)
                  end
              end) am2 r2)
    end
end = Node am1 o am2
      destruct o; trivial.
    Qed.
    Hint Resolve merge_base_2 : assocmap.

    Lemma merge_add_assoc :
      forall r am am' v,
      merge (set r v am) am' = set r v (merge am am').
A:Type
forall (r : positive) (am am' : t A) (v : A),
merge (set r v am) am' = set r v (merge am am')
    Proof.
A:Type
forall (r : positive) (am am' : t A) (v : A),
merge (set r v am) am' = set r v (merge am am')
      induction r; intros; destruct am; destruct am'; try (destruct o); simpl;
        try rewrite IHr; try reflexivity.
    Qed.
    Hint Resolve merge_add_assoc : assocmap.

    Lemma merge_correct_1 :
      forall am bm k v,
      get k am = Some v ->
      get k (merge am bm) = Some v.
A:Type
forall (am bm : t A) (k : positive) (v : A),
am ! k = Some v -> (merge am bm) ! k = Some v
    Proof.
A:Type
forall (am bm : t A) (k : positive) (v : A),
am ! k = Some v -> (merge am bm) ! k = Some v
      induction am; intros; destruct k; destruct bm; try (destruct o); simpl;
        try rewrite gempty in H; try discriminate; try assumption; auto.
    Qed.
    Hint Resolve merge_correct_1 : assocmap.

    Lemma merge_correct_2 :
      forall am bm k v,
      get k am = None ->
      get k bm = Some v ->
      get k (merge am bm) = Some v.
A:Type
forall (am bm : t A) (k : positive) (v : A),
am ! k = None ->
bm ! k = Some v -> (merge am bm) ! k = Some v
    Proof.
A:Type
forall (am bm : t A) (k : positive) (v : A),
am ! k = None ->
bm ! k = Some v -> (merge am bm) ! k = Some v
      induction am; intros; destruct k; destruct bm; try (destruct o); simpl;
        try rewrite gempty in H; try discriminate; try assumption; auto.
    Qed.
    Hint Resolve merge_correct_2 : assocmap.

    Definition merge_fold (am bm : t A) : t A :=
      fold_right (fun p a => set (fst p) (snd p) a) bm (elements am).

    Lemma add_assoc :
      forall (k : elt) (v : A) l bm,
      List.In (k, v) l ->
      list_norepet (List.map fst l) ->
      @get A k (fold_right (fun p a => set (fst p) (snd p) a) bm l) = Some v.
A:Type
forall (k : elt) (v : A) (l : list (elt * A))
  (bm : t A),
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm l) ! k = Some v
    Proof.
A:Type
forall (k : elt) (v : A) (l : list (elt * A))
  (bm : t A),
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm l) ! k = Some v
      induction l; intros.
A:Type
k:elt
v:A
bm:t A
H:In (k, v) nil
H0:list_norepet (List.map fst nil)
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm nil) ! k = Some v
A:Type
k:elt
v:A
a:(elt * A)%type
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) (a :: l)
H0:list_norepet (List.map fst (a :: l))
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm (a :: l)) ! k = Some v
      -
A:Type
k:elt
v:A
bm:t A
H:In (k, v) nil
H0:list_norepet (List.map fst nil)
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm nil) ! k = Some v contradiction.
      -
A:Type
k:elt
v:A
a:(elt * A)%type
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) (a :: l)
H0:list_norepet (List.map fst (a :: l))
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm (a :: l)) ! k = Some v destruct a as [k' v'].
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v
        destruct (peq k k').
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
e:k = k'
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v
        +
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
e:k = k'
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v inversion H.
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
e:k = k'
H1:(k', v') = (k, v)
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
e:k = k'
H1:In (k, v) l
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v inversion H1.
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
e:k = k'
H1:(k', v') = (k, v)
H3:k' = k
H4:v' = v
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k, v) :: l)) ! k =
Some v
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
e:k = k'
H1:In (k, v) l
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v inversion H0.
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
e:k = k'
H1:(k', v') = (k, v)
H3:k' = k
H4:v' = v
hd:elt
tl:list elt
H6:~ In k' (List.map fst l)
H7:list_norepet (List.map fst l)
H2:hd = k'
H5:tl = List.map fst l
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k, v) :: l)) ! k =
Some v
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
e:k = k'
H1:In (k, v) l
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v subst.
A:Type
v:A
k':elt
l:list (elt * A)
IHl:forall bm : t A,
In (k', v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k' = Some v
bm:t A
H0:list_norepet (List.map fst ((k', v) :: l))
H:In (k', v) ((k', v) :: l)
H3:k' = k'
H1:(k', v) = (k', v)
H6:~ In k' (List.map fst l)
H7:list_norepet (List.map fst l)
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v) :: l)) ! k' =
Some v
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
e:k = k'
H1:In (k, v) l
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v
          simpl.
A:Type
v:A
k':elt
l:list (elt * A)
IHl:forall bm : t A,
In (k', v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k' = Some v
bm:t A
H0:list_norepet (List.map fst ((k', v) :: l))
H:In (k', v) ((k', v) :: l)
H3:k' = k'
H1:(k', v) = (k', v)
H6:~ In k' (List.map fst l)
H7:list_norepet (List.map fst l)
(set k' v
   (fold_right
      (fun (p : positive * A) (a : t A) =>
       set (fst p) (snd p) a) bm l)) ! k' = Some v
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
e:k = k'
H1:In (k, v) l
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v auto with assocmap.
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
e:k = k'
H1:In (k, v) l
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v

          inversion H0; subst.
A:Type
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k', v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k' = Some v
bm:t A
H:In (k', v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
H1:In (k', v) l
H4:~ In k' (List.map fst l)
H5:list_norepet (List.map fst l)
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k' =
Some v apply in_map with (f:=fst) in H1.
A:Type
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k', v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k' = Some v
bm:t A
H:In (k', v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
H1:In (fst (k', v)) (List.map fst l)
H4:~ In k' (List.map fst l)
H5:list_norepet (List.map fst l)
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k' =
Some v contradiction.

        +
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v inversion H.
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
H1:(k', v') = (k, v)
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
H1:In (k, v) l
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v inversion H1.
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
H1:(k', v') = (k, v)
H3:k' = k
H4:v' = v
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k, v) :: l)) ! k =
Some v
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
H1:In (k, v) l
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v inversion H0.
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
H1:(k', v') = (k, v)
H3:k' = k
H4:v' = v
hd:elt
tl:list elt
H6:~ In k' (List.map fst l)
H7:list_norepet (List.map fst l)
H2:hd = k'
H5:tl = List.map fst l
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k, v) :: l)) ! k =
Some v
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
H1:In (k, v) l
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v subst.
A:Type
k:elt
v:A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H1:(k, v) = (k, v)
n:k <> k
H:In (k, v) ((k, v) :: l)
H0:list_norepet (List.map fst ((k, v) :: l))
H6:~ In k (List.map fst l)
H7:list_norepet (List.map fst l)
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k, v) :: l)) ! k =
Some v
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
H1:In (k, v) l
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v simpl.
A:Type
k:elt
v:A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H1:(k, v) = (k, v)
n:k <> k
H:In (k, v) ((k, v) :: l)
H0:list_norepet (List.map fst ((k, v) :: l))
H6:~ In k (List.map fst l)
H7:list_norepet (List.map fst l)
(set k v
   (fold_right
      (fun (p : positive * A) (a : t A) =>
       set (fst p) (snd p) a) bm l)) ! k = Some v
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
H1:In (k, v) l
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v rewrite gso; try assumption.
A:Type
k:elt
v:A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H1:(k, v) = (k, v)
n:k <> k
H:In (k, v) ((k, v) :: l)
H0:list_norepet (List.map fst ((k, v) :: l))
H6:~ In k (List.map fst l)
H7:list_norepet (List.map fst l)
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm l) ! k = Some v
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
H1:In (k, v) l
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v
          apply IHl.
A:Type
k:elt
v:A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H1:(k, v) = (k, v)
n:k <> k
H:In (k, v) ((k, v) :: l)
H0:list_norepet (List.map fst ((k, v) :: l))
H6:~ In k (List.map fst l)
H7:list_norepet (List.map fst l)
In (k, v) l
A:Type
k:elt
v:A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H1:(k, v) = (k, v)
n:k <> k
H:In (k, v) ((k, v) :: l)
H0:list_norepet (List.map fst ((k, v) :: l))
H6:~ In k (List.map fst l)
H7:list_norepet (List.map fst l)
list_norepet (List.map fst l)
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
H1:In (k, v) l
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v contradiction.
A:Type
k:elt
v:A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H1:(k, v) = (k, v)
n:k <> k
H:In (k, v) ((k, v) :: l)
H0:list_norepet (List.map fst ((k, v) :: l))
H6:~ In k (List.map fst l)
H7:list_norepet (List.map fst l)
list_norepet (List.map fst l)
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
H1:In (k, v) l
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v contradiction.
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
H1:In (k, v) l
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v
          simpl.
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
H1:In (k, v) l
(set k' v'
   (fold_right
      (fun (p : positive * A) (a : t A) =>
       set (fst p) (snd p) a) bm l)) ! k = Some v rewrite gso; try assumption.
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
H1:In (k, v) l
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm l) ! k = Some v apply IHl.
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
H1:In (k, v) l
In (k, v) l
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
H1:In (k, v) l
list_norepet (List.map fst l) assumption.
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
H1:In (k, v) l
list_norepet (List.map fst l) inversion H0.
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
H1:In (k, v) l
hd:elt
tl:list elt
H4:~ In k' (List.map fst l)
H5:list_norepet (List.map fst l)
H2:hd = k'
H3:tl = List.map fst l
list_norepet (List.map fst l) subst.
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
In (k, v) l ->
list_norepet (List.map fst l) ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:In (k, v) ((k', v') :: l)
H0:list_norepet (List.map fst ((k', v') :: l))
n:k <> k'
H1:In (k, v) l
H4:~ In k' (List.map fst l)
H5:list_norepet (List.map fst l)
list_norepet (List.map fst l) assumption.
    Qed.
    Hint Resolve add_assoc : assocmap.

    Lemma not_in_assoc :
      forall k v l bm,
      ~ List.In k (List.map (@fst elt A) l) ->
      @get A k bm = Some v ->
      get k (fold_right (fun p a => set (fst p) (snd p) a) bm l) = Some v.
A:Type
forall (k : elt) (v : A) (l : list (elt * A))
  (bm : t A),
~ In k (List.map fst l) ->
bm ! k = Some v ->
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm l) ! k = Some v
    Proof.
A:Type
forall (k : elt) (v : A) (l : list (elt * A))
  (bm : t A),
~ In k (List.map fst l) ->
bm ! k = Some v ->
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm l) ! k = Some v
      induction l; intros.
A:Type
k:elt
v:A
bm:t A
H:~ In k (List.map fst nil)
H0:bm ! k = Some v
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm nil) ! k = Some v
A:Type
k:elt
v:A
a:(elt * A)%type
l:list (elt * A)
IHl:forall bm : t A,
~ In k (List.map fst l) ->
bm ! k = Some v ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:~ In k (List.map fst (a :: l))
H0:bm ! k = Some v
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm (a :: l)) ! k = Some v
      -
A:Type
k:elt
v:A
bm:t A
H:~ In k (List.map fst nil)
H0:bm ! k = Some v
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm nil) ! k = Some v assumption.
      -
A:Type
k:elt
v:A
a:(elt * A)%type
l:list (elt * A)
IHl:forall bm : t A,
~ In k (List.map fst l) ->
bm ! k = Some v ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:~ In k (List.map fst (a :: l))
H0:bm ! k = Some v
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm (a :: l)) ! k = Some v destruct a as [k' v'].
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
~ In k (List.map fst l) ->
bm ! k = Some v ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:~ In k (List.map fst ((k', v') :: l))
H0:bm ! k = Some v
(fold_right
   (fun (p : positive * A) (a : t A) =>
    set (fst p) (snd p) a) bm ((k', v') :: l)) ! k =
Some v
        destruct (peq k k'); subst;
          simpl in *; apply Decidable.not_or in H; destruct H.
A:Type
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
~ In k' (List.map fst l) ->
bm ! k' = Some v ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k' = Some v
bm:t A
H0:bm ! k' = Some v
H:k' <> k'
H1:~ In k' (List.map fst l)
(set k' v'
   (fold_right
      (fun (p : positive * A) (a : t A) =>
       set (fst p) (snd p) a) bm l)) ! k' = Some v
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
~ In k (List.map fst l) ->
bm ! k = Some v ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:k' <> k
H1:~ In k (List.map fst l)
H0:bm ! k = Some v
n:k <> k'
(set k' v'
   (fold_right
      (fun (p : positive * A) (a : t A) =>
       set (fst p) (snd p) a) bm l)) ! k = Some v contradiction.
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forall bm : t A,
~ In k (List.map fst l) ->
bm ! k = Some v ->
(fold_right (fun (p : positive * A) (a : t A) => set (fst p) (snd p) a) bm l)
! k = Some v
bm:t A
H:k' <> k
H1:~ In k (List.map fst l)
H0:bm ! k = Some v
n:k <> k'
(set k' v'
   (fold_right
      (fun (p : positive * A) (a : t A) =>
       set (fst p) (snd p) a) bm l)) ! k = Some v
        rewrite AssocMap.gso; auto.
    Qed.
    Hint Resolve not_in_assoc : assocmap.

    Lemma elements_iff :
      forall am k,
      (exists v, get k am = Some v) <->
      List.In k (List.map (@fst _ A) (elements am)).
A:Type
forall (am : t A) (k : positive),
(exists v : A, am ! k = Some v) <->
In k (List.map fst (elements am))
    Proof.
A:Type
forall (am : t A) (k : positive),
(exists v : A, am ! k = Some v) <->
In k (List.map fst (elements am))
      split; intros.
A:Type
am:t A
k:positive
H:exists v : A, am ! k = Some v
In k (List.map fst (elements am))
A:Type
am:t A
k:positive
H:In k (List.map fst (elements am))
exists v : A, am ! k = Some v
      destruct H.
A:Type
am:t A
k:positive
x:A
H:am ! k = Some x
In k (List.map fst (elements am))
A:Type
am:t A
k:positive
H:In k (List.map fst (elements am))
exists v : A, am ! k = Some v apply elements_correct in H.
A:Type
am:t A
k:positive
x:A
H:In (k, x) (elements am)
In k (List.map fst (elements am))
A:Type
am:t A
k:positive
H:In k (List.map fst (elements am))
exists v : A, am ! k = Some v apply in_map with (f := fst) in H.
A:Type
am:t A
k:positive
x:A
H:In (fst (k, x)) (List.map fst (elements am))
In k (List.map fst (elements am))
A:Type
am:t A
k:positive
H:In k (List.map fst (elements am))
exists v : A, am ! k = Some v apply H.
A:Type
am:t A
k:positive
H:In k (List.map fst (elements am))
exists v : A, am ! k = Some v
      apply list_in_map_inv in H.
A:Type
am:t A
k:positive
H:exists x : positive * A,
  k = fst x /\ In x (elements am)
exists v : A, am ! k = Some v destruct H.
A:Type
am:t A
k:positive
x:(positive * A)%type
H:k = fst x /\ In x (elements am)
exists v : A, am ! k = Some v destruct H.
A:Type
am:t A
k:positive
x:(positive * A)%type
H:k = fst x
H0:In x (elements am)
exists v : A, am ! k = Some v subst.
A:Type
am:t A
x:(positive * A)%type
H0:In x (elements am)
exists v : A, am ! (fst x) = Some v
      exists (snd x).
A:Type
am:t A
x:(positive * A)%type
H0:In x (elements am)
am ! (fst x) = Some (snd x) apply elements_complete.
A:Type
am:t A
x:(positive * A)%type
H0:In x (elements am)
In (fst x, snd x) (elements am) assert (x = (fst x, snd x)) by apply surjective_pairing.
A:Type
am:t A
x:(positive * A)%type
H0:In x (elements am)
H:x = (fst x, snd x)
In (fst x, snd x) (elements am)
      rewrite H in H0; assumption.
    Qed.
    Hint Resolve elements_iff : assocmap.

    Lemma elements_correct' :
      forall am k,
      ~ (exists v, get k am = Some v) <->
      ~ List.In k (List.map (@fst _ A) (elements am)).
A:Type
forall (am : t A) (k : positive),
~ (exists v : A, am ! k = Some v) <->
~ In k (List.map fst (elements am))
    Proof.
A:Type
forall (am : t A) (k : positive),
~ (exists v : A, am ! k = Some v) <->
~ In k (List.map fst (elements am)) auto using not_iff_compat with assocmap. Qed.
    Hint Resolve elements_correct' : assocmap.

    Lemma elements_correct_none :
      forall am k,
      get k am = None ->
      ~ List.In k (List.map (@fst _ A) (elements am)).
A:Type
forall (am : t A) (k : positive),
am ! k = None -> ~ In k (List.map fst (elements am))
    Proof.
A:Type
forall (am : t A) (k : positive),
am ! k = None -> ~ In k (List.map fst (elements am))
      intros.
A:Type
am:t A
k:positive
H:am ! k = None
~ In k (List.map fst (elements am)) apply elements_correct'.
A:Type
am:t A
k:positive
H:am ! k = None
~ (exists v : A, am ! k = Some v) unfold not.
A:Type
am:t A
k:positive
H:am ! k = None
(exists v : A, am ! k = Some v) -> False intros.
A:Type
am:t A
k:positive
H:am ! k = None
H0:exists v : A, am ! k = Some v
False
      destruct H0.
A:Type
am:t A
k:positive
H:am ! k = None
x:A
H0:am ! k = Some x
False rewrite H in H0.
A:Type
am:t A
k:positive
H:am ! k = None
x:A
H0:None = Some x
False discriminate.
    Qed.
    Hint Resolve elements_correct_none : assocmap.

    Lemma merge_fold_add :
      forall k v am bm,
      am ! k = Some v ->
      (merge_fold am bm) ! k = Some v.
A:Type
forall (k : positive) (v : A) (am : PTree.t A)
  (bm : t A),
am ! k = Some v -> (merge_fold am bm) ! k = Some v
    Proof.
A:Type
forall (k : positive) (v : A) (am : PTree.t A)
  (bm : t A),
am ! k = Some v -> (merge_fold am bm) ! k = Some v unfold merge_fold; auto with assocmap. Qed.
    Hint Resolve merge_fold_add : assocmap.

    Lemma merge_fold_not_in :
      forall k v am bm,
      get k am = None ->
      get k bm = Some v ->
      get k (merge_fold am bm) = Some v.
A:Type
forall (k : positive) (v : A) (am bm : t A),
am ! k = None ->
bm ! k = Some v -> (merge_fold am bm) ! k = Some v
    Proof.
A:Type
forall (k : positive) (v : A) (am bm : t A),
am ! k = None ->
bm ! k = Some v -> (merge_fold am bm) ! k = Some v intros.
A:Type
k:positive
v:A
am, bm:t A
H:am ! k = None
H0:bm ! k = Some v
(merge_fold am bm) ! k = Some v apply not_in_assoc; auto with assocmap. Qed.
    Hint Resolve merge_fold_not_in : assocmap.

    Lemma merge_fold_base :
      forall am,
      merge_fold (empty A) am = am.
A:Type
forall am : t A, merge_fold (empty A) am = am
    Proof.
A:Type
forall am : t A, merge_fold (empty A) am = am auto. Qed.
    Hint Resolve merge_fold_base : assocmap.

  End Operations.

End AssocMapExt.
Import AssocMapExt.

Definition assocmap := AssocMap.t value.

Definition find_assocmap (n : nat) : reg -> assocmap -> value :=
  get_default value (ZToValue 0).

Definition empty_assocmap : assocmap := AssocMap.empty value.

Definition merge_assocmap : assocmap -> assocmap -> assocmap := merge value.

Ltac unfold_merge :=
  unfold merge_assocmap; try (repeat (rewrite merge_add_assoc));
  rewrite AssocMapExt.merge_base_1.

Declare Scope assocmap.
Notation "a ! b" := (AssocMap.get b a) (at level 1) : assocmap.
Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1) : assocmap.
Notation "a # b" := (find_assocmap 32 b a) (at level 1) : assocmap.
Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1) : assocmap.
Notation "a # b '<-' c" := (AssocMap.set b c a) (at level 1, b at next level) : assocmap.

Local Open Scope assocmap.
Lemma find_get_assocmap :
  forall assoc r v,
  assoc ! r = Some v ->
  assoc # r = v.
forall (assoc : AssocMap.t value) (r : positive)
  (v : value), assoc ! r = Some v -> assoc # r = v
Proof.
forall (assoc : AssocMap.t value) (r : positive)
  (v : value), assoc ! r = Some v -> assoc # r = v intros.
assoc:AssocMap.t value
r:positive
v:value
H:assoc ! r = Some v
assoc # r = v unfold find_assocmap, AssocMapExt.get_default.
assoc:AssocMap.t value
r:positive
v:value
H:assoc ! r = Some v
match assoc ! r with
| Some v => v
| None => ZToValue 0
end = v rewrite H.
assoc:AssocMap.t value
r:positive
v:value
H:assoc ! r = Some v
v = v trivial. Qed.