Zulip Chat Archive

Stream: new members

Topic: Slow Lean


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 10:33):

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

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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!

view this post on Zulip Nicolò Cavalleri (Jun 19 2020 at 10:51):

(the lemma is at the end)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 11:02):

The issue will probably be the simplifier.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Nicolò Cavalleri (Jun 19 2020 at 11:09):

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

view this post on Zulip Nicolò Cavalleri (Jun 19 2020 at 11:09):

Is this required to PR things on Mathlib?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 11:11):

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

view this post on Zulip 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!)

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 11:24):

You don't need any simps for this lemma

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Jun 19 2020 at 11:40):

but does it take 8 seconds again?

view this post on Zulip 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]

view this post on Zulip Reid Barton (Jun 19 2020 at 11:40):

tidy likes simp * at * as a pretty early move

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 11:45):

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

view this post on Zulip 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 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?

view this post on Zulip Nicolò Cavalleri (Jun 19 2020 at 12:25):

How does rintro work?

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 12:30):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Nicolò Cavalleri (Jun 19 2020 at 12:35):

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

view this post on Zulip 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,

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jun 19 2020 at 12:41):

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

view this post on Zulip Reid Barton (Jun 19 2020 at 12:42):

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

view this post on Zulip Reid Barton (Jun 19 2020 at 12:42):

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

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 12:43):

Can we tell tidy not to use simp?

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 12:43):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 12:47):

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

view this post on Zulip Reid Barton (Jun 19 2020 at 12:48):

try changing fsplit to split

view this post on Zulip Reid Barton (Jun 19 2020 at 12:48):

I'm curious whether this helps

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 12:48):

fsplit >> pure "fsplit",

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 12:48):

Just the one on the left?

view this post on Zulip Reid Barton (Jun 19 2020 at 12:49):

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

view this post on Zulip Reid Barton (Jun 19 2020 at 12:49):

but at least the one on the left yes

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 12:49):

Works!

view this post on Zulip 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 },

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 12:51):

which is compiling in just over 100ms

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 12:53):

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

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 12:54):

oh wait I can roll back the tidy edit :D

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 12:56):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 12:58):

tactic#rcases ?

view this post on Zulip 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

view this post on Zulip Nicolò Cavalleri (Jun 19 2020 at 12:59):

Ok thanks!

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 12:59):

do you mean original tidy succeeding with fsplit?

view this post on Zulip Reid Barton (Jun 19 2020 at 13:00):

Oh yes, sorry

view this post on Zulip 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

view this post on Zulip Nicolò Cavalleri (Jun 19 2020 at 13:11):

Well never mind maybe I got it

view this post on Zulip 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

view this post on Zulip Nicolò Cavalleri (Jun 19 2020 at 13:13):

Ok thanks!!

view this post on Zulip 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 xf(Y)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)

view this post on Zulip 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⟩⟩

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 13:16):

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

view this post on Zulip 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.

view this post on Zulip 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,

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 13:18):

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

view this post on Zulip Nicolò Cavalleri (Jun 19 2020 at 14:07):

Ok thank you very much!

view this post on Zulip 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?

view this post on Zulip Nicolò Cavalleri (Jun 19 2020 at 14:10):

I mean what is the standard practice in mathlib?

view this post on Zulip Alex J. Best (Jun 19 2020 at 14:12):

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

view this post on Zulip Reid Barton (Jun 19 2020 at 14:12):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Nicolò Cavalleri (Jun 19 2020 at 14:19):

But the proof still works

view this post on Zulip Nicolò Cavalleri (Jun 19 2020 at 14:19):

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

view this post on Zulip 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.

view this post on Zulip Alex J. Best (Jun 19 2020 at 14:40):

And squeeze simp output takes 0.07s!

view this post on Zulip 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