leanprover/lean4

Bug with nested ifs and lets

Closed this issue · 8 comments

fgdorais commented

Prerequisites

Please put an X between the brackets as you perform the following steps:

Description

The following code gives (kernel) declaration has free variables 'getHexDigit?' on Lean 4.9.0-rc1.

def getHexDigit? (char : Char) : Option (Fin 16) :=
  if char.toNat < 0x0030 then
    none
  else
    let n := if char.toNat < 0xFF10 then char.toNat - 0x0030 else char.toNat - 0xFF10
    if h : n < 10 then
      some ⟨n, Nat.lt_trans h (by decide)⟩
    else if n >= 17 then
      let n := n - 7
      if h : n < 16 then
        some ⟨n, h⟩
      else if n >= 32 then
        let n := n - 32
        if h : n < 16 then
          some ⟨n, h⟩
        else
          none
      else
        none
    else
      none

Removing the second let or the third let eliminates the problem.

Context

Discovered while updating lean4-unicode-basic to v4.9.0-rc1. Posted on Zulip.

Versions

Lean (version 4.9.0-rc1, arm64-apple-darwin23.5.0, commit be6c4894e0a6, Release)

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

llllvvuu commented

I've minimized it to:

def dif (p : Prop) (_ : p → Nat) : Nat := Nat.zero

set_option trace.Meta.isDefEq.assign true in
example : Nat :=
  let n : Nat := Nat.zero
  dif True (fun (_ : True) =>
    let m : Nat := n
    dif (m = m) fun (_ : m = m) => (
      let x := 0
      Nat.zero
    )
  )

This is broken all the way back to Lean 4.0.0. Similarly, removing the (char : Char) argument from OP's example causes it to break on 4.0.0.

In either example, if there is an argument in the declaration header, the bug only shows up in f97a7d4 and later.

  • 👍1
fgdorais commented

Great insight! I thought let reassignments might be the issue but that was a red herring.

hwatheod commented

I also found a (kernel) declaration has free variables issue involving let which I minimized to the following:

example: Nat :=
  let a: Nat := 1
  have: a = 1 := by rfl
  let b: Nat := 2
  have: b = 2 := by rfl
  have: a = a := by rfl
  let c := 1
  0

It also fails at version 4.0.0. I thought it might be related to this issue so I am adding it here.

  • 👍1
llllvvuu commented

I also found a (kernel) declaration has free variables issue involving let which I minimized to the following:

example: Nat :=
  let a: Nat := 1
  have: a = 1 := by rfl
  let b: Nat := 2
  have: b = 2 := by rfl
  have: a = a := by rfl
  let c := 1
  0

It also fails at version 4.0.0. I thought it might be related to this issue so I am adding it here.

Yup, same bug indeed, since have is let_fun, which plays the role of the dite in the OP's example. Can remove all mvars but the last OfNat:

set_option trace.Meta.isDefEq.assign true in
example: Nat :=
  let a: Nat := Nat.zero
  have: True := trivial
  let b: Nat := Nat.zero
  have: a = b := Eq.refl a
  (fun (_ : Nat) => 0) Nat.zero

The _uniq.4 here looks suspicious:

[Meta.isDefEq.assign.beforeMkLambda] ?m.43 [this✝, this, x✝] := instOfNatNat 0
?m.43 := fun (this : True) => let b : Nat := Nat.zero; fun (this : Eq.{?_uniq.10} Nat _uniq.4 b) (x._@.repro._hyg.40 : Nat) => instOfNatNat 0
  • 👍1
kmill commented

I do not think that this was fixed by #4410. The change in #4410 seems fine, but it does not fix the underlying issue in (I think!) isDefEq.

Here's another test case that's simpler still:

example :=
  let a : Nat := Nat.zero
  fun (_ : True) =>
  let b : Nat := Nat.zero
  (fun (_ : a = b) => 0)

While #4110 makes some ill-formed metavariable assignments end up not mattering, they are still present. The issue seems to be that the OfNat instance metavariable for 0 forgets to include a as one of the let bindings it depends on.

If you add well-formedness checks to checkTypesAndAssign like so, then you can see this reflected as an elaboration error, as "typeclass instance problem is stuck".

private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
  withTraceNodeBefore `Meta.isDefEq.assign.checkTypes (return m!"({mvar} : {← inferType mvar}) := ({v} : {← inferType v})") do
    if !mvar.isMVar then
      trace[Meta.isDefEq.assign.checkTypes] "metavariable expected"
      return false
    else
      -- must check whether types are definitionally equal or not, before assigning and returning true
      let mvarType ← inferType mvar
      let vType ← inferType v
      if (← withTransparency TransparencyMode.default <| Meta.isExprDefEqAux mvarType vType) then
        unless (← MetavarContext.isWellFormed (← mvar.mvarId!.getDecl).lctx v) do
          throwError "in checkTypesAndAssign: metavariable has incompatible local context for value\n{indentD v}\nMetavariable:{indentD mvar.mvarId!}"
        unless (← MetavarContext.isWellFormed (← mvar.mvarId!.getDecl).lctx vType) do
          throwError "in checkTypesAndAssign: metavariable has incompatible local context for type\n{indentD vType}\nMetavariable:{indentD mvar.mvarId!}"
        mvar.mvarId!.assign v
        pure true
      else
        pure false

Is there any justification in the PR for not zeta reducing being called a bug in this comment? It seems to me that instantiateMVars is not responsible for correcting for incorrect metavariable assignments, and I think a followup fix should change that comment.

llllvvuu commented

I had a similar theory prior to changing the fix: 625b45c (this implementation is not good but the idea was essentially to change mkLambdaFVarsWithLetDeps behavior to include let decls that come before the first arg xs[0]:

lean4/src/Lean/Meta/ExprDefEq.lean

Lines 390 to 420 in 93fa9c8

/--
Auxiliary method for solving constraints of the form `?m xs := v`.
It creates a lambda using `mkLambdaFVars ys v`, where `ys` is a superset of `xs`.
`ys` is often equal to `xs`. It is a bigger when there are let-declaration dependencies in `xs`.
For example, suppose we have `xs` of the form `#[a, c]` where
```
a : Nat
b : Nat := f a
c : b = a
```
In this scenario, the type of `?m` is `(x1 : Nat) -> (x2 : f x1 = x1) -> C[x1, x2]`,
and type of `v` is `C[a, c]`. Note that, `?m a c` is type correct since `f a = a` is definitionally equal
to the type of `c : b = a`, and the type of `?m a c` is equal to the type of `v`.
Note that `fun xs => v` is the term `fun (x1 : Nat) (x2 : b = x1) => v` which has type
`(x1 : Nat) -> (x2 : b = x1) -> C[x1, x2]` which is not definitionally equal to the type of `?m`,
and may not even be type correct.
The issue here is that we are not capturing the `let`-declarations.
This method collects let-declarations `y` occurring between `xs[0]` and `xs.back` s.t.
some `x` in `xs` depends on `y`.
`ys` is the `xs` with these extra let-declarations included.
In the example above, `ys` is `#[a, b, c]`, and `mkLambdaFVars ys v` produces
`fun a => let b := f a; fun (c : b = a) => v` which has a type definitionally equal to the type of `?m`.
Recall that the method `checkAssignment` ensures `v` does not contain offending `let`-declarations.
This method assumes that for any `xs[i]` and `xs[j]` where `i < j`, we have that `index of xs[i]` < `index of xs[j]`.
where the index is the position in the local context.
-/
private partial def mkLambdaFVarsWithLetDeps (xs : Array Expr) (v : Expr) : MetaM (Option Expr) := do

^Is this what you're referring to?

I backtracked on that idea because the existing behavior looked intentional / I couldn't be sure.

Kha commented

@kmill Your test case is failing for me on "Mathlib stable" but not latest or nightly

Kha commented

Closing until reconfirmation