Zulip Chat Archive

Stream: maths

Topic: lifting arithmetic


view this post on Zulip 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

view this post on Zulip 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?)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jalex Stark (May 18 2020 at 21:45):

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

view this post on Zulip Jalex Stark (May 18 2020 at 21:46):

hmm no, it's defined for nats

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 18 2020 at 21:49):

I think field_simp is doing something similar

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (May 18 2020 at 21:50):

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

view this post on Zulip Jalex Stark (May 18 2020 at 21:51):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 18 2020 at 21:51):

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

view this post on Zulip Kevin Buzzard (May 18 2020 at 21:52):

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

view this post on Zulip Jalex Stark (May 18 2020 at 21:52):

fixed

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 18 2020 at 21:57):

wait, that's the easy version

view this post on Zulip Mario Carneiro (May 18 2020 at 21:57):

there are no subtracts

view this post on Zulip Jalex Stark (May 18 2020 at 21:57):

Yeah, we xy'ed the subtraction away

view this post on Zulip Jalex Stark (May 18 2020 at 21:57):

the easy version is the thing I wanted

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (May 18 2020 at 22:01):

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

view this post on Zulip Kevin Buzzard (May 18 2020 at 22:01):

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

view this post on Zulip 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}

view this post on Zulip Kevin Buzzard (May 18 2020 at 22:02):

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

view this post on Zulip Mario Carneiro (May 18 2020 at 22:02):

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

view this post on Zulip 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 bab\leq a.

view this post on Zulip Mario Carneiro (May 18 2020 at 22:03):

but it's not an ill formed question

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 18 2020 at 22:05):

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

view this post on Zulip Kevin Buzzard (May 18 2020 at 22:05):

That's interesting.

view this post on Zulip 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:ℤ)

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 18 2020 at 22:06):

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

view this post on Zulip Mario Carneiro (May 18 2020 at 22:06):

so you can't rewrite with that

view this post on Zulip Kevin Buzzard (May 18 2020 at 22:06):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 18 2020 at 22:08):

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

view this post on Zulip Kevin Buzzard (May 18 2020 at 22:08):

but formalising the proof has brought this out explicitly.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 18 2020 at 22:09):

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

view this post on Zulip Kevin Buzzard (May 18 2020 at 22:10):

Mathematicians do not write these things.

view this post on Zulip Mario Carneiro (May 18 2020 at 22:10):

Yes, but we aren't in that situation

view this post on Zulip Kevin Buzzard (May 18 2020 at 22:10):

Indeed!

view this post on Zulip Mario Carneiro (May 18 2020 at 22:10):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 18 2020 at 22:11):

which your comments seem to suggest

view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 18 2020 at 22:13):

which of course it is in this case

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (May 18 2020 at 22:19):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 18 2020 at 22:20):

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

view this post on Zulip Yury G. Kudryashov (May 18 2020 at 22:20):

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

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (May 18 2020 at 22:22):

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

view this post on Zulip Kevin Buzzard (May 18 2020 at 22:23):

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

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (May 18 2020 at 22:28):

Someday we'll need both of them anyway

view this post on Zulip Yury G. Kudryashov (May 18 2020 at 22:29):

@Kevin Buzzard Yes, search for deriv_log

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 18 2020 at 22:34):

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

view this post on Zulip 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: )

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 18 2020 at 22:51):

and they said semirings were useless ;)

view this post on Zulip Jalex Stark (May 18 2020 at 22:51):

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

view this post on Zulip 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?)

view this post on Zulip Matt Earnshaw (May 18 2020 at 22:53):

yeah, I suppose the theorem would suffice

view this post on Zulip 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

view this post on Zulip Jalex Stark (May 18 2020 at 23:11):

doing math for fun? crazy

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 18 2020 at 23:14):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Jalex Stark (May 19 2020 at 04:26):

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

view this post on Zulip Mario Carneiro (May 19 2020 at 04:27):

right

view this post on Zulip Jalex Stark (May 19 2020 at 04:27):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 19 2020 at 04:28):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (May 19 2020 at 04:28):

I guess maybe not with this latest idea.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Jalex Stark (May 19 2020 at 05:39):

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

view this post on Zulip 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

view this post on Zulip 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