Fil-C on Nix

Filnix wiki

the formal campaign

rocq/theories/Maps.v

Finite maps keyed by names, the model's counterpart of library(assoc), which ir.pl and cfg.pl use for every table indexed by a block label or a temporary.

The association lists of Term.v (lookup, put) take time linear in their length, and a function of a thousand blocks and twenty thousand temporaries asks them millions of questions. A name map hashes each name to an integer and keeps, under each hash, an association list of the names that share it. A lookup compares names with name_eqb within its bucket, so two names with one hash stay apart: the hash decides only speed, never an answer.

The buckets are kept in the stdlib's AVL tree keyed by integers, whose extracted lookups compare integers. A tree keyed by positives (FMapPositive) walks its key bit by bit, and each bit is a division of a zarith integer once extracted: the validator was thirty times slower with it.

From Stdlib Require Import String ZArith List Ascii OrderedTypeEx FMapAVL FMapFacts
From Nanofil Require Import Term
Import ListNotations
Open Scope Z_scope

The stdlib's AVL trees keyed by integers, which hold the buckets.

27Module ZMap ≔ FMapAVL.Make Z_as_OT

Hashing

The bound of every hash: hashes are the integers below 2^20.

32Definition hash_bound: Z ≔
2 ^ 20

One step of a hash: the hash h so far times 31, plus the next number x, modulo hash_bound.

36Definition hash_steph x : Z : Z ≔
h × 31 + x mod hash_bound

The hash of the string s, its character codes folded into the hash h by hash_step.

40Fixpoint string_hashs : string h : Z : Z ≔
match s with
EmptyString
⇒
h
Stringc s′
⇒
string_hashs′ hash_steph Z.of_NN_of_asciic

A hash of the ground term t, from its form (each of the four starts from its own seed) and its parts.

48Fixpoint term_hasht : term : Z ≔
let fix list_hash ts : listterm h : Z : Z ≔
match ts with
[ ]
⇒
h
t :: ts′
⇒
list_hashts′ hash_steph term_hasht
in
match t with
TIntn
⇒
hash_step1 n mod hash_bound
TAtoma
⇒
string_hasha 2
TAppf args
⇒
list_hashargs string_hashf 3
TListts
⇒
list_hashts 4

The key of the bucket a name n sits in: its term_hash.

62Definition name_keyn : name : Z ≔
term_hashn

Name maps

A name map from names to values of A: under each hash, the association list of the names with that hash and their values.

69Definition nmapA : Type : Type ≔
ZMap.tlistname × A

The map with no names, empty_assoc/1.

72Definition nm_emptyA : Type : nmapA ≔
ZMap.empty_

As get_assoc(Key, Assoc, V): the value of the name n in the map m, found in n's bucket by lookup, which compares names, not hashes.

77Definition nm_findA : Type n : name m : nmapA : optionA ≔
match ZMap.findname_keyn m with
Somebucket
⇒
lookupn bucket
None
⇒
None

As put_assoc(Key, Assoc0, V, Assoc): the map m with the name n now mapped to v.

85Definition nm_addA : Type n : name v : A m : nmapA : nmapA ≔
let k ≔ name_keyn in
let bucket ≔
match ZMap.findk m with
Someb
⇒
b
None
⇒
[ ]
in
ZMap.addk putn v bucket m

As del_assoc(Key, Assoc0, V, Assoc): the map m in which the name n no longer has a value.

92Definition nm_removeA : Type n : name m : nmapA : nmapA ≔
let k ≔ name_keyn in
match ZMap.findk m with
Somebucket
⇒
ZMap.addk filterλp ⇒ negbname_eqbn fstp bucket m
None
⇒
m

Whether the name n has a value in the map m.

100Definition nm_memA : Type n : name m : nmapA : bool ≔
match nm_findn m with
Some_
⇒
true
None
⇒
false

As list_to_assoc(Pairs, Assoc): the map of the pairs ps, for pairs whose keys differ (here a later pair would replace an earlier one; list_to_assoc/2 throws).

106Definition nm_of_listA : Type ps : listname × A : nmapA ≔
fold_leftλm p ⇒ nm_addfstp sndp m ps nm_empty

What a lookup answers

The lemmas below say what each operation does to a lookup, by name and not by hash: a map answers as the association list of its puts would.

The stdlib's facts about ZMap's lookups, for the proofs below.

116Module ZF ≔ FMapFacts.WFacts_fun Z_as_OT ZMap

Names a and b that name_eqb calls equal have the same name_key, so they share a bucket.

120Lemma name_key_eqb
∀ a b
name_eqba b = true
name_keya = name_keyb
Explore proof 4 tactics

Initial goal

⊢
∀a b : name, name_eqba b = true → name_keya = name_keyb

intros a b H

a, b :
name
H :
name_eqba b = true
⊢
name_keya = name_keyb

apply term_eqb_eq in H

a, b :
name
H :
a = b
⊢
name_keya = name_keyb

subst

b :
name
⊢
name_keyb = name_keyb

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros a b H
apply term_eqb_eq in H
subst
reflexivity

Looking up the name k after put n v answers v if k is n, and otherwise what the association list ps answered before.

125Lemma lookup_put_name
∀ A : Type k n v : A ps
lookupk putn v ps
=
name_eqbk n
→
Somev
else
lookupk ps
Explore proof 10 tactics

Initial goal

⊢
∀ A : Type k n : name v : A ps : listname × A  ,
lookupk putn v ps
=
name_eqbk n
→
Somev
else
lookupk ps

intros A k n v ps

A :
Type
k, n :
name
v :
A
ps :
listname × A
⊢
lookupk putn v ps
=
name_eqbk n
→
Somev
else
lookupk ps

simpl

A :
Type
k, n :
name
v :
A
ps :
listname × A
⊢
name_eqbk n
→
Somev
else
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps
=
name_eqbk n
→
Somev
else
lookupk ps

destruct name_eqbk n eqn: E ; reflexivity |

A :
Type
k, n :
name
v :
A
ps :
listname × A
E :
name_eqbk n = false
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps = lookupk ps

induction ps as | k′ v′ ps IH ; simpl ; reflexivity |

A :
Type
k, n :
name
v :
A
k′ :
name
v′ :
A
ps :
listname × A
E :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps = lookupk ps
⊢
lookupk
negbname_eqbn k′
→
k′, v′ :: filterλp : name × A ⇒ negbname_eqbn fstp ps
else
filterλp : name × A ⇒ negbname_eqbn fstp ps
=
name_eqbk k′
→
Somev′
else
lookupk ps

destruct name_eqbn k′ eqn: E′ ; simpl

2 open

A :
Type
k, n :
name
v :
A
k′ :
name
v′ :
A
ps :
listname × A
E :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps = lookupk ps
E′ :
name_eqbn k′ = true
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps
=
name_eqbk k′
→
Somev′
else
lookupk ps
focused goal
A :
Type
k, n :
name
v :
A
k′ :
name
v′ :
A
ps :
listname × A
E :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps = lookupk ps
E′ :
name_eqbn k′ = false
⊢
name_eqbk k′
→
Somev′
else
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps
=
name_eqbk k′
→
Somev′
else
lookupk ps

–apply term_eqb_eq in E′

2 open

A :
Type
k, n :
name
v :
A
k′ :
name
v′ :
A
ps :
listname × A
E :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps = lookupk ps
E′ :
n = k′
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps
=
name_eqbk k′
→
Somev′
else
lookupk ps
deferred goal
A :
Type
k, n :
name
v :
A
k′ :
name
v′ :
A
ps :
listname × A
E :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps = lookupk ps
E′ :
name_eqbn k′ = false
⊢
name_eqbk k′
→
Somev′
else
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps
=
name_eqbk k′
→
Somev′
else
lookupk ps

subst k′

2 open

A :
Type
k, n :
name
v, v′ :
A
ps :
listname × A
E :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps = lookupk ps
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps
=
name_eqbk n
→
Somev′
else
lookupk ps
deferred goal
A :
Type
k, n :
name
v :
A
k′ :
name
v′ :
A
ps :
listname × A
E :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps = lookupk ps
E′ :
name_eqbn k′ = false
⊢
name_eqbk k′
→
Somev′
else
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps
=
name_eqbk k′
→
Somev′
else
lookupk ps

rewrite E

2 open

A :
Type
k, n :
name
v, v′ :
A
ps :
listname × A
E :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps = lookupk ps
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps = lookupk ps
deferred goal
A :
Type
k, n :
name
v :
A
k′ :
name
v′ :
A
ps :
listname × A
E :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps = lookupk ps
E′ :
name_eqbn k′ = false
⊢
name_eqbk k′
→
Somev′
else
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps
=
name_eqbk k′
→
Somev′
else
lookupk ps

exact IH

deferred goal
A :
Type
k, n :
name
v :
A
k′ :
name
v′ :
A
ps :
listname × A
E :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps = lookupk ps
E′ :
name_eqbn k′ = false
⊢
name_eqbk k′
→
Somev′
else
lookupk filterλp : name × A ⇒ negbname_eqbn fstp ps
=
name_eqbk k′
→
Somev′
else
lookupk ps

–destruct name_eqbk k′ ; reflexivity | exact IH

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros A k n v ps
simpl
destruct name_eqbk n eqn: E ; reflexivity |
induction ps as | k′ v′ ps IH ; simpl ; reflexivity |
destruct name_eqbn k′ eqn: E′ ; simpl
–apply term_eqb_eq in E′
subst k′
rewrite E
exact IH
–destruct name_eqbk k′ ; reflexivity | exact IH

The empty map has no value for any name k.

136Lemma nm_find_empty
∀ A : Type k
nm_findk @nm_emptyA = None
Explore proof 4 tactics

Initial goal

⊢
∀A : Type k : name, nm_findk nm_empty = None

intros A k

A :
Type
k :
name
⊢
nm_findk nm_empty = None

unfold nm_find , nm_empty

A :
Type
k :
name
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.emptylistname × A with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
None

rewrite ZF.empty_o

A :
Type
k :
name
⊢
None = None

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros A k
unfold nm_find , nm_empty
rewrite ZF.empty_o
reflexivity

After nm_add n v, the map answers v for the name n and what it answered before for every other name k: a shared hash never shows.

142Lemma nm_find_add
∀ A : Type k n v : A m
nm_findk nm_addn v m
=
name_eqbk n
→
Somev
else
nm_findk m
Explore proof 15 tactics

Initial goal

⊢
∀ A : Type k n : name v : A m : nmapA  ,
nm_findk nm_addn v m
=
name_eqbk n
→
Somev
else
nm_findk m

intros A k n v m

A :
Type
k, n :
name
v :
A
m :
nmapA
⊢
nm_findk nm_addn v m
=
name_eqbk n
→
Somev
else
nm_findk m

unfold nm_find , nm_add

A :
Type
k, n :
name
v :
A
m :
nmapA
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn putn v match ZMap.findelt ≔ listname × A name_keyn m with Someb ⇒ b | None ⇒ [ ] end m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
Somev
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

destruct Z.eq_decname_keyn name_keyk as E | E

2 open

A :
Type
k, n :
name
v :
A
m :
nmapA
E :
name_keyn = name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn putn v match ZMap.findelt ≔ listname × A name_keyn m with Someb ⇒ b | None ⇒ [ ] end m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
Somev
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
focused goal
A :
Type
k, n :
name
v :
A
m :
nmapA
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn putn v match ZMap.findelt ≔ listname × A name_keyn m with Someb ⇒ b | None ⇒ [ ] end m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
Somev
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

–rewrite ZF.add_eq_o by exact E

2 open

A :
Type
k, n :
name
v :
A
m :
nmapA
E :
name_keyn = name_keyk
⊢
lookupk
putn v
match ZMap.findelt ≔ listname × A name_keyn m with
Someb
⇒
b
None
⇒
[ ]
=
name_eqbk n
→
Somev
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
deferred goal
A :
Type
k, n :
name
v :
A
m :
nmapA
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn putn v match ZMap.findelt ≔ listname × A name_keyn m with Someb ⇒ b | None ⇒ [ ] end m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
Somev
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

rewrite lookup_put_name

2 open

A :
Type
k, n :
name
v :
A
m :
nmapA
E :
name_keyn = name_keyk
⊢
name_eqbk n
→
Somev
else
lookupk
match ZMap.findelt ≔ listname × A name_keyn m with
Someb
⇒
b
None
⇒
[ ]
=
name_eqbk n
→
Somev
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
deferred goal
A :
Type
k, n :
name
v :
A
m :
nmapA
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn putn v match ZMap.findelt ≔ listname × A name_keyn m with Someb ⇒ b | None ⇒ [ ] end m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
Somev
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

destruct name_eqbk n eqn: Ek ; reflexivity |

2 open

A :
Type
k, n :
name
v :
A
m :
nmapA
E :
name_keyn = name_keyk
Ek :
name_eqbk n = false
⊢
lookupk
match ZMap.findelt ≔ listname × A name_keyn m with
Someb
⇒
b
None
⇒
[ ]
=
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
deferred goal
A :
Type
k, n :
name
v :
A
m :
nmapA
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn putn v match ZMap.findelt ≔ listname × A name_keyn m with Someb ⇒ b | None ⇒ [ ] end m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
Somev
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

rewrite <- E

2 open

A :
Type
k, n :
name
v :
A
m :
nmapA
E :
name_keyn = name_keyk
Ek :
name_eqbk n = false
⊢
lookupk
match ZMap.findelt ≔ listname × A name_keyn m with
Someb
⇒
b
None
⇒
[ ]
=
match ZMap.findelt ≔ listname × A name_keyn m with
Somebucket
⇒
lookupk bucket
None
⇒
None
deferred goal
A :
Type
k, n :
name
v :
A
m :
nmapA
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn putn v match ZMap.findelt ≔ listname × A name_keyn m with Someb ⇒ b | None ⇒ [ ] end m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
Somev
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

destruct ZMap.findname_keyn m ; reflexivity

deferred goal
A :
Type
k, n :
name
v :
A
m :
nmapA
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn putn v match ZMap.findelt ≔ listname × A name_keyn m with Someb ⇒ b | None ⇒ [ ] end m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
Somev
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

–rewrite ZF.add_neq_o by exact E

A :
Type
k, n :
name
v :
A
m :
nmapA
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
Somev
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

destruct name_eqbk n eqn: Ek ; | reflexivity

A :
Type
k, n :
name
v :
A
m :
nmapA
E :
name_keyn ≠ name_keyk
Ek :
name_eqbk n = true
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
Somev

exfalso

A :
Type
k, n :
name
v :
A
m :
nmapA
E :
name_keyn ≠ name_keyk
Ek :
name_eqbk n = true
⊢
False

apply E

A :
Type
k, n :
name
v :
A
m :
nmapA
E :
name_keyn ≠ name_keyk
Ek :
name_eqbk n = true
⊢
name_keyn = name_keyk

symmetry

A :
Type
k, n :
name
v :
A
m :
nmapA
E :
name_keyn ≠ name_keyk
Ek :
name_eqbk n = true
⊢
name_keyk = name_keyn

apply name_key_eqb

A :
Type
k, n :
name
v :
A
m :
nmapA
E :
name_keyn ≠ name_keyk
Ek :
name_eqbk n = true
⊢
name_eqbk n = true

exact Ek

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros A k n v m
unfold nm_find , nm_add
destruct Z.eq_decname_keyn name_keyk as E | E
–rewrite ZF.add_eq_o by exact E
rewrite lookup_put_name
destruct name_eqbk n eqn: Ek ; reflexivity |
rewrite <- E
destruct ZMap.findname_keyn m ; reflexivity
–rewrite ZF.add_neq_o by exact E
destruct name_eqbk n eqn: Ek ; | reflexivity
exfalso
apply E
symmetry
apply name_key_eqb
exact Ek

After nm_remove n, the map has no value for the name n and its old value for every other name k.

156Lemma nm_find_remove
∀ A : Type k n m : nmapA
nm_findk nm_removen m
=
name_eqbk n
→
None
else
nm_findk m
Explore proof 34 tactics

Initial goal

⊢
∀ A : Type k n : name m : nmapA  ,
nm_findk nm_removen m
=
name_eqbk n
→
None
else
nm_findk m

intros A k n m

A :
Type
k, n :
name
m :
nmapA
⊢
nm_findk nm_removen m
=
name_eqbk n
→
None
else
nm_findk m

unfold nm_find , nm_remove

A :
Type
k, n :
name
m :
nmapA
⊢
match ZMap.findelt ≔ listname × A name_keyk match ZMap.findelt ≔ listname × A name_keyn m with Somebucket ⇒ ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m | None ⇒ m end with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

destruct ZMap.findname_keyn m as bucket | eqn: Eb

2 open

A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
focused goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

–destruct Z.eq_decname_keyn name_keyk as E | E

3 open

A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn = name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
focused goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

+rewrite ZF.add_eq_o by exact E

3 open

A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn = name_keyk
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp bucket
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

rewrite <- E , Eb

3 open

A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn = name_keyk
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp bucket
=
name_eqbk n
→
None
else
lookupk bucket
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

destruct name_eqbk n eqn: Ek

4 open

A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn = name_keyk
Ek :
name_eqbk n = true
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp bucket = None
focused goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn = name_keyk
Ek :
name_eqbk n = false
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp bucket = lookupk bucket
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

∗apply term_eqb_eq in Ek

4 open

A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn = name_keyk
Ek :
k = n
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp bucket = None
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn = name_keyk
Ek :
name_eqbk n = false
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp bucket = lookupk bucket
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

subst k

4 open

A :
Type
n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn = name_keyn
⊢
lookupn filterλp : name × A ⇒ negbname_eqbn fstp bucket = None
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn = name_keyk
Ek :
name_eqbk n = false
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp bucket = lookupk bucket
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

clear Eb E

4 open

A :
Type
n :
name
m :
nmapA
bucket :
listname × A
⊢
lookupn filterλp : name × A ⇒ negbname_eqbn fstp bucket = None
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn = name_keyk
Ek :
name_eqbk n = false
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp bucket = lookupk bucket
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

induction bucket as | k′ v′ b IH ; simpl ; reflexivity |

4 open

A :
Type
n :
name
m :
nmapA
k′ :
name
v′ :
A
b :
listname × A
IH :
lookupn filterλp : name × A ⇒ negbname_eqbn fstp b = None
⊢
lookupn
negbname_eqbn k′
→
k′, v′ :: filterλp : name × A ⇒ negbname_eqbn fstp b
else
filterλp : name × A ⇒ negbname_eqbn fstp b
=
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn = name_keyk
Ek :
name_eqbk n = false
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp bucket = lookupk bucket
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

destruct name_eqbn k′ eqn: E′ ; simpl ; exact IH |

4 open

A :
Type
n :
name
m :
nmapA
k′ :
name
v′ :
A
b :
listname × A
IH :
lookupn filterλp : name × A ⇒ negbname_eqbn fstp b = None
E′ :
name_eqbn k′ = false
⊢
name_eqbn k′
→
Somev′
else
lookupn filterλp : name × A ⇒ negbname_eqbn fstp b
=
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn = name_keyk
Ek :
name_eqbk n = false
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp bucket = lookupk bucket
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

rewrite E′

4 open

A :
Type
n :
name
m :
nmapA
k′ :
name
v′ :
A
b :
listname × A
IH :
lookupn filterλp : name × A ⇒ negbname_eqbn fstp b = None
E′ :
name_eqbn k′ = false
⊢
lookupn filterλp : name × A ⇒ negbname_eqbn fstp b = None
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn = name_keyk
Ek :
name_eqbk n = false
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp bucket = lookupk bucket
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

exact IH

3 open

deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn = name_keyk
Ek :
name_eqbk n = false
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp bucket = lookupk bucket
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

∗clear Eb E

3 open

A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Ek :
name_eqbk n = false
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp bucket = lookupk bucket
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

induction bucket as | k′ v′ b IH ; simpl ; reflexivity |

3 open

A :
Type
k, n :
name
m :
nmapA
k′ :
name
v′ :
A
b :
listname × A
Ek :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp b = lookupk b
⊢
lookupk
negbname_eqbn k′
→
k′, v′ :: filterλp : name × A ⇒ negbname_eqbn fstp b
else
filterλp : name × A ⇒ negbname_eqbn fstp b
=
name_eqbk k′
→
Somev′
else
lookupk b
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

destruct name_eqbn k′ eqn: E′ ; simpl

4 open

A :
Type
k, n :
name
m :
nmapA
k′ :
name
v′ :
A
b :
listname × A
Ek :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp b = lookupk b
E′ :
name_eqbn k′ = true
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp b
=
name_eqbk k′
→
Somev′
else
lookupk b
focused goal
A :
Type
k, n :
name
m :
nmapA
k′ :
name
v′ :
A
b :
listname × A
Ek :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp b = lookupk b
E′ :
name_eqbn k′ = false
⊢
name_eqbk k′
→
Somev′
else
lookupk filterλp : name × A ⇒ negbname_eqbn fstp b
=
name_eqbk k′
→
Somev′
else
lookupk b
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

--apply term_eqb_eq in E′

4 open

A :
Type
k, n :
name
m :
nmapA
k′ :
name
v′ :
A
b :
listname × A
Ek :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp b = lookupk b
E′ :
n = k′
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp b
=
name_eqbk k′
→
Somev′
else
lookupk b
deferred goal
A :
Type
k, n :
name
m :
nmapA
k′ :
name
v′ :
A
b :
listname × A
Ek :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp b = lookupk b
E′ :
name_eqbn k′ = false
⊢
name_eqbk k′
→
Somev′
else
lookupk filterλp : name × A ⇒ negbname_eqbn fstp b
=
name_eqbk k′
→
Somev′
else
lookupk b
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

subst k′

4 open

A :
Type
k, n :
name
m :
nmapA
v′ :
A
b :
listname × A
Ek :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp b = lookupk b
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp b
=
name_eqbk n
→
Somev′
else
lookupk b
deferred goal
A :
Type
k, n :
name
m :
nmapA
k′ :
name
v′ :
A
b :
listname × A
Ek :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp b = lookupk b
E′ :
name_eqbn k′ = false
⊢
name_eqbk k′
→
Somev′
else
lookupk filterλp : name × A ⇒ negbname_eqbn fstp b
=
name_eqbk k′
→
Somev′
else
lookupk b
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

rewrite Ek

4 open

A :
Type
k, n :
name
m :
nmapA
v′ :
A
b :
listname × A
Ek :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp b = lookupk b
⊢
lookupk filterλp : name × A ⇒ negbname_eqbn fstp b = lookupk b
deferred goal
A :
Type
k, n :
name
m :
nmapA
k′ :
name
v′ :
A
b :
listname × A
Ek :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp b = lookupk b
E′ :
name_eqbn k′ = false
⊢
name_eqbk k′
→
Somev′
else
lookupk filterλp : name × A ⇒ negbname_eqbn fstp b
=
name_eqbk k′
→
Somev′
else
lookupk b
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

exact IH

3 open

deferred goal
A :
Type
k, n :
name
m :
nmapA
k′ :
name
v′ :
A
b :
listname × A
Ek :
name_eqbk n = false
IH :
lookupk filterλp : name × A ⇒ negbname_eqbn fstp b = lookupk b
E′ :
name_eqbn k′ = false
⊢
name_eqbk k′
→
Somev′
else
lookupk filterλp : name × A ⇒ negbname_eqbn fstp b
=
name_eqbk k′
→
Somev′
else
lookupk b
deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

--destruct name_eqbk k′ ; reflexivity | exact IH

2 open

deferred goal
A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk ZMap.addname_keyn filterλp : name × A ⇒ negbname_eqbn fstp bucket m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

+rewrite ZF.add_neq_o by exact E

2 open

A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

destruct name_eqbk n eqn: Ek ; | reflexivity

2 open

A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
Ek :
name_eqbk n = true
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket0
⇒
lookupk bucket0
None
⇒
None
=
None
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

exfalso

2 open

A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
Ek :
name_eqbk n = true
⊢
False
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

apply E

2 open

A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
Ek :
name_eqbk n = true
⊢
name_keyn = name_keyk
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

symmetry

2 open

A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
Ek :
name_eqbk n = true
⊢
name_keyk = name_keyn
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

apply name_key_eqb

2 open

A :
Type
k, n :
name
m :
nmapA
bucket :
listname × A
Eb :
ZMap.findelt ≔ listname × A name_keyn m = Somebucket
E :
name_keyn ≠ name_keyk
Ek :
name_eqbk n = true
⊢
name_eqbk n = true
deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

exact Ek

deferred goal
A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
name_eqbk n
→
None
else
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None

–destruct name_eqbk n eqn: Ek ; | reflexivity

A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
Ek :
name_eqbk n = true
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
None

apply term_eqb_eq in Ek

A :
Type
k, n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
Ek :
k = n
⊢
match ZMap.findelt ≔ listname × A name_keyk m with
Somebucket
⇒
lookupk bucket
None
⇒
None
=
None

subst k

A :
Type
n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
match ZMap.findelt ≔ listname × A name_keyn m with
Somebucket
⇒
lookupn bucket
None
⇒
None
=
None

rewrite Eb

A :
Type
n :
name
m :
nmapA
Eb :
ZMap.findelt ≔ listname × A name_keyn m = None
⊢
None = None

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros A k n m
unfold nm_find , nm_remove
destruct ZMap.findname_keyn m as bucket | eqn: Eb
–destruct Z.eq_decname_keyn name_keyk as E | E
+rewrite ZF.add_eq_o by exact E
rewrite <- E , Eb
destruct name_eqbk n eqn: Ek
∗apply term_eqb_eq in Ek
subst k
clear Eb E
induction bucket as | k′ v′ b IH ; simpl ; reflexivity |
destruct name_eqbn k′ eqn: E′ ; simpl ; exact IH |
rewrite E′
exact IH
∗clear Eb E
induction bucket as | k′ v′ b IH ; simpl ; reflexivity |
destruct name_eqbn k′ eqn: E′ ; simpl
--apply term_eqb_eq in E′
subst k′
rewrite Ek
exact IH
--destruct name_eqbk k′ ; reflexivity | exact IH
+rewrite ZF.add_neq_o by exact E
destruct name_eqbk n eqn: Ek ; | reflexivity
exfalso
apply E
symmetry
apply name_key_eqb
exact Ek
–destruct name_eqbk n eqn: Ek ; | reflexivity
apply term_eqb_eq in Ek
subst k
rewrite Eb
reflexivity

A name k has a value after adding the name n exactly when k is n or it had one already.

178Lemma nm_mem_add
∀ A : Type k n v : A m
nm_memk nm_addn v m = name_eqbk n || nm_memk m
Explore proof 4 tactics

Initial goal

⊢
∀A : Type k n : name v : A m : nmapA, nm_memk nm_addn v m = name_eqbk n || nm_memk m

intros A k n v m

A :
Type
k, n :
name
v :
A
m :
nmapA
⊢
nm_memk nm_addn v m = name_eqbk n || nm_memk m

unfold nm_mem

A :
Type
k, n :
name
v :
A
m :
nmapA
⊢
match nm_findk nm_addn v m with
Some_
⇒
true
None
⇒
false
=
name_eqbk n
||
match nm_findk m with
Some_
⇒
true
None
⇒
false

rewrite nm_find_add

A :
Type
k, n :
name
v :
A
m :
nmapA
⊢
match if name_eqbk n then Somev else nm_findk m with
Some_
⇒
true
None
⇒
false
=
name_eqbk n
||
match nm_findk m with
Some_
⇒
true
None
⇒
false

destruct name_eqbk n ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros A k n v m
unfold nm_mem
rewrite nm_find_add
destruct name_eqbk n ; reflexivity

A lookup of k in two association lists joined, ps then qs, answers from ps if k is there, and otherwise from qs.

184Lemma lookup_app
∀ A : Type k ps qs : listname × A
lookupk ps ++ qs
=
match lookupk ps with
Somev
⇒
Somev
None
⇒
lookupk qs
Explore proof 3 tactics

Initial goal

⊢
∀ A : Type k : name ps qs : listname × A  ,
lookupk ps ++ qs
=
match lookupk ps with
Somev
⇒
Somev
None
⇒
lookupk qs

intros A k ps qs

A :
Type
k :
name
ps, qs :
listname × A
⊢
lookupk ps ++ qs
=
match lookupk ps with
Somev
⇒
Somev
None
⇒
lookupk qs

induction ps as | k′ v′ ps IH ; simpl ; reflexivity |

A :
Type
k, k′ :
name
v′ :
A
ps, qs :
listname × A
IH :
lookupk ps ++ qs
=
match lookupk ps with
Somev
⇒
Somev
None
⇒
lookupk qs
⊢
name_eqbk k′
→
Somev′
else
lookupk ps ++ qs
=
match if name_eqbk k′ then Somev′ else lookupk ps with
Somev
⇒
Somev
None
⇒
lookupk qs

destruct name_eqbk k′ ; reflexivity | exact IH

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros A k ps qs
induction ps as | k′ v′ ps IH ; simpl ; reflexivity |
destruct name_eqbk k′ ; reflexivity | exact IH

Adding the pairs ps to a map m one by one, as nm_of_list does from the empty map, a later pair replaces an earlier one: a lookup of k answers as the reversed list does, and falls back to m.

194Lemma nm_find_fold_add
∀ A : Type k ps : listname × A m
nm_findk fold_leftλm p ⇒ nm_addfstp sndp m ps m
=
match lookupk revps with
Somev
⇒
Somev
None
⇒
nm_findk m
Explore proof 6 tactics

Initial goal

⊢
∀ A : Type k : name ps : listname × A m : nmapA  ,
nm_findk fold_leftλm0 : nmapA p : name × A ⇒ nm_addfstp sndp m0 ps m
=
match lookupk revps with
Somev
⇒
Somev
None
⇒
nm_findk m

intros A k ps

A :
Type
k :
name
ps :
listname × A
⊢
∀ m : nmapA  ,
nm_findk fold_leftλm0 : nmapA p : name × A ⇒ nm_addfstp sndp m0 ps m
=
match lookupk revps with
Somev
⇒
Somev
None
⇒
nm_findk m

induction ps as | k′ v′ ps IH ; intros m ; simpl ; reflexivity |

A :
Type
k, k′ :
name
v′ :
A
ps :
listname × A
IH :
∀ m : nmapA  ,
nm_findk fold_leftλm0 : nmapA p : name × A ⇒ nm_addfstp sndp m0 ps m
=
match lookupk revps with
Somev
⇒
Somev
None
⇒
nm_findk m
m :
nmapA
⊢
nm_findk fold_leftλm0 : nmapA p : name × A ⇒ nm_addfstp sndp m0 ps nm_addk′ v′ m
=
match lookupk revps ++ k′, v′ with
Somev
⇒
Somev
None
⇒
nm_findk m

rewrite IH , lookup_app , nm_find_add

A :
Type
k, k′ :
name
v′ :
A
ps :
listname × A
IH :
∀ m : nmapA  ,
nm_findk fold_leftλm0 : nmapA p : name × A ⇒ nm_addfstp sndp m0 ps m
=
match lookupk revps with
Somev
⇒
Somev
None
⇒
nm_findk m
m :
nmapA
⊢
match lookupk revps with
Somev
⇒
Somev
None
⇒
name_eqbk k′
→
Somev′
else
nm_findk m
=
match match lookupk revps with Somev ⇒ Somev | None ⇒ lookupk k′, v′ end with
Somev
⇒
Somev
None
⇒
nm_findk m

simpl

A :
Type
k, k′ :
name
v′ :
A
ps :
listname × A
IH :
∀ m : nmapA  ,
nm_findk fold_leftλm0 : nmapA p : name × A ⇒ nm_addfstp sndp m0 ps m
=
match lookupk revps with
Somev
⇒
Somev
None
⇒
nm_findk m
m :
nmapA
⊢
match lookupk revps with
Somev
⇒
Somev
None
⇒
name_eqbk k′
→
Somev′
else
nm_findk m
=
match match lookupk revps with Somev ⇒ Somev | None ⇒ if name_eqbk k′ then Somev′ else None end with
Somev
⇒
Somev
None
⇒
nm_findk m

destruct lookupk revps ; reflexivity |

A :
Type
k, k′ :
name
v′ :
A
ps :
listname × A
IH :
∀m : nmapA, nm_findk fold_leftλm0 : nmapA p : name × A ⇒ nm_addfstp sndp m0 ps m = nm_findk m
m :
nmapA
⊢
name_eqbk k′
→
Somev′
else
nm_findk m
=
match if name_eqbk k′ then Somev′ else None with
Somev
⇒
Somev
None
⇒
nm_findk m

destruct name_eqbk k′ ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros A k ps
induction ps as | k′ v′ ps IH ; intros m ; simpl ; reflexivity |
rewrite IH , lookup_app , nm_find_add
simpl
destruct lookupk revps ; reflexivity |
destruct name_eqbk k′ ; reflexivity