Using data.rat

Stream: new members

[Bhavik Mehta]

I'm struggling with proving basic things for rational numbers - could anyone provide some hints for this problem?

example {a b n : ℕ} {h : n ≠ 0} : rat.mk a b / ↑n = rat.mk a (b * n) := sorry

[Kevin Buzzard]

I can't find anything useful in data.rat.basic

[Bhavik Mehta]

Yeah, similarly

[Reid Barton]

rat.mk a b equals (\u a) / (\u b) right? (\u being the up arrow)

[Bhavik Mehta]

I think I've got the skeleton of the proof, with some (I think easy) technicalities missing:

example {a b n : ℕ} {h : n ≠ 0} : rat.mk a b / ↑n = rat.mk a (b * n) :=
begin
  suffices : rat.mk a b = rat.mk a (b * n) * ↑n,
    rw this, rw mul_div_cancel, sorry,
  rw [rat.coe_nat_eq_mk, rat.mul_def, mul_one, rat.div_mk_div_cancel_left], sorry
end

[Bhavik Mehta]

rat.mk a b equals (\u a) / (\u b) right? (\u being the up arrow)

Yeah, if the \u are casting correctly to Q

[Reid Barton]

If you rewrite with that first, then it should be a general div_mul or something

[Reid Barton]

Well, after more facts about casts I guess...

[Bhavik Mehta]

rw [rat.mk_eq_div, rat.mk_eq_div], simp, rw div_div_eq_div_mul does it, thanks!

[Kevin Buzzard]

Is the idea that you're not supposed to be using rat.mk?

[Yury G. Kudryashov]

BTW, is there any good reason not to define structures on data.rat by equiv.discrete_field (_ : equiv data.rat (fraction_field int))? Won't we get many theorems for free in this case?

[Bhavik Mehta]

data.rat says: "It is defined as the set of pairs ⟨n, d⟩ of integers such that d is positive and n and d are coprime. This representation is preferred to the quotient because without periodic reduction, the numerator and denominator can grow exponentially (for example, adding 1/2 to itself repeatedly)."

[Chris Hughes]

The best solution is to use division and not rat.mk

[Kevin Buzzard]

Coerce everything to Q first?

[Yury G. Kudryashov]

@Bhavik Mehta I was talking about operations on rat and theorems about these operations, not the data type.

[Bhavik Mehta]

@Yury G. Kudryashov Ah okay, my mistake

[Yury G. Kudryashov]

Most operations (except for neg?) need "cancel numerator and denominator" step anyway.

[Yury G. Kudryashov]

And this is exactly what functions from equiv/algebra will do.

[Bhavik Mehta]

The best solution is to use division and not rat.mk

This is so much less painful, thanks!!

[Kevin Buzzard]

I think the way it works is that there's a "mathlib standard way" to do things, and you have to learn it for the things you want to do.

[Kevin Buzzard]

Often you can learn it by simply reading the relevant mathlib files.

[Mario Carneiro]

rat.mk is indeed supposed to be internal to the data.rat file and not used once \u a / \u b works

[Mario Carneiro]

unless you care about computation and need a more efficient way of building the number

[Bhavik Mehta]

Is there some general way of finding out this sort of thing? Reading the mathlib files around data/rat seemed to mostly use rat.mk

[Kevin Buzzard]

I suspect that Chris has used rat sufficiently often to know the tricks. Should his observation be made in the module docstring?

[Bhavik Mehta]

I'd certainly have appreciated that

[Chris Hughes]

I think it probably should since it's something I've seen a few people do.

[Chris Hughes]

Maybe a docstring on rat.mk as well.

[Bhavik Mehta]

Tangentially related, I've now got my goal in a slightly nicer form, but there's \us around - I can't tell if they're casting my nats up to ints or to Q, is there some way I could find out?

[Kevin Buzzard]

I can't help but thinking that it shouldn't matter nowadays, because of all the cast tactics. One answer to your question is to write set_option pp.all true above your work.

[Kevin Buzzard]

There might be a less drastic way to do it. This way tells you exactly which term you're looking at.

[Bhavik Mehta]

Yikes, that's far harder to parse

[Bhavik Mehta]

Wait - cast tactics

[Kevin Buzzard]

If you post fully working code I can try and make sense of the pp.all output if you want

[Kevin Buzzard]

norm_cast and friends should I think sort out problems with casts from nat to int to rat nowadays.

[Bhavik Mehta]

I didn't know cast tactics were a thing! norm_cast managed perfectly

[Kevin Buzzard]

You are trying to do mathematics in Lean and you are running into exactly the problems which me and my students started running into two years ago, but you have the advantage that some of our problems were solved by computer scientists in the mean time.

[Kevin Buzzard]

This is why I have so much hope in this software.

[Kevin Buzzard]

When I came here I asked how to prove $2+2=4$ and they said "which 2?" and I said "the real number 2" and they said "oh boy that's hard"

[Bhavik Mehta]

That's good to hear - I think I'd still like some documentation for this sort of thing

[Kevin Buzzard]

When Chris came here he asked how to prove $(x+y)^3=x^3+3x^2y+3xy^2+y^3$ and they said "oh boy that's hard"

[Kevin Buzzard]

but then people like Rob and Mario and people supervised by them pop out of the woodwork and write tactics which solve these things.

[Mario Carneiro]

to clarify, 2 + 2 = 4 is not hard at all, but it is hard to "do it without doing it" because that's asking to have a general procedure

[Chris Hughes]

example {α : Type*} [has_one α] [has_add α] : (2 : α) + 2 = 4 := rfl

[Kevin Buzzard]

I think the precise example was (1 : real) \ne 2

[Kevin Buzzard]

and there was no norm_num at the time

[Kevin Buzzard]

and the other one was (2 : real)^2 - 3 * 2 + 2 = 0

[Mario Carneiro]

it's still easy, it's just that you get upset when I tell you that the answer is to reduce 1 != 2 to 1 < 2 and then 0 < 1 and finish

[Kevin Buzzard]

2 years ago this was harder for a newbie, that's all I'm saying.

[Mario Carneiro]

you don't want that proof

[Kevin Buzzard]

I want that 1 : real and 2 : real are not equal by schoolkid, because any schoolkid knows it.

[Kevin Buzzard]

And we now have that with norm_num

[Mario Carneiro]

exactly, you want a proof which doesn't look like a proof

[Kevin Buzzard]

Right. It's obvious so it doesn't need a proof.

[Mario Carneiro]

that's false

[Kevin Buzzard]

Not to a mathematician.

[Mario Carneiro]

but you want a tactic to pretend it is true

[Kevin Buzzard]

Right. I want to speak to Lean like a mathematician.

[Chris Hughes]

it's still easy, it's just that you get upset when I tell you that the answer is to reduce 1 != 2 to 1 < 2 and then 0 < 1 and finish

Can you do this example : (1 : ℂ) ≠ 2 :=? You're even allowed to use norm_num if you want.

[Kevin Buzzard]

Why do you think I sunk several hours this evening into making X + Y make sense for X Y : set real?

[Mario Carneiro]

In that case, I would either reduce to 0 != 1, or for larger numbers I would interpret them in real or nat and then use <

[Kevin Buzzard]

This (X + Y) is something which doesn't even need a definition for mathematicians, they will expect to be able to sum subsets of the reals, but we can't do it in mathlib yet.

[Mario Carneiro]

We can do it, but the notation is funky

[Mario Carneiro]

it is (+) <$> X <*> Y

[Kevin Buzzard]

Yeah well not only do I want X + Y to work, but I want X + (Y + Z) to be provably X + Y + Z by undergraduate.

[Mario Carneiro]

There is also the issue that this notation is very general and overloaded in maths

[Kevin Buzzard]

sure but the notation here is reasonable. It's standard in maths to add two subsets of the reals when you're teaching sups.

[Mario Carneiro]

you also have things like A + a and B - A (and -A is already being used for complement)

[Kevin Buzzard]

Yes sure, we do that too, but I'm not asking for that yet :D

[Kevin Buzzard]

I'm just asking for X+Y which I don't think is unreasonable. Do you have a problem with the PR or are you just observing that I won't be able to get much further?

[Mario Carneiro]

I would suggest you not pretend this is actually addition of sets

[Mario Carneiro]

use another notation

[Kevin Buzzard]

But you're happy to have X * Y for X Y : set M with monoid M?

[Mario Carneiro]

I think it's probably a bad idea, because it will beg the question

[Kevin Buzzard]

But this is already in mathlib.

[Mario Carneiro]

probably a sneak attack

[Kevin Buzzard]

I'm happy to make the additive version local notation, I definitely want it in the real number game

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib/blob/61ccaf65c4cfc9c6ff103463342e034347eb8b89/src/algebra/pointwise.lean#L27

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib/blob/61ccaf65c4cfc9c6ff103463342e034347eb8b89/src/algebra/pointwise.lean#L65

[Kevin Buzzard]

I note that they're not instances.

[Kevin Buzzard]

How about I make them defs?

[Kevin Buzzard]

I mean https://github.com/leanprover-community/mathlib/blob/a9a8e6975cf8b7c9b75edb0231c207ae5f2b9a17/src/algebra/pointwise.lean#L188 and https://github.com/leanprover-community/mathlib/blob/a9a8e6975cf8b7c9b75edb0231c207ae5f2b9a17/src/algebra/pointwise.lean#L191 (change from instance to def)

[Mario Carneiro]

Oh, I see I was involved in merging #854 and I think the reason was because it didn't make them instances

[Mario Carneiro]

If it's just a def, then it's just a theory about these operations and this is certainly useful

[Mario Carneiro]

make it a local instance and you should be golden

[Kevin Buzzard]

it is (+) <$> X <*> Y

If Hales had his controlled natural language, could he have $X+Y$ meaning this? I have realised that sometimes one can use the CNL instead of notation.

[Mario Carneiro]

anything is possible

[Kevin Buzzard]

My understanding is that he wants a language which is readable both by humans and by Lean.

[Mario Carneiro]

the translator might become unbounded in complexity, but it's not exactly an unsolvable problem from the CS point of view

[Mario Carneiro]

it's just that once you pin down an actual notation system, certain things become more difficult or impossible because the limitations are explicit

[Mario Carneiro]

If you are okay with a behemoth of a notation parser, then anything is possible, but it makes it harder for the user to predict what things mean if the parser isn't perfect, fails on some input, or gives a wrong result

[Mario Carneiro]

I recall seeing snippets of Hales's CNL and if I understand correctly the proposed solution is to have an unambiguous notation system (in the form of a bunch of tex macros) which "decays" to lean notation and also to latex notation, and I see no problem with this except that I thought that mathematicians can't tolerate unambiguous notation. If putting things in the latex context helps mathematicians get over this mental hurdle then I'm all for it

[Reid Barton]

I would have said mathematical notation is often ambiguous. I guess whether or not something is ambiguous depends on how much of the context you consider. This ability isn't even just about being a human, it depends on knowing which of the possible interpretations is plausible, and consistent with the surrounding arguments, etc.

[Reid Barton]

As a lame example, I'm always going to guess $\sin^2 x$ means $(\sin x)^2$ because there's no plausible reason to ever have $\sin(\sin x)$, and then if in the next line it is replaced by $1 - \cos^2 x$, then I'm even more certain.

[Reid Barton]

However you end up doing it, it seems reasonable to give the machine something more specific but present an abbreviated, ambiguous form to the human reader

[Mario Carneiro]

Norm Megill, the author of metamath, has some strong opinions on this which I partly agree with. Even if notations are unambiguous in the computer, if they are ambiguated during printing, then it is easy to create misleading statements. This is what "Pollack consistency" is all about. I don't like the idea that the statement of a theorem should not be understandable without its proof, but I very commonly have to deal with this when reading actual maths papers

[Kevin Buzzard]

When I started using Lean I was really all for mathematical imprecision to be possible, like $f(X)$ just meaning $\{f(x):x\in X\}$.

[Mario Carneiro]

In some ways it makes sense: as a method of human communication, we often use the "principle of charity", where we take the most lenient possible understanding in order to justify an argument, and sometimes this can be taken to extremes in maths where you have folks like Mochizuki who produce something that clearly fails to communicate but the maths community is only willing to say "we aren't sure if this is correct" even after years of analysis rather than "this is nonsense" like a formal theorem prover would do

[Kevin Buzzard]

But the more I use it the more I realise that actually I think we should start to think as mathematicans about firstly forcing ourselves to distinguish between these closely-related (for us) notions and secondly about formalising exactly the notation-cheats which we are prepared to tolerate. If one mathematician is genuinely using a piece of notation to mean one thing in dependent type theory, and another mathematician is using the same piece of notation to mean a different thing, then that should be OK, as long as each mathematician is consistent. That's what we want from our notation.

[Mario Carneiro]

I think even this, the CS people are happy to tolerate, provided the different notations go in different namespaces or some similar broad scoping. But then they say "but you promise not to use these at the same time, right?" and you say "uhh...". Of course some enterprising mathematician is later going to want to work in both fields, and use both conflicting notations, maybe apologize but use them anyway, and now the CS person is scratching their head trying to figure out what means what when and how you can possibly tell

[Reid Barton]

Well we don't really know how we can tell either, but it's easy

[Mario Carneiro]

humans have the advantage here, because they can "cross that bridge when they come to it", give it a bit of thought, and maybe change the game if it's too hard (by changing notations later)

[Reid Barton]

How do we tell whether $\otimes$ is the tensor product of modules, the tensor product of elements or the tensor product of maps? It's hard to imagine being confused about this--provided you understand roughly what is going on.

[Reid Barton]

Maybe Lean 3 can just about do this, with overloaded notations

[Kevin Buzzard]

@Patrick Massot found a very subtle notational instance in Bourbaki where I think the completion notation was being used in some very subtle ways.

[Reid Barton]

Perhaps it's not the case for metamath, but Lean already does a lot of context-sensitive elaboration anyways, so I'm not sure you lose much by erasing more distinctions.

[Mario Carneiro]

in metamath we use only global notations, with variables acting as local notations when needed

[Mario Carneiro]

as I said, Norm definitely doesn't want "hidden magic" and all metamath terms are basically pp.all

[Mario Carneiro]

I think it's impressive how close metamath gets to a passable mathematical notation with zero implicit arguments and no type inference

[Kevin Buzzard]

Why don't you make type inference for metamath using prolog?

[Kevin Buzzard]

that would be an interesting project

[Mario Carneiro]

I mean metamath the language doesn't have type inference

[Mario Carneiro]

the IDEs have a couple things that get close to type inference

[Kevin Buzzard]

Gotcha. Do the IDE's use prolog or do they roll their own -- didn't Leo roll his own?

[Kevin Buzzard]

And they're rolling out a completely new one for Lean 4 I guess.

[Mario Carneiro]

I wrote a "prolog-like search" but it doesn't do any backtracking, so it only uses lemmas that are always useful to apply when applicable

[Mario Carneiro]

there isn't much distinction made between goals that are about typing and goals that are theorems

[Mario Carneiro]

of course, the whole point of DTT is that the distinction is fuzzy

[Kevin Buzzard]

Can you say that thing about goals within type theory? By a goal do you mean a proposition or a proof?

[Mario Carneiro]

a metavariable standing for a proof of a known expression

[Mario Carneiro]

i.e. what the tactic state normally calls a goal

[Kevin Buzzard]

Are you talking about expr?

[Kevin Buzzard]

I don't know anything about how the tactic state works.

[Kevin Buzzard]

All I know is that it's a much better fit for my brain than term mode

[Mario Carneiro]

you have a hole where a proof is expected, and you refine that hole with a partial proof

[Kevin Buzzard]

right

[Mario Carneiro]

sure, that's how almost every theorem prover works

[Mario Carneiro]

But in programming languages, where it is an outgrowth of term construction, you work from the bottom up, inferring types of known expressions rather than refining unknown proofs of known types

[Mario Carneiro]

There was once a tactic called back that I thought was going to land in mathlib, not sure what happened to it. The tactic I wrote for metamath was basically that, and it allowed you to discharge a variety of problems like equality proofs (rewrite), closure proofs (typing), and other limited decision procedures similar to type class inference like continuity inference

[Mario Carneiro]

Interestingly, continuity inference in metamath is possible by a matching based method that doesn't work in lean because of the way lambdas are handled in type theory

[Johan Commelin]

@Scott Morrison Hi! People are talking about back. How are things going? :wink:

[Johan Commelin]

@Mario Carneiro I've made several serious attempts at parsing metamath statements in that web-rendered version of set.mm. I've always failed miserably. I really can't read mm at the moment. There is quite a gap to bridge. With lean I had no such issue at all.

[Mario Carneiro]

In the corner of every metamath page, there is a "structured version" button, that is trying out an experimental rendering method using mathjax instead of unicode. Does that help at all? We are of course always looking for ways to increase readability

[Johan Commelin]

What is a good example...

[Johan Commelin]

Let me see if I can parse PNT

[Johan Commelin]

I end up on a page like this: http://us.metamath.org/mpeuni/mudivsum.html and nothing feels familiar...

[Johan Commelin]

I don't know how to pronounce mpeuni. I can make a guess for mudivsum

[Mario Carneiro]

it stands for metamath proof explorer, unicode version

[Mario Carneiro]

mudivsum says that $\sum_{n\le x}\frac{\mu(n)}n=O(1)$

[Mario Carneiro]

where $\mu$ is the number-theoretic Mobius function

[Mario Carneiro]

If you wanted to know what "sum", "mu", or "O(1)" mean in that statement, you can find them in the "syntax hints" at the bottom of the page

[Johan Commelin]

Aha, I see