Typo in Lean4's Int.add

Stream: general

[François G. Dorais]

Lean4 devs aren't currently taking community feedback, but this tiny typo has been annoying me for a long while so I hope some of the Lean4 devs notice this post and fix it!

In the file src/Init/Data/Int/Basic.lean the definition of integer addition is:

@[extern "lean_int_add"]
protected def add (m n : @& Int) : Int :=
match m, n with
| ofNat m,   ofNat n   => ofNat (m + n)
| ofNat m,   negSucc n => subNatNat m (succ n)
| negSucc m, ofNat n   => subNatNat n (succ m)
| negSucc m, negSucc n => negSucc (m + n)

The last case should be:

| negSucc m, negSucc n => negSucc (succ (m + n))

In other words: -[1+m]+-[1+n] = -[1+((m+n)+1)]

The external lean_int_add seems okay but the official spec makes for really confusing bugs when using integers.

[Mario Carneiro]

heh, I guess they aren't unit testing these definitions yet

[Johan Commelin]

@Sebastian Ullrich :up:

[Gabriel Ebner]

Yes, apparently the test we have in Lean 3 for exactly this issue didn't make it into Lean 4: https://github.com/leanprover-community/lean/blob/523dc8ac17b6d825eebb3b5f0df846dac3d6e695/tests/lean/run/exhaustive_vm_impl_test.lean

[Sebastian Ullrich]

@François G. Dorais Now I'm curious what you're doing with Lean 4 that this has been annoying you for a long time!

[Patrick Massot]

This thing is pretty scary, how do we know such a mismatch between the Lean spec and VM code won't allow us to prove false (I'm not worried, I only try to understand how things will be setup).

[Sebastian Ullrich]

Since you cannot reason about the native implementation, the best you can do is to set up partial tests as above

[Rob Lewis]

Is the native implementation in Lean 4 more trusted than in Lean 3?

[Kenny Lau]

what does this concretely affect? Would rfl be able to prove (-3) + (-4) = -6?

[Reid Barton]

yes, but because that was the way addition was defined

[Reid Barton]

AFAIK, as far as proving is concerned, the compiler is not any more trusted than the VM of Lean 3, unless you opt in to trusting it

[Reid Barton]

(not sure if opting in is possible yet/ever)

[Reid Barton]

It might be the case that you can prove something about a program that is not true when you actually go and run it--you can view this as either a bug in the specification (like here) or a bug in the compiler/runtime; in any case it won't lead to a proof of false.

[Kenny Lau]

but then OP also mentioned "external lean_int_add". How would that affect someone like me contributing to mathlib?

[Kenny Lau]

would #eval (-3) + (-4) become -7?

[Reid Barton]

probably, and tactics like norm_num would also get mighty confused

[Sebastian Ullrich]

Reid Barton said:

(not sure if opting in is possible yet/ever)

See https://github.com/leanprover/lean4/blob/8630d78b3fcaaa6dd6bd387e5f3d7d0983d1ca90/src/Init/Core.lean#L1721-L1743

[Rob Lewis]

Is there/will there be a way to test whether a declaration opts in to this?

[Rob Lewis]

Or a compiler flag to turn off this reflection, or something like that? Any way to avoid accidentally depending on evaluation.

[Sebastian Ullrich]

It would make sense to me to integrate it into the #print axioms check

[Reid Barton]

don't know if this would break the setup, but reduceBool could be a constant and a propositional reduceBool b = b an axiom

[Reid Barton]

I guess you probably really want a defeq, though. So then I suppose you need separate logic to track usage of this reduction rule.

[Reid Barton]

Actually now I don't think my suggestion made any sense in the first place--never mind.

[Reid Barton]

Now I'm wondering what the intended guarantees are here. Is it supposed to be the case that this feature only gives you faster access to definitional equalities that the kernel could have proved anyways (under the assumption that the compiler and any untrusted code are correct)?

[Reid Barton]

and is the argument supposed to be by canonicity for bool and nat?

[Reid Barton]

Is canonicity true for all those terms which the compiler can generate for, even in the presence of axioms?

[Reid Barton]

I'm wondering whether it is possible to leak in some extensionality x = y implies x defeq y

[Reid Barton]

to be clear, the two possibilities here are: Assuming correctness of the compiler (whatever that means),

• no new defeqs are available when this feature is used,
• some new defeqs are available, but only ones which are propositionally correct

[Reid Barton]

(obviously if new defeqs are available that aren't even propositionally valid, the compiler can't be considered correct)

[Reid Barton]

Here I'm including use of unsafe features under the umbrella of the compiler, so this might be relevant to whether certain usages of unsafe features are considered to be correct or not

[Mario Carneiro]

Is canonicity true for all those terms which the compiler can generate for, even in the presence of axioms?

Certainly not for lean 3

[Mario Carneiro]

At least, there are closed terms of type nat or bool that will block via #reduce and evaluate via #eval

[Mario Carneiro]

so any use of the VM in this way is going to entail some new defeqs

[Reid Barton]

I feel like we've discussed this before; can you remind me of an example?

[Mario Carneiro]

def foo : nat :=
@eq.rec_on _ _ (λ _, ℕ) _ (propext (and_self true)) 42

#reduce foo
#eval foo

[Mario Carneiro]

I believe it is possible to leak extensionality, although because it is limited to closed terms I don't know how extensive the leakage is

[Mario Carneiro]

Even propositional equality of VM validated equalities in lean is currently an open question, meaning that the consistency of the overall system becomes open

[Mario Carneiro]

there is a proof of correctness of an erasure map similar to the lean VM in Coq Coq Correct!, which might be possible to adapt