Can someone explain what's going on here?

Stream: mathlib4

[Dan Velleman]

Here's a silly file:

import Mathlib

example : True := by
  let A : Set (Nat × Nat) := {x | match x with | (a, b) => a > 0 ∧ b > 0}
  trivial

theorem test : True := by
  let A : Set (Nat × Nat) := {x | match x with | (a, b) => a > 0 ∧ b > 0}
  trivial

example : True := by
  let A : Set (Nat × Nat) := {x | match x with | (a, b) => a > 0 ∧ b > 0}
  trivial

If I position the cursor at the end of the first let line, then the tactic state includes this:

A : Set (ℕ × ℕ) := { x | _example.match_1 (fun x => Prop) x fun a b => a > 0 ∧ b > 0 }

If I position the cursor at the end of either the second or the third let line, then the tactic state includes this:

A : Set (ℕ × ℕ) := { x |
  match x with
  | (a, b) => a > 0 ∧ b > 0 }

Why the difference? The two examples are exactly the same; why does putting a theorem between them cause Lean to treat the second example differently? (And what does _example.match_1 mean?)

[Gabriel Ebner]

(deleted)

[Sebastian Ullrich]

Fixed by https://github.com/leanprover/lean4/pull/1880

[Dan Velleman]

Thanks. I wonder if the following behavior is related. This example works:

import Mathlib

theorem test : {x : Nat × Nat | match x with | (a, b) => a = b} ⊆ {x : Nat × Nat | x.1 = x.2} := by
  intro p
  intro h
  exact h

After intro h, the tactic state includes h : p ∈ { x | match x with | (a, b) => a = b }. But the following doesn't work:

import Mathlib

theorem test : {x : Nat × Nat | match x with | (a, b) => a = b} ⊆ {x : Nat × Nat | x.1 = x.2} := by
  intro p
  intro (h : p ∈ {x : Nat × Nat | match x with | (a, b) => a = b})
  exact h

I get a red squiggle under (a, b), and the error message is invalid pattern, constructor or constant marked with '[match_pattern]' expected. Shouldn't this work?
Will your change fix this too, or is it a different problem? Or am I doing something wrong?

[Sebastian Ullrich]

That looks like an unrelated bug. Could you file an issue with an MWE?

[Dan Velleman]

Will the example I gave count as a MWE? (I'm not sure I understand what counts as a MWE.)

[Sebastian Ullrich]

Mathlib should generally be avoided in an MWE :) . This issue should be independent of it.

[Dan Velleman]

OK, I think I have an example that doesn't require Mathlib:

example : ∀ (x : Nat × Nat), match x with | (a, b) => a = b → (x.1 = x.2) := by
  intro p
  intro (h : match p with | (a, b) => a = b)
  exact h

I get the same error on the intro. This should work, right?

[Dan Velleman]

Should I call this a problem with match? Or a problem with intro?

[Sebastian Ullrich]

Mmh, more probably intro?

[Sebastian Ullrich]

I don't think the usage intro (x : A) was intended to be honest, but it usually works as a pattern

[Dan Velleman]

I've been writing tactics for use by students learning to write proofs. One of my tactics is for introducing assumptions. I want students to write assume h : p. My tactic checks that the goal is an implication, and then it does intro (h : p). For students learning to write proofs, I think it might be helpful to ask them to state what they are assuming, so that Lean can correct them if they are confused about what the assumption is. And then it is helpful if h is listed in the tactic state as p, not something definitionally equal to p.

I'll file an issue.

[Dan Velleman]

I don't know if this is related, but I tried this:

theorem test (p : Nat × Nat) : (match p with | (a, b) => a = b) → (p.1 = p.2) := by
  intro h'
  have h : match p with | (a, b) => a = b := h'
  exact h

This works, but in the tactic state, h is listed as match p, h' with | (a, b), h' => a = b. Is that what it's supposed to be? Shouldn't it be what I said I wanted h to be?

[Sebastian Ullrich]

This is probably due to match auto generalization. I would avoid restating match terms like this. If you need the same match twice, it should be a function.

[Dan Velleman]

I was trying it as a possible workaround for the problem with intro (h : match ...). I thought perhaps my tactic, instead of calling intro (h : p), could instead do intro h'; have h : p := h'; clear h'. But it looks like that won't work if p is a match?