## Stream: new members

### Topic: Understanding Alist

#### Scott Viteri (Nov 13 2019 at 19:18):

https://github.com/leanprover-community/mathlib/blob/c28497fa056ae52b93aa9aca2fd20155d57fa016/src/data/list/alist.lean#L16 says that alist should have unique keys, but it in not clear to me how this is enforced. The alist.nodupkeys descructor is austensibly a proof that the keys are duplicated, but would this proof make more sense as a constuctor?

#### Scott Viteri (Nov 13 2019 at 19:23):

For example,  #reduce alist.keys (list.to_alist [{2,3}, {4,2}, {2,4}]) gives list.map sigma.fst (list.erase_dupkeys._match_1 {2, 3} (list.erase_dupkeys._match_1 {4, 2} (list.erase_dupkeys._match_1 {2, 4} list.nil))) , and #reduce (list.to_alist [{2,3}, {4,2}, {2,4}]).nodupkeys triggers a memory consumption error (emacs).

#### Marc Huisinga (Nov 13 2019 at 19:24):

in order to create an alist you need to provide an element of entries.nodupkeys, which is a proof that there are no duplicate keys

#### Marc Huisinga (Nov 13 2019 at 19:25):

to_alist ensures this by calling erase_dupkeys, which removes all duplicates from the input

#### Bryan Gin-ge Chen (Nov 13 2019 at 19:26):

The structure syntax is a helper for defining inductive types with a single constructor (TPiL section). As Marc says, to construct an alist, you must supply both entries and nodupkeys.

#### Rob Lewis (Nov 13 2019 at 19:26):

By the way, unless you know what you're doing, you probably want to use #eval instead of #reduce for this kind of experimenting.

#### Scott Viteri (Nov 13 2019 at 19:31):

By the way, unless you know what you're doing, you probably want to use #eval instead of #reduce for this kind of experimenting.

Ok, I'll use #eval

#### Scott Viteri (Nov 13 2019 at 19:34):

So suppose I were to omit using nodupkeys_erase_dupkeys in list.to_alist.
Then why does #check (alist.mk [{2,3}, {4,2}, {2,4}] _).nodupkeys typecheck?

#### Scott Viteri (Nov 13 2019 at 19:36):

My understanding is that by using _ I am inferring a proof, which in this case should not exist.
Maybe the distinction is that running eval on this expressions produces don't know how to synthesize placeholder.

#### Scott Viteri (Nov 13 2019 at 19:39):

The structure syntax is a helper for defining inductive types with a single constructor (TPiL section). As Marc says, to construct an alist, you must supply both entries and nodupkeys.

My bad, nodupkeys is in fact a constructor here, thanks.

#### Rob Lewis (Nov 13 2019 at 19:49):

So suppose I were to omit using nodupkeys_erase_dupkeys in list.to_alist.
Then why does #check (alist.mk [{2,3}, {4,2}, {2,4}] _).nodupkeys typecheck?

If you look at the output of #check you'll see a metavariable (?M_1 or something). #check is displaying what the type would be, assuming you were to fill in all the placeholders that couldn't be filled in automatically.

#### Marc Huisinga (Nov 13 2019 at 19:53):

if you do this in regular code, you'll get don't know how to synthesize placeholder.
e.g.

abbreviation f : ℕ → Type := λ n, ℕ
def xs : list (sigma f) := [⟨2,3⟩, ⟨4,2⟩, ⟨2,4⟩]
def foo : alist f := alist.mk xs _


#### Kevin Buzzard (Nov 13 2019 at 19:56):

So suppose I were to omit using nodupkeys_erase_dupkeys in list.to_alist.
Then why does #check (alist.mk [{2,3}, {4,2}, {2,4}] _).nodupkeys typecheck?

#check _ : 0 = 1 typechecks.

#### Marc Huisinga (Nov 13 2019 at 20:08):

My bad, nodupkeys is in fact a constructor here, thanks.

structures only have a single constructor mk. a value/proof of entries.nodupkeys is a parameter to that constructor, not a constructor of alist itself. one might also call it a projection ;)

#### Scott Viteri (Nov 13 2019 at 21:53):

This all makes sense. When I actually go to fill in the proof in the first place, I get the following error:

example : list.nodupkeys [sigma.mk 1 3, sigma.mk 2 4] :=
begin
simp, exact eq.mp (ne.def 1 2) (nat.succ_ne_self 1).symm
end

tactic failed, result contains meta-variables
state: no goals


#### Scott Viteri (Nov 13 2019 at 21:56):

I think I read somewhere that simp should only be used in a finishing position but it seems that my alternative is a to use a long string of rewrites. Is this preferable?

#### Rob Lewis (Nov 13 2019 at 22:08):

The problem here is that Lean isn't inferring the type of sigma.mk 1 3. It's of type sigma f where f : nat -> Type where f 1 = nat and f 2 = nat, but that's not enough to know f is the constant function.

#### Rob Lewis (Nov 13 2019 at 22:09):

example : list.nodupkeys [(sigma.mk 1 3 : sigma (λ _, ℕ)), sigma.mk 2 4] :=
begin
simp, exact eq.mp (ne.def 1 2) (nat.succ_ne_self 1).symm
end


#### Scott Viteri (Nov 13 2019 at 22:18):

Great, I now have a working toy example:

#eval alist.keys (alist.mk [(sigma.mk 1 3 : sigma (λ _, ℕ)), sigma.mk 2 4]
(by {simp; exact eq.mp (ne.def 1 2) (nat.succ_ne_self 1).symm}))


produces [1,2]

#### Scott Viteri (Nov 13 2019 at 22:28):

The following also works

#eval (alist.keys (alist.mk [(sigma.mk 1 [1] : sigma (λ _, list ℕ)), sigma.mk 2 [4,5]]
(by {simp; exact eq.mp (ne.def 1 2) (nat.succ_ne_self 1).symm})))


So now my question is the following:
I plan on using assoc lists with natural numbers in the sigma.fst spot.
Is there a tactic that I can use that will take care of disequality proofs between nats when I first define an alist?

#### Mario Carneiro (Nov 13 2019 at 22:49):

You can try dec_trivial

#### Rob Lewis (Nov 13 2019 at 23:16):

For proving specific disequalities like 1 ≠ 2 you can use norm_num.

#### Scott Viteri (Nov 13 2019 at 23:18):

 failed to synthesize type class instance for |- decidable (list.nodupkeys [<1,3>,<2,4>])
I think this means that I need to provide information that checking if for key duplicates is a decidable proposition.
dec_trivial points to of_as_true, which implicitly asks for a decidable proposition. Should I somehow provide decidable_eq nat to @of_as_true?

#### Scott Viteri (Nov 13 2019 at 23:23):

For proving specific disequalities like 1 ≠ 2 you can use norm_num.

#eval (alist.keys (alist.mk [(sigma.mk 1 [3] : sigma (λ _,list ℕ)), sigma.mk 2 [4]] (by norm_num)))
Woohoo!

#### Scott Viteri (Nov 13 2019 at 23:27):

But somehow not in this form??:

def a : list (sigma (λ _, list ℕ)) := [sigma.mk 1 [3], sigma.mk 2 [4]]
#eval (alist.keys (alist.mk a (by norm_num)))


What kind of witchcraft is this?

#### Scott Viteri (Nov 13 2019 at 23:32):

But somehow not in this form??:

def a : list (sigma (λ _, list ℕ)) := [sigma.mk 1 [3], sigma.mk 2 [4]]
#eval (alist.keys (alist.mk a (by norm_num)))

What kind of witchcraft is this?


Nevermind, this works:

def a : list (sigma (λ _, list ℕ)) := [sigma.mk 1 [3], sigma.mk 2 [4]]
#eval (alist.keys (alist.mk a (by rw a; norm_num)))


#### Mario Carneiro (Nov 13 2019 at 23:37):

failed to synthesize type class instance for |- decidable (list.nodupkeys [<1,3>,<2,4>])
I think this means that I need to provide information that checking if for key duplicates is a decidable proposition.

That should be in mathlib, I guess it was missed. I'm sure list.nodup already has a decidable instance, and alist.nodupkeys is just a wrapper around that, so the proof should be easy

#### Marc Huisinga (Nov 13 2019 at 23:37):

alternatively:

abbreviation a : list (sigma (λ _, list ℕ)) := [sigma.mk 1 [3], sigma.mk 2 [4]]
#eval (alist.keys (alist.mk a (by norm_num)))


#### Mario Carneiro (Nov 13 2019 at 23:38):

I would suggest norm_num [a] instead of making it an abbreviation

#### Scott Viteri (Nov 13 2019 at 23:43):

also

#eval (let a : list (sigma (λ _, list ℕ)) := [sigma.mk 1 [3], sigma.mk 2 [4]] in
(alist.keys (alist.mk a (by norm_num)))


works

#### Scott Viteri (Nov 13 2019 at 23:50):

alternatively:

abbreviation a : list (sigma (λ _, list ℕ)) := [sigma.mk 1 [3], sigma.mk 2 [4]]
#eval (alist.keys (alist.mk a (by norm_num)))

defs are semi-reducible (see https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html?highlight=semi%20reducible#elaboration-hints)


I read this section, but it does not mention the abbreviation keyword. Where is this documented?

#### Scott Viteri (Nov 13 2019 at 23:51):

I would suggest norm_num [a] instead of making it an abbreviation

Can I put a list of lemmas/definitions to rewrite with after any tactic?

#### Marc Huisinga (Nov 13 2019 at 23:53):

I read this section, but it does not mention the abbreviation keyword. Where is this documented?

no idea, sebastian told me about it some day. you can also just tag the def as reducible instead

#### Marc Huisinga (Nov 13 2019 at 23:55):

looks like it used to be in an old version of TPIL: https://leanprover.github.io/tutorial/tutorial.pdf

#### Scott Viteri (Nov 14 2019 at 19:13):

Consider the following alists:

def a : alist (λ (_:ℕ), ℕ) :=
alist.mk [sigma.mk 1 2, sigma.mk 2 3, sigma.mk 3 4] (by norm_num)

def b : alist (λ (_:ℕ), list ℕ) :=
alist.mk [sigma.mk 1 [2], sigma.mk 2 [], sigma.mk 3 [1,2]] (by norm_num)

#reduce (alist.replace 1 3 a)
#reduce (alist.replace 1 [3] b)


Only the last line generates an error, saying that it failed to synthesize type class instance for decidable_eq or has_one. Looking at alist.replace and kreplace, I do not see any mention of decidability. Where is this coming from and how do I fix it?

#### Kevin Buzzard (Nov 14 2019 at 19:19):

What do you mean by alist.replace 1 [3] b? Lean is trying to interpret this, and the errors are what it gets. What do you want it to mean?

#### Kevin Buzzard (Nov 14 2019 at 19:21):

You know about the implicit inputs to the function, right? If you hover over alist.replace in VS Code you will see Π {α : Type u} {β : α → Type v} [_inst_1 : decidable_eq α]. Lean is trying to figure out what alpha and beta are -- what do you think they are?

#### Scott Viteri (Nov 14 2019 at 19:23):

When I look for alist.replace I see the following:

def replace (a : α) (b : β a) (s : alist β) : alist β :=
⟨kreplace a b s.entries, (kreplace_nodupkeys a b).2 s.nodupkeys⟩


#### Scott Viteri (Nov 14 2019 at 19:23):

In mathlib/src/data/list/alist.lean

#### Kevin Buzzard (Nov 14 2019 at 19:23):

But if you read the mathlib code then you don't see the variables. If you hover over the function then you'll see all the stuff I posted.

#### Kevin Buzzard (Nov 14 2019 at 19:24):

Alternatively try #check @alist.replace

#### Kevin Buzzard (Nov 14 2019 at 19:25):

The @ means "tell me all the details of all the inputs to this function, including the stuff which Lean is going to figure out by itself"

#### Kevin Buzzard (Nov 14 2019 at 19:25):

alist.replace :
Π {α : Type u_1} {β : α → Type u_2} [_inst_1 : decidable_eq α] (a : α), β a → alist β → alist β


Lean says "ok I'll guess alpha, I'll guess beta, typeclass inference will guess _inst_1, now it's your turn"

#### Kevin Buzzard (Nov 14 2019 at 19:29):

You wrote alist.replace 1 [3] b. Lean thinks "OK, so a is supposed to be 1, so alpha is some type which has a 1, gosh, there are lots of possibilities". Lean then gets [3] and thinks "Ok so beta 1 is supposed to be [3], I'll bear that in mind". Lean then gets b and thinks "OK so b must have type alist beta, but b definitely has type alist (λ (_:ℕ), list ℕ) so beta must be  (λ (_:ℕ), list ℕ). Hey this looks like it should work. I am now intrigued.

#### Scott Viteri (Nov 14 2019 at 19:32):

I can get a more helpful error message if I put

#check (alist.replace (1:ℕ) ([1]:list ℕ) b)


#### Scott Viteri (Nov 14 2019 at 19:33):

type mismatch at application
alist.replace 1 [1]
term
[1]
has type
list var : Type
but is expected to have type
?m_1 1 : Type ?


#### Kevin Buzzard (Nov 14 2019 at 19:35):

You should comment out those #reduces, they really slow things down. So here's how I would start debugging:

#check @alist.replace _ _ _ 1 [3] b


#### Kevin Buzzard (Nov 14 2019 at 19:35):

OK so indeed if we tell Lean what beta is, it works fine:

#check @alist.replace _ (λ (_:ℕ), list ℕ) _ 1 [3] b


#### Kevin Buzzard (Nov 14 2019 at 19:36):

So the problem is that Lean is failing to guess beta.

#### Kevin Buzzard (Nov 14 2019 at 19:36):

This is some issue with the elaborator and it's beyond my pay grade to solve it. I would just fix it with the @ trick and move on.

#### Scott Viteri (Nov 14 2019 at 19:39):

Great. +1 for showing how you would debug

#### Scott Viteri (Nov 14 2019 at 19:52):

FYI, same problem and solution for alist.insert

Last updated: May 17 2021 at 22:15 UTC