(kernel) application type mismatch

Stream: new members

[Snir Broshi]

import Mathlib
theorem Nat.foo {n : ℕ} (h : Even n) : n ^^^ 1 = n + 1 := by
  cases n
  · simp [HXor.hXor, instXorOp, xor]
  · simp [HXor.hXor, instXorOp, xor, bitwise, even_iff.mp h, ← mul_two, div_two_mul_two_of_even h]

gives the following error:

(kernel) application type mismatch
  @Eq.ndrec ℕ 0 (fun {n} => Even n → n ^^^ 1 = n + 1) fun h =>
    of_eq_true
      (Eq.trans
        (congr
          (congrArg Eq
            (Eq.trans (bitwise_zero_left 1)
              (ite_cond_eq_true 1 0
                (Eq.trans (congrArg (fun x => x = true) (Eq.trans (Bool.bne_true false) Bool.not_false))
                  (eq_self true)))))
          (zero_add 1))
        (eq_self 1))
argument has type
  Even 0 → bitwise bne 0 1 = 0 + 1
but function has type
  (fun {n} => Even n → n ^^^ 1 = n + 1) → ∀ {b : ℕ}, 0 = b → fun {n} => Even n → n ^^^ 1 = n + 1

The first branch can just be rfl, but this simp causes this strange error.
Is this a bug?

[Alfredo Moreira-Rosa]

not sure what's the issue, but this fixes it :

import Mathlib

theorem Nat.foo {n : ℕ} (h : Even n) : n ^^^ 1 = n + 1 := by
  cases n
  · simp
  · simp [HXor.hXor, XorOp.xor, xor, bitwise, even_iff.mp h, ← mul_two, div_two_mul_two_of_even h]

[Snir Broshi]

Yes like I said rfl fixes it, and simp here isn't that different, but the question is whether that's a bug

[Ruben Van de Velde]

Sounds like a bug

[Ruben Van de Velde]

Does it happen without mathlib imports? (Replacing \N by Nat)

[Snir Broshi]

Ruben Van de Velde said:

Does it happen without mathlib imports? (Replacing \N by Nat)

Yes, here are 2 examples without mathlib:

theorem Nat.foo (n : Nat) : n ^^^ 0 = n ^^^ 0 := by
  cases n
  · simp only [HXor.hXor, instXorOp, xor, bitwise, Bool.bne_true, Bool.not_false, ↓reduceIte]
  · sorry

theorem Nat.foo' : 0 ^^^ 0 = 0 ^^^ 0 := by
  simp only [HXor.hXor, instXorOp, xor, bitwise, Bool.bne_true, Bool.not_false, ↓reduceIte]

[Robin Arnez]

Oh this is a bad one; it eagerly reduces 0 ^^^ 0 through the natural number reduction things to 0 but it can't do the same with bitwise bne 0 0 because Nat.bitwise is defined through wellfounded recursion:

example : Nat.bitwise bne 0 0 = 0 ^^^ 0 := rfl -- fails even though that's the definition

[Robin Arnez]

The solution is probably fuel?

[Snir Broshi]

Robin Arnez said:

The solution is probably fuel?

A workaround specifically for xor might be nice, but isn't this a bug in Lean itself? (probably in simp)

[Snir Broshi]

If simp fails it should not throw an error, at most a warning

[Robin Arnez]

Well, it's a bug but more so in definitional equality than in simp:

-- works, basically just unfolding (which is part of what rfl should be capable of)
example : Nat.xor 0 0 = Nat.bitwise bne 0 0 := by rw [Nat.xor]

-- fails
example : Nat.xor 0 0 = Nat.bitwise bne 0 0 := rfl

In particular, it's the special casing for Nat.xor that clashes with regular unfolding. That means that the definitional equality checker won't even try to unfold Nat.xor and instead just uses its capabilities to reduce it directly to 0. However, it would need to unfold Nat.xor to be able to see that this is a true equality.

[Ruben Van de Velde]

So yes, this is a bug in lean and you should file an issue on GitHub leanprover/lean4

[Snir Broshi]

Thanks for confirming, opened lean4#11181