# Zulip Chat Archive

## Stream: lean4

### Topic: mathport:numbers

#### Daniel Selsam (Mar 23 2021 at 19:34):

Currently, `mathport`

detects Lean3 numerals (has_zero, has_one, bit0, bit1) and simply wraps them in `ofNat`

. However, these are not the instances that would be found by Lean4's typeclass synthesis, which (assuming Mario's TC-construction suggestion will never be merged) will need to synthesize something like https://github.com/dselsam/mathport/blob/master/Lib4/PrePort/Numbers.lean#L49 that will not compute in the kernel. It seems desirable to have a standard encoding, which would involve replacing the Lean3 numbers with this Lean4 encoding. However, Lean3 relies on some numeral operations computing in the kernel in a few places, e.g. to prove that `bit0 1 + bit0 1 = bit0 (bit0 1)`

. How about backporting this never happening (i.e. using `norm_num`

in a few additional places), so that `mathport`

can replace numbers with the lean4-friendly `OfNat`

instances?

#### Yury G. Kudryashov (Mar 23 2021 at 19:46):

What is the Lean4 way to define an `ofNat`

instance for every additive monoid?

#### Yury G. Kudryashov (Mar 23 2021 at 19:46):

Even if it will never happen in kernel, we'll definitely need this instance in `mathlib`

.

#### Yury G. Kudryashov (Mar 23 2021 at 19:48):

(then we'll probably have a diamond for `OfNat int _`

)

#### Daniel Selsam (Mar 23 2021 at 19:55):

@Yury G. Kudryashov Can you please clarify?

```
import algebra.group.defs
def mk5 (a : Type) [add_monoid a] : a := (5 : a)
-- ^ error: failed to synthesize type class instance for ... has_one a
```

#### Daniel Selsam (Mar 23 2021 at 19:56):

Shouldn't `add_monoid`

only have `0`

? I did not mention above but that is handled separately in the proposal, i.e.

```
instance instZero2Nat : OfNat α (nat_lit 0) := ⟨HasZero.zero⟩
```

(https://github.com/dselsam/mathport/blob/master/Lib4/PrePort/Numbers.lean#L39)

#### Yury G. Kudryashov (Mar 23 2021 at 19:56):

Sorry, I meant "add monoid with one". E.g.,

```
import algebra.group.defs
def mk5 (a : Type) [add_monoid a] [has_one a] : a := (5 : a)
```

#### Yury G. Kudryashov (Mar 23 2021 at 19:59):

I'm afraid that with `(5 : a)`

depending on a typeclass instance we'll have two definitions of `(5 : int)`

: one comes from the fact that `int`

is a ring (and we definitely want numerals in any ring in `mathlib`

), and the other is some default computationally efficient implementation.

#### Yury G. Kudryashov (Mar 23 2021 at 19:59):

Then a user will see a goal `(5 : int) = (5 : int)`

that is not a `rfl`

.

#### Yury G. Kudryashov (Mar 23 2021 at 20:09):

Even worse, we'll have two meanings of `(5 : Nat)`

. Now we can have `(coe : nat → nat) 5 = 5`

but it shows an up arrow in the goal view.

#### Yakov Pechersky (Mar 23 2021 at 20:11):

For the latter case, we have docs#nat.cast_id

#### Yury G. Kudryashov (Mar 23 2021 at 20:12):

Probably we'll need to make sure that Lean4 parses `(5 : Nat)`

using the generic `[AddMonoid Nat] [HasOne Nat]`

definition and simplify the prelude instance `OfNat Nat n`

(I guess, it is defined as the identity map) to the generic one.

#### Yury G. Kudryashov (Mar 23 2021 at 20:13):

@Yakov Pechersky Of course, we can have a lemma "these two definitions are equal" but I want to apply a lemma about `[Semiring R] (5 : R)`

to `(5 : Nat)`

without converting between two instances of `OfNat`

.

#### Daniel Selsam (Mar 23 2021 at 20:42):

@Yury G. Kudryashov Just to confirm, this is the issue you are concerned about:

```
axiom abstract_5_eq_0 (α : Type) [semiring α] : (5 : α) = (0 : α)
theorem elabAcceptsKernelRejects : (5 : Nat) = (0 : Nat) := abstract_5_eq_0 Nat
-- error: (kernel) declaration type mismatch, 'elabAcceptsKernelRejects' has type ...
```

where the `OfNat`

instances are not definitionally equal in both the elaborator and the kernel

#### Yury G. Kudryashov (Mar 23 2021 at 20:46):

Yes.

#### Daniel Selsam (Mar 23 2021 at 20:51):

Zooming out, here are the proposals for numbers that I am aware of:

- write custom elab/delab for lean3-style numerals, possibly not even mapping
`nat`

->`Nat`

- extend Lean4 TC (on lean-community fork) with ability to post-process instances (https://github.com/dselsam/mathport/issues/17#issuecomment-781430391)
- some kind of
`nat2bits`

instance as in https://github.com/dselsam/mathport/blob/master/Lib4/PrePort/Numbers.lean#L49 which would (once partial is replaced with WF) still use WF and so not compute reliabliy

#### Yury G. Kudryashov (Mar 23 2021 at 21:17):

My concern is not about porting of our lean 3 code but about Lean 4 mathlib that we want to have in future: should we somehow disable the default instance `OfNat Nat _`

? If not, how should we deal with conflicting instances? I assume that we definitely want to have `instance (R : Type*) [Semiring R] (n : Nat) : OfNat R n`

.

#### Yury G. Kudryashov (Mar 23 2021 at 21:20):

It seems to me that something like `nat2bits`

(probably with an override that uses better functions for `Nat`

and `Int`

) + disabling the default `OfNat`

instances is the way to go. Am I wrong for some reason?

#### Yury G. Kudryashov (Mar 23 2021 at 21:24):

Basically, this means replicating Lean 3 numerals on top of Lean 4. I would be happy to see a solution that (a) does not involve disabling the default `OfNat Nat n`

instance; (b) does not create this problem.

#### Mario Carneiro (Mar 23 2021 at 23:26):

I think we will need a typeclass `Numeric := \all n, OfNat Nat n`

, and this will be mixed in to `Semiring`

and other relevant classes. This is onerous for constructing instances of `Semiring`

but lets individual types decide how best to implement it. Daniel's well founded instance looks like a "last resort" instance similar to docs#uniform_space.of_core

#### Daniel Selsam (Mar 24 2021 at 00:33):

@Mario Carneiro How would `normNum`

work in this proposal?

#### Mario Carneiro (Mar 24 2021 at 00:44):

We would need the `OfNat`

instance to be coherent with the semiring structure, of course; one way would be to posit `ofNat R n + ofNat R m = ofNat R (n + m)`

and similar axioms for the other operations. Then `normNum`

would work by using these to rewrite operations on add and mul to primitive add and mul on nat, using kernel evaluation to finish the job

#### Mario Carneiro (Mar 24 2021 at 04:00):

```
import Lean
class Numeric (α : Type _) where
ofNat : Nat → α
instance Numeric.OfNat (α) [Numeric α] (n) : OfNat α n := ⟨Numeric.ofNat n⟩
class Semiring (α : Type _) extends Add α, Mul α, Numeric α where
add_assoc (a b c : α) : a + b + c = a + (b + c)
add_zero (a : α) : a + 0 = a
add_comm (a : α) : a + b = b + a
mul_assoc (a b c : α) : a * b * c = a * (b * c)
one_mul (a b c : α) : 1 * a = a
mul_one (a b c : α) : a * 1 = a
zero_mul (a b c : α) : 0 * a = a
mul_zero (a b c : α) : a * 0 = a
mul_add (a b c : α) : a * (b + c) = a * b + a * c
add_mul (a b c : α) : (a + b) * c = a * c + b * c
ofNat_add (a b : Nat) : ofNat (a + b) = ofNat a + ofNat b
ofNat_mul (a b : Nat) : ofNat (a * b) = ofNat a * ofNat b
instance Semiring.OfNat (α) [Semiring α] (n) : OfNat α n := Numeric.OfNat _ _
syntax (name := normNum) "normNum" : tactic
open Lean Meta Elab Tactic
def mkOfNatLit (u : Level) (α sα n : Expr) : Expr :=
let inst := mkApp3 (mkConst `Semiring.OfNat [u]) α sα n
mkApp3 (mkConst `OfNat.ofNat [u]) α n inst
namespace NormNum
theorem ofNat_add {α} [Semiring α] : (a b : α) → (a' b' c : Nat) →
a = OfNat.ofNat a' → b = OfNat.ofNat b' → a' + b' = c → a + b = OfNat.ofNat c
| _, _, _, _, _, rfl, rfl, rfl => (Semiring.ofNat_add _ _).symm
theorem ofNat_mul {α} [Semiring α] : (a b : α) → (a' b' c : Nat) →
a = OfNat.ofNat a' → b = OfNat.ofNat b' → a' * b' = c → a * b = OfNat.ofNat c
| _, _, _, _, _, rfl, rfl, rfl => (Semiring.ofNat_mul _ _).symm
partial def eval : Expr → MetaM (Expr × Expr)
| e => e.withApp fun f args => do
if f.isConstOf `HAdd.hAdd then
evalB `NormNum.ofNat_add (·+·) args
else if f.isConstOf `HMul.hMul then
evalB `NormNum.ofNat_mul (·*·) args
else if f.isConstOf `OfNat.ofNat then pure (e, ← mkEqRefl e)
else throwError "fail"
where
evalB (name : Name) (f : Nat → Nat → Nat)
(args : Array Expr) : MetaM (Expr × Expr) := do
if let #[_, _, α, _, a, b] ← args then
let Level.succ u _ ← getLevel α | throwError "fail"
let sα ← synthInstance (mkApp (mkConst `Semiring [u]) α)
let (a', pa) ← eval a
let (b', pb) ← eval b
let la := Expr.getRevArg! a' 1
let some na ← la.natLit? | throwError "fail"
let lb := Expr.getRevArg! b' 1
let some nb ← lb.natLit? | throwError "fail"
let lc := mkNatLit (f na nb)
let c := mkOfNatLit u α sα lc
pure (c, mkApp10 (mkConst name [u]) α sα a b la lb lc pa pb (← mkEqRefl lc))
else throwError "fail"
@[tactic normNum] def evalNormNum : Tactic := fun stx =>
liftMetaTactic fun g => do
let some (α, lhs, rhs) ← matchEq? (← getMVarType g) | throwError "fail"
let (lhs2, p) ← NormNum.eval lhs
unless ← isDefEq lhs2 rhs do throwError "fail"
assignExprMVar g p
pure []
end NormNum
set_option trace.Meta.debug true
variable (α) [Semiring α]
example : (2 + 2 + 2 : α) = 6 := by normNum
example : (0 + (2 + 3) + 7 : α) = 12 := by normNum
example : (70 * (33 + 2) : α) = 2450 := by normNum
```

#### Yury G. Kudryashov (Mar 24 2021 at 18:19):

Probably it suffices to require `ofNat 0 = 0`

and `ofNat (n + 1) = ofNat n + 1`

#### Yury G. Kudryashov (Mar 24 2021 at 18:21):

The solution with `Numeric`

typeclass looks very nice.

#### Mario Carneiro (Mar 24 2021 at 22:21):

@Sebastian Ullrich Constructing terms in this `normNum`

port is super painful. Is there a trick I'm missing? Both matching terms and constructing terms using expr quotations are sorely missing here

#### Mario Carneiro (Mar 24 2021 at 22:23):

Also double backtick name quotations don't seem to work properly

#### Sebastian Ullrich (Mar 24 2021 at 22:30):

Mario Carneiro said:

Also double backtick name quotations don't seem to work properly

In what way?

#### Sebastian Ullrich (Mar 24 2021 at 22:31):

Mario Carneiro said:

Is there a trick I'm missing?

I don't think so, it's just a kind of program no-one else has written in Lean 4 before

#### Mario Carneiro (Mar 24 2021 at 22:33):

Ah, nvm about double backtick name quotations, I think there were just less things in scope than I thought

#### Mario Carneiro (Mar 24 2021 at 22:35):

Would it be possible to have `(·+·)`

expand to `HAdd.hAdd`

instead of `fun x y => x + y`

? I think that will eventually turn into a mathport issue

#### Mario Carneiro (Mar 24 2021 at 22:37):

It looks like expr quotations like ` `((·+·) : Nat → Nat → Nat).subst a`

don't work anymore

#### Daniel Selsam (Apr 01 2021 at 03:48):

(I was offline for a few days) @Mario Carneiro I like this approach for Lean4. It would be extremely ambitious to try to automate this change in mathport though. Will you be able to backport it?

EDIT: Actually, I am not sure yet how hard it would be to autoport this change. I will think more about it.

#### Mario Carneiro (Apr 01 2021 at 06:58):

Which part? The `normNum`

implementation was intended to be a lean 4 tactic; it would be hard to backport it since it relies on primitive nats

#### Daniel Selsam (Apr 01 2021 at 15:17):

The main thing that mathport certainly cannot do automatically is guess the desired `Semiring`

instances. If you backport the change to `semiring`

, then even if you don't connect the `ofNat`

to anything else, it may be feasible for mathport to detect old numerals and replace them with new numerals, and detect old `norm_num`

proofs and replace them with `normNum`

proofs.

#### Daniel Selsam (Apr 01 2021 at 15:17):

Also, it would be nice if `norm_num`

wrapped its proofs with `idNormNum`

.

#### Daniel Selsam (Apr 09 2021 at 17:19):

@Mario Carneiro What do you think about backporting the `semiring`

change?

#### Mario Carneiro (Apr 09 2021 at 17:21):

We don't need it to make mathlib work, right? I think it would be better to do as a refactor on lean 4 mathlib

#### Daniel Selsam (Apr 09 2021 at 17:23):

Yes, it could be a future refactor in Lean4, after the `.lean`

files have been manually resurrected.

#### Mario Carneiro (Apr 09 2021 at 17:25):

It will solve some defeq diamond issues but those are second order concerns

#### Daniel Selsam (Apr 09 2021 at 17:25):

In the meantime, we will still need to be able to implement a `normNum`

that works for both auto-ported terms and newly-elaborated terms. The three options for now are still roughly https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/mathport.3Anumbers/near/231541759

#### Mario Carneiro (Apr 09 2021 at 17:27):

I don't know, it sounds like running before we can walk. We still need the mathlib tactic suite

#### Mario Carneiro (Apr 09 2021 at 17:28):

it makes more sense for `normNum`

to just deal with lean 4 numerals expressed the way we want them to be expressed

#### Mario Carneiro (Apr 09 2021 at 17:30):

if it's not possible to get mathport to do the translation, a tactic on the lean 4 side can also simplify numerals and other lean 3 cruft

#### Daniel Selsam (Apr 09 2021 at 17:34):

Are you suggesting option (3)? We define a generic `nat2bits`

non-computing instance, and then have `normNum`

use `semiring`

lemmas in terms of these instances? Then once `semiring`

adds `Numeric`

, we can just change the instances to ones that compute (when applicable)?

#### Daniel Selsam (Apr 09 2021 at 17:35):

Mario Carneiro said:

I don't know, it sounds like running before we can walk. We still need the mathlib tactic suite

I am not sure I follow your line of thought here -- `normNum`

is a core part of the mathlib tactic suite with few dependencies

#### Mario Carneiro (Apr 09 2021 at 17:41):

Perhaps, but it depends a lot on how the library is set up and it's not particularly hard to write otherwise. I would like to see us get the infrastructure so that we can actually port basic files. I tried doing a nontrivial lean 4 proof a few days ago and I hit a whole bunch of issues that made it pretty hard even for non-mathlib proofs (aside from just missing lemmas). Right now no one is actually trying to prove theorems with lean 4 and getting the rough edges polished there is a higher priority IMO

#### Daniel Selsam (Apr 09 2021 at 17:46):

Do you think needing to build a custom lean is prohibitive for would-be tinkerers? If so, I can look into the VSCode-docker setup.

EDIT: oh you mean playing with Lean4 independent of mathport

#### Brandon Brown (Apr 09 2021 at 19:00):

Mario Carneiro said:

...I tried doing a nontrivial lean 4 proof a few days ago and I hit a whole bunch of issues that made it pretty hard even for non-mathlib proofs (aside from just missing lemmas). Right now no one is actually trying to prove theorems with lean 4 and getting the rough edges polished there is a higher priority IMO

Out of curiosity, could you mention some of the current limitations to doing non-trivial proofs in Lean 4 (ignoring the lack of existing lemmas etc to build off of)?

#### Daniel Selsam (Apr 09 2021 at 19:07):

@Brandon Brown In my own experience doing mini-experiments on top of mathport, there are a few open Lean4 issues that are painful (e.g. https://github.com/leanprover/lean4/issues/382), a bunch of somewhat-annoying loose-ends (e.g. some name clashes, can't use dot notation for aligned types), but for basic stuff the elaborator works well. And all the lemmas are there and usable. There isn't much that can be proved without `normNum`

, `ring`

, etc. though.

#### Daniel Selsam (Apr 09 2021 at 19:10):

I have not played around much with tactics either way though, so I don't know how dense the rough edges are still in the lean4 built-in tactics.

#### Daniel Selsam (Apr 09 2021 at 19:34):

Mario Carneiro said:

I hit a whole bunch of issues

Can you tell us more?

#### Mario Carneiro (Apr 10 2021 at 03:43):

I'll make another topic for it.

Last updated: May 18 2021 at 22:15 UTC