lifting arithmetic

Stream: maths

[Jalex Stark]

Here's an example of an arithmetic fact that's somewhat harder to prove in ℕ than ℤ. It's also clear to a mathematician that the latter one implies the former.

example (n : ℕ) : 2 ^ (n + 2) - 2 ^ (n + 1) = 2 ^ (n + 1) :=
begin
    rw nat.sub_eq_iff_eq_add,
    {rw nat.pow_succ, ring},
    apply le_add_left, refl,
end

example (n : ℕ) : (2: ℤ) ^ (n + 2) - 2 ^ (n + 1) = 2 ^ (n + 1) :=
begin
ring_exp, norm_num, ring,
end

[Jalex Stark]

After a bit of thought, it seems the reason it's clear that one implies the other is because there's an embedding of semirings ℕ → ℤ. Is it feasible to make a tactic that helps you figure out that that's what you need? (And then, is typeclass instance search able to find that embedding?)

[Jalex Stark]

I'm imagining that at the commented point in this proof you say something like transfer key and the goal gets replaced with asking you for a semiring embedding (or maybe it asks for separate embeddings for the has_add and has_pow)

example (n : ℕ) : 2 ^ (n + 2) - 2 ^ (n + 1) = 2 ^ (n + 1) :=
begin
have key :  (2: ℤ) ^ (n + 2) = 2 ^ (n + 1) + 2 ^ (n + 1) := by {ring_exp, norm_num, ring},
rw nat.sub_eq_iff_eq_add,
-- apply an embedding of semirings ℕ → ℤ?
end

[Kevin Buzzard]

I am now strongly of the opinion that one should not even be proving results like your example

[Kevin Buzzard]

I don't think that your question should typecheck because I don't think subtraction should be defined on nat

[Jalex Stark]

Here's where it came from

import tactic

import algebra.big_operators
import data.real.basic

noncomputable theory
open_locale classical
open_locale big_operators
open finset

lemma p1 (n : ℕ) :
1/2 ≤ ∑ k in (finset.Ico (2^(n+1)) (2^(n+2))), (1:ℚ)/k  :=
begin
    transitivity ∑ k in (finset.Ico (2^(n+1)) (2^(n+2))), (1 : ℚ) / 2^(n+2),
    rw sum_const,
    rw Ico.card,
    apply le_of_eq,
    field_simp,

    have calc2 : 2 ^ (n + 2) - 2 ^ (n + 1) = 2 ^ (n + 1),
    rw nat.sub_eq_iff_eq_add, ring_exp, norm_num, ring,
    ring_exp, rw mul_comm,
    rw mul_le_mul_right, norm_num, refine pow_pos _ n, norm_num,
end

[Jalex Stark]

oh, I guess finset.Ico would be fine working with integers!

[Jalex Stark]

hmm no, it's defined for nats

[Kevin Buzzard]

There is more to it than your claim that the inclusion is a morphism of semirings. The problem is that the inclusion does not commute with - and the reason for this is that if mathematicians were in charge then subtraction on naturals would not make sense

[Mario Carneiro]

It's also clear to a mathematician that (1 : int) - 2 + 2 = 1 implies (1 : nat) - 2 + 2 = 1 but this is false

[Jalex Stark]

I think my question still makes sense after rw nat.sub_eq_iff_eq_add so that there's no subtraction

[Kevin Buzzard]

But presumably there's a side condition of the form "we're in the region where natural subtraction is not a pathological operation"

[Jalex Stark]

I think in this pair of examples, the second proof is still harder than the first

example (n : ℕ) : 2 ^ (n + 2)  = 2 ^ (n + 1) + 2 ^ (n + 1):=
begin
    rw nat.pow_succ, ring,
end

example (n : ℕ) : (2: ℤ) ^ (n + 2) = 2 ^ (n + 1) + 2 ^ (n + 1) :=
begin
ring_exp, norm_num, ring,
end

[Mario Carneiro]

You can freely move between nat and int versions of a theorem provided you have assumptions saying that all subterms are well defined

[Mario Carneiro]

I think field_simp is doing something similar

[Jalex Stark]

Mario Carneiro said:

You can freely move between nat and int versions of a theorem provided you have assumptions saying that all subterms are well defined

That sounds like what I'm trying to learn about, can you say more?

[Mario Carneiro]

For every subterma - b of the theorem, a >= b must be in the context or otherwise provable

[Jalex Stark]

sure, but how do you do actually do the moving between nat and int?

[Mario Carneiro]

I think you can apply int.coe_nat_inj and then use simp [*] to push the coercions to the leaves

[Kevin Buzzard]

I can't get anything to compile. Can you supply the imports?

[Kevin Buzzard]

(I mean the "Here's where it came from" post)

[Jalex Stark]

fixed

[Jalex Stark]

Mario Carneiro said:

I think you can apply int.coe_nat_inj and then use simp [*] to push the coercions to the leaves

Yes, this works

import tactic

example (n : ℕ)  (h : (2: ℤ) ^ (n + 2)  = 2 ^ (n + 1) + 2 ^ (n + 1)) : 2 ^ (n + 2) = 2 ^ (n + 1) + 2 ^ (n + 1) :=
begin
    apply int.coe_nat_inj, simp, exact h,
end

[Mario Carneiro]

wait, that's the easy version

[Mario Carneiro]

there are no subtracts

[Jalex Stark]

Yeah, we xy'ed the subtraction away

[Jalex Stark]

the easy version is the thing I wanted

[Mario Carneiro]

I'm saying, if you have a goal with subtracts in it and want to get rid of them by casting to int, that's the procedure

[Kevin Buzzard]

And I'm saying, if you have a goal with nat.sub in it then you already made a mistake.

[Mario Carneiro]

In your case you get a subtract from Ico.card, which actually has a genuine use for the nat.sub because it is actually a truncated subtraction

[Kevin Buzzard]

And I know that Mario will know counterexamples in CS, but in maths I am sticking to my guns

[Mario Carneiro]

Mathematician speak for the theorem would be |{a..b}| = max(0, b - a), and so there is an extra step to rewrite the max(0, b-a) into b-a

[Jalex Stark]

I think Ico.card is useful for maths, so maybe we can think of an API that doesn't expose the nat substract

[Kevin Buzzard]

Mathematicians would not use Ico x y if y<<x. We have certain conventions which preclude this.

[Jalex Stark]

I think the a maths-ier version of Ico carries a proof of a \le b
(Edit: this is exactly what kevin just said)

[Kevin Buzzard]

Right, it's like division. I'm not complaining about division on $\mathbb{Q}$ because we never divide by 0.

[Kevin Buzzard]

I will only write $\sum_{x=a}^b$ if $b\geq a-1$.

[Mario Carneiro]

But we still need to be able to talk about the cardinality of {x \in int | a <= x < b}

[Kevin Buzzard]

I'm happy with $\sum_{i=1}^0$ but $\sum_{i=2}^0$ is "not allowed" as part of math interface.

[Mario Carneiro]

that's a mathematical question independent of whether that is called Ico or not

[Kevin Buzzard]

In mathematics one does not usually find oneself in the situation where you need the cardinality of that set and $b\leq a$.

[Mario Carneiro]

but it's not an ill formed question

[Kevin Buzzard]

It's just the way it works. And if you do, then yeah rotten luck, it's some max.

[Jalex Stark]

maybe we can leave Ico as is and have something math friendly like ∑ from a to b

[Mario Carneiro]

We could have a theorem about Ico.card in the presence of a le assumption, but there isn't much the theorem can say that is more informative

[Kevin Buzzard]

Right, it's not an ill-formed question, and the well-formed answer is that it's a max. There is this weird thing going on which I still don't really understand, where mathematicians only really see objects when they are at some certain level of "decency" which is hard to quantify.

[Mario Carneiro]

Maybe a better version of the theorem is a + c = b -> (Ico b a).card = c

[Kevin Buzzard]

That's interesting.

[Jalex Stark]

Mario Carneiro said:

We could have a theorem about Ico.card in the presence of a le assumption, but there isn't much the theorem can say that is more informative

it can say that the length is (a:ℤ) - (b:ℤ)

[Kevin Buzzard]

Yeah this is a really funny situation. Nat subtraction is clearly made for this kind of question.

[Mario Carneiro]

no, it can say that the length casted to int is that

[Mario Carneiro]

so you can't rewrite with that

[Kevin Buzzard]

Oh I see. The original question is "mathematical" so it carries an implicit assumption then $2^{n+1}\leq 2^{n+2}$.

[Kevin Buzzard]

The very fact that you're summing over that range means that the subtraction is going to be OK.

[Kevin Buzzard]

It is implicit in the question itself that $2^{n+1}\leq 2^{n+2}$, and mathematicians would not state this because ass Jalex says, it is "obvious to us".

[Kevin Buzzard]

but formalising the proof has brought this out explicitly.

[Mario Carneiro]

sure, but if you have the necessary in range assumptions, then a - b is not a bad thing to write, and it is exactly as bad as Ico b a itself, so the theorem Ico.card is fine

[Kevin Buzzard]

But Ico b a is a "mathematically" bad thing to write if $a<b$, like $1/0$ is a bad thing to write

[Kevin Buzzard]

Mathematicians do not write these things.

[Mario Carneiro]

Yes, but we aren't in that situation

[Kevin Buzzard]

Indeed!

[Mario Carneiro]

Ico.card has applicability to that situation but that doesn't matter here

[Mario Carneiro]

I'm saying that it's not necessary to ban nat.sub even in the places where it is well defined

[Mario Carneiro]

which your comments seem to suggest

[Kevin Buzzard]

Sure. But I want to argue that if a mathematician has run into it then either they've done something wrong or the inequality which enables you to rewrite as an addition is "in the context somewhere".

[Mario Carneiro]

the original question, 2 ^ (n + 2) - 2 ^ (n + 1) = 2 ^ (n + 1), is within the mathematician strike zone

[Mario Carneiro]

and the assumption that this is a mathematically reasonable assertion allows you to assume that 2 ^ (n + 1) <= 2 ^ (n + 2) is provable

[Mario Carneiro]

which of course it is in this case

[Mario Carneiro]

Mario Carneiro said:

I think you can apply int.coe_nat_inj and then use simp [*] to push the coercions to the leaves

This is how you deal with mathematically reasonable questions involving nat.sub

[Yury G. Kudryashov]

It seems that you're going to prove that $\sum \frac{1}{n}$ diverges. I think that it should come with the p-series test.

[Kevin Buzzard]

I've had to apply int.coe_nat_inj before, when I wanted to use proper subtraction. I wonder if there should be a shortcut for this? I always have to look up the name because I can never remember (a) whether it's coe or cast and (b) which namespace it's in

[Mario Carneiro]

You can also generalize the proof method to the Cauchy condensation test

[Yury G. Kudryashov]

BTW, you can easily prove the integral test without actual integrals using MVT.

[Kevin Buzzard]

You can do it with the integral test as well, which would be simple if the infrastructure was there

[Yury G. Kudryashov]

@Kevin Buzzard If you start with $F'=f$, then you only need MVT, and it's there.

[Kevin Buzzard]

Do we know the derivative of log is 1/x?

[Mario Carneiro]

The integral test method might be useful if we want to define the Euler-Mascheroni constant, but otherwise I would say the condensation test is quite simple and elementary

[Yury G. Kudryashov]

Someday we'll need both of them anyway

[Yury G. Kudryashov]

@Kevin Buzzard Yes, search for deriv_log

[Mario Carneiro]

In metamath I've advocated for never using integrals at all, in favor of antiderivatives, because when the antiderivative is elementary you are writing both sides anyway

[Mario Carneiro]

for all the usual analysis applications all you use about intervals is additivity, breaking one along a partition and bounding by constants, and all these things are also true of antiderivatives using the MVT

[Mario Carneiro]

(you also need countable choice to define the lebesgue integral but not derivatives)

[Matt Earnshaw]

(mathematician voice) nat.sub is the most natural operation in the world ... being simply the adjoint to addition operators in a poset x + a ≥ y iff x ≥ y - a (playing devil's advocate and hoping Kevin won't notice this is the lambda abstraction rule in disguise :grinning_face_with_smiling_eyes: )

[Matt Earnshaw]

on a more serious note, I have been wondering if this work would provide the foundations for a useful tactic https://arxiv.org/abs/math/0212377

[Mario Carneiro]

Matt Earnshaw said:

I have been wondering if this work would provide the foundations for a useful tactic <link>

This is the kind of message spammers should send :D

[Jalex Stark]

Matt Earnshaw said:

on a more serious note, I have been wondering if this work would provide the foundations for a useful tactic https://arxiv.org/abs/math/0212377

Do you mean just the part about lifting identities from rings to rigs (Theorem 5.1), or the whole rig category stuff?

[Matt Earnshaw]

Jalex Stark said:

Matt Earnshaw said:

on a more serious note, I have been wondering if this work would provide the foundations for a useful tactic https://arxiv.org/abs/math/0212377

Do you mean just the part about lifting identities from rings to rigs (Theorem 5.1), or the whole rig category stuff?

the former really, though I have a personal interest in the rig category side of things

[Mario Carneiro]

and they said semirings were useless ;)

[Jalex Stark]

What's the tactic? Don't you just need the theorem?

[Jalex Stark]

(Or, if there might eventually be a useful tactic, then the theorem on its own should be useful?)

[Matt Earnshaw]

yeah, I suppose the theorem would suffice

[Matt Earnshaw]

I'll try and have a crack at the lemmas this week, for a bit of fun even if it would seldom find application

[Jalex Stark]

doing math for fun? crazy

[Kevin Buzzard]

Someone on Twitter had the gall to suggest that funding agencies did not consider "PI will have fun doing this" as evidence that a project should be funded

[Kevin Buzzard]

It's pretty much the only reason I've ever done anything

[Reid Barton]

If - on nat were a partial function, you would always have the information you need to reduce questions about it to int on hand.

[Reid Barton]

Obviously as a mathematician I am biased, but I suspect that using partial functions is generally better than totalizing in principle, it's just not that practical without better automation than we currently have.

[Mario Carneiro]

My impression is that it is this thinking that leads to the general huge difference in sizes of terms between DTT and ZFC. Obviously I am also biased, but I would like to see if it is possible to instead implement type theory with an undefinedness logic where bad applications evaluate to a bottom value

[Jalex Stark]

so a type theory where the option monad is always open?

[Mario Carneiro]

right

[Jalex Stark]

yeah i think that's closer to how i think than Lean's type theory is

[Mario Carneiro]

possibly also done in a way where you can "invert" well definedness assumptions, i.e. x+y is well defined implies that x and y are

[Mario Carneiro]

because this really cuts down on the number of assumptions you have to keep around

[Reid Barton]

But this doesn't really solve the issue here because then you still need to synthesize a proof that the -s are well-formed to convert to int.

[Reid Barton]

I guess maybe not with this latest idea.

[Reid Barton]

The term size issue is indeed awkward. One would like to say that we can just forget the proof term by definitional proof irrelevance. We just need to keep track of the fact that x >= y, we don't need to remember how to prove it.

[Johan Commelin]

Jalex Stark said:

What's the tactic? Don't you just need the theorem?

I guess, once you have the theorem, the tactic could try to automatically show that in the special case of nat all the a < b conditions for nat.cast_sub are satisfied.

[Jalex Stark]

uh by "the theorem" i meant theorem 5.1 in the "a tree is seven trees" paper

[Jalex Stark]

which says that under mild assumptions, for polynomials $p,q,q'$, if $x = p(x) \implies q(x) = q'(x)$ in arbitrary rings, then the same implication holds in arbitrary rigs

[Mario Carneiro]

I think you would have difficulty applying this theorem directly in the context of categories though, because it's an isomorphism not an equality

[Jalex Stark]

yes, I think matt's aim was mostly to use it for bare rigs and rings