v4.8.0-rc1 issue

Stream: batteries

[François G. Dorais]

I can't make sense of this error message. I don't know if this is a std or a core issue. I'm still in the process of minimizing but this is sufficiently self-contained for others to help investigate.

import Std

namespace ASCII

/-- Uppercase letter -/
@[inline] def isUpper (c : UInt8) :=
  65 ≤ c.toNat && c.toNat ≤ 90

theorem isUpper_iff (c : UInt8) : ASCII.isUpper c ↔ 65 ≤ c.toNat && c.toNat ≤ 90 := by simp

/-- Convert to lowercase -/
def toLower (c : UInt8) : UInt8 :=
  if h : isUpper c then
    have h : c.toNat + 32 < 256 := sorry
    ⟨c.val+32, h⟩
  else c

theorem not_isUpper_toLower (c : UInt8) : ¬ isUpper (toLower c) := by
  simp [isUpper_iff, toLower]
  split
  · rw [UInt8.toNat]
    simp
    omega
  · omega

The theorem gives me this out-of-the-blue error:

application type mismatch
  of_decide_eq_true (Eq.refl true)
argument has type
  true = true
but function has type
  decide (65 ≤ 32) = true → 65 ≤ 32

I can't figure out where this of_decide_eq_true application is coming from.

[François G. Dorais]

I've tried a bunch of things, eliminating omega and split doesn't change anything.

[François G. Dorais]

Simp fiddling doesn't do much either.

[Mario Carneiro]

note, 65 is (default : Char).toNat

[Mario Carneiro]

although it also appears in isUpper_iff so maybe not completely out of the blue

[François G. Dorais]

These are UInt8 not Char.

[François G. Dorais]

The code this comes from works fine in v4.7.0, so the arithmetic is good. There's just no place where the question whether 65 ≤ 32 actually occurs in the code (with the expected answer true).

[Mario Carneiro]

minimized:

example (x : Nat) : ¬65 ≤ x + 32 := by simp; sorry

[François G. Dorais]

Can't get smaller than that! Probably not std then. Not sure what to file in core though.

[Mario Carneiro]

the Simproc.le_add_ge in the proof term points right to the offending line

[Mario Carneiro]

lean4#4065

[François G. Dorais]

As always, thanks for the help Mario!

[François G. Dorais]

@Mario Carneiro Out of curiosity and to sharpen my own skills, how did you diagnose this?

[Mario Carneiro]

before or after the minimization?

[François G. Dorais]

Both?

[Mario Carneiro]

The minimization was obtained by isolating which tactic was producing the kernel error

[François G. Dorais]

That was simp. I think I got that far on my own.

[François G. Dorais]

(Not efficiently though!)

[Mario Carneiro]

more specifically, it was the second simp in the first branch before the omega

[François G. Dorais]

I had also figured out the problematic branch. That was easy.

[Mario Carneiro]

to isolate that, we just state the goal beforehand as an example and run simp on it, run simp only and remove everything unneeded, then simplify the goal itself until the problematic behavior doesn't occur

[Mario Carneiro]

I also simplified the definition of isUpper to just the first conjunct

[François G. Dorais]

OK. This is a great tip! I will use that going forward.

[Mario Carneiro]

after the minimization, the proof term (using by?) is small enough to be able to locate the ill-typed subterm

[François G. Dorais]

Ah! by? is new to me, I haven't learned how to use it. This is great!

[Mario Carneiro]

and then Nat.Simproc.le_add_ge, being a lemma used by a proof producing program, is used only once in the code, on line 279 of BuiltinSimprocs.lean, so we just have to audit the arithmetic reasoning here and the issue is that mkGENat yo x flips the arguments twice (they are passed in reverse order and mkGE also flips the arguments) instead of once

[Mario Carneiro]

you can also use show_term by instead of by?

[François G. Dorais]

This is incredibly helpful! Thank you very much Mario!

[Kim Morrison]

Thanks for this. I've merged, and also cherry-picked it on to releases/v4.8.0 so in the (likely) event of an rc2 it will arrive there too.