Is there a way to search a particular rewrite?

Stream: new members

[YH]

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.

[Bhavik Mehta]

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

[YH]

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?

[YH]

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

[Marc Huisinga]

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

[Alex J. Best]

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

[YH]

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

[YH]

Not actual numbers, any a:ℝ

[Alex J. Best]

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.

[YH]

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 ℝ)

[Kevin Buzzard]

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

[YH]

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

Yeah I realized this later...