mathport:numbers

Stream: lean4

[Daniel Selsam]

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]

What is the Lean4 way to define an ofNat instance for every additive monoid?

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Daniel Selsam]

@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]

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]

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]

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]

Then a user will see a goal (5 : int) = (5 : int) that is not a rfl.

[Yury G. Kudryashov]

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]

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

[Yury G. Kudryashov]

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]

@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]

@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]

Yes.

[Daniel Selsam]

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

1. write custom elab/delab for lean3-style numerals, possibly not even mapping nat -> Nat
2. extend Lean4 TC (on lean-community fork) with ability to post-process instances (https://github.com/dselsam/mathport/issues/17#issuecomment-781430391)
3. 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]

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]

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]

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]

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]

@Mario Carneiro How would normNum work in this proposal?

[Mario Carneiro]

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]

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]

Probably it suffices to require ofNat 0 = 0 and ofNat (n + 1) = ofNat n + 1

[Yury G. Kudryashov]

The solution with Numeric typeclass looks very nice.

[Mario Carneiro]

@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]

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

[Sebastian Ullrich]

Mario Carneiro said:

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

In what way?

[Sebastian Ullrich]

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]

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

[Mario Carneiro]

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]

It looks like expr quotations like `((·+·) : Nat → Nat → Nat).subst a don't work anymore

[Daniel Selsam]

(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]

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]

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]

Also, it would be nice if norm_num wrapped its proofs with idNormNum.

[Daniel Selsam]

@Mario Carneiro What do you think about backporting the semiring change?

[Mario Carneiro]

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]

Yes, it could be a future refactor in Lean4, after the .lean files have been manually resurrected.

[Mario Carneiro]

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

[Daniel Selsam]

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]

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

[Mario Carneiro]

it makes more sense for normNum to just deal with lean 4 numerals expressed the way we want them to be expressed

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

@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]

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]

Mario Carneiro said:

I hit a whole bunch of issues

Can you tell us more?

[Mario Carneiro]

I'll make another topic for it.