nlinarith is affected by `example`s

Stream: mathlib4

[Eric Wieser]

In the following example, the nlinarith tactic stops working if the file contains the wrong number of example := 1s

import Mathlib.Data.Complex.Exponential

open Real (sin)

run_cmd do
  -- fails for 4, 5, 6, 8, 9, 11, 13, 16, 17, ...
  let how_many := 4
  -- create `how_many` examples.
  for i in [0:how_many] do
    Lean.Elab.Command.elabCommandTopLevel <| ← `(command|
      example := 1)

theorem works_only_with_example_above (x : ℝ) :
    (√(1 + Real.sin x) - √(1 - Real.sin x)) ^ 2 ≤ 4 := by
  -- underscores aren't allowed in `have`, so use `let` + `clear_value`
  let h : _ = 1 + (_ : ℝ) ∧ _ = 1 - (_ : ℝ) := by
    constructor <;> exact Real.sq_sqrt <| by nlinarith [x.sin_sq]
  clear_value h -- makes the goal clearer, not needed for the bug
  nlinarith [(1 + sin x).sqrt_nonneg, (1 - sin x).sqrt_nonneg]

[Eric Wieser]

What is the mechanism behind the nondeterminism here? example doesn't even add anything to the environment, so what is it that nlinarith is finding?

[Eric Wieser]

My best guess so far is that something is using Expr.lt somewhere, which is nondeterministic (at least, under most user's mental model of lean)

[llllvvuu]

Could be unrelated to the last nlinarith:

import Mathlib.Data.Complex.Exponential

run_cmd do
  let how_many := 3
  for _ in [0:how_many] do
    Lean.Elab.Command.elabCommandTopLevel <| ← `(command|
      example := 1)

example (x : ℝ) :
    (√(1 + Real.sin x) - √(1 - Real.sin x)) ^ 2 ≤ 4 := by
  -- underscores aren't allowed in `have`, so use `let` + `clear_value`
  let h : _ = 1 + (_ : ℝ) ∧ _ = 1 - (_ : ℝ) := by
    constructor <;> exact Real.sq_sqrt <| by nlinarith [x.sin_sq]
  clear_value h -- makes the goal clearer, not needed for the bug
  -- fails only for `how_many := 4, 5, 6, 8, 9, 11, 13, 16, 17, ...`
  guard_hyp h :ₛ √(1 + Real.sin x) ^ 2 = 1 + Real.sin x ∧ √(1 - Real.sin x) ^ 2 = 1 - Real.sin x
  -- succeeds only for `how_many := 4, 5, 6, 8, 9, 11, 13, 16, 17, ...`
  guard_hyp h :ₛ √(1 + Real.cos x) ^ 2 = 1 + Real.cos x ∧ √(1 - Real.cos x) ^ 2 = 1 - Real.cos x
  sorry

[llllvvuu]

What's interesting to me is that by nlinarith [x.sin_sq] could even fill in the placeholders (by sorry throws an error). My mental model was that these kind of tactics couldn't affect the expected type. Turning on trace.linarith is very interesting here

[Kyle Miller]

Something I learned recently is that Name.quickLt can make some things "nondeterministic" since it causes numeric parts to be considered first rather than second in the lex order. The example := 1 command creates some mvars, so it bumps up the name generator, so the mvarids will have different num parts depending on how many examples there are.

Here's an illustration showing how the mvar ids increment:

set_option pp.raw true

example : True := by
  let n : Nat := ?_
  -- n : Nat := ?_uniq.5
  sorry; sorry

example : True := by
  let n : Nat := ?_
  -- n : Nat := ?_uniq.18
  sorry; sorry

example : True := by
  let n : Nat := ?_
  -- n : Nat := ?_uniq.31
  sorry; sorry

[Kyle Miller]

It looks like the nondeterminism for @llllvvuu's example comes from docs#Linarith.nlinarithExtras

You can see it with set_option trace.linarith true, where depending on the number of examples you get either

[linarith] nlinarith preprocessing found squares

[linarith] [(Real.cos x, true), (Real.sin x, true)]

or

[linarith] nlinarith preprocessing found squares

[linarith] [(Real.sin x, true), (Real.cos x, true)]

The square finding uses a HashMap to accumulate, and then it doesn't sort the list of expressions. The order depends somehow on the hash.

Using set_option pp.raw true, we can see that these two lists are [(Real.cos _uniq.1217, true), (Real.sin _uniq.1217, true)] and [(Real.sin _uniq.1248, true), (Real.cos _uniq.1248, true)] . The _uniq.NNNN is the fvarid for the local variable x.

The hashes of these expressions supports the theory that the hash determines the ordering:

open Lean

#eval Hashable.hash <| Expr.app (Expr.const ``Real.cos []) (Expr.fvar ⟨.num `_uniq 1217⟩)
-- 347606854
#eval Hashable.hash <| Expr.app (Expr.const ``Real.sin []) (Expr.fvar ⟨.num `_uniq 1217⟩)
-- 3872104533

#eval Hashable.hash <| Expr.app (Expr.const ``Real.cos []) (Expr.fvar ⟨.num `_uniq 1248⟩)
-- 3978123476
#eval Hashable.hash <| Expr.app (Expr.const ``Real.sin []) (Expr.fvar ⟨.num `_uniq 1248⟩)
-- 2494617287

[Eric Wieser]

Using AtomM and keying the map with integers seems to fix it

[Kyle Miller]

I'd guess sorting new_es by Expr.lt would fix it, for a one-line change

[Kyle Miller]

Are you saying you are already working on a fix?

[Eric Wieser]

Kyle Miller said:

I'd guess sorting new_es by Expr.lt would fix it, for a one-line change

Isn't this vulnerable to meta variable names still?