Qq error in MOP update

Stream: mathlib4

[Patrick Massot]

If any meta-expert want to help bumping @Heather Macbeth's book, the first challenge is to fix:

import Mathlib.Data.Int.Basic
import Mathlib.Tactic.Ring
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Linarith

open Lean hiding Rat mkRat
open Lean.Meta Qq Lean.Elab Term
open Lean.Parser.Tactic Mathlib.Meta.NormNum

/-- Two integers are congruent modulo `n`, if their difference is a multiple of `n`. -/
def Int.ModEq (n a b : ℤ) : Prop := n ∣ a - b

notation:50 a " ≡ " b " [ZMOD " n "]" => Int.ModEq n a b

namespace Mathlib.Meta.NormNum

theorem isInt_ModEq_true : {a b a' b' n : ℤ} → IsInt a a' → IsInt b b' → decide (a' = b') = true →
    Int.ModEq n a b
  | _, _, a', b', n, ⟨rfl⟩, ⟨rfl⟩, hab =>
    by
      dsimp
      replace hab := of_decide_eq_true hab
      rw [hab]
      use 0
      ring

theorem isInt_ModEq_false : {a b a' b' n : ℤ} → IsInt a a' → IsInt b b' → decide (0 < n) = true →
    decide (a' < n) = true → decide (b' < n) = true → decide (0 ≤ a') = true →
    decide (0 ≤ b') = true → decide (a' ≠ b') = true → ¬ Int.ModEq n a b
  | _, _, a', b', n, ⟨rfl⟩, ⟨rfl⟩, hn, han, hbn, ha, hb, hab =>
    by
      dsimp
      change ¬ n ∣ _
      replace hn := of_decide_eq_true hn
      replace han := of_decide_eq_true han
      replace hbn := of_decide_eq_true hbn
      replace ha := of_decide_eq_true ha
      replace hb := of_decide_eq_true hb
      replace hab := of_decide_eq_true hab
      rw [← Int.exists_lt_and_lt_iff_not_dvd _ hn]
      cases' lt_or_gt_of_ne hab with hab hab
      · exact ⟨-1, by linarith, by linarith⟩
      · exact ⟨0, by linarith, by linarith⟩

end Mathlib.Meta.NormNum

/-- The `norm_num` extension which identifies expressions of the form `a ≡ b [ZMOD n]`,
such that `norm_num` successfully recognises both `a` and `b` and they are small compared to `n`. -/
@[norm_num Int.ModEq _ _ _] def evalModEq : NormNumExt where eval (e : Q(Prop)) := do
  let .app (.app (.app f (n : Q(ℤ))) (a : Q(ℤ))) (b : Q(ℤ)) ← whnfR e | failure
  guard <|← withNewMCtxDepth <| isDefEq f q(Int.ModEq)
  let ra : Result a ← derive a
  let rb : Result b ← derive b
  let rn : Result q($n) ← derive n
  let i : Q(Ring ℤ) := q(Int.instRingInt)
  let ⟨za, na, pa⟩ ← ra.toInt
  let ⟨zb, nb, pb⟩ ← rb.toInt
  let ⟨zn, _, _⟩ ← rn.toInt i
  if za = zb then
    -- reduce `a ≡ b [ZMOD n]` to `true` if `a` and `b` reduce to the same integer
    let pab : Q(decide ($na = $nb) = true) := (q(Eq.refl true) : Expr)
    let r : Q(Int.ModEq $n $a $b) := q(isInt_ModEq_true $pa $pb $pab)
    return (.isTrue r : Result q(Int.ModEq $n $a $b))
  else
    -- reduce `a ≡ b [ZMOD n]` to `false` if `0 < n`, `a` reduces to `a'` with `0 ≤ a' < n`,
    -- and `b` reduces to `b'` with `0 ≤ b' < n`
    let pab : Q(decide ($na ≠ $nb) = true) := (q(Eq.refl true) : Expr)
    if zn = 0 then failure
    let pn : Q(decide (0 < $n) = true) := (q(Eq.refl true) : Expr)
    if zn ≤ za then failure
    let pan : Q(decide ($na < $n) = true) := (q(Eq.refl true) : Expr)
    if zn ≤ zb then failure
    let pbn : Q(decide ($nb < $n) = true) := (q(Eq.refl true) : Expr)
    if za < 0 then failure
    let pa0 : Q(decide (0 ≤ $na) = true) := (q(Eq.refl true) : Expr)
    if zb < 0 then failure
    let pb0 : Q(decide (0 ≤ $nb) = true) := (q(Eq.refl true) : Expr)
    let r : Q(¬Int.ModEq $n $a $b) := q(isInt_ModEq_false $pa $pb $pn $pan $pbn $pa0 $pb0 $pab)
    return (.isFalse r : Result q(¬Int.ModEq $n $a $b))

[Eric Wieser]

I'll take a quick look

[Eric Wieser]

It would be great if CI were enabled for that repo so that I could see the erro in the PR

[Bhavik Mehta]

More generally, it might be nice if there were a CI template made explicitly somewhere that projects could copy / adapt, to ease the setup for people making Lean 4 projects

[Eric Wieser]

I think you can just copy the one in mathlib?

[Patrick Massot]

Maybe it isn't clear but the snippet I pasted above is a mwe.

[Patrick Massot]

You can paste it into a scratch file in current mathlib.

[Eric Wieser]

Adding

  let pa' : Q(IsInt «$a» «$na») := pa
  let pb' : Q(IsInt «$b» «$nb») := pb

seems to fix it

[Eric Wieser]

(and using the primed versions later)

[Eric Wieser]

The infoview can't be trusted to show the types that Qq actually sees

[Eric Wieser]

Hmm, actually somehow that makes an error appear on an earlier line

[Eric Wieser]

Working:

/-- The `norm_num` extension which identifies expressions of the form `a ≡ b [ZMOD n]`,
such that `norm_num` successfully recognises both `a` and `b` and they are small compared to `n`. -/
@[norm_num Int.ModEq _ _ _] def evalModEq : NormNumExt where eval (e : Q(Prop)) := do
  let .app (.app (.app f (n : Q(ℤ))) (a : Q(ℤ))) (b : Q(ℤ)) ← whnfR e | failure
  guard <|← withNewMCtxDepth <| isDefEq f q(Int.ModEq)
  let ra : Result a ← derive a
  let rb : Result b ← derive b
  let rn : Result n ← derive n
  let i : Q(Ring ℤ) := q(Int.instRingInt)
  let ⟨za, na, pa⟩ ← ra.toInt
  let ⟨zb, nb, pb⟩ ← rb.toInt
  let pa' : Q(IsInt «$a» «$na») := pa
  let pb' : Q(IsInt «$b» «$nb») := pb
  let ⟨zn, _, _⟩ ← rn.toInt i
  if za = zb then
    -- reduce `a ≡ b [ZMOD n]` to `true` if `a` and `b` reduce to the same integer
    let pab : Q(decide ($na = $nb) = true) := (q(Eq.refl true) : Expr)
    let r : Q($a ≡ $b [ZMOD $n]) := q(isInt_ModEq_true $pa' $pb' $pab)
    return (.isTrue r : Result q(Int.ModEq $n $a $b))
  else
    -- reduce `a ≡ b [ZMOD n]` to `false` if `0 < n`, `a` reduces to `a'` with `0 ≤ a' < n`,
    -- and `b` reduces to `b'` with `0 ≤ b' < n`
    let pab : Q(decide ($na ≠ $nb) = true) := (q(Eq.refl true) : Expr)
    if zn = 0 then failure
    let pn : Q(decide (0 < $n) = true) := (q(Eq.refl true) : Expr)
    if zn ≤ za then failure
    let pan : Q(decide ($na < $n) = true) := (q(Eq.refl true) : Expr)
    if zn ≤ zb then failure
    let pbn : Q(decide ($nb < $n) = true) := (q(Eq.refl true) : Expr)
    if za < 0 then failure
    let pa0 : Q(decide (0 ≤ $na) = true) := (q(Eq.refl true) : Expr)
    if zb < 0 then failure
    let pb0 : Q(decide (0 ≤ $nb) = true) := (q(Eq.refl true) : Expr)
    let r : Q(¬Int.ModEq $n $a $b) := q(isInt_ModEq_false $pa' $pb' $pn $pan $pbn $pa0 $pb0 $pab)
    return (.isFalse r : Result q(¬Int.ModEq $n $a $b))

[Patrick Massot]

Thanks. Any idea what was the explanation?

[Eric Wieser]

let rn : Result q($n) ← derive n was redundant and I guess confused Qq

[Eric Wieser]

Otherwise, the problem is that the destructuring let binding doesn't actually record the type information in a way that Qq can see it

[Eric Wieser]

As a general strategy, if something fails in Qq, try adding a let binding with an explicit type somewhere; even if the goal view says Lean already knows the type

[Eric Wieser]

I think Qq elaborates the terms before the goal view does, and so gets them in a less-elaborated state

[Patrick Massot]

It doesn't really explained why it worked before, but thanks.

[Eric Wieser]

Eric Wieser said:

It would be great if CI were enabled for that repo so that I could see the erro in the PR

Looking at the repo again, I think the answer is "this is a generated repo that is committed to by a script, the real repo is somewhere secret and may or may not have CI"

[Heather Macbeth]

@Patrick Massot I'm sorry you went to all this work, I actually have a bump in the private version which covers the Qq changes, but I didn't want to change the book version mid-semester.

[Heather Macbeth]

I'll add you to the private version.

[Patrick Massot]

Are you currently using the book? I thought that would happen next semester.

[Patrick Massot]

I pushed a fully fixed Library folder in my PR.

[Heather Macbeth]

Yes, I am teaching the couse three semesters in a row.

[Yaël Dillies]

Tangentially, how does one debug Qq troubles?