Try this

Stream: general

[Johan Commelin]

The new "Try this" stuff is really cool! Thanks @Gabriel Ebner @Bryan Gin-ge Chen @Alexander Bentkamp for this marvelous feature!

[Gabriel Ebner]

I only pressed the merge button. All thanks should go to @Bryan Gin-ge Chen and @Alexander Bentkamp!

[Bryan Gin-ge Chen]

I just made a few suggestions, @Alexander Bentkamp did all the hard work!

[Kevin Buzzard]

What is this feature?

[Patrick Massot]

You need to update mathlib and try suggest or squeeze_simp. Then you'll see.

[Patrick Massot]

I wanted to try it on rintro so I tested:

example : ∀ n : ℕ, n=n :=
begin
  rintro?

end

The result is pretty funny.

[Patrick Massot]

I guess there must be some depth limitation (which looks wise).

[Patrick Massot]

https://github.com/leanprover-community/mathlib/blob/cd0e2f6af4201b832c1f6ebefbc352108ff38458/src/tactic/rcases.lean#L356-L357

[Kevin Buzzard]

import tactic

example : ∀ n : ℕ, n=n :=
begin
  suggest, -- exact rfl
  exact rfl -- fails
end

Has the behaviour of squeeze_simp changed? It still seems to do the same for me.

commit 8700aa7d78b10b65cf8db1d9e320872ae313517a (HEAD, origin/lean-3.5.1)
Author: Gabriel Ebner <gebner@gebner.org>
Date:   Wed Feb 19 00:13:13 2020 +0100

    feat(docs): install mathlibtools package with pip (#2010)

[Patrick Massot]

Yes, it has changed.

[Rob Lewis]

Update the VSCode extension too.

[Patrick Massot]

He should still see "Try this:" without updating, right?

[Kevin Buzzard]

squeeze_simp !? only? (* | [(* | (- id | expr)), ...]?) (with id*)? (at (* | (⊢ | id)*))? <error while executing interactive.param_desc: don't know how to pretty print [has_bind.bind (monad.to_has_bind lean.parser)] (lean.parser.tk "{") (λ (_x : unit), lean.parser.sep_by (lean.parser.skip_info (lean.parser.tk ",")) (sum.inl <$> (lean.parser.tk ".." *> interactive.types.texpr) <|> sum.inr <$> (prod.mk <$> lean.parser.ident <* lean.parser.tk ":=" <*> interactive.types.texpr)) >>= λ (ls : list (pexpr ⊕ name × pexpr)), lean.parser.tk "}" >>= λ (_x : unit), (λ (_a : list pexpr × list (name × pexpr)), prod.cases_on _a (λ (fst : list pexpr) (snd : list (name × pexpr)), id_rhs ((λ (_a : list name × list pexpr), lean.parser pexpr) (list.unzip snd)) ((λ (_a : list name × list pexpr), prod.cases_on _a (λ (fst_1 : list name) (snd : list pexpr), id_rhs (lean.parser pexpr) (pure (pexpr.mk_structure_instance {struct := none name, field_names := fst_1, field_values := snd, sources := fst})))) (list.unzip snd)))) (list.partition_map id ls))>

Best error message ever

[Rob Lewis]

I'm guessing Kevin doesn't remember that it didn't always say "Try this:" :slight_smile:

[Kevin Buzzard]

I haven't seen it saying that yet!

[Kevin Buzzard]

gaargh I didn't restart Lean :D

[Rob Lewis]

Then you're not running the version of mathlib you claimed...

[Kevin Buzzard]

Woo!

[Rob Lewis]

Although, you raise a good point about suggest, why does it think rfl should prove ∀ n : ℕ, n=n?

[Rob Lewis]

Oh, it's messing up its implicit arguments.

[Patrick Massot]

What is funny is that suggest makes the same mistake one of beginners made a couple of weeks ago.

[Kevin Buzzard]

1 goal
a b c : set ℕ
⊢ a ⊆ a ∪ (b ∪ c)
scratch2.lean:5:2: information trace output
Try this: exact set.subset_union_left a (b ∪ c)
Try this: refine set.preimage_mono _
Try this: refine set.diff_eq_empty.mp _
Try this: refine set.diff_subset_iff.mp _
Try this: refine set.image_subset_iff.mp _
Try this: refine (set.mem_powerset_iff a (a ∪ (b ∪ c))).mp _
Try this: refine set.compl_subset_compl.mp _
Try this: refine set.preimage_subset_iff.mpr _
Try this: refine set.set_of_subset_set_of.mpr _
Try this: refine set.subset_of_mem_powerset _
Try this: refine set.subset_union_of_subset_left _ (b ∪ c)
Try this: refine set.subset_union_of_subset_right _ a
Try this: refine set.subset.trans _ _
Try this: refine set.sUnion_subset_iff.mp _ a _
Try this: refine (set.image_subset_image_iff _).mp _
Try this: refine (set.preimage_subset_preimage_iff _).mp _

I don't know which one to try!

[Patrick Massot]

You should have tried hint instead of suggest.

[Mario Carneiro]

At least the exact is at the top of the list

[Patrick Massot]

And this is yet another goal that norm_num mysteriously crushes :open_mouth:

[Mario Carneiro]

That's because norm_num > simp

[Patrick Massot]

I know, but I'm frequently surprised by this.

[Kevin Buzzard]

the following tactics make progress:
----
Try this: norm_num
Try this: finish
Try this: simp at *
Try this: intros1

But intros1 gives me unknown identifier 'intros1'

[Mario Carneiro]

I wish it were more restrictive, but people seem to be fine with it

[Patrick Massot]

And it's annoying when teaching. I want norm_num to kill only things like 1 < 3

[Mario Carneiro]

Have you tried using norm_num1? That does no simplification

[Patrick Massot]

intros1 should be tactic.intros1 probably

[Patrick Massot]

Too late for this year, but I'll try to remember next year (although next year I may teach using Lean 4!)

[Rob Lewis]

Patrick Massot said:

intros1 should be tactic.intros1 probably

Or just intro?

[Patrick Massot]

Of course the correct hint is intro, but suggest is trying to suggest intros1.

[Rob Lewis]

hint shouldn't return noninteractive tactics.

[Patrick Massot]

I guess we'll discover many small bugs in those tactics in the coming days while everybody tries to play with Try this

[Kevin Buzzard]

1 goal
⊢ 0 = 0
scratch2.lean:5:2: information trace output
the following tactics make progress:
----
Try this: omega
Try this: linarith
Try this: ring
Try this: norm_num
Try this: tauto
Try this: finish
Try this: solve_by_elim
Try this: fsplit
Try this: simp at *
Try this: exact dec_trivial
Try this: refl

I'm loving fsplit for that one. It does close it!

[Rob Lewis]

Partly my fault for not catching that in review, I assumed there was an interactive intro1.

[Mario Carneiro]

why aren't split and constructor on the list as well?

[Kevin Buzzard]

too easy

[Kevin Buzzard]

1 goal
⊢ 0 = 1
scratch2.lean:5:2: information trace output
the following tactics make progress:
----
Try this: norm_num

Loving the definition of "progress" there.

[Mario Carneiro]

I was hoping left would work too but it's too smart

[Rob Lewis]

Tagging @Scott Morrison so he sees suggestions for hint!

[Rob Lewis]

I don't think we need it running both split and fsplit, right?

[Patrick Massot]

Although, you raise a good point about suggest, why does it think rfl should prove ∀ n : ℕ, n=n?

@Scott Morrison any idea?

[Patrick Massot]

Also, we now have three tactics suggesting stuff to users: library_search, suggest and hint. Should we somehow merge them? Or do they have clearly delimited ranges (like hint is strictly for new users and suggest is slower than library search or something?).

[Jasmin Blanchette]

I'd say library_search has a quite different role to play than the other two and should be kept separate. There are all sorts of situations where you're looking for a specific lemma and not an arbitrary tactical proof.

[Rob Lewis]

suggest and library_search share most of an implementation but have different use cases, they should definitely stay separate.

[Rob Lewis]

One could argue that hint should call suggest, since applying a lemma is another tactic that can make progress.

[Rob Lewis]

But suggest will usually be way slower than hint.

[Patrick Massot]

Could you explain how suggest and library_search have different use cases?

[Rob Lewis]

Often I care if a lemma is in the library already, but not if some random terms make progress, since I know how to bash it away. library_search is what I want there, and it will stop as soon as it solves the goal. suggest potentially gives me a long list of things I don't care about and it takes a long time to find it.

[Rob Lewis]

Maybe it's reasonable to have hint! call both hint and suggest. I really don't think we should combine them by default though.

[Scott Morrison]

I diagnosed the "does rfl solve ∀ n : ℕ, n=n" bug at https://github.com/leanprover-community/mathlib/issues/2029. It seems to be a problem with the pretty printer, and I'm not sure how to work around it.