use and exists_prop

Stream: general

[Patrick Massot]

For teaching purposes, I wonder whether we should slightly modify use to try rw exsists_prop at the end. It shouldn't break too many proofs since you can still use use when the goal is a conjunction

[Patrick Massot]

I'm thinking of goal that look like ∃ δ > 0, ... where the goal becomes ∃ (H : δ > 0), ... after giving the required δ

[Johan Commelin]

I think this is a very good idea if we want this tactic to be user-friendly.

[Johan Commelin]

You have my vote.

[Johan Commelin]

/me wrote edited his first tactic...

[Johan Commelin]

Voila:

namespace tactic
namespace interactive
open interactive interactive.types

meta def use_this (l : parse pexpr_list_or_texpr) : tactic unit :=
(tactic.use l >> (triv <|> try `[rw exists_prop]))

end interactive
end tactic

[Johan Commelin]

In fact, I would rather see that ∃ p ≥ n, prime p is expanded to the sane thing as soon as I enter the begin end-block.
Now I see ∃ (p : ℕ) (H : p ≥ n), prime p, which is of course quite ugly. Can't some magic in begin turn this into
∃ (p : ℕ), p ≥ n ∧ prime p immediately?

[Johan Commelin]

@Keeley Hoek you seem to be able to make begin do magic tricks. Is this something that could be done?

[Reid Barton]

Well, in general, we don't want begin to replace things by non-defeq things

[Johan Commelin]

I wish ∃ p ≥ n, prime p was syntactic sugar for ∃ (p : ℕ), p ≥ n ∧ prime p.

[Johan Commelin]

I would like set_option newbie_mode true that would fix some of these things.
Even if we don't want that option in mathlib.

[Reid Barton]

Maybe better than rw exists_prop would be whatever the version with apply would be, so that it only applies at the outermost position

[Johan Commelin]

Hmm, that makes sense.

[Patrick Massot]

I'm revisiting an old thread since it's Lean-teaching time again. Should we replace https://github.com/leanprover-community/mathlib/blob/3053a16942cf8bc388eb4758cf9f9f5c0ff02ccb/src/tactic/interactive.lean#L615-L616 by:

meta def use (l : parse pexpr_list_or_texpr) : tactic unit :=
do tactic.use l,
   try triv,
   try (do
           `(Exists %%p) ← target,
           to_expr ``(exists_prop.mpr) >>= tactic.apply >> skip)

I tried and it doesn't break mathlib. I guess one could use a more primitive approach without using apply but I have no idea whether it would be faster.

[Patrick Massot]

Recall the goal is to avoid ∃ δ > 0 becoming ∃ (H : δ > 0) after calling use.

[Reid Barton]

Probably best to wrap it in a focus1 $ , so the trys can't randomly affect other goals (not sure this is possible with the current version of use)

[Patrick Massot]

Thanks Reid. See https://github.com/leanprover-community/mathlib/pull/1882.

[Yury G. Kudryashov]

BTW, how hard would be making use a as good in reporting errors as refine ⟨a, _⟩. Currently if I make a typo in a, it fails with very uninformative message, and I have to write let a := ... or have a := ... first to find out what's wrong.

[Rob Lewis]

This is added to my list of things to think about when I have spare cycles, but it sounds generally fine to me.

[Rob Lewis]

BTW, how hard would be making use a as good in reporting errors as refine ⟨a, _⟩. Currently if I make a typo in a, it fails with very uninformative message, and I have to write let a := ... or have a := ... first to find out what's wrong.

use is more general, since use a doesn't know the pattern ⟨a, _⟩. It will work for something like ⟨⟨a, _⟩, _⟩ as well. Perhaps the error messages can be improved.

[Reid Barton]

Yeah, I never use use, because refine is already ingrained and there's a ~25% chance I have a type error in which case I will need to change it to refine to get a useful error message.

[Kevin Buzzard]

I always use use, because I am often writing Lean code in front of people who have very little clue about Lean, and the word use explains really well what is going on. When it works, it works great.

[Kevin Buzzard]

I suspect Patrick will be in a similar position this term.