writing lemmas about `ofNat`

Stream: mathlib4

[Jireh Loreaux]

This is probably an #xy, but I would like to know how to do this anyway: Given a ring R, both (37 : R) and ((37 : ℕ) : R) make sense, where the former is elaborated as @OfNat.ofNat R 37 _ and the latter is elaborated as Nat.cast (@OFNat.ofNat ℕ 37 _) with the 37s here being nat literals (I think, my understanding is weak here). My question is, how do I write the following lemma correctly? I'm just wondering about the statement, not the proof. Also, I know it holds in more generality for SubsemiringClass, but let's ignore that for now.

lemma ofNat_mem {R : Type*} [Ring R] (S : Subring R) (n : ℕ) [n.AtLeastTwo] : OfNat.ofNat (α := R) n ∈ S := sorry

I want this to be able to prove that 5 ∈ S where the 5 is the OfNat for R coming from the AddMonoidWithOne instance.

[Mario Carneiro]

Did you try that? It seems like it would work

[Jireh Loreaux]

Oh it elaborates just fine, but I thought I was getting a double-wrapping of OfNat.ofNat, maybe not though. Perhaps my problems lie elsewhere.

[Mario Carneiro]

no I mean try applying it to 5 \in S

[Mario Carneiro]

in the lemma itself there is nothing to double wrap as there is a variable instead of a numeral

[Jireh Loreaux]

oh, I see. Yes, it does work to prove that, but aesop doesn't like to apply it for some reason (like I said, probably an #xy). :thinking: I'll write the example in a minute, but I have to leave in about 5, so I won't see the reply.

[Jireh Loreaux]

import Mathlib

set_option autoImplicit true

@[aesop safe apply]
lemma ofNat_mem [Ring R] (S : Subring R) (n : ℕ) [n.AtLeastTwo] :
    OfNat.ofNat (α := R) n ∈ S := by
  rw [←Nat.cast_eq_ofNat]; exact natCast_mem S n

example [Ring R] (S : Subring R) : 5 ∈ S := ofNat_mem S 5
example [Ring R] (S : Subring R) : 5 ∈ S := by aesop -- fails

[Jannis Limperg]

Looks like a bug somewhere. Aesop's indexing doesn't realise that ofNat_mem could be applicable to the target 5 ∈ S. I suspect that the numeric literal is to blame somehow.

[Jireh Loreaux]

I can confirm that this works, so it indeed seems to be numeric literals that are the problem.

example [Ring R] (S : Subring R) (n : ℕ) [n.AtLeastTwo] : OfNat.ofNat n ∈ S := by aesop -- works

[Jireh Loreaux]

@Jannis Limperg any idea how to fix this issue?

[Alex J. Best]

@[aesop safe apply]
lemma ofNat_mem [Ring R] (S : Subring R) (n : ℕ) [n.AtLeastTwo] :
    no_index (OfNat.ofNat (α := R) n) ∈ S := by
  rw [←Nat.cast_eq_ofNat]; exact natCast_mem S n

works

[Jireh Loreaux]

What does no_index do?

[Eric Wieser]

I think it allows matching up to defeq, rather than syntactically

[Eric Wieser]

Though I don't know what the defeq would be

[Patrick Massot]

Ruben Van de Velde said:

Same here. I searched through mathlib to figure out how exactly theorems about ofNat need to be written, and they all had that

Is there anyone who can explain that noindex thing? Eric W asked about is in review too. I am talking about

@[simp]
theorem coeff_ofNat_zero {R : Type*} [Semiring R] (a : ℕ) [a.AtLeastTwo] :
    coeff (no_index (ofNat a : R[X])) 0 = a :=
  coeff_monomial

@Mario Carneiro?

[Mario Carneiro]

That makes simp ignore any structure under coeff, meaning it will try to apply the lemma on any subterm of the form coeff _ 0 instead of coeff (ofNat a) 0

[Mario Carneiro]

this is useful if you want it to match when you have coeff X 0 where X is defeq to ofNat a but not reducibly

[Patrick Massot]

Thanks. Why is it needed in that particular case? Remember the goal was to get

example {R : Type*} [CommRing R] : (X^2 + 2*X + 3 : R[X]).coeff 1 = 2 := by
  simp

working. In this case it looks like the target is exactly ofNat.

[Mario Carneiro]

if I had to guess, it's inferring an extra ofNat to avoid raw numerals and this messes up theorems that want to work on all ofNat expressions

[Patrick Massot]

What is "it"? Lean? Where is it inferring that extra ofNat?

[Mario Carneiro]

inside simp

[Mario Carneiro]

IIRC

[Eric Wieser]

Is that a bug in simp?

[Alex J. Best]

Last I looked at these ofNat things the only difference I would see between my lemmas and the goals was that in the goal they had some weird [AtLeastTwo (7 + 2)] stuff inwhich meant that [AtLeastTwo n] didn't match syntactically (as n is already fixed to be 9 by that point) and hence some noindex was needed

[Eric Wieser]

Could the no_index go in the docs#Nat.AtLeastTwo instances instead?

[Eric Wieser]

Pinging this; are we any closed to understanding why no_index is a good idea here? We have a library note here (pointing back to this thread), but it feels like we're cargo-culting it with no understanding; should no_index go on both the LHS and RHS? Is it only needed for simp lemmas?

[Eric Wieser]

(deleted: I move the discussion instead)

[Notification Bot]

Eric Wieser has marked this topic as unresolved.

[Notification Bot]

14 messages were moved here from #mathlib4 > ✔ Polynomial.coeff example by Eric Wieser.

[Timo Carlin-Burns]

I don't understand why we need no_index with ofNat, but experimentally, it seems it's necessary on the LHS for simp to apply the lemma at all, and it's necessary on both sides of the equation in order to be found by exact?. It's also necessary on the RHS of any equation if we want simp [← not_a_simp_lemma] to work.

[Timo Carlin-Burns]

It seems to me like we want no_index around every occurence of OfNat.ofNat in the library, except in the cases where that leaves no constants to index on so will cause a significant performance regression

[Eric Wieser]

Perhaps we should write an of_nat% n elaborator that inserts the no_index so that we don't have to remember to do this?

[Eric Wieser]

The exact? behavior is interesting, thanks for finding that!

[Timo Carlin-Burns]

Here's a pretty simple repro using exact?:

import Mathlib.Tactic.LibrarySearch

def MyProp (_ : Nat) := False

-- Note: Using `instOfNatNat`, not `instOfNat` (the `NatCast` instance from Mathlib)
theorem myProp_ofNat (n : Nat) : MyProp (OfNat.ofNat n) := sorry

example : MyProp 2 := by exact? -- fails
example : MyProp (OfNat.ofNat 2) := by exact? -- fails
example : MyProp 2 := by exact myProp_ofNat 2

theorem myProp_ofNat' (n : Nat) : MyProp (no_index (OfNat.ofNat n)) := sorry

example : MyProp 2 := by exact? -- succeeds

[Timo Carlin-Burns]

This rules out the hypothesis that the problem has to do with the Nat.AtLeastTwo instance argument

[Timo Carlin-Burns]

For comparison, id behaves a bit differently from OfNat.ofNat here

import Mathlib.Tactic.LibrarySearch

def MyProp (_ : Nat) := False

theorem myProp_id (n : Nat) : MyProp (id n) := sorry

example : MyProp 2 := by exact? -- fails
example : MyProp (id 2) := by exact? -- succeeds, unlike with `OfNat.ofNat`
example : MyProp 2 := by exact myProp_id 2

theorem myProp_id' (n : Nat) : MyProp (no_index (id n)) := sorry

example : MyProp 2 := by exact? -- succeeds

[Timo Carlin-Burns]

It looks like myProp_ofNat ends up in the discrimination tree under [MyProp, OfNat.ofNat, Nat, *, *], which is later not matched when looking for [MyProp, 2]

[Timo Carlin-Burns]

I think this is a bug in core DiscrTree. Should I open an issue? (Using simp for the mwe)

[Eric Wieser]

What's the 2 there in [MyProp, 2]?

[Timo Carlin-Burns]

Lean.Meta.DiscrTree.Key.lit (Lean.Literal.natVal 2)

[Eric Wieser]

That would explain why your PR is such a performance hit too, because the no_index means that we try the lemma on all foo _ goals, not just foo (OfNat _)

[Eric Wieser]

Presumably the lemma is going to the right place in the tree, but the lookup is incorrect?

[Timo Carlin-Burns]

In comparison, a lemma theorem myProp_nat (n : Nat) : MyProp n looks like [MyProp, *] in the discrimination tree, which does get found when looking up MyProp 2. I think there needs to be a special case in the lookup code for when the expression being searched for is a nat literal of type α so it matches both [*] and [OfNat.ofNat, α, *, *]

[Timo Carlin-Burns]

Interestingly, lemmas using natural number "offsets" such as n.succ are special-cased as no_index in the DiscrTree code.

-- DiscrTree key: [MyProp, *] due to `isOffset` special case
theorem myProp_succ (n : Nat) : MyProp (Nat.succ n) := sorry

example : MyProp 2 := by exact? -- succeeds

[Timo Carlin-Burns]

and there used to be one for literals like OfNat.ofNat 2 well, but it was removed in https://github.com/leanprover/lean4/commit/425f42cd839fab576e9be4ba18e76f2bf837615a

[Timo Carlin-Burns]

Ah.. And the reason that explicitly adding OfNat.ofNat 2 to the goal doesn't help is because there's code that normalizes that needle if it's a numeral to just the literal key 2

[Timo Carlin-Burns]

Issue posted lean4#2867

[Eric Wieser]

How exactly are you finding out the DiscrTree key?

[Timo Carlin-Burns]

Hackily..

import Mathlib.Tactic.LibrarySearch

def MyProp (_ : Nat) := False

theorem myProp_ofNat (n : Nat) : MyProp (OfNat.ofNat n) := sorry

theorem myProp_two : MyProp 2 := by exact? -- fails

theorem myProp_ofNat' (n : Nat) : MyProp (no_index (OfNat.ofNat n)) := sorry

theorem myProp_nat (n : Nat) : MyProp n := sorry

open Lean Meta Elab Tactic

def defnName : String := "myProp_ofNat"

elab "dbg_discr_key" : tactic => do
  let cinfo := ((←getEnv).find? defnName).get!
  let processed ← Mathlib.Tactic.LibrarySearch.processLemma defnName cinfo
  logInfo m!"{processed}"

example : True :=by
  dbg_discr_key
  trivial

[Timo Carlin-Burns]

Once lean4#2867 is fixed and we can write lemmas about OfNat.ofNat without needing no_index, it would be really nice to avoid having to duplicate lemmas for both the Nat.cast case and OfNat.ofNat case. Could we avoid this by making some small tweaks to Mathlib's nat casting instances to make Nat.cast and OfNat.ofNat reducibly defeq? Here is one proposal that I think might work:

import Mathlib.Data.Nat.Cast.Defs

-- Redefine `NatCast` so that `Nat.cast n` will be defeq to `OfNat.ofNat n`
abbrev NatCast' (R : Type*) := ∀ n, OfNat R n
abbrev Nat.cast' {R : Type*} [NatCast' R] (n : ℕ) : R := OfNat.ofNat n

-- We can no longer extend `NatCast R`, so we need to add an explicit `natCast` field.
class AddMonoidWithOne' (R : Type u) extends AddMonoid R, One R where
  natCast : ℕ → R := Nat.unaryCast
  natCast_zero : natCast 0 = 0 := by intros; rfl
  natCast_succ : ∀ n, natCast (n + 1) = natCast n + 1 := by intros; rfl

-- Define the `OfNat` instance for all n, removing the `AtLeastTwo` assumption.
instance instOfNat' {R : Type*} {n : ℕ} [AddMonoidWithOne' R] : OfNat R n where
  ofNat := match n with
    | 0 => 0
    | 1 => 1
    | _ => AddMonoidWithOne'.natCast n

example {R : Type*} [AddMonoidWithOne' R] (n : ℕ) : (Nat.cast' n : R) = OfNat.ofNat n := by
  with_reducible rfl

-- Note: Although there are now two instances of `OfNat R 0`, they are reducibly defeq.
example {R : Type*} [AddMonoidWithOne' R] : @OfNat.ofNat R 0 Zero.toOfNat0 = @OfNat.ofNat R 0 instOfNat' := by
  with_reducible rfl

[Johan Commelin]

I kicked

fix: add missing no_index around OfNat.ofNat #8317

on the queue. But clearly this approach isn't sustainable. So I hope some elaborator trickery, or some patch to simp, will allow us to revert this PR in the future.

[Oliver Nash]

Is there an issue capturing for this anywhere? This no_index stuff is pretty undesirable.

[Eric Wieser]

Yes, lean4#2867 referenced two messages above