# Zulip Chat Archive

## Stream: maths

### Topic: lifting arithmetic

#### Jalex Stark (May 18 2020 at 21:39):

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 (May 18 2020 at 21:40):

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 (May 18 2020 at 21:42):

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 (May 18 2020 at 21:44):

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

#### Kevin Buzzard (May 18 2020 at 21:45):

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

#### Jalex Stark (May 18 2020 at 21:45):

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 (May 18 2020 at 21:45):

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

#### Jalex Stark (May 18 2020 at 21:46):

hmm no, it's defined for nats

#### Kevin Buzzard (May 18 2020 at 21:46):

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 (May 18 2020 at 21:47):

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 (May 18 2020 at 21:47):

I think my question still makes sense after `rw nat.sub_eq_iff_eq_add`

so that there's no subtraction

#### Kevin Buzzard (May 18 2020 at 21:48):

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 (May 18 2020 at 21:49):

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 (May 18 2020 at 21:49):

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 (May 18 2020 at 21:49):

I think `field_simp`

is doing something similar

#### Jalex Stark (May 18 2020 at 21:49):

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 (May 18 2020 at 21:50):

For every subterm`a - b`

of the theorem, `a >= b`

must be in the context or otherwise provable

#### Jalex Stark (May 18 2020 at 21:51):

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

#### Mario Carneiro (May 18 2020 at 21:51):

I think you can apply `int.coe_nat_inj`

and then use `simp [*]`

to push the coercions to the leaves

#### Kevin Buzzard (May 18 2020 at 21:51):

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

#### Kevin Buzzard (May 18 2020 at 21:52):

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

#### Jalex Stark (May 18 2020 at 21:52):

fixed

#### Jalex Stark (May 18 2020 at 21:56):

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 (May 18 2020 at 21:57):

wait, that's the easy version

#### Mario Carneiro (May 18 2020 at 21:57):

there are no subtracts

#### Jalex Stark (May 18 2020 at 21:57):

Yeah, we xy'ed the subtraction away

#### Jalex Stark (May 18 2020 at 21:57):

the easy version is the thing I wanted

#### Mario Carneiro (May 18 2020 at 21:58):

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 (May 18 2020 at 21:58):

And I'm saying, if you have a goal with `nat.sub`

in it then you already made a mistake.

#### Mario Carneiro (May 18 2020 at 21:59):

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 (May 18 2020 at 21:59):

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

#### Mario Carneiro (May 18 2020 at 22:00):

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 (May 18 2020 at 22:00):

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 (May 18 2020 at 22:00):

Mathematicians would not use `Ico x y`

if `y<<x`

. We have certain conventions which preclude this.

#### Jalex Stark (May 18 2020 at 22:00):

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 (May 18 2020 at 22:01):

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

#### Kevin Buzzard (May 18 2020 at 22:01):

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

#### Mario Carneiro (May 18 2020 at 22:01):

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

#### Kevin Buzzard (May 18 2020 at 22:02):

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

#### Mario Carneiro (May 18 2020 at 22:02):

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

or not

#### Kevin Buzzard (May 18 2020 at 22:03):

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 (May 18 2020 at 22:03):

but it's not an ill formed question

#### Kevin Buzzard (May 18 2020 at 22:03):

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

.

#### Jalex Stark (May 18 2020 at 22:04):

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

#### Mario Carneiro (May 18 2020 at 22:04):

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 (May 18 2020 at 22:04):

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 (May 18 2020 at 22:05):

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

#### Kevin Buzzard (May 18 2020 at 22:05):

That's interesting.

#### Jalex Stark (May 18 2020 at 22:05):

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 (May 18 2020 at 22:05):

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

#### Mario Carneiro (May 18 2020 at 22:06):

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

is that

#### Mario Carneiro (May 18 2020 at 22:06):

so you can't rewrite with that

#### Kevin Buzzard (May 18 2020 at 22:06):

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

#### Kevin Buzzard (May 18 2020 at 22:07):

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

#### Kevin Buzzard (May 18 2020 at 22:08):

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 (May 18 2020 at 22:08):

but formalising the proof has brought this out explicitly.

#### Mario Carneiro (May 18 2020 at 22:09):

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 (May 18 2020 at 22:09):

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 (May 18 2020 at 22:10):

Mathematicians do not write these things.

#### Mario Carneiro (May 18 2020 at 22:10):

Yes, but we aren't in that situation

#### Kevin Buzzard (May 18 2020 at 22:10):

Indeed!

#### Mario Carneiro (May 18 2020 at 22:10):

`Ico.card`

has applicability to that situation but that doesn't matter here

#### Mario Carneiro (May 18 2020 at 22:11):

I'm saying that it's not necessary to ban `nat.sub`

even in the places where it is well defined

#### Mario Carneiro (May 18 2020 at 22:11):

which your comments seem to suggest

#### Kevin Buzzard (May 18 2020 at 22:11):

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 (May 18 2020 at 22:12):

the original question, `2 ^ (n + 2) - 2 ^ (n + 1) = 2 ^ (n + 1)`

, is within the mathematician strike zone

#### Mario Carneiro (May 18 2020 at 22:13):

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 (May 18 2020 at 22:13):

which of course it is in this case

#### Mario Carneiro (May 18 2020 at 22:14):

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 (May 18 2020 at 22:19):

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 (May 18 2020 at 22:20):

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 (May 18 2020 at 22:20):

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

#### Yury G. Kudryashov (May 18 2020 at 22:20):

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

#### Kevin Buzzard (May 18 2020 at 22:21):

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

#### Yury G. Kudryashov (May 18 2020 at 22:22):

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

#### Kevin Buzzard (May 18 2020 at 22:23):

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

#### Mario Carneiro (May 18 2020 at 22:24):

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 (May 18 2020 at 22:28):

Someday we'll need both of them anyway

#### Yury G. Kudryashov (May 18 2020 at 22:29):

@Kevin Buzzard Yes, search for `deriv_log`

#### Mario Carneiro (May 18 2020 at 22:31):

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 (May 18 2020 at 22:33):

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 (May 18 2020 at 22:34):

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

#### Matt Earnshaw (May 18 2020 at 22:37):

(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 (May 18 2020 at 22:40):

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 (May 18 2020 at 22:41):

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 (May 18 2020 at 22:47):

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 (May 18 2020 at 22:50):

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 (May 18 2020 at 22:51):

and they said semirings were useless ;)

#### Jalex Stark (May 18 2020 at 22:51):

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

#### Jalex Stark (May 18 2020 at 22:52):

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

#### Matt Earnshaw (May 18 2020 at 22:53):

yeah, I suppose the theorem would suffice

#### Matt Earnshaw (May 18 2020 at 23:03):

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 (May 18 2020 at 23:11):

doing math for fun? crazy

#### Kevin Buzzard (May 18 2020 at 23:13):

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 (May 18 2020 at 23:14):

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

#### Reid Barton (May 19 2020 at 04:18):

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 (May 19 2020 at 04:20):

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 (May 19 2020 at 04:25):

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 (May 19 2020 at 04:26):

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

#### Mario Carneiro (May 19 2020 at 04:27):

right

#### Jalex Stark (May 19 2020 at 04:27):

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

#### Mario Carneiro (May 19 2020 at 04:27):

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 (May 19 2020 at 04:28):

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

#### Reid Barton (May 19 2020 at 04:28):

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 (May 19 2020 at 04:28):

I guess maybe not with this latest idea.

#### Reid Barton (May 19 2020 at 04:29):

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 (May 19 2020 at 05:13):

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 (May 19 2020 at 05:37):

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

#### Jalex Stark (May 19 2020 at 05:39):

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 (May 19 2020 at 06:07):

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 (May 19 2020 at 06:09):

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

Last updated: May 11 2021 at 02:05 UTC