Term to tactic error

Stream: lean4

[Ioannis Konstantoulas]

The following snippet works fine:

theorem ne_self (n a b : Nat) : (a < b) ∧ (a = n) ∧ (b = n) → (n < n) :=
  fun ⟨ineq, an, bn⟩ =>
    have := an ▸ bn ▸ ineq
    by exact this

But, rewriting directly as a term,

theorem ne_self2 (n a b : Nat) : (a < b) ∧ (a = n) ∧ (b = n) → (n < n) :=
  fun ⟨ineq, an, bn⟩ =>
     an ▸ bn ▸ ineq

produces the error

invalid `▸` notation, expected result type of cast is
  a < a
however, the equality
  bn
of type
  b = n
does not contain the expected result type on either the left or the right hand side

I thought the two snippets were equivalent as Lean code, and I would think the second snippet is correct code; am I making a mistake, do I need to write an explicit cast somewhere, or is this a bug? I am using

Lean (version 4.0.0-nightly-2023-08-05, commit 254582c00040, Release)

[Marcus Rossel]

Hmm, even just adding an explicit type for this causes the error, too:

example (n a b : Nat) : (a < b) ∧ (a = n) ∧ (b = n) → (n < n) :=
  fun ⟨ineq, an, bn⟩ =>
    have : n < n := an ▸ bn ▸ ineq -- error
    by exact this

[Ioannis Konstantoulas]

Should I open an issue for this? Is it a bug?

[Scott Morrison]

No, it's not a bug. The elaboration procedure is different when there is an expected type.

[Scott Morrison]

In this situation you can usually write by exact an ▸ bn ▸ ineq, leaving out the have step.

[Scott Morrison]

You'll find plenty of by exact X in the library, where just plain X doesn't typecheck.

[Ioannis Konstantoulas]

If one wanted to avoid tactics, how would one proceed?

[Scott Morrison]

(Although I'm now noticing that many of these do actually typecheck with just plain X. If someone wants to do a clean-up pass on the library for this I would happily merge. :-)

[Scott Morrison]

I would proceed by deciding not to avoid tactics. :-)

[Ioannis Konstantoulas]

But the following also fails:

theorem ne_self (n a b : Nat) : (a < b) ∧ (a = n) ∧ (b = n) → (n < n) :=
  fun ⟨ineq, an, bn⟩ =>
    by exact an ▸ bn ▸ ineq

[Scott Morrison]

theorem ne_self (n a b : Nat) : (a < b) ∧ (a = n) ∧ (b = n) → (n < n) :=
  fun ⟨ineq, an, bn⟩ => by exact (an ▸ bn ▸ ineq : _)

works

[Scott Morrison]

(This removes the expected type.)

[Scott Morrison]

Ah:

theorem ne_self (n a b : Nat) : (a < b) ∧ (a = n) ∧ (b = n) → (n < n) :=
  fun ⟨ineq, an, bn⟩ => (an ▸ bn ▸ ineq : )

is what you want.

[Scott Morrison]

But I think this is just syntactical sugar, nothing profound. I forget where (x : ) is defined.

[Ioannis Konstantoulas]

OK; although I am losing heart a bit.

[Scott Morrison]

Sorry. :-) Could you say why? If it is that you are sad that whether or not there is an expected type affects elaboration, then I think you should be happy instead that you can control elaboration in this way. :-)

[Scott Morrison]

Note that my last suggestion "avoids tactics".

[Ioannis Konstantoulas]

I am sad because the original code is very simple, something I wrote as a beginner following instructions from the books, and fails due to an issue I cannot be expected to understand at this point. I.e. there is a gap between the level of the code, and the nature of the failure. I have gotten stuck like this several times.

Furthermore, the error message Lean gives is:

invalid `▸` notation, expected result type of cast is
  a < a
however, the equality
  bn
of type
  b = n
does not contain the expected result type on either the left or the right hand side

which is baffling to me, because the substitution is supposed to target the inequality, so why is Lean complaining about one of the two equations?

[Scott Morrison]

I'm curious actually, which book is teaching ▸? I would say that ▸ is an advanced topic for obsessive code golfers, and everyone else should be using rw!

[Scott Morrison]

(Less strongly, the same sentiment for term mode vs tactic mode.)

[Richard Copley]

TPIL teaches term mode first. Tactics are chapter 5. See the examples above the exercise at the end of <https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html>.

[Notification Bot]

A message was moved here from #lean4 > mmap by Buster.

[Ruben Van de Velde]

Scott Morrison said:

(Although I'm now noticing that many of these do actually typecheck with just plain X. If someone wants to do a clean-up pass on the library for this I would happily merge. :-)

These wouldn't be for performance reasons, would they? But that's maybe worth re-checking anyway now that we're in lean 4

[Scott Morrison]

Oof, some may be for performance reasons, I guess. The ones I noticed still seemed instant after I removed them.

If any are for performance reasons, ideally they would have a comment saying so ... but I know Mathlib isn't (yet) like that. :-)

[Kevin Buzzard]

@Ioannis Konstantoulas the triangle symbol attempts to perform higher order unification, which is known to be an undecidable problem. I think that an algorithm which provably cannot always work, failing to work in your use case without some hints, is not a reason to lose heart.

[Kevin Buzzard]

The rw tactic is a far more robust version of the triangle, using a more sophisticated algorithm. If you want to avoid tactics then you can simply tell lean the explicit motive (this is the part for which there is no algorithm) and you will have much more luck with the triangle. But the whole point of tactics is to make your life easier in these situations.

[Mario Carneiro]

My experience is that the lean 4 ▸ is much more robust than the lean 3 ▸, and no longer avoid it in new code. It is basically equivalent to:

by
  first
  | rw [h]; exact e
  | rw [<- h]; exact e
  | have := e; rw [h] at e; exact this
  | have := e; rw [<- h] at e; exact this

In other words, it's like rw, but in a more "do what I mean" sense, it tries a few things that could be intended and takes the one that would make progress.

[Mario Carneiro]

The lean 2 ▸ was much more powerful than either lean 3 or lean 4 and would do full HO unification with backtracking. You could do some magic with it (like rewriting an unspecified subset of the occurrences of the LHS in the goal) but it was liable to cause performance issues which is why it was scrapped in lean 3 in favor of a deterministic algorithm (just replace everything) which users can better reason about. Lean 4 ▸ does not try to do this either, it's just rewriting backwards and forwards with rw, so mostly you can just think of it as the term-mode syntax for rw.