Stream: new members

Topic: Slow simp

Patrick Massot (Jun 19 2020 at 16:48):

Kevin Buzzard said:

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, note this idiom is so common that you can abbreviate by simpa using this to by simpa.

Kevin Buzzard (Jun 19 2020 at 16:56):

@Nicolò Cavalleri the point of this is that instead of just letting simp change the goal to something you can't quite control, you say "simp, change the goal to this" and then let it do it; that way, changes in the behaviour of simp are less likely to break your proof.

Scott Morrison (Jun 20 2020 at 09:32):

We could have tidy? produce simp only ... scripts. The right solution to this would be to provide a non-interactive version of squeeze_simp that returns a list of names directly, and then an outer interactive layer that takes care of producing a trace message. From what I remember, it didn't look trivial to refactor it like this, but of course it just can't be that hard.

Scott Morrison (Jun 20 2020 at 09:33):

If someone wants to do that refactor of squeeze_simp I'll promise to do the corresponding improvement to tidy. :-)

(Deleted)

Nicolò Cavalleri (Jun 22 2020 at 15:30):

Kevin Buzzard said:

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


When you got this proof with tidy did you write the rintros by hand or did tidy write them for you? It does not write it for me but instead it writes intro and then cases!

Kevin Buzzard (Jun 22 2020 at 15:31):

I did not make this proof with tidy, I wrote it by hand.

Nicolò Cavalleri (Jun 22 2020 at 15:31):

Kevin Buzzard said:

I did not make this proof with tidy, I wrote it by hand.

Ok thanks I got it wrong then!

Kevin Buzzard (Jun 22 2020 at 15:32):

The tidy auto-generated proof has all the work_on_goal stuff in

Kevin Buzzard (Jun 22 2020 at 15:32):

You can write rintro? I think, to get Lean to suggest what you want the line to be.

Kevin Buzzard (Jun 22 2020 at 15:37):

Oh that's interesting, the suggestion doesn't compile. @Scott Morrison the rfl is too optimistic in rintro? here. The issue is that the term of type f a = (b, d).fst doesn't want to be rfl despite the fact that it would fine if the RHS were dsimped first.

Kenny Lau (Jun 22 2020 at 15:46):

Kevin Buzzard said:

The reason that mathlib is written in heiroglyphics is precisely because they want all proofs to compile as fast as possible.

If only

Scott Morrison (Jun 22 2020 at 23:28):

I didn't write the ? mode for rintro, do I'm not too sure how it decided what to propose. We should raise an issue about the bad suggestion.

Bryan Gin-ge Chen (Jun 23 2020 at 00:14):

You could add some more examples to #2794.

Last updated: May 12 2021 at 05:19 UTC