(* * 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.Definitionreg := positive.ModuleAssocMap := Maps.PTree.ModuleAssocMapExt.Import AssocMap.Hint Resolve elements_correct elements_complete
elements_keys_norepet : assocmap.Hint Resolve gso gss : assocmap.SectionOperations.VariableA : Type.Definitionget_default (a : A) (k : reg) (m : t A) : A :=
match get k m with
| None => a
| Some v => v
end.Fixpointmerge (m1m2 : 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.
A:Type
forallam : t A, merge (empty A) am = am
A:Type
forallam : t A, merge (empty A) am = am
auto.Qed.Hint Resolve merge_base_1 : assocmap.
A:Type
forallam : t A, merge am (empty A) = am
A:Type
forallam : t A, merge am (empty A) = am
A:Type
forallam : 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)
endend) am (empty A) = am
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)
endend) 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)
endend) 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)
endend) 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)
endend) am2 r2)
endend = Node am1 o am2
forall (ambm : t A) (k : positive) (v : A),
am ! k = None ->
bm ! k = Some v -> (merge am bm) ! k = Some v
A:Type
forall (ambm : 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;
tryrewrite gempty in H; trydiscriminate; tryassumption; auto.Qed.Hint Resolve merge_correct_2 : assocmap.Definitionmerge_fold (ambm : t A) : t A :=
fold_right (funpa => set (fst p) (snd p) a) bm (elements am).
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
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
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:forallbm : 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:forallbm : 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
k':elt
v':A
l:list (elt * A)
IHl:forallbm : 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
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forallbm : 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:forallbm : 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:forallbm : 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:forallbm : 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:forallbm : 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
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forallbm : 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:forallbm : 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
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forallbm : 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:forallbm : 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
A:Type
v:A
k':elt
l:list (elt * A)
IHl:forallbm : 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:forallbm : 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
A:Type
v:A
k':elt
l:list (elt * A)
IHl:forallbm : 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:forallbm : 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
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forallbm : 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
A:Type
v:A
k':elt
v':A
l:list (elt * A)
IHl:forallbm : 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
A:Type
v:A
k':elt
v':A
l:list (elt * A)
IHl:forallbm : 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:forallbm : 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:forallbm : 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:forallbm : 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
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forallbm : 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:forallbm : 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
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forallbm : 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:forallbm : 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
A:Type
k:elt
v:A
l:list (elt * A)
IHl:forallbm : 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:forallbm : 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
A:Type
k:elt
v:A
l:list (elt * A)
IHl:forallbm : 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:forallbm : 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
A:Type
k:elt
v:A
l:list (elt * A)
IHl:forallbm : 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:forallbm : 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
A:Type
k:elt
v:A
l:list (elt * A)
IHl:forallbm : 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:forallbm : 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:forallbm : 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
A:Type
k:elt
v:A
l:list (elt * A)
IHl:forallbm : 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:forallbm : 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
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forallbm : 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
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forallbm : 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
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forallbm : 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
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forallbm : 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:forallbm : 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)
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forallbm : 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)
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forallbm : 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)
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forallbm : 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.
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
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
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:forallbm : 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:forallbm : 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
k':elt
v':A
l:list (elt * A)
IHl:forallbm : 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
A:Type
v:A
k':elt
v':A
l:list (elt * A)
IHl:forallbm : 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:forallbm : 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
A:Type
k:elt
v:A
k':elt
v':A
l:list (elt * A)
IHl:forallbm : 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