Understanding Alist

Stream: new members

[Scott Viteri]

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]

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]

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]

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

[Bryan Gin-ge Chen]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

You can try dec_trivial

[Rob Lewis]

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

[Scott Viteri]

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]

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]

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]

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]

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]

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)

[Mario Carneiro]

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

[Scott Viteri]

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]

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]

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]

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]

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

[Scott Viteri]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

Alternatively try #check @alist.replace

[Kevin Buzzard]

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]

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]

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]

I can get a more helpful error message if I put

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

[Scott Viteri]

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]

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]

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

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Great. +1 for showing how you would debug

[Scott Viteri]

FYI, same problem and solution for alist.insert