norm_num characteristic functionality

Stream: mathlib4

[Thomas Murrills]

While the functionality for rational numbers now works (yay!), the given example in mathlib4#1102 (example {α} [DivisionRing α] [CharZero α] : (-1:α) ≠ 2 := by norm_num) still doesn't, because characteristic functionality is something else. Maybe there should be a new issue for that? @Heather Macbeth how time-sensitive is support for characteristics vs., say, ring?

[Thomas Murrills]

(Or, actually—would this count as ≠ functionality? :thinking:)

[Mario Carneiro]

yes

[Mario Carneiro]

we need inequalities, including !=

[Thomas Murrills]

tracking issue for inequalities: mathlib4#1567

[Thomas Murrills]

open PR for ≠ in particular: mathlib4#1568

[Heather Macbeth]

Thomas Murrills said:

Heather Macbeth how time-sensitive is support for characteristics vs., say, ring?

cross-ref to https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Rat.20in.20norm_num/near/321399782 for further discussion of Thomas' questions about priorities.

[Thomas Murrills]

Am I right in thinking we’ll need something like .isProp typeExpr proof as a constructor for Result(')? or possibly .isNe α proof, .isLe α proof, etc.?

If so is one of these obviously better? And if the latter, what about e.g. .isNe α lhs rhs proof instead for results lhs and rhs? I’m wondering about the latter in case any later tactics will need to actually string these results together somehow, and I’m wondering if they might need some extra info from a result.

[Thomas Murrills]

(We could also do something like isRel α rel lhs rhs proof with rel representing the (name of the) relation somehow, e.g. tokens .le, .ne or something if we wanted to cut down on how many constructors we have for Result.)

[Thomas Murrills]

I think I’ve got an idea for how to structure things in the move to give norm_num the ability to prove props.

so, there are really only two possible purposes of any given norm_num extension: it’s either constructing a literal value (a number) or proving a Prop. We know its purpose in advance.

So the thought is: what if we added a(n essentially boolean) parameter to Result and NormNumExt to keep track of which kind of thing they’re doing? This would make the code easier to handle since we could keep the two cases separate. .isRat etc. would construct values of Result .num e, whereas e.g. .isLe (or however exactly we did it) would construct values of Result .prop e. That should mean we wouldn’t be matching on constructors in extension code that didn’t make sense to match on. We’d also know e.g. whether it made sense to extract a literal from a Result based on the type (though I guess that’s not too much of an issue since we work in Option and can have things just fail, but still).

This might mean maintaining two discrimination trees, one for NormNumExt .prop and one for NormNumExt .num—not sure. derive would get an extra argument like this as well, saying whether it should try to derive a number or a prop. (We’d need to infer the kind of result we wanted from the expression at the beginning of the outermost norm_num process, but it’s easy to test an expression for Prophood, iirc?)

I think it would keep the code cleaner, but what I don’t know is whether it would be good for performance. Keeping the two discrimination trees separate might be good for performance, or it could be negligible; likewise for matching on less constructors and the opposite for having more arguments in Result.

Giving norm_num the ability to handle Props will mean refactoring/updating code in one place or another, and this is the least annoying way I can think of—it lets us leave basically all of our number-handling code as-is at the cost of a little change to the infrastructure. Plus we get useful information in the type.

If this sounds good lmk and I’ll have fun implementing it!

[Mario Carneiro]

@Thomas Murrills I pushed some changes to your branch to set up inequality proving and I tried to do one of everything so that there are enough clues to do the rest. For ne, the proof approach which is used in mathlib3 is to prove either lt or gt depending on which one we can establish, so the main work is on le/lt.

[Thomas Murrills]

Sounds great! I see we went with the “add another constructor to Result” approach, and we just treat them as boolean literals.

All that I don’t get is why we return a proof of the negation of a prop even when we’re apparently trying to prove the prop. (the else branch at the end of <). Does this yield useful error messages or something? Or does it work differently?

[Thomas Murrills]

(Also, just as a disclaimer, the weekends are when I have the least amount of time to actually code—I might have a bit of time today, but if I can’t finish it today, I will tomorrow.)

[Mario Carneiro]

When norm_num is given an inequality like 2 < 5 or 4 < 1, it's supposed to normalize it, to True or False (that is to say, prove or disprove it). This is important for three reasons: (1) when used as a non-goal-closing normalization it's supposed to replace subterms like 2 < 5 with True even if it's not at the top level, (2) reducing a goal to False is a way to communicate that norm_num didn't just fail but actually disproved the claim, and (3) norm_num at h can close goals by reducing them to False

[Mario Carneiro]

Remember that in all other cases when we are given an expression like 2 + 3 we are supposed to return a normal form expression which is provably equal to the input. For 2 < 3 it's the same thing, the normal form expression provably equal to that is True

[Thomas Murrills]

That makes sense!

[Mario Carneiro]

No problem if you can't get to it soon, I just wanted to make sure I got the architecture stuff in first :)

[Thomas Murrills]

Ok, finally working on it! Schedule's clear, thought about it when I could, and I hope to finish it today.

[Thomas Murrills]

Two technical questions about the setup:

[Thomas Murrills]

1. Why is the setup for < different than for ≠? For < we do

  let .app (.app f a) b ← whnfR e | failure
  let ⟨.succ u, α, a⟩ ← inferTypeQ a | failure
  have b : Q($α) := b

but for ≠ we do

let .app (.app f (a : Q($α))) (b : Q($α)) ← withReducible (whnf e) | failure

[Thomas Murrills]

2. Why do we wait so long to check if it's lt (guard <|← withNewMCtxDepth <| isDefEq f q(LT.lt (α := $α))) compared to the other extensions? Seems like we only do it in the nat arm right now. Presumably we'll do it in all arms once implemented, but why wait til we're inside the arms? Guess: because somehow the ordered semiring instance _i inferred right before bears on it invisibly EDIT: Oh, I get it, we need to synthesize the instance for LT.

[Thomas Murrills]

Is there a reason we don't have a norm_num extension for Eq? It seems kind of asymmetric. Shouldn't we be able to normalize 2 = 2 to True?

[Thomas Murrills]

(I'm going to make one given that I have (a good chunk of) ≠ and if it explodes it explodes...)

[Heather Macbeth]

Thomas Murrills said:

Is there a reason we don't have a norm_num extension for Eq? It seems kind of asymmetric. Shouldn't we be able to normalize 2 = 2 to True?

Not an expert, but indeed I do think this should exist. It was there in Lean 3:

import tactic.norm_num
import data.real.basic

example : (1:ℝ) + 3 = 4 := by norm_num1

[Mario Carneiro]

@Thomas Murrills said:

1. Why is the setup for < different than for ≠? For < we do

  let .app (.app f a) b ← whnfR e | failure
  let ⟨.succ u, α, a⟩ ← inferTypeQ a | failure
  have b : Q($α) := b

but for ≠ we do

let .app (.app f (a : Q($α))) (b : Q($α)) ← withReducible (whnf e) | failure

That's because I didn't look carefully at the ne code, it needs to do the same thing as the other relations. You can't use alpha here because alpha is the type of the relation itself, which is Prop

[Mario Carneiro]

the purpose of those lines in the le code is to find the alpha we actually care about

[Thomas Murrills]

Makes sense! I managed to figure it out and ≠ functionality is done up to two Rat-related sorries. I did it via = and Not, though—is that alright? (I kept around some early ≠-specific versions from an earlier draft in case it's not) I also didn't use the mathlib3 approach, since we don't have order in the general case; I just used congruence or {injectivity given CharZero} directly.

[Thomas Murrills]

Still left to do is < and ≤ (and subtraction for natural numbers, apparently, which I found out when refining the tests; simp had been taking care of those tests)

[Heather Macbeth]

(personally, I consider nat subtraction very low priority, something that could wait for a future version)

[Thomas Murrills]

Cool! Teaching priorities are definitely the guide here :)

[Thomas Murrills]

I hope to finish < and ≤ tomorrow (if they don't get done in the meantime)—the infrastructure is in place (thanks to Mario! :) ) and I just need to go through the motions. I'm going to change the ≠ PR title/description to cover all of them.

[Thomas Murrills]

mathlib4#1568 now updated

[Thomas Murrills]

Is the smallest thing that's a division ring and has a (compatible) order a LinearOrderedField? (If so is this a mathematical fact or just a mathlib fact?)

[Heather Macbeth]

I don't know, but that is certainly good enough for practical purposed!

[Damiano Testa]

As for the mathematical question, it seems that there are non-commutative ordered division rings: see @Alex J. Best answer here.

[Thomas Murrills]

We should have an instance for Nontrivial given CharZero:

variable [AddMonoidWithOne α] [CharZero α]
#synth Nontrivial α -- failed to synthesize instance Nontrivial α

(< lemmas depend on Nontrivial, not CharZero, but often I'd imagine we have the latter)

Does this exist but just in a weird place?

If not, where should it go?

[Thomas Murrills]

Also, what about the other way when we have enough structure? Specifically, an instance for CharZero given a Nontrivial OrderedRing?

[Damiano Testa]

In Lean3 there are docs#char_zero.infinite and docs#infinite.nontrivial.

[Heather Macbeth]

If it's easier you can stick to LinearOrderedRing, which is automatically Nontrivial and CharZero.

[Thomas Murrills]

Heather Macbeth said:

If it's easier you can stick to LinearOrderedRing, which is automatically Nontrivial and CharZero.

Okay, all tests work for LinearOrderedRing currently! It's just the case where we have OrderedRing and CharZero where e.g. -1 < 2 will fail, because it needs Nontrivial.

[Heather Macbeth]

I'm sure someone, someday, will demand that functionality! :-). But it's rather low priority.

[Thomas Murrills]

Damiano Testa said:

In Lean3 there are docs#char_zero.infinite and docs#infinite.nontrivial.

Interesting, I guess it hasn't been ported yet. Would it make sense to put a direct instance in either the file that defines CharZero or Nontrivial, whichever comes "second" (if either)? Or do we need to avoid diamonds (well, here a triangle) for when infinite stuff gets ported? (I would hope not with Props, but...)

[Gabriel Ebner]

CharZero and Nontrivial are both props, so there's no danger of diamonds.

[Thomas Murrills]

Great, that's what I hoped!

[Damiano Testa]

There are also a few "shortcut" instances in mathlib, similar to the one that you are proposing.

[Damiano Testa]

My view is that, if it makes stuff work, definitely go for it!

[Thomas Murrills]

Hmm, is OrderedRing sufficient to prove na * ⅟da ≤ nb * ⅟db given na * db ≤ nb * da? OrderedRing tells us that 0 ≤ 1, addition preserves ≤, and that the set of nonnegative elements is closed under multiplication (by each other). We only demand a partial order.

It seems to me like ℤ with 1/2 adjoined keeping only ≤ relations among integers (and all half-odd integers not related to anything but each other) might be fine. We can't have 1/2 ≤ 0, otherwise 0 ≤ -1/2 and multiplying by 2 gets us 0 ≤ -1—not allowed since the ring is nontrivial. But keeping it unrelated to 0 might be ok.

For now I'm going to use LinearOrderedRing for rat functionality since we need an instance of that in most cases anyway, but I was still just wondering.

[Kevin Buzzard]

What about na=nb=da=1, db=-1?

[Thomas Murrills]

Ah, sorry, I forgot to specify: da and db are natural numbers here

[Thomas Murrills]

Ok, I proved the last sorry! It all works (and I made a bunch more tests to check), and mathlib4#1568 has a green check. :)

[Thomas Murrills]

However, I might have made some questionable choices surrounding the definitions I chose and some instance management. @Mario Carneiro, want to take a look when you get a chance? I left comments labeled with !! where I thought there might be an issue with what I did.

[Mario Carneiro]

I pushed some changes and addressed all the !! open questions

[Mario Carneiro]

One thing I wanted to remark: for the "rationals are equal" case, it suffices to just have numerator and denominator the same syntactically, we don't have to check that they are multiples of each other because we maintain an invariant that the rationals are reduced and expressions are in canonical form, so if the rational values are equal then the normalized expressions are syntactically equal

[Thomas Murrills]

Nice! I scrolled through the latest commit; really nice minimizations in general! Should I change the PR’s label to awaiting-review? EDIT: I read through it once more and it looked good to me, so I put it on the queue!

[Kevin Buzzard]

Re na/da<=nb/db: Yes I think you're right. Z[1/2] (note that this contains 1/4 and 1/2^{100} because it's a ring; the general element is of the form a/2^n with a an integer and n a natural) with the order defined by a<=b iff b-a is a natural, seems to be an ordered ring as far as mathlib is concerned, and 0/2=0<=1/2 is false whereas 0<=2 is true.