Behavior of 'have' tactic changing with imports

Stream: new members

[Andreas Gittis]

On a lean file with no imports, I get an error with the following:

theorem test_have2 (p q : Prop) : ((p ∧ ¬q) ∨ (q ∧ ¬p)) ↔ ((p ∨ q) ∧ ¬(p ∧ q)) := by
  have (h₁ : ((p ∧ ¬q) ∨ (q ∧ ¬p))) : (p ∨ q) ∧ ¬(p ∧ q) := by
    sorry
  sorry

The error appears as a red line under the h1 term and says:

type mismatch
  h₁
has type
  p ∧ ¬q ∨ q ∧ ¬p : Prop
but is expected to have type
  (p ∨ q) ∧ ¬(p ∧ q) : PropLean 4

In a lean file from the Mathematics in Lean repo, I can enter the same theorem as above, and there is no issue. The proof state after the 'have' tactic is:

α: Type u_1
stu: Set α
pq: Prop
h₁: p ∧ ¬q ∨ q ∧ ¬p
⊢ (p ∨ q) ∧ ¬(p ∧ q)

The stuff on top is from some variable declarations earlier in the file, but the point is the added context to the 'have' tactic appears with the given name. Here are the imports from the MIL file:

import Mathlib.Data.Set.Lattice
import Mathlib.Data.Nat.Prime
import Mathlib.Data.Nat.Parity
import MIL.Common

section
variable {α : Type*}
variable (s t u : Set α)
open Set

When the have : t := tactic is discussed in tutorials I don't remember encountering the option of putting extra context before the colon. Given the description it makes sense why it wouldn't be allowed (and anyway its the equivalent of an implication after the colon). However I wondered if it was possible and tried it in MIL and it seemed to work. Then when I used it outside of MIL I couldn't figure out what was going wrong. Can anyone explain why this happens? I assume there is something being imported from mathlib that allows you to do something you wouldn't be able to otherwise. If that's the case, is there a way to know which tactics have been adjusted/have different behavior due to imports and what those behaviors are? Thanks.

[Ruben Van de Velde]

Your have syntax makes no sense. I'm not sure why it would ever work

[Ruben Van de Velde]

Try

have h₁ : p ∧ ¬q ∨ q ∧ ¬p := by
  sorry

[Utensil Song]

The syntax that works in #mil seems to have the intention to make have ( h: p1 ) : p2 := by ... to mean have : p1 -> p2 := by intro h ..., mimicking the syntax for theorems.

[Utensil Song]

But throughout #mil there is no such usage taught and although MIL.Common modifies binder, pi types, it doesn't seem to be intentionally making this syntax work.

[Utensil Song]

The extension may be coming from Mathlib? https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Have.lean

[Andreas Gittis]

Ruben Van de Velde said:

Try

have h₁ : p ∧ ¬q ∨ q ∧ ¬p := by
  sorry

Well no it would have to be an implication from the context to the goal of the malformed have statement. Also I'm not trying to prove the theorem or write the have tactic, just to understand the discrepancy.

Utensil Song said:

The syntax that works in #mil seems to have the intention to make have ( h: p1 ) : p2 := by ... to mean have : p1 -> p2 := by intro h ..., mimicking the syntax for theorems.

Yes that seems to be exactly what it's doing, and it works for numerous inputs to the context as well.

Utensil Song said:

But throughout #mil there is no such usage taught and although MIL.Common modifies binder, pi types, it doesn't seem to be intentionally making this syntax work.

So I guess in an arbitrary Lean project the standard built-in tactics can be modified to do anything? Or other basic things about Lean can be changed so that the behavior of a built-in tactic changes unexpectedly, and a-priori there's not a clear way to know which tactics have been ultimately affected?

[Utensil Song]

The same tactic could have different behavior in raw Lean 4, Mathlib and the tutorial, but 3-layer is the max of it. People change tactic behaviors to make them feel natural to their audiences using meta-programming. It's a source of power and also confusion.

[Kevin Buzzard]

The behaviour of rw and induction is different in the natural number game to the behaviour in Lean/mathlib/etc for pedagogical reasons

[Utensil Song]

import Mathlib.Tactic.Have

theorem test_have2 (p q : Prop) : ((p ∧ ¬q) ∨ (q ∧ ¬p)) ↔ ((p ∨ q) ∧ ¬(p ∧ q)) := by
  have (h₁ : ((p ∧ ¬q) ∨ (q ∧ ¬p))) : (p ∨ q) ∧ ¬(p ∧ q) := by
    sorry
  sorry

This #mwe seems to work.

[Utensil Song]

As well as an additional attempt to add a name to the preposition:

theorem test_have3 (p q : Prop) : ((p ∧ ¬q) ∨ (q ∧ ¬p)) ↔ ((p ∨ q) ∧ ¬(p ∧ q)) := by
  have my_p (h₁ : ((p ∧ ¬q) ∨ (q ∧ ¬p))) : (p ∨ q) ∧ ¬(p ∧ q) := by
    sorry
  sorry

[Eric Wieser]

I think this is a deliberate feature like let f (x : A) : A := x ^ 2 which I think is also legal

[Eric Wieser]

import Mathlib.Tactic is a fairly safe import to add to any code you write to get all the mathlib-specific features

[Eric Wieser]

Though maybe this version of have belongs in Std?

[Mario Carneiro]

I think it's in core?

[Mario Carneiro]

the only thing mathlib adds is have-without-:=

[Mario Carneiro]

Andreas Gittis said:

On a lean file with no imports, I get an error with the following:

theorem test_have2 (p q : Prop) : ((p ∧ ¬q) ∨ (q ∧ ¬p)) ↔ ((p ∨ q) ∧ ¬(p ∧ q)) := by
  have (h₁ : ((p ∧ ¬q) ∨ (q ∧ ¬p))) : (p ∨ q) ∧ ¬(p ∧ q) := by
    sorry
  sorry

I can't replicate this. I think this behavior might have changed, so possibly your lean version is out of date relative to the one in MIL

[Andreas Gittis]

Utensil Song said:

The same tactic could have different behavior in raw Lean 4, Mathlib and the tutorial, but 3-layer is the max of it. People change tactic behaviors to make them feel natural to their audiences using meta-programming. It's a source of power and also confusion.

Okay thanks. I think I will be doing pretty much everything in Mathlib anyway, but it's good to know.

Mario Carneiro said:

I can't replicate this. I think this behavior might have changed, so possibly your lean version is out of date relative to the one in MIL

It looks like my MIL Lean is version 4.0.0-nightly-2023-08-23, and the other is version 4.0.0-nightly-2023-04-20. I assumed whenever I used VS Code the version of Lean was consistent, which is definitely not the case - every directory I look at has a different version. When I changed to a new directory the error went away. So it looks like the different have behavior was a result of different Lean versions (sorry about that :sweat_smile: ) but it is possible for tactics to have different behaviors in different projects. Thanks everyone who responded.

[Mario Carneiro]

@Andreas Gittis For reproducibility, the lean version used by your project is specified in the lean-toolchain file. It is recommended to bump that to the latest (e.g. by copying the lean-toolchain of the mathlib4 repo) periodically. (Unfortunately there is not yet a tool that will do the bumping automatically. cc: @Sebastian Ullrich , elan update stable will download the latest stable but it doesn't actually put it in the lean-toolchain, right?)

[Mario Carneiro]

oh wait, elan update stable actually downloads v3.51.1, that's not latest... (ah, it does v4.1.0 after elan self update)

[Utensil Song]

The syntax (the example with my_p) seems to work out-of-the-box on https://live.lean-lang.org/ without Mathlib import (or locally with leanprover/lean4:v4.2.0-rc1), so it's implemented in Lean itself.

[Utensil Song]

Syntax-wise it's parsed by this line in Lean.Parser.Term

def haveIdLhs    := ((ppSpace >> binderIdent) <|> hygieneInfo) >> many (ppSpace >> letIdBinder) >> optType

where letIdBinder can have bracketedBinder which are the familiar (h₁ : ((p ∧ ¬q) ∨ (q ∧ ¬p))) in theorems and optType is the optional type spec (i.e. : + the proposition statement of type Prop here).

And the elaboration is inherited somehow I assume.