## Stream: general

### Topic: Typo in Lean4's Int.add

#### François G. Dorais (Aug 24 2020 at 09:00):

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 (Aug 24 2020 at 09:49):

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

#### Johan Commelin (Aug 24 2020 at 10:04):

@Sebastian Ullrich :up:

#### Gabriel Ebner (Aug 24 2020 at 10:23):

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 (Aug 24 2020 at 12:05):

@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 (Aug 24 2020 at 12:07):

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 (Aug 24 2020 at 12:11):

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

#### Rob Lewis (Aug 24 2020 at 12:22):

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

#### Kenny Lau (Aug 24 2020 at 12:23):

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

#### Reid Barton (Aug 24 2020 at 12:24):

yes, but because that was the way addition was defined

#### Reid Barton (Aug 24 2020 at 12:25):

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 (Aug 24 2020 at 12:25):

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

#### Reid Barton (Aug 24 2020 at 12:27):

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 (Aug 24 2020 at 12:36):

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

#### Kenny Lau (Aug 24 2020 at 12:36):

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

#### Reid Barton (Aug 24 2020 at 12:37):

probably, and tactics like norm_num would also get mighty confused

#### Sebastian Ullrich (Aug 24 2020 at 12:44):

Reid Barton said:

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

#### Rob Lewis (Aug 24 2020 at 12:46):

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

#### Rob Lewis (Aug 24 2020 at 12:47):

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

#### Sebastian Ullrich (Aug 24 2020 at 13:05):

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

#### Reid Barton (Aug 24 2020 at 13:11):

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 (Aug 24 2020 at 13:26):

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 (Aug 24 2020 at 13:28):

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

#### Reid Barton (Aug 24 2020 at 13:58):

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 (Aug 24 2020 at 14:00):

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

#### Reid Barton (Aug 24 2020 at 14:02):

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

#### Reid Barton (Aug 24 2020 at 14:02):

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

#### Reid Barton (Aug 24 2020 at 14:05):

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 (Aug 24 2020 at 14:07):

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

#### Reid Barton (Aug 24 2020 at 14:14):

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 (Aug 24 2020 at 19:29):

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 (Aug 24 2020 at 19:30):

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

#### Mario Carneiro (Aug 24 2020 at 19:30):

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

#### Reid Barton (Aug 24 2020 at 19:33):

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

#### Mario Carneiro (Aug 24 2020 at 19:35):

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

#reduce foo
#eval foo


#### Mario Carneiro (Aug 24 2020 at 19:38):

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 (Aug 24 2020 at 19:46):

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 (Aug 24 2020 at 19:49):

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

Last updated: May 12 2021 at 22:15 UTC