proof finishes too soon?

Stream: new members

[rzeta0]

I tried experimenting with creating my first definition. That seemed to work.

However, when testing it, the proof seemed to finished before I expected, with "no goals".

import Mathlib.Tactic

def Triangle (a : ℕ) : Prop := ∃ n, a = n * (n + 1)

example : Triangle 20 := by
  dsimp [Triangle]
  use 4
  -- < -- apparently resolved ?!
  -- < ---no calc? no norm_num ?

I was expecting there would be a goal remaining to prove after use 4, typically resolved with a calc or a simple norm_num ..

I say, expecting, because this is my experience with existence proofs following the Mechanics of Proof.

---

(I realise n*(n+1) isn't a triangle number .. I'll have to grapple with division by 2 with Nat later. )

[Damiano Testa]

If I remember correctly, use tries a weak from of rfl on the remaining goal and it looks like in this case it might be enough to prove the assertion about natural numbers.

[rzeta0]

Thanks Damiano - is there a form of use that doesn't do that? That only rewrites the goal's variable with the chosen value?

[rzeta0]

(also I don't now what rfl is .. everyone mentions it so perhaps I should find out)

[Damiano Testa]

You could try refine \<4, ?_\> instead of use 4 (untested).

[Damiano Testa]

This is instructing lean to construct the existential by filling in 4 as the first parameter and creating a goal for the second.

[Damiano Testa]

rfl means "check that the two sides of an equality are equal by definition", where definition is a very limited selection of equalities.

[rzeta0]

Thanks - that's useful for me to know.

I won't create an example with it as refine looks too much for the level we're at in the beginners course.

I'll just accept that use is sometimes going to be too clever!

[rzeta0]

Last question - is this cleverness by use a new behaviour in recent Lean versions?

I'm wondering why none of the Mechanics of Proof examples and exercises hit this behaviour? Perhaps MoP is pinned to an older specific version of Lean?

[Damiano Testa]

No, I remember it from lean 3, and I simply assumed that it stayed in lean 4.

[Damiano Testa]

It is actually not too easy to have use x close the goal "in real life", as normally there is some actual proof to be done to check that the predicate holds for the witness that you provided.

[rzeta0]

I'm now seeing "too clever" behaviour here:

def Triangle (a : ℕ) : Prop := ∃ n, a = n * (n + 1) / 2

example : Triangle (1 + 2 + 3 + 4 + 5) := by
  dsimp [Triangle]

and the goal state is

unsolved goals
⊢ ∃ n, 15 = n * (n + 1) / 2

what I would have expected is:

unsolved goals
⊢ ∃ n, 1+2+3+4+5 = n * (n + 1) / 2

[Damiano Testa]

dsimp is another way of getting lean to rewrite using equalities that hold by rfl (more or less).

[rzeta0]

ok - I didn't know that. I thought dsimp was only used to show the actual definition of a def in the info view, unfolding I believe it is called.

(src https://hrmacbeth.github.io/math2001/03_Parity_and_Divisibility.html?highlight=dsimp#example )

[Damiano Testa]

dsimp roughly uses simp lemmas whose proof is rfl (or maybe also by rfl, I forget the details).

[Damiano Testa]

This means that, depending on how your proof continues, dsimp is possibly superfluous.

[Damiano Testa]

If you just want to unfold a definition, unfold <definition> should do just that.

[rzeta0]

I wonder why the MoP course introduces dsimp and not unfold?

[Kevin Buzzard]

For a weaker use you can try existsi if that still exists in lean 4, it solved the problem of use being "too smart" in lean 3 but I can't remember if it survived the port. I had the same sort of problem with rw trying a weak rfl when it was done, meaning that some levels of NNG would finish early, confusing users

[Kevin Buzzard]

rzeta0 said:

I wonder why the MoP course introduces dsimp and not unfold?

Because usually we want to get things done, and finishing early is usually helpful.

[Kevin Buzzard]

You could try dsimp only [Triangle] -- that might (or might not) do less.

[Damiano Testa]

Probably also because dsimp leaves you in a state that is likelier yo have better automation, via exact? for instance.

[Damiano Testa]

(d)simp lemmas are chosen to leave you in a better state after you apply them and a lot of basic results start from where (d)simp would leave you to make further progress.

[Kevin Buzzard]

To someone who's writing a theorem prover, probably the mental model they have of their users is that the more help they get, the better. I agree that sometimes this goes against principles of teaching. One thing I did in NNG was to weaken rw so that it didn't try rfl afterwards, but this was problematic in the sense that when people switched from NNG to real lean they were confused, as opposed to being confused when playing NNG. Teaching is hard!

[rzeta0]

Kevin, you've described the challenge of teaching with a tool intended to get stuff done!

Thanks both for your insightful replies.

[rzeta0]

(I think I will have to go back and redo the examples that used dsimp and change them to unfold. I had also promised readers that dsimp only changed what was shown in info view, but this is clearly false)

[Mario Carneiro]

Kevin Buzzard said:

For a weaker use you can try existsi if that still exists in lean 4, it solved the problem of use being "too smart" in lean 3 but I can't remember if it survived the port. I had the same sort of problem with rw trying a weak rfl when it was done, meaning that some levels of NNG would finish early, confusing users

It's called exists in lean 4

[rzeta0]

I just tried exists and it also competes the proof sooner than expected.

[Damiano Testa]

The doc-string of exists mentions that it tries trivial after passing the witnesses.

[Dan Velleman]

Another possibility is apply Exists.intro 4.

[Heather Macbeth]

Here's the configuration used in Mechanics of Proof to "dumb down" use:
https://github.com/hrmacbeth/math2001/blob/main/Library/Config/Use.lean

[Heather Macbeth]

Note that MoP is still on Lean v4.3.0, so I can't promise this will still work on current Lean (bumping is a constant fight against core tactics getting cleverer). edit: seems still to work

[Heather Macbeth]

rzeta0 said:

I'm now seeing "too clever" behaviour here:

def Triangle (a : ℕ) : Prop := ∃ n, a = n * (n + 1) / 2

example : Triangle (1 + 2 + 3 + 4 + 5) := by
  dsimp [Triangle]

and the goal state is

unsolved goals
⊢ ∃ n, 15 = n * (n + 1) / 2

what I would have expected is:

unsolved goals
⊢ ∃ n, 1+2+3+4+5 = n * (n + 1) / 2

You can make dsimp less clever here by including the line

attribute [-simp] Nat.reduceAdd

[Heather Macbeth]

(this particular too-clever feature of (d)simp dates from lean4#3124, in v4.6.0)

[Heather Macbeth]

Summary: this behaves the way you want on current Lean

import Mathlib.Tactic

attribute [-simp] Nat.reduceAdd
macro_rules | `(tactic| use_discharger) => `(tactic| skip)

def Triangle (a : ℕ) : Prop := ∃ n, 2 * a = n * (n + 1)

example : Triangle (1 + 2 + 3 + 4 + 5) := by
  dsimp [Triangle]
  use 5
  norm_num

[Kyle Miller]

Here's the list of tactics use uses to discharge trivial side goals: https://github.com/leanprover-community/mathlib4/blob/5b47f1161179e5293ffb65d3e5d16f5de2c6846a/Mathlib/Tactic/Use.lean#L141

[Kyle Miller]

I think the syntax is use (discharger := skip) 4 to skip discharging.

[Kyle Miller]

Heather's suggestion permanently disables discharging, this syntax is to do one-off disabling.

[Edward van de Meent]

using dsimp only [Triangle] works wonders here, actually