# Zulip Chat Archive

## Stream: new members

### Topic: Slow Lean

#### Nicolò Cavalleri (Jun 19 2020 at 10:13):

At some point through a proof Lean started being very slow (each time I write something, even simple tactics, it takes more than 1 minute to update the goal) and the rest of my laptop seems to work fine! Does anyone have any tip on what I could try to do or any way I can troubleshoot Lean?

#### Kevin Buzzard (Jun 19 2020 at 10:24):

What is probably happening is that you have written a proof which takes a lot of time to compile, and every time you press a key Lean is recompiling the proof.

#### Kevin Buzzard (Jun 19 2020 at 10:27):

The reason that mathlib is written in heiroglyphics is precisely because they want all proofs to compile as fast as possible. There are several ways you can proceed. Firstly, there's some trick with putting `end.`

instead of `end`

after the problematic proof; this is supposed to tell Lean not to keep compiling it. This won't work if the problem is the proof you're currently working on though. Assuming the problem is a long proof you're finished with, another quick fix is to comment out the long proof, replace it with `sorry`

, and then put it back in the end, and another is to take out that proof and put it in another file, which you can import. Note that the problematic line can just be one line such as `finish`

or another expensive tactic.

#### Kevin Buzzard (Jun 19 2020 at 10:29):

If the problem is with a proof you're working on (i.e. you've still not finished the proof but Lean takes an age to compile the proof) then you might want to think about refactoring the proof. Best Lean style is lots of short proofs, not one big one -- this is how Grothendieck wrote mathematics as well. Deligne once said that it was amazing, he seemed to be doing a bunch of things which all looked trivial, and then something highly non-trivial would come out at the end. Lean likes to see mathematicians isolating the trivial steps and proving them as independent lemmas, rather than proving everything you need in one big proof. If you find yourself writing `have sublemma : <independent thing>, {proof of sublemma}`

in the middle of your proof then that's a great example of something which can go outside instead.

#### Nicolò Cavalleri (Jun 19 2020 at 10:30):

Ok thanks that is very useful. I am a bit surprised because it looks to be a fairly simple and basic proof, so I am wondering if I am doing something specific that slows it down. Do you have any specific tip for improving it?

```
import data.set.function
lemma prod_of_images_eq_image_of_prod {A : Type*} {B : Type*} {C : Type*} {D : Type*}
(f : A → B) (g : C → D) (s : set A) (t : set C):
(f '' s).prod (g '' t) = (λ x : A × C, (f x.fst, g x.snd)) '' s.prod t
:=
begin
ext x,
split,
{
simp,
intros y h1 h2 z h3 h4,
use y,
use z,
split,
exact ⟨h1, h3⟩,
exact prod.ext h2 h4
},
{
simp,
intros y z,
intros h1 h2 h3,
split,
{
use y,
split,
exact h1,
have h4 := congr_arg prod.fst h3,
exact h4,
},
{
use z,
split,
exact h2,
have h4 := congr_arg prod.snd h3,
exact h4,
},
}
end
```

#### Kevin Buzzard (Jun 19 2020 at 10:33):

Can you please make it a #mwe ? The code above doesn't compile as it stands.

#### Nicolò Cavalleri (Jun 19 2020 at 10:35):

Kevin Buzzard said:

Can you please make it a #mwe ? The code above doesn't compile as it stands.

Done, sorry, I did not include the set import!

#### Kevin Buzzard (Jun 19 2020 at 10:36):

Thanks. This code takes under a second to compile for me. Did you say something was taking a minute?

#### Nicolò Cavalleri (Jun 19 2020 at 10:36):

Yes but it does compile fast for me as well on a separate file, is it possible that it conflicts with something on my original file?

#### Kevin Buzzard (Jun 19 2020 at 10:37):

With `set_option profiler true`

I get

```
parsing took 33.7ms
type checking of prod_of_images_eq_image_of_prod took 0.102ms
decl post-processing of prod_of_images_eq_image_of_prod took 0.00224ms
elaboration of prod_of_images_eq_image_of_prod took 798ms
```

It's hard to help if I cannot easily reproduce the problem at my end.

#### Kevin Buzzard (Jun 19 2020 at 10:37):

You ideally need to post some code which enables me to reproduce the problem at my end without any effort on my part -- this is the best way to get help.

#### Kevin Buzzard (Jun 19 2020 at 10:38):

If this entails posting 1000 lines of code then you can post it on a gist or other pastey sites

#### Nicolò Cavalleri (Jun 19 2020 at 10:42):

Ok thanks! I will try to understand first on my own as I did not realize it compiled fast on a separate file before sending the code to you and my code uses files downloaded from still-non-approved push-requests so it takes a bit of effort to produce a mwe right now, but I will definitely come back if I do not manage to solve this on my own! Thanks a lot for the help up to now!

#### Kevin Buzzard (Jun 19 2020 at 10:44):

Don't underestimate `leanproject`

. If you have 1000 lines of code which compiles only with a non-master branch of mathlib then you can just post the code, say which branch to use, and I can use leanproject to check out the non-master branch oleans.

#### Kevin Buzzard (Jun 19 2020 at 10:45):

Even a non-PR'ed branch of mathlib, as long as it's on the leanprover-community version, gets compiled by the system and the oleans get dumped on the azure server.

#### Kevin Buzzard (Jun 19 2020 at 10:46):

And if you're pushing to a fork of mathlib on github because you don't have push access to non-master branches of mathlib, then you can just ask for access (the advantage of access is precisely that the system makes oleans for everyone; this makes PR reviews much easier for people).

#### Nicolò Cavalleri (Jun 19 2020 at 10:51):

Ok I think I managed to create a mwe that compiles extremely slow for me. Here it is

```
import geometry.manifold.real_instances
noncomputable theory
namespace local_homeomorph
variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
[topological_space α] [topological_space β] [topological_space γ] [topological_space δ]
lemma prod_symm (e : local_homeomorph α β) (e' : local_homeomorph γ δ) :
(e.prod e').symm = (e.symm.prod e'.symm) :=
by ext x : 1; simp
lemma prod_comp {η : Type*} {ε : Type*} [topological_space η] [topological_space ε]
(e : local_homeomorph α β) (f : local_homeomorph β γ)
(e' : local_homeomorph δ η) (f' : local_homeomorph η ε):
(e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f') :=
begin
ext x : 1,
{ simp },
{ simp },
{ ext y,
rcases y with ⟨a, b⟩,
simp [local_equiv.trans_source],
tauto }
end
lemma times_cont_diff_on.general_prod {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
{E : Type*} [normed_group E] [normed_space 𝕜 E]
{T : Type*} [normed_group T] [normed_space 𝕜 T]
{F : Type*} [normed_group F] [normed_space 𝕜 F]
{G : Type*} [normed_group G] [normed_space 𝕜 G]
{s : set E} {t : set T} {n : with_top ℕ} {f : E → F} {g : T → G}
(hf : times_cont_diff_on 𝕜 n f s) (hg : times_cont_diff_on 𝕜 n g t) :
times_cont_diff_on 𝕜 n (λ x : E × T, (f x.fst, g x.snd)) (set.prod s t) :=
begin
sorry,
end
lemma comp_of_prod_eq_prod_of_comp {A : Type*} {B : Type*} {C : Type*} {D : Type*} {E : Type*} {F : Type*}
(f : A → B) (g : C → D) (h : B → E) (k : D → F) :
(λ x : B × D, (h x.fst, k x.snd)) ∘ (λ x : A × C, (f x.fst, g x.snd)) = (λ x : A × C, ((h ∘ f) x.fst, (k ∘ g) x.snd)) := rfl
lemma prod_of_images_eq_image_of_prod {A : Type*} {B : Type*} {C : Type*} {D : Type*}
(f : A → B) (g : C → D) (s : set A) (t : set C):
(f '' s).prod (g '' t) = (λ x : A × C, (f x.fst, g x.snd)) '' s.prod t
:=
begin
ext x,
split,
{
simp,
intros y h1 h2 z h3 h4,
use y,
use z,
split,
exact ⟨h1, h3⟩,
exact prod.ext h2 h4
},
{
simp,
intros y z,
intros h1 h2 h3,
split,
{
use y,
split,
exact h1,
have h4 := congr_arg prod.fst h3,
exact h4,
},
{
use z,
split,
exact h2,
have h4 := congr_arg prod.snd h3,
exact h4,
},
}
end
end local_homeomorph
```

Let me know if you get the same problem!

#### Nicolò Cavalleri (Jun 19 2020 at 10:51):

(the lemma is at the end)

#### Kevin Buzzard (Jun 19 2020 at 10:59):

OK great, `prod_of_images_eq_image_of_prod`

is taking 8 seconds to compile for me according to the profiler, so we have something to work on.

#### Kevin Buzzard (Jun 19 2020 at 11:02):

It is being caused by the import. The below is slow, but if you change the import to a more primitive one, it is quick.

```
import geometry.manifold.real_instances
--import data.set.basic
set_option profiler true
lemma prod_of_images_eq_image_of_prod {A : Type*} {B : Type*} {C : Type*} {D : Type*}
(f : A → B) (g : C → D) (s : set A) (t : set C):
(f '' s).prod (g '' t) = (λ x : A × C, (f x.fst, g x.snd)) '' s.prod t
:=
begin
ext x,
split,
{
simp,
intros y h1 h2 z h3 h4,
use y,
use z,
split,
exact ⟨h1, h3⟩,
exact prod.ext h2 h4
},
{
simp,
intros y z,
intros h1 h2 h3,
split,
{
use y,
split,
exact h1,
have h4 := congr_arg prod.fst h3,
exact h4,
},
{
use z,
split,
exact h2,
have h4 := congr_arg prod.snd h3,
exact h4,
},
}
end
```

#### Kevin Buzzard (Jun 19 2020 at 11:02):

The issue will probably be the simplifier.

#### Kevin Buzzard (Jun 19 2020 at 11:03):

Using the simplifier in the middle of a proof is not recommended, because its behaviour can change over time, which makes your proofs brittle (you update mathlib and they break).

#### Kevin Buzzard (Jun 19 2020 at 11:07):

Yes, it's the simplifier. The much heavier import gave it far more options. You're not closing a goal with it, so maybe it spends a lot of time trying a gazillion simp lemmas before it decides to quit. If you use `squeeze_simp`

instead of `simp`

it will tell you a smaller simp set to use. Here is a fix for your problem, found with `squeeze_simp`

:

```
import geometry.manifold.real_instances
lemma prod_of_images_eq_image_of_prod {A : Type*} {B : Type*} {C : Type*} {D : Type*}
(f : A → B) (g : C → D) (s : set A) (t : set C):
(f '' s).prod (g '' t) = (λ x : A × C, (f x.fst, g x.snd)) '' s.prod t
:=
begin
ext x,
split,
{
simp only [and_imp, set.mem_image, set.mem_prod, exists_imp_distrib, prod.exists],
intros y h1 h2 z h3 h4,
use y,
use z,
split,
exact ⟨h1, h3⟩,
exact prod.ext h2 h4
},
{
simp only [and_imp, set.mem_image, set.mem_prod, exists_imp_distrib, prod.exists],
intros y z,
intros h1 h2 h3,
split,
{
use y,
split,
exact h1,
have h4 := congr_arg prod.fst h3,
exact h4,
},
{
use z,
split,
exact h2,
have h4 := congr_arg prod.snd h3,
exact h4,
},
}
end
```

#### Kevin Buzzard (Jun 19 2020 at 11:07):

However even this would not be regarded as good practice -- `simp`

is supposed to close goals only.

#### Nicolò Cavalleri (Jun 19 2020 at 11:09):

So you would suggest replacing the `simp only`

s with the lemmas in square brackets and find the good combination that works?

#### Nicolò Cavalleri (Jun 19 2020 at 11:09):

Is this required to PR things on Mathlib?

#### Nicolò Cavalleri (Jun 19 2020 at 11:10):

In any case it is weird that it took 8 seconds for you and more than 20 for me (yet I thought I had a good processor: an Intel i9)

#### Kevin Buzzard (Jun 19 2020 at 11:10):

Mathlib would not accept code with non-terminal simps in. If you *really* want to use a non-terminal simp, then there's an idiom which you can do instead: you run `simp`

, see the new goal, and then write `suffices : <new goal>, by simpa using this`

#### Kevin Buzzard (Jun 19 2020 at 11:11):

But my instinct is that a lemma of this size should have a very short proof; I'll see if I can find one for you.

#### Kevin Buzzard (Jun 19 2020 at 11:11):

You can tell it's the end of term :D

#### Nicolò Cavalleri (Jun 19 2020 at 11:13):

Haha thanks a lot! In if you suggest not using simps in the middle of proof I will just look for a combination of rws that works instead with the lemmas indicated by squeeze simp (it's not that I really want to use simp, but I did not really know what the standard practice was!)

#### Alex J. Best (Jun 19 2020 at 11:23):

Using simp only is ok (no need to express it in terms of rewrites) just not simp on its own.

#### Kevin Buzzard (Jun 19 2020 at 11:24):

You don't need any simps for this lemma

#### Kevin Buzzard (Jun 19 2020 at 11:25):

```
import geometry.manifold.real_instances
lemma prod_of_images_eq_image_of_prod {A : Type*} {B : Type*} {C : Type*} {D : Type*}
(f : A → B) (g : C → D) (s : set A) (t : set C):
(f '' s).prod (g '' t) = (λ x : A × C, (f x.fst, g x.snd)) '' s.prod t
:=
begin
ext ⟨b, d⟩,
split,
{ rintro ⟨⟨a, ha, hfa⟩, ⟨c, hc, hgc⟩⟩,
use [(a, c), ⟨ha, hc⟩],
ext, exact hfa, exact hgc
},
{ rintro ⟨⟨a, c⟩, ⟨ha, hc⟩, ⟨h⟩⟩,
use [a, ha, c, hc]
}
end
```

#### Kevin Buzzard (Jun 19 2020 at 11:39):

or

```
import data.set.basic
lemma prod_of_images_eq_image_of_prod {A : Type*} {B : Type*} {C : Type*} {D : Type*}
(f : A → B) (g : C → D) (s : set A) (t : set C):
(f '' s).prod (g '' t) = (λ x : A × C, (f x.fst, g x.snd)) '' s.prod t
:=
set.ext $ λ ⟨b, d⟩, ⟨λ ⟨⟨a, ha, hfa⟩, ⟨c, hc, hgc⟩⟩, ⟨(a, c), ⟨ha, hc⟩, prod.ext hfa hgc⟩,
λ ⟨⟨a, c⟩, ⟨ha, hc⟩, h⟩, ⟨⟨a, ha, (prod.ext_iff.1 h).1⟩, ⟨c, hc, (prod.ext_iff.1 h).2⟩⟩⟩
```

as they'd say in mathlib

#### Kevin Buzzard (Jun 19 2020 at 11:39):

but here's the coolest proof:

```
import data.set.basic tactic
lemma prod_of_images_eq_image_of_prod {A : Type*} {B : Type*} {C : Type*} {D : Type*}
(f : A → B) (g : C → D) (s : set A) (t : set C):
(f '' s).prod (g '' t) = (λ x : A × C, (f x.fst, g x.snd)) '' s.prod t
:= by tidy
```

#### Reid Barton (Jun 19 2020 at 11:40):

but does it take 8 seconds again?

#### Kevin Buzzard (Jun 19 2020 at 11:40):

Yeah, that mathlib proof was just the output of `squeeze_tidy`

[note to beginners: squeeze_tidy doesn't exist]

#### Reid Barton (Jun 19 2020 at 11:40):

`tidy`

likes `simp * at *`

as a pretty early move

#### Kevin Buzzard (Jun 19 2020 at 11:42):

Yes, with `tidy`

the proof time goes up again (to 3.5 seconds) if you import the manifold file.

#### Kevin Buzzard (Jun 19 2020 at 11:43):

`tidy?`

finds

```
:= by {ext1, cases x, dsimp at *, simp at *, fsplit, work_on_goal 0 { intros a, cases a, cases a_right, cases a_left, cases a_left_h, cases a_right_h, induction a_right_h_right, induction a_left_h_right, fsplit, work_on_goal 1 { fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 0 { assumption }, assumption }, simp at * } } }, intros a, cases a, cases a_h, cases a_h_h, cases a_h_h_right, cases a_h_h_left, induction a_h_h_right_right, induction a_h_h_right_left, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { assumption }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { assumption }, refl }}
```

which takes about half a second.

#### Kevin Buzzard (Jun 19 2020 at 11:45):

The mathlib proof is lightning fast even with the import, of course

#### Kevin Buzzard (Jun 19 2020 at 12:06):

So in fact proving the result with `tidy?`

, posting in the proof, removing the irrelevant `dsimp`

and changing both `simp`

s to `squeeze_simp`

and then `simp only`

cuts the time down to about 150ms, which is pretty respectable.

```
import geometry.manifold.real_instances
lemma prod_of_images_eq_image_of_prod {A : Type*} {B : Type*} {C : Type*} {D : Type*}
(f : A → B) (g : C → D) (s : set A) (t : set C):
(f '' s).prod (g '' t) = (λ x : A × C, (f x.fst, g x.snd)) '' s.prod t
:= by
{ ext1, cases x, simp only [set.mem_image, prod.mk.inj_iff, set.prod_mk_mem_set_prod_eq, prod.exists] at *, fsplit,
work_on_goal 0 {
intros a, cases a, cases a_right, cases a_left, cases a_left_h, cases a_right_h,
induction a_right_h_right, induction a_left_h_right,
fsplit,
work_on_goal 1 {
fsplit, work_on_goal 1 {
fsplit, work_on_goal 0 {
fsplit, work_on_goal 0 { assumption },
assumption },
simp only [eq_self_iff_true, and_self] at *}
}
},
intros a, cases a, cases a_h, cases a_h_h, cases a_h_h_right, cases a_h_h_left,
induction a_h_h_right_right, induction a_h_h_right_left,
fsplit,
work_on_goal 0 {
fsplit, work_on_goal 1 {
fsplit, work_on_goal 0 { assumption },
refl
}
},
fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { assumption }, refl }}
```

@Scott Morrison this is a pretty long proof found by `tidy`

-- pretty neat! Can you do post-processing to make `tidy?`

use `simp only`

instead of `simp`

?

#### Nicolò Cavalleri (Jun 19 2020 at 12:25):

How does rintro work?

#### Kevin Buzzard (Jun 19 2020 at 12:30):

`rintro`

is `intro`

and then `rcases`

, and `rcases`

is just iterated `cases`

#### Kevin Buzzard (Jun 19 2020 at 12:31):

I think it's pretty easy to see what it's doing -- just look at the tactic state before and after the `rintro`

. I am just doing `intro`

and then completely taking everything apart.

#### Kevin Buzzard (Jun 19 2020 at 12:33):

I'm introing a term of type `(b, d) ∈ (f '' s).prod (g '' t)`

but I don't really want that term, I want witnesses to what's going on, i.e. I want the `a \in s`

such that `f a = b`

etc.

#### Nicolò Cavalleri (Jun 19 2020 at 12:35):

Ok thanks! And just for the records: would `tidy`

be an acceptable proof for Mathlib?

#### Kevin Buzzard (Jun 19 2020 at 12:35):

`rintro ⟨⟨a, ha, hfa⟩, ⟨c, hc, hgc⟩⟩,`

is the same as

```
intro ac,
cases ac with hb hd,
cases hb with a ha',
cases ha' with ha hfa,
cases hd with c hc',
cases hc' with hc hgc,
```

#### Kevin Buzzard (Jun 19 2020 at 12:36):

The question of whether `tidy`

is acceptable for mathlib is a contentious one. The argument for is that it's very clear what's happening -- the proof is "just shuffle everything around and don't really think". The argument against is that it makes mathlib take longer to compile.

#### Kevin Buzzard (Jun 19 2020 at 12:38):

The ext1...proof was generated by `tidy`

so in some sense that's the happy medium, especially after I replaced the simp with simp only -- the tidy-generated proof was pretty quick. But because tidy is just doing a bunch of very simple things (it's only using ext and cases and stuff like that) one can often construct a lightning-fast term proof and then argue that it doesn't matter that it's incomprehensible because the proof was trivial anyway so nobody actually wants to read it.

#### Kevin Buzzard (Jun 19 2020 at 12:39):

Of course you can just search mathlib for tidy -- there are 288 results, but some of them are in comments.

#### Reid Barton (Jun 19 2020 at 12:40):

If you removed some of the things `tidy`

does (mostly `simp`

) it would probably quickly produce a fast proof in this example

#### Reid Barton (Jun 19 2020 at 12:40):

In any case, I don't think it is that hard to write a tactic that produces basically your "mathlib mode" proof

#### Kevin Buzzard (Jun 19 2020 at 12:41):

That's an interesting point. Note that the majority of times `tidy`

appears is in the category theory part of the repo, where it plays a very important role.

#### Reid Barton (Jun 19 2020 at 12:41):

another thing `tidy`

does that is probably useless most of the time is `simp ... at *`

#### Reid Barton (Jun 19 2020 at 12:42):

but maybe this isn't that much more expensive than `simp ...`

--I don't know

#### Reid Barton (Jun 19 2020 at 12:42):

I mean, in human proofs the `at *`

part is probably used < 10% of the time.

#### Kevin Buzzard (Jun 19 2020 at 12:43):

Can we tell tidy not to use simp?

#### Kevin Buzzard (Jun 19 2020 at 12:43):

It never occurred to me to use simp when I was constructing the tactic-free proof.

#### Reid Barton (Jun 19 2020 at 12:44):

I don't think you can easily remove tactics from the list but you can copy https://github.com/leanprover-community/mathlib/blob/master/src/tactic/tidy.lean#L41-L57 and pare it down

#### Kevin Buzzard (Jun 19 2020 at 12:47):

dammit stupid tidy doesn't solve it if I remove simp! It can't solve this:

```
state:
6 goals
A : Type u_1,
B : Type u_2,
C : Type u_3,
D : Type u_4,
f : A → B,
g : C → D,
s : set A,
t : set C,
a_w_fst : A,
a_w_snd : C,
a_h_left_left : (a_w_fst, a_w_snd).fst ∈ s,
a_h_left_right : (a_w_fst, a_w_snd).snd ∈ t,
x_snd : D,
x_fst : B
⊢ A
```

#### Kevin Buzzard (Jun 19 2020 at 12:47):

hey, `simp`

can't solve it either :-/

#### Reid Barton (Jun 19 2020 at 12:48):

try changing `fsplit`

to `split`

#### Reid Barton (Jun 19 2020 at 12:48):

I'm curious whether this helps

#### Kevin Buzzard (Jun 19 2020 at 12:48):

` fsplit >> pure "fsplit",`

#### Kevin Buzzard (Jun 19 2020 at 12:48):

Just the one on the left?

#### Reid Barton (Jun 19 2020 at 12:49):

well, both if you want the proof output to be accurate

#### Reid Barton (Jun 19 2020 at 12:49):

but at least the one on the left yes

#### Kevin Buzzard (Jun 19 2020 at 12:49):

Works!

#### Kevin Buzzard (Jun 19 2020 at 12:50):

Modded `tidy`

finds

```
ext1, cases x, split, work_on_goal 0 { intros a, cases a, cases a_right, cases a_left, cases a_left_h, cases a_right_h, split, work_on_goal 0 { split, work_on_goal 0 { split }, work_on_goal 2 { tactic.ext1 [] {new_goals := tactic.new_goals.all}, work_on_goal 0 { unfold_coes }, work_on_goal 1 { unfold_coes } } }, work_on_goal 4 { split }, work_on_goal 0 { assumption }, work_on_goal 0 { assumption }, work_on_goal 0 { assumption }, work_on_goal 0 { assumption } }, intros a, cases a, cases a_h, cases a_w, cases a_h_left, split, work_on_goal 0 { split, work_on_goal 0 { split, work_on_goal 0 { assumption }, injections_and_clear, assumption } }, split, work_on_goal 0 { split, work_on_goal 0 { assumption }, injections_and_clear, assumption },
```

#### Kevin Buzzard (Jun 19 2020 at 12:51):

which is compiling in just over 100ms

#### Kevin Buzzard (Jun 19 2020 at 12:51):

I'm assuming that adding the manifold import won't change the timing, but of course I'm now orangebaring.

#### Kevin Buzzard (Jun 19 2020 at 12:53):

oh rofl the import doesn't compile now :-)

#### Kevin Buzzard (Jun 19 2020 at 12:54):

oh wait I can roll back the tidy edit :D

#### Kevin Buzzard (Jun 19 2020 at 12:56):

yeah bingo, so this is really an instance where the weakened tidy finds a better proof, because it's not allowed to use simp so the import doesn't screw it up. Recall that normal `tidy?`

produces a proof which with the manifold import takes 500ms to compile.

#### Kevin Buzzard (Jun 19 2020 at 12:56):

Weakened `tidy?`

produces a proof which takes 100ms to compile with the manifold import.

#### Nicolò Cavalleri (Jun 19 2020 at 12:58):

Sorry again for another low level question: how does `rcases`

work? I can't find its syntax

#### Kevin Buzzard (Jun 19 2020 at 12:58):

#### Reid Barton (Jun 19 2020 at 12:58):

I had a story for why `split`

should help over `fsplit`

but now I realize it's not really compatible with the original tidy succeeding with `split`

#### Nicolò Cavalleri (Jun 19 2020 at 12:59):

Ok thanks!

#### Kevin Buzzard (Jun 19 2020 at 12:59):

do you mean original tidy succeeding with `fsplit`

?

#### Reid Barton (Jun 19 2020 at 13:00):

Oh yes, sorry

#### Nicolò Cavalleri (Jun 19 2020 at 13:09):

Do you know also a place where I can find an example of `rcases`

? I don't understand the documentation

#### Nicolò Cavalleri (Jun 19 2020 at 13:11):

Well never mind maybe I got it

#### Kevin Buzzard (Jun 19 2020 at 13:12):

```
lemma prod_of_images_eq_image_of_prod {A : Type*} {B : Type*} {C : Type*} {D : Type*}
(f : A → B) (g : C → D) (s : set A) (t : set C):
(f '' s).prod (g '' t) = (λ x : A × C, (f x.fst, g x.snd)) '' s.prod t
:=
begin
ext ⟨b, d⟩,
split,
{ intro temp,
rcases temp with ⟨⟨a, ha, hfa⟩, ⟨c, hc, hgc⟩⟩,
use [(a, c), ⟨ha, hc⟩],
ext, exact hfa, exact hgc
},
{ rintro ⟨⟨a, c⟩, ⟨ha, hc⟩, ⟨h⟩⟩,
use [a, ha, c, hc]
}
end
```

#### Nicolò Cavalleri (Jun 19 2020 at 13:13):

Ok thanks!!

#### Kevin Buzzard (Jun 19 2020 at 13:14):

When a term is just made up directly of smaller terms, we're just pulling the smaller terms out. For example a term of type $x\in f(Y)$ can be taken apart into a term `y : Y`

and a proof that `f y = x`

(which is another term, in type theory)

#### Kevin Buzzard (Jun 19 2020 at 13:15):

The commas in the pointy brackets are right associative, so `⟨a, ha, hfa⟩`

means `⟨a, ⟨ha, hfa⟩⟩`

#### Kevin Buzzard (Jun 19 2020 at 13:16):

Look at how I took `temp`

apart with `cases`

, each time turning one term into 2.

#### Kevin Buzzard (Jun 19 2020 at 13:16):

It's just some kind of tree, and `rcases`

enables me to take it all apart in one go.

#### Kevin Buzzard (Jun 19 2020 at 13:17):

(`ac`

= `temp`

)

```
intro ac,
cases ac with hb hd,
cases hb with a ha',
cases ha' with ha hfa,
cases hd with c hc',
cases hc' with hc hgc,
```

#### Kevin Buzzard (Jun 19 2020 at 13:18):

Everything has only one constructor so there are no `|`

s involved.

#### Nicolò Cavalleri (Jun 19 2020 at 14:07):

Ok thank you very much!

#### Nicolò Cavalleri (Jun 19 2020 at 14:10):

Moreover I was wondering: as a general strategy, if when doing a proof I need to use simps to make it human, supposing that at the end of the proof I realize the simps can be removed, should I remove them or replace them with the output of squeeze_simp, to leave the proof readable?

#### Nicolò Cavalleri (Jun 19 2020 at 14:10):

I mean what is the standard practice in mathlib?

#### Alex J. Best (Jun 19 2020 at 14:12):

Standard practice is to replace a non-terminal simp with the output of squeeze simp.

#### Reid Barton (Jun 19 2020 at 14:12):

For really basic statements like this, it's better to avoid simp completely if possible

#### Alex J. Best (Jun 19 2020 at 14:12):

If you can write it as a chain of rewrites thats nice, but you'll find a lot of `simp only`

in mathlib.

#### Reid Barton (Jun 19 2020 at 14:13):

in other words, if the human proof is something like "they're the same", then human readability of the proof is not a factor

#### Nicolò Cavalleri (Jun 19 2020 at 14:19):

Ok but I mean what if the simp can be completely removed without replacing them with the output of `squeeze_simp`

? The point is that if I remove them completely, if someone clicks in the middle of my proofs the goal is like 20 lines of incomprehensible symbols

#### Nicolò Cavalleri (Jun 19 2020 at 14:19):

But the proof still works

#### Nicolò Cavalleri (Jun 19 2020 at 14:19):

Not in the proof of this post I mean, in other proofs

#### Alex J. Best (Jun 19 2020 at 14:38):

What do you mean by completely removed? Presumably simp was doing something that should then be done by another tactic or term?

It depends, for one example: a lot of simp lemmas are proved by `rfl`

and so a combination of lemmas proved in this way might also be provable by `rfl`

instead of `simp, refl`

. Then `simp`

could be removed but `refl`

would have to work harder to reprove all the simp lemmas along the way. For example:

```
import tactic
import data.real.basic
set_option profiler true
example : (10 : ℚ) = ↑(10:ℕ) :=
begin
refl,
end
example : (10 : ℚ) = ↑(10:ℕ) :=
begin
simp,
end
```

on my machine the first takes 1.3 s and the second 0.3s, so "removing simp" and replacing it with a more low level tactic in this case is not helpful.

#### Alex J. Best (Jun 19 2020 at 14:40):

And squeeze simp output takes 0.07s!

#### Alex J. Best (Jun 19 2020 at 14:49):

And finally the explicit rw proof `rw [nat.cast_bit0, nat.cast_bit1, nat.cast_bit0, nat.cast_one],`

takes only 9ms, but nobody wants to write that out every time ;) they have a goal like this. `norm_num`

takes about 0.1s and `norm_cast`

roughly the same as simp only.

Of these I'd say the "best" is the tactic specialised to goals like this "norm_cast", it's efficient, short and you are saying what you mean which makes it far more readable than the rw or simps really.

In conclusion use the profiler and experiment and have fun ;)!

Last updated: May 11 2021 at 12:15 UTC