Zulip Chat Archive

Stream: new members

Topic: Understanding Alist


view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Marc Huisinga (Nov 13 2019 at 19:25):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 _

view this post on Zulip 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.

view this post on Zulip 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 ;)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 13 2019 at 22:49):

You can try dec_trivial

view this post on Zulip Rob Lewis (Nov 13 2019 at 23:16):

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

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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)))

view this post on Zulip 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

view this post on Zulip 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)))

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

view this post on Zulip Mario Carneiro (Nov 13 2019 at 23:38):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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⟩

view this post on Zulip Scott Viteri (Nov 14 2019 at 19:23):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 14 2019 at 19:24):

Alternatively try #check @alist.replace

view this post on Zulip 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"

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 14 2019 at 19:36):

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

view this post on Zulip 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.

view this post on Zulip Scott Viteri (Nov 14 2019 at 19:39):

Great. +1 for showing how you would debug

view this post on Zulip 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