Slow simp

Stream: new members

[Patrick Massot]

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]

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

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]

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

[Shing Tak Lam]

(Deleted)

[Nicolò Cavalleri]

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]

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

[Nicolò Cavalleri]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

You could add some more examples to #2794.