Zulip Chat Archive

I'm currently about 1/3 of the way through porting Data.Fin.Basic and I ran into an interesting problem. I tried to minimize it, but I can maybe take it further if need be. The problem is that some variables were declared at the beginning of the file, and in one declaration they were not used, but Lean still assumed that they were, so they were included in the type signature. In Lean 3 if this sort of problem came up we could use omit, but that's not an option anymore. (EDIT: ignore the mwe and look at the message with foo below)

mwe

import Mathlib.Algebra.Order.WithZero
import Mathlib.Order.RelIso.Basic

variable {n m : Nat}
variable {a b : Fin n} -- everything is fine until the last declaration!

namespace Fin

theorem val_injective : Function.Injective (@Fin.val n) :=
  @Fin.eq_of_veq n

#check @val_injective

instance {n : ℕ} : LinearOrder (Fin n) :=
  @LinearOrder.lift (Fin n) _ _ ⟨fun x y => ⟨max x y, max_rec' (· < n) x.2 y.2⟩⟩
    ⟨fun x y => ⟨min x y, min_rec' (· < n) x.2 y.2⟩⟩ Fin.val Fin.val_injective (fun _ _ => rfl)
    fun _ _ => rfl

#check Fin.instLinearOrderFin

@[simps apply]
def valEmbedding : Fin n ↪ ℕ :=
  ⟨val, val_injective⟩

#check @valEmbedding

@[simps apply]
def valOrderEmbedding (n) : Fin n ↪o ℕ :=
  ⟨valEmbedding, Iff.rfl⟩

#check @valOrderEmbedding

/-- The ordering on `Fin n` is a well order. -/
instance Lt.isWellOrder (n) : IsWellOrder (Fin n) (· < ·) :=
  OrderEmbedding.isWellOrder (valOrderEmbedding n)

#check @Lt.isWellOrder

theorem one_pos : (0 : Fin (n + 2)) < 1 :=
  Nat.succ_pos 0

#check @one_pos

theorem zero_ne_one : (0 : Fin (n + 2)) ≠ 1 :=
  ne_of_lt one_pos

#check @zero_ne_one

@[simp]
theorem zero_eq_one_iff : (0 : Fin (n + 1)) = 1 ↔ n = 0 := by
  constructor
  · cases n <;> intro h
    · rfl
    · exact False.elim <| zero_ne_one h
  · rintro rfl
    rfl

#check @zero_eq_one_iff
-- @zero_eq_one_iff : ∀ {n : ℕ} {a b : Fin n}, 0 = 1 ↔ n = 0

Jireh Loreaux (Dec 16 2022 at 21:06):

I think the reason this might be happening is that the proof does cases n and a b : Fin n, so these are affected by the cases, which makes Lean think these variables were used.

Jireh Loreaux (Dec 16 2022 at 21:10):

Confirmed.

variable {n : Nat}
variable {a : Fin n}

theorem foo (c : Fin n) : c = c := by
  cases n
  · rfl
  · rfl

#check @foo
-- @foo : ∀ {n : Nat} {a : Fin n} (c : Fin n), c = c

theorem bar (c : Fin n) : c = c := rfl

#check @bar
-- @bar : ∀ {n : Nat} (c : Fin n), c = c

Jireh Loreaux (Dec 16 2022 at 21:15):

One short-term workaround is to do clear a before cases, but that seems really gross. This feels like a bug to me, but I'll wait for someone with more knowledge to weigh in.

Kevin Buzzard (Dec 16 2022 at 21:18):

Oh that's interesting! I've seen tactic states which are randomly full of variables you're not using, but I had the impression that the actual signature of the declaration didn't mention them. But here clearly a should not be involved, and yet is.

Jireh Loreaux (Dec 16 2022 at 21:22):

Right, I think what happens is that it looks through the proof to see if you used them and if you didn't, then it omits them, but if you did then they are included. In this case, I think it's getting confused because when you do cases n then you get (in the first case) a : Fin Nat.zero in the tactic state. I assume then that the term being produced includes this modification to a somehow, even though it wasn't necessary, and then Lean includes it in the type signature.