Zulip Chat Archive

Stream: new members

Topic: Is there a way to search a particular rewrite?


view this post on Zulip YH (Dec 12 2019 at 00:08):

There are some trivial things like (a^b)^c = a^(b*c) that I want to find in the library, but how? I searched for things whose name containing "pow" or "exp" but it doesn't help much.

view this post on Zulip Bhavik Mehta (Dec 12 2019 at 00:09):

You can use the tactic library_search for this sort of thing! I think this one is called pow_mul

view this post on Zulip YH (Dec 12 2019 at 00:12):

You can use the tactic library_search for this sort of thing! I think this one is called pow_mul

I am aware of library_search but it seems it only search for tactics that handles the whole problem?

What if I want to find some rewrite x so that I can do rw x at h for a particular h, can I use that one?

view this post on Zulip YH (Dec 12 2019 at 00:17):

Let's say after pow_mul I get a^(1/2 + 1/2), what do I do to make it a^1 or a?

view this post on Zulip Marc Huisinga (Dec 12 2019 at 00:21):

you can temporarily split off the statement you're looking for into a lemma (or a have-subproof) and then use library_search

view this post on Zulip Alex J. Best (Dec 12 2019 at 00:36):

For your specific example what you would split off could just be

example : (1:)/2 + 1/2  = 1 := add_halves 1 -- by library_search

-- so now we can do
open real
example : pi ^ ((1:)/2 + 1/2) = pi :=
begin
rw add_halves (1 : ),
exact rpow_one pi, -- library_search again
end

but the best way if you have actual numbers is probably example : pi ^ ((1:ℝ)/2 + 1/2) = pi := by norm_num

view this post on Zulip YH (Dec 12 2019 at 00:40):

add_halves? What if I had a^(1/3 + 2/3)?

view this post on Zulip YH (Dec 12 2019 at 00:41):

Not actual numbers, any a:ℝ

view this post on Zulip Alex J. Best (Dec 12 2019 at 00:44):

Right, library search isn't good for that, it won't find tactics for you just lemmas. Thats why the norm_num tactic may be better depending on your actual application, the trade -off is that a tactic may take (slightly) longer to do its thing than calling an explicit lemma.

view this post on Zulip YH (Dec 12 2019 at 00:55):

add_halves? What if I had a^(1/3 + 2/3)?

Oh I just realized I can't prove lemma b : 1/2 + 1/2 = 1 := by sorry yet... (where 1 is not of type )

view this post on Zulip Kevin Buzzard (Dec 12 2019 at 07:52):

If everything has type nat (which it might do by default) then this might not even be true

view this post on Zulip YH (Dec 12 2019 at 07:53):

If everything has type nat (which it might do by default) then this might not even be true

Yeah I realized this later...


Last updated: May 15 2021 at 23:13 UTC