Can't unify seemingly identical terms

Stream: new members

[Daniel Weber]

I'm trying to prove a theorem in additive combinatorics, but there's a weird bug - when I'm trying to do exact to something which looks like the goal, it fails to unify. A #mwe:

import Mathlib

open Classical Pointwise

lemma card_of_inv {α : Type*} [Field α] [Fintype α] (A : Finset α) (a : α) (h : a ≠ 0) : (a • A).card = A.card := by
  sorry

theorem GUS (p : ℕ) [Fact (p.Prime)] (A : Finset (ZMod p)) : (3 • A^2 - 3 • A^2).card ≥
    ((min (A.card^2) p) / 2 : ℚ) := by
  rw [ge_iff_le]
  have a : ZMod p := sorry
  have b : ZMod p := sorry
  have c : ZMod p := sorry
  have d : ZMod p := sorry
  calc ((min (A.card^2) p) / 2 : ℚ)
    _ ≤ (A + ((a - b) / (c - d) + 1) • A).card := by
      sorry
    _ = ((c - d) • (A + ((a - b) / (c - d) + 1) • A)).card := by
      norm_cast
      apply Eq.symm
      have : c - d ≠ 0 := sorry
      have := card_of_inv (α := ZMod p) (a := c - d) (h := this) (A := (A + ((a - b) / (c - d) + 1) • A))
      exact this
      -- type mismatch
      --   this
      -- has type
      --   ((c - d) • (A + ((a - b) / (c - d) + 1) • A)).card = (A + ((a - b) / (c - d) + 1) • A).card : Prop
      -- but is expected to have type
      --   ((c - d) • (A + ((a - b) / (c - d) + 1) • A)).card = (A + ((a - b) / (c - d) + 1) • A).card : Prop
      sorry
    _ ≤ _ := sorry

Additionally, if I try to end the calc with (3 • A^2 - 3 • A^2).card it fails, with:

'calc' tactic failed, has type
  ↑(min (A.card ^ 2) p) / 2 ≤ ?m.24439
but it is expected to have type
  ↑(min (A.card ^ 2) p) / 2 ≤ ↑(3 • A ^ 2 - 3 • A ^ 2).card

I don't know if this is related. Regardless, what's going on there, and are there general ways to debug something like this?

[Daniel Weber]

In fact

import Mathlib

open Classical Pointwise

lemma card_of_inv {α : Type*} [Field α] [Fintype α] (A : Finset α) (a : α) (h : a ≠ 0) : (a • A).card = A.card := by
  sorry

lemma card_of_inv_zmod (p : ℕ) [Fact (p.Prime)] (A : Finset (ZMod p)) (a : ZMod p) (h : a ≠ 0) : (a • A).card = A.card := by
  have := card_of_inv A a h
  exact this

already fails, so it shouldn't be related to the calc. I'm suspecting there might be a diamond or something, but I don't know what to do about that

[Daniel Weber]

Oh, I figured it out, there's a diamond with DecidableEq α. Removing Classical and adding DecidableEq works, although calc still fails. I realized I should try and remove Classical for my whole project, but I have another problem: is DecidableEq and DecidableMem for submodules over a DecidableEq Fintype defined somewhere?

[Notification Bot]

This topic was moved here from #general > Can't unify seemingly identical terms by Riccardo Brasca.

[Riccardo Brasca]

Can you write precisely what you are looking for? A #mwe would be great

[Daniel Weber]

Sure:

import Mathlib

variable {α : Type*} [Field α] [Fintype α] [DecidableEq α]

def Line (α : Type*) [Ring α] := {x : Submodule α (α × α × α) // FiniteDimensional.finrank α x = 2}

instance instSetLike : SetLike (Line α) (α × α × α) where
  coe x := x.val
  coe_injective' x1 x2 h := by
    apply Subtype.ext
    simp_all

instance mem2 : Membership (α × α) (Line α) where
  mem x l := ⟨x.1, x.2, 1⟩ ∈ l

instance instDecidableMem2 (x : α × α) (y : Line α) : Decidable (x ∈ y) := inferInstance -- fails

instance instDecidableEqLine : DecidableEq (Line α) := inferInstance -- fails

[Riccardo Brasca]

Are you really interested in these instances or you want them just because Lean is complaining? It Lean wants them is a proof you can just start the proof with classical and the problem will disappear.

[Daniel Weber]

Riccardo Brasca said:

Are you really interested in these instances or you want them just because Lean is complaining? It Lean wants them is a proof you can just start the proof with classical and the problem will disappear.

But wouldn't that potentially cause a diamond?

[Kyle Miller]

You're not going to be able to create these two instances. These are additional assumptions you'll have to add to theorems if you don't want to go with classical.

[Kyle Miller]

For your original problem, do you know about convert? It's like exact, but it tries to handle dealing with small differences between terms automatically, and for whatever it can't handle you get new subgoals.

[Kyle Miller]

If you replace exact this with convert this, it works.

[Riccardo Brasca]

Daniel Weber said:

Riccardo Brasca said:

Are you really interested in these instances or you want them just because Lean is complaining? It Lean wants them is a proof you can just start the proof with classical and the problem will disappear.

But wouldn't that potentially cause a diamond?

Using classical in a proof is fine. In your previous example you used it in the statement, and that can indeed create diamond.

[Kevin Buzzard]

In your initial example all those have a : ZMod p := should be let a : ZMod p := btw

[Kevin Buzzard]

The basic rule for classical/decidable is that if you can state the theorems without decidability then do this and use the classical tactic in the proof and you'll be fine.

[Daniel Weber]

Kyle Miller said:

For your original problem, do you know about convert? It's like exact, but it tries to handle dealing with small differences between terms automatically, and for whatever it can't handle you get new subgoals.

Interesting, I didn't know of it, thanks

[Bolton Bailey]

Concerning to me that this is giving the unhelpful error message where it reports a distinction between terms that are visually identical. I thought we fixed this issue. Isn't the error message supposed to automatically show the more elaborate terms when the pretty-printings are equal?

[Bolton Bailey]

@Joachim Breitner

[Bolton Bailey]

lean4#3234 was the relevant PR. Maybe that only fixed apply and not exact?

[Joachim Breitner]

My PR wasn’t good and I ran out of cycles for this feature; it needs more refactoring to make the error message “lazy enough“ so that you don’t run an expensive algorithm when the users never sees the message (e.g. when backtracking tactics.)