Slow Lean

Stream: new members

[Nicolò Cavalleri]

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]

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]

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]

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]

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]

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

[Nicolò Cavalleri]

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]

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

[Nicolò Cavalleri]

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]

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]

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]

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

[Nicolò Cavalleri]

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]

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]

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]

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]

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]

(the lemma is at the end)

[Kevin Buzzard]

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]

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]

The issue will probably be the simplifier.

[Kevin Buzzard]

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]

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]

However even this would not be regarded as good practice -- simp is supposed to close goals only.

[Nicolò Cavalleri]

So you would suggest replacing the simp onlys with the lemmas in square brackets and find the good combination that works?

[Nicolò Cavalleri]

Is this required to PR things on Mathlib?

[Nicolò Cavalleri]

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]

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]

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]

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

[Nicolò Cavalleri]

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]

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

[Kevin Buzzard]

You don't need any simps for this lemma

[Kevin Buzzard]

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]

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]

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]

but does it take 8 seconds again?

[Kevin Buzzard]

Yeah, that mathlib proof was just the output of squeeze_tidy [note to beginners: squeeze_tidy doesn't exist]

[Reid Barton]

tidy likes simp * at * as a pretty early move

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

So in fact proving the result with tidy?, posting in the proof, removing the irrelevant dsimp and changing both simps 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]

How does rintro work?

[Kevin Buzzard]

rintro is intro and then rcases, and rcases is just iterated cases

[Kevin Buzzard]

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]

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]

Ok thanks! And just for the records: would tidy be an acceptable proof for Mathlib?

[Kevin Buzzard]

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]

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]

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]

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

[Reid Barton]

If you removed some of the things tidy does (mostly simp) it would probably quickly produce a fast proof in this example

[Reid Barton]

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

[Kevin Buzzard]

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]

another thing tidy does that is probably useless most of the time is simp ... at *

[Reid Barton]

but maybe this isn't that much more expensive than simp ...--I don't know

[Reid Barton]

I mean, in human proofs the at * part is probably used < 10% of the time.

[Kevin Buzzard]

Can we tell tidy not to use simp?

[Kevin Buzzard]

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

[Reid Barton]

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]

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]

hey, simp can't solve it either :-/

[Reid Barton]

try changing fsplit to split

[Reid Barton]

I'm curious whether this helps

[Kevin Buzzard]

fsplit >> pure "fsplit",

[Kevin Buzzard]

Just the one on the left?

[Reid Barton]

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

[Reid Barton]

but at least the one on the left yes

[Kevin Buzzard]

Works!

[Kevin Buzzard]

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]

which is compiling in just over 100ms

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

oh wait I can roll back the tidy edit :D

[Kevin Buzzard]

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]

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

[Nicolò Cavalleri]

Sorry again for another low level question: how does rcases work? I can't find its syntax

[Kevin Buzzard]

tactic#rcases ?

[Reid Barton]

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]

Ok thanks!

[Kevin Buzzard]

do you mean original tidy succeeding with fsplit?

[Reid Barton]

Oh yes, sorry

[Nicolò Cavalleri]

Do you know also a place where I can find an example of rcases? I don't understand the documentation

[Nicolò Cavalleri]

Well never mind maybe I got it

[Kevin Buzzard]

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]

Ok thanks!!

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Look at how I took temp apart with cases, each time turning one term into 2.

[Kevin Buzzard]

It's just some kind of tree, and rcases enables me to take it all apart in one go.

[Kevin Buzzard]

(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]

Everything has only one constructor so there are no |s involved.

[Nicolò Cavalleri]

Ok thank you very much!

[Nicolò Cavalleri]

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]

I mean what is the standard practice in mathlib?

[Alex J. Best]

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

[Reid Barton]

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

[Alex J. Best]

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]

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]

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]

But the proof still works

[Nicolò Cavalleri]

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

[Alex J. Best]

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]

And squeeze simp output takes 0.07s!

[Alex J. Best]

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 ;)!