Nat.ble ???

Stream: new members

[Burkhardt Renz]

This is very strange:

#eval 42 ≤ 42 -- true

-- ble defined like Nat.ble (Init.Prelude.lean lines 1628-1640 )
def ble ( n m : Nat) : Bool :=
  match n, m with
  | .zero,  .zero   => true
  | .zero,  .succ _ => true
  | .succ _, .zero   => false
  | .succ n, .succ m => ble n m

#eval ble 42 42 -- true

-- But !!
#eval Nat.ble 42 42 --false

[Kevin Buzzard]

docs#Nat.ble

[Kevin Buzzard]

shrug

[Burkhardt Renz]

docs#Nat.ble

The (Boolean) less-equal relation on natural numbers.

I would expect that
Nat.ble 42 42 evaluates to true

[Kevin Buzzard]

I think most people here would agree with you that 42 <= 42. Did you try with 37?

[Burkhardt Renz]

#eval Nat.ble 37 37 -- false
#eval Nat.ble 0 0 -- false

[Daniel Weber]

This gives a soundness bug (also in nightly):

theorem oops : False :=
  nomatch (rfl : Nat.ble 0 0 = true) ▸ (by native_decide : Nat.ble 0 0 = false)

#print axioms oops

[Chris Bailey]

At least it requires native decide.

#reduce Nat.ble 0 0 -- true
#reduce Nat.ble 42 42 -- true

/-
Fails:
tactic 'decide' proved that the proposition
  Nat.ble 0 0 = false
is false
-/
example : False := by
  have : Nat.ble 0 0 = false := by decide
  sorry

[Daniel Weber]

This bug also occurs with docs#Nat.blt

[Daniel Weber]

If I understand correctly the problem is that https://github.com/leanprover/lean4/blob/a074bd9a2bd20cc470fbff4f80f2cd7b51ec0d0a/src/include/lean/lean.h#L1278 and https://github.com/leanprover/lean4/blob/a074bd9a2bd20cc470fbff4f80f2cd7b51ec0d0a/src/include/lean/lean.h#L1290 are missing lean_unbox

[Daniel Weber]

@Burkhardt Renz , could you make a bug report at https://github.com/leanprover/lean4/issues/new/choose ?

[Burkhardt Renz]

https://github.com/leanprover/lean4/issues/6086

[Mauricio Collares]

But isn't the boxed version of the scalar x just (x<<1) | 1? That shouldn't mess up the order relation.

[Markus Himmel]

My unverified and speculative guess is that since b_lean_obj_arg is a pointer type, this comparison is actually undefined behavior and the compiler optimized it out entirely.

[Sebastian Ullrich]

It's a bug in the old code generator

[compiler.cce] >> n
let _x_1 := instOfNatNat 0;
let _x_2 := _x_1.1;
_x_2.ble _x_2
[compiler.inline] instOfNatNat
[compiler.simp] >> n
false

[Markus Himmel]

Yes, this looks incorrect: https://github.com/leanprover/lean4/blob/7dc1ceb8d4312850b39cef9e751e0a3b651946e3/src/Lean/Compiler/ConstFolding.lean#L136-L136

[Mauricio Collares]

Markus Himmel said:

My unverified and speculative guess is that since b_lean_obj_arg is a pointer type, this comparison is actually undefined behavior and the compiler optimized it out entirely.

The result of comparing two pointers that don't point to the same object is not defined, so it would be good to unbox in either case. But I can't see what the compiler would remove to improve speed, unless it can somehow prove that the two pointers in question never point to the same object.

[Sebastian Ullrich]

@Markus Himmel Are you submitting a fix?

[Ruben Van de Velde]

Hah

[Philippe Duchon]

This means the current version of Lean is unsound, right? Any idea how long this has been present? (I don't think my version is up to date, and the bug does occur here).

[Kevin Buzzard]

Not really. It's easy to prove False if you assume the native decide axiom.

[Marc Huisinga]

Philippe Duchon said:

This means the current version of Lean is unsound, right? Any idea how long this has been present? (I don't think my version is up to date, and the bug does occur here).

It's only unsound with the ofReduceBool axiom, which pulls the entire Lean compiler into the trusted code base (whereas it's usually just the Lean kernel, which is a much smaller code base).

Formalization projects of mathematics avoid it for this reason, whereas program verification projects tend to sometimes use it because they need to trust the Lean compiler anyways to produce correct code, so they might as well grab the performance benefits of native_decide, too.

[Kevin Buzzard]

Mathlib only allows three axioms -- propext, Classical.choice and Quot.sound. If you can prove False using only those axioms then that is definitely a problem. But it's easy to define a constant as one thing, then tell Lean to implement it as another thing, and prove false; your proof will then rely on a fourth axiom Lean.ofReduceBool. It's also easy to prove False with sorry and then your proof will rely on a fifth axiom sorryAx. The key thing to check with a proof of False is #print axioms proof_name.

[Kevin Buzzard]

Mathematicians care very much about soundness, but there will be programmers who are less bothered about this but want the benefits of native_decide. It's horses for courses, but #print axioms always tells you whether or not to worry.

[Philippe Duchon]

OK - I see this via the contextual help on native_decide.

The disturbing part is that one doesn't need to import anything for this to become available.

So basically, anytime you obtain a proof of something, you should check its used axioms. Right? (Or could the untrusty compiler itself mess with this?)

[Kevin Buzzard]

Here's a proof of false (originally due to Mac here) which doesn't import anything and is not a bug, but which relies on the Lean.ofReduceBool axiom.

def not_zero := 37
@[implemented_by not_zero] def zero := 0
theorem oops : False := by
  have : zero ≠ not_zero := by decide -- kernel checks this, no axioms
  have : zero = not_zero := by native_decide -- trusts `implemented_by`
  contradiction
#print axioms oops
-- 'oops' depends on axioms: [Lean.ofReduceBool]

[Kevin Buzzard]

This code just demonstrates the flexibility of Lean rather than anything else. I literally tell the compiler a lie and then show that you can prove false if you trust the compiler.

The example which this thread is about is caused by the fact that someone accidentally told the compiler a lie. But I don't trust the compiler (precisely because you can tell it lies) so this is of no relevance to me as a mathematician.

[Kevin Buzzard]

Philippe Duchon said:

So basically, anytime you obtain a proof of something, you should check its used axioms. Right?

Sure. For example you want to check that the proof is sorry-free! (the file might be, but it might import a file with a sorry). And #print axioms will check this.

[Alex Meiburg]

Why does not implemented_by not take a theorem to prove that it's equal, I still don't understand.

[Abraham Solomon]

Philippe Duchon said:

This means the current version of Lean is unsound, right? Any idea how long this has been present? (I don't think my version is up to date, and the bug does occur here).

Essentially consistency(or soundness) revolves around axioms, really overall inconsistency(strictly speaking unsoundness) is something like existence of an axiom-free closed term with type 'False'.

[Chris Bailey]

Alex Meiburg said:

Why does not implemented_by not take a theorem to prove that it's equal, I still don't understand.

This exists as csimp. People are going to want a feature that does this kind of substitution for things at are opaque or don't have an equality proof no matter what you do. Adding a proof requirement to implemented_by just moves the issue to whatever the replacement is.

[Alex Meiburg]

I guess I would prefer to see csimp ... by sorry over implemented_by usually, which is my complaint. I'm totally fine with people not proving everything, or skipping things that can't be proven. I just believe that such things should be more obvious when we choose to do them. sorryAx is, imo, a better representation of this than ofReduceBool.