Zulip Chat Archive

Stream: general

Topic: Typo in Lean4's Int.add


view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 24 2020 at 09:49):

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

view this post on Zulip Johan Commelin (Aug 24 2020 at 10:04):

@Sebastian Ullrich :up:

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Rob Lewis (Aug 24 2020 at 12:22):

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

view this post on Zulip Kenny Lau (Aug 24 2020 at 12:23):

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

view this post on Zulip Reid Barton (Aug 24 2020 at 12:24):

yes, but because that was the way addition was defined

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 24 2020 at 12:25):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Aug 24 2020 at 12:36):

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

view this post on Zulip Reid Barton (Aug 24 2020 at 12:37):

probably, and tactics like norm_num would also get mighty confused

view this post on Zulip Sebastian Ullrich (Aug 24 2020 at 12:44):

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

view this post on Zulip Rob Lewis (Aug 24 2020 at 12:46):

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

view this post on Zulip 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.

view this post on Zulip Sebastian Ullrich (Aug 24 2020 at 13:05):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)?

view this post on Zulip Reid Barton (Aug 24 2020 at 14:00):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 24 2020 at 19:30):

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

view this post on Zulip Reid Barton (Aug 24 2020 at 19:33):

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

view this post on Zulip Mario Carneiro (Aug 24 2020 at 19:35):

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

#reduce foo
#eval foo

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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