Zulip Chat Archive

Stream: new members

Topic: unfolding specific instance


view this post on Zulip Miroslav Olšák (Mar 29 2021 at 07:07):

Is it possible to tell lean to unfold only a specific instance of a typeclass function? This typically happens when I have my own instance of a typeclass, so I need to dig inside, but then there are also other instances of the same typeclass in the library. For example, what I mean:

example (l : list ) (s : set ) (n : )
  : (n  l) = (n  s) :=
begin
  unfold has_mem.mem /- somehow only for set -/, unfold set.mem,
  sorry
end

I would like it to end up with the goal n ∈ l = s n. I tried unfold set.has_mem.mem but that fails.

view this post on Zulip Kevin Buzzard (Mar 29 2021 at 07:07):

You can use change to get there manually

view this post on Zulip Kevin Buzzard (Mar 29 2021 at 07:08):

Or you can zoom into the term in conv mode and just unfold the part you want

view this post on Zulip Miroslav Olšák (Mar 29 2021 at 07:10):

change (or show) can be impractical in practice when I deal with more complex terms, I don't know conv mode (I can look at it)

view this post on Zulip Miroslav Olšák (Mar 29 2021 at 07:12):

I just thought whether it could be possible to directly target an instance, it feels quite natural to me.

view this post on Zulip Miroslav Olšák (Mar 29 2021 at 07:26):

Otherwise, I can write my own unfolding lemmata, I guess.

view this post on Zulip Kevin Buzzard (Mar 29 2021 at 07:48):

I can't get unfold to work in conv mode. change you can make easier by using wildcards:

example (l : list ) (s : set ) (n : )
  : (n  l) = (n  s) :=
begin
  change _ = s _,
  -- ⊢ n ∈ l = s n
  sorry
end

view this post on Zulip Kevin Buzzard (Mar 29 2021 at 07:51):

But rw works

view this post on Zulip Kevin Buzzard (Mar 29 2021 at 07:57):

lemma set.has_mem_def {α : Type*} (s : set α) (a : α) : a  s = s a := rfl

example (l : list ) (s : set ) (n : )
  : (n  l) = (n  s) :=
begin
  rw set.has_mem_def,
  -- ⊢ n ∈ l = s n
  sorry
end

view this post on Zulip Miroslav Olšák (Mar 29 2021 at 08:04):

OK, I will do it this way, that is what I meant with writing custom unfolding lemmata.


Last updated: May 16 2021 at 20:13 UTC