Zulip Chat Archive

Stream: new members

Topic: rw show by


Anatole Dedecker (Jul 18 2020 at 20:31):

Is there a prettier way to do things like that ?

rw (show ? = ?, by {...}),

Jalex Stark (Jul 18 2020 at 20:35):

I'm not sure I understand what's going on there, but maybe you want tactic#convert

Alex J. Best (Jul 18 2020 at 20:39):

I'd say that and have : ? = ? := by blah, rw this are your main choices, depending on the length of blah.

Markus Himmel (Jul 18 2020 at 20:40):

Sometimes you can avoid these constructions by restructuring your proof into a calc proof.

Anatole Dedecker (Jul 18 2020 at 20:41):

Yes but the problem of calc proofs is they need to close the goal :sad:

Jalex Stark (Jul 18 2020 at 20:43):

so start by creating the goal which is the last statement of the calc proof?

Anatole Dedecker (Jul 18 2020 at 20:45):

Indeed, but the whole objective of using the rw (show ..., by ...) syntax is we don't need to create a 1-use subgoal

Jalex Stark (Jul 18 2020 at 20:46):

does the following work as a way to introduce a lemma A = C?

have := calc A = B : by sorry
... = C : by sorry

Adam Topaz (Jul 18 2020 at 20:47):

You can also refine calc foo = bar : _ etc

Alex J. Best (Jul 18 2020 at 20:48):

Well you're still introducing it when you prove it it just disappears out of scope after, you can clear a have if you're finding you have two many of these one time things floating around.

Anatole Dedecker (Jul 18 2020 at 20:49):

Oh yes I forget about this all the time x)

Alex J. Best (Jul 18 2020 at 20:49):

Or prove it as a lemma if its not too specific ! So you can rewrite it without introducing it.

Anatole Dedecker (Jul 18 2020 at 20:50):

Jalex Stark said:

does the following work as a way to introduce a lemma A = C?

have := calc A = B : by sorry
... = C : by sorry

It does, that's clever

Anatole Dedecker (Jul 18 2020 at 20:53):

The use I had in mind was for things like that :

import topology.instances.real

open filter
open_locale topological_space filter

example : tendsto (λ x : , x * (1 - x)) (𝓝 1) (𝓝 0) :=
begin
  rw (show (0 : ) = 1 * 0, by simp),
  apply tendsto.mul,
  exact tendsto_id,
  rw (show (0 : ) = 1 - 1, by simp),
  exact tendsto.sub tendsto_const_nhds tendsto_id,
end

Jalex Stark (Jul 18 2020 at 20:55):

in this case, both lemmas have names

import topology.instances.real

open filter
open_locale topological_space filter

example : tendsto (λ x : , x * (1 - x)) (𝓝 1) (𝓝 0) :=
begin
  rw  one_mul (0:),
  apply tendsto.mul, { exact tendsto_id },
  rw  sub_self (1:),
  apply tendsto.sub, { exact tendsto_const_nhds },
  exact tendsto_id,
end

Anatole Dedecker (Jul 18 2020 at 20:56):

Indeed, but that's a simple example

Jalex Stark (Jul 18 2020 at 20:59):

one can also do this which feels silly but maybe demonstrates convert:

import topology.instances.real

open filter
open_locale topological_space filter

example : tendsto (λ x : , x * (1 - x)) (𝓝 1) (𝓝 0) :=
begin
  convert tendsto.mul _ _, rw one_mul, apply_instance,
  { exact tendsto_id },
  convert tendsto.sub _ _, rw sub_self, exact 1, apply_instance,
  { exact tendsto_const_nhds },
  exact tendsto_id,
end

Anatole Dedecker (Jul 18 2020 at 21:01):

Oh interesting. I need to learn how to use convert

Kevin Buzzard (Jul 19 2020 at 10:11):

convert is great. It is like rw on steroids. Once you have a hypothesis h which is basically equal to your goal modulo a few differences, convert h will just explicitly give you the differences as new goals, saving you the trouble of having to work with them as subterms of a larger term


Last updated: Dec 20 2023 at 11:08 UTC