Zulip Chat Archive

Stream: mathlib4

Topic: Data.Int.Order.Basic

Scott Morrison (Dec 13 2022 at 22:25):

mathlib4#938, which is on the critical path, is down to one annoying error, which I wouldn't mind some help with.

Scott Morrison (Dec 13 2022 at 22:27):

We get to a point where the goal is ¬↑(k + 2) < (2 : ℤ), and the translated proof is by decide, but this doesn't work, with expected type must not contain free or meta variables. Trying instead by revert k; decide gives failed to synthesize Decidable (∀ (k : ℕ), ↑(k + 2) < 2 → 0 ≤ ↑(k + 2) → ¬↑(k + 2) < 2).

Scott Morrison (Dec 13 2022 at 22:27):

Happy to have either a fix/explanation of how to get decide working there, or any arbitrary workaround.

Gabriel Ebner (Dec 13 2022 at 22:32):

Yeah that error is a bit patronizing. I wonder if we should just add a decide! tactic.

Eric Wieser (Dec 13 2022 at 22:41):

Presumably this worked before because int.lt was defined inductively in a way that made it always true?

Mario Carneiro (Dec 13 2022 at 22:49):

it's still defined like that

Mario Carneiro (Dec 13 2022 at 22:49):

decide just doesn't want to try reducing an open term to ofTrue

Mario Carneiro (Dec 13 2022 at 22:50):

FYI we already have a decide! tactic

Mario Carneiro (Dec 13 2022 at 22:50):

it reverts everything before calling decide

Mario Carneiro (Dec 13 2022 at 22:51):

I think we should just remove the error message, and instead only use that check to enable the fast path

Scott Morrison (Dec 13 2022 at 23:02):

The more immediate question here is that decide! is not working either, and this is what I would like help with.

Kevin Buzzard (Dec 13 2022 at 23:07):

theorem emod_two_eq_zero_or_one (n : ℤ) : n % 2 = 0 ∨ n % 2 = 1 :=
  have h : n % 2 < 2 := abs_of_nonneg (show 0 ≤ (2 : ℤ) by decide) ▸ Int.emod_lt _ (by decide)
  have h₁ : 0 ≤ n % 2 := Int.emod_nonneg _ (by decide)
  match n % 2, h, h₁ with
  | (0 : ℕ), _ ,_ => Or.inl rfl
  | (1 : ℕ), _ ,_ => Or.inr rfl
  | (k + 2 : ℕ), h₁, _ => absurd h $ False.elim $ h₁.not_le $ by
    rw [Nat.cast_add]
    exact (le_add_iff_nonneg_left 2).2 (NonNeg.mk k)
  | -[a+1], _, h₁ => by cases h₁

is a proof if you want to keep the port moving while you worry about decidability.

Scott Morrison (Dec 13 2022 at 23:18):

I made an issue for this, linked to it, and will merge the PR now.

https://github.com/leanprover-community/mathlib4/issues/994

Kevin Buzzard (Dec 13 2022 at 23:27):

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
#check @natAbs_dvd_iff_dvd /- Left-hand side simplifies from
  natAbs a ∣ natAbs b
to
  (match a with
  | ofNat m => m
  | -[m+1] => Nat.succ m) ∣
  match b with
  | ofNat m => m
  | -[m+1] => Nat.succ m
using
  simp only [Int.natAbs]
Try to change the left-hand side to the simplified term!
 -/