## Stream: new members

### Topic: Using data.rat

#### Bhavik Mehta (Nov 16 2019 at 21:54):

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 (Nov 16 2019 at 22:02):

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

Yeah, similarly

#### Reid Barton (Nov 16 2019 at 22:07):

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

#### Bhavik Mehta (Nov 16 2019 at 22:07):

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 (Nov 16 2019 at 22:10):

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 (Nov 16 2019 at 22:13):

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

#### Reid Barton (Nov 16 2019 at 22:13):

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

#### Bhavik Mehta (Nov 16 2019 at 22:20):

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

#### Kevin Buzzard (Nov 16 2019 at 22:23):

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

#### Yury G. Kudryashov (Nov 16 2019 at 22:25):

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 (Nov 16 2019 at 22:26):

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 (Nov 16 2019 at 22:26):

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

#### Kevin Buzzard (Nov 16 2019 at 22:26):

Coerce everything to Q first?

#### Yury G. Kudryashov (Nov 16 2019 at 22:27):

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

#### Bhavik Mehta (Nov 16 2019 at 22:28):

@Yury G. Kudryashov Ah okay, my mistake

#### Yury G. Kudryashov (Nov 16 2019 at 22:29):

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

#### Yury G. Kudryashov (Nov 16 2019 at 22:29):

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

#### Bhavik Mehta (Nov 16 2019 at 22:55):

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

This is so much less painful, thanks!!

#### Kevin Buzzard (Nov 16 2019 at 22:56):

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 (Nov 16 2019 at 22:56):

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

#### Mario Carneiro (Nov 16 2019 at 22:57):

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

#### Mario Carneiro (Nov 16 2019 at 22:58):

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

#### Bhavik Mehta (Nov 16 2019 at 23:00):

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 (Nov 16 2019 at 23:01):

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

#### Bhavik Mehta (Nov 16 2019 at 23:01):

I'd certainly have appreciated that

#### Chris Hughes (Nov 16 2019 at 23:01):

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

#### Chris Hughes (Nov 16 2019 at 23:02):

Maybe a docstring on rat.mk as well.

#### Bhavik Mehta (Nov 16 2019 at 23:02):

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 (Nov 16 2019 at 23:03):

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 (Nov 16 2019 at 23:04):

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

#### Bhavik Mehta (Nov 16 2019 at 23:04):

Yikes, that's far harder to parse

#### Bhavik Mehta (Nov 16 2019 at 23:05):

Wait - cast tactics

#### Kevin Buzzard (Nov 16 2019 at 23:05):

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

#### Kevin Buzzard (Nov 16 2019 at 23:06):

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

#### Bhavik Mehta (Nov 16 2019 at 23:06):

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

#### Kevin Buzzard (Nov 16 2019 at 23:08):

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 (Nov 16 2019 at 23:08):

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

#### Kevin Buzzard (Nov 16 2019 at 23:08):

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 (Nov 16 2019 at 23:09):

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

#### Kevin Buzzard (Nov 16 2019 at 23:09):

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 (Nov 16 2019 at 23:10):

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 (Nov 16 2019 at 23:23):

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 (Nov 16 2019 at 23:23):

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

#### Kevin Buzzard (Nov 16 2019 at 23:24):

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

#### Kevin Buzzard (Nov 16 2019 at 23:24):

and there was no norm_num at the time

#### Kevin Buzzard (Nov 16 2019 at 23:24):

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

#### Mario Carneiro (Nov 16 2019 at 23:25):

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 (Nov 16 2019 at 23:25):

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

#### Mario Carneiro (Nov 16 2019 at 23:25):

you don't want that proof

#### Kevin Buzzard (Nov 16 2019 at 23:26):

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

#### Kevin Buzzard (Nov 16 2019 at 23:26):

And we now have that with norm_num

#### Mario Carneiro (Nov 16 2019 at 23:26):

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

#### Kevin Buzzard (Nov 16 2019 at 23:26):

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

that's false

#### Kevin Buzzard (Nov 16 2019 at 23:26):

Not to a mathematician.

#### Mario Carneiro (Nov 16 2019 at 23:26):

but you want a tactic to pretend it is true

#### Kevin Buzzard (Nov 16 2019 at 23:27):

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

#### Chris Hughes (Nov 16 2019 at 23:27):

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 (Nov 16 2019 at 23:27):

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

#### Mario Carneiro (Nov 16 2019 at 23:28):

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 (Nov 16 2019 at 23:28):

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 (Nov 16 2019 at 23:28):

We can do it, but the notation is funky

it is (+) <$> X <*> Y #### Kevin Buzzard (Nov 16 2019 at 23:29): 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 (Nov 16 2019 at 23:30): There is also the issue that this notation is very general and overloaded in maths #### Kevin Buzzard (Nov 16 2019 at 23:31): 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 (Nov 16 2019 at 23:31): you also have things like A + a and B - A (and -A is already being used for complement) #### Kevin Buzzard (Nov 16 2019 at 23:31): Yes sure, we do that too, but I'm not asking for that yet :D #### Kevin Buzzard (Nov 16 2019 at 23:32): 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 (Nov 16 2019 at 23:32): I would suggest you not pretend this is actually addition of sets #### Mario Carneiro (Nov 16 2019 at 23:32): use another notation #### Kevin Buzzard (Nov 16 2019 at 23:32): But you're happy to have X * Y for X Y : set M with monoid M? #### Mario Carneiro (Nov 16 2019 at 23:33): I think it's probably a bad idea, because it will beg the question #### Kevin Buzzard (Nov 16 2019 at 23:33): But this is already in mathlib. #### Mario Carneiro (Nov 16 2019 at 23:33): probably a sneak attack #### Kevin Buzzard (Nov 16 2019 at 23:34): I'm happy to make the additive version local notation, I definitely want it in the real number game #### Kevin Buzzard (Nov 16 2019 at 23:34): https://github.com/leanprover-community/mathlib/blob/61ccaf65c4cfc9c6ff103463342e034347eb8b89/src/algebra/pointwise.lean#L27 #### Kevin Buzzard (Nov 16 2019 at 23:34): https://github.com/leanprover-community/mathlib/blob/61ccaf65c4cfc9c6ff103463342e034347eb8b89/src/algebra/pointwise.lean#L65 #### Kevin Buzzard (Nov 16 2019 at 23:35): I note that they're not instances. #### Kevin Buzzard (Nov 16 2019 at 23:35): How about I make them defs? #### Kevin Buzzard (Nov 16 2019 at 23:37): #### Mario Carneiro (Nov 16 2019 at 23:38): Oh, I see I was involved in merging #854 and I think the reason was because it didn't make them instances #### Mario Carneiro (Nov 16 2019 at 23:39): If it's just a def, then it's just a theory about these operations and this is certainly useful #### Mario Carneiro (Nov 16 2019 at 23:39): make it a local instance and you should be golden #### Kevin Buzzard (Nov 17 2019 at 01:11): 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 (Nov 17 2019 at 01:12):

anything is possible

#### Kevin Buzzard (Nov 17 2019 at 01:13):

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

#### Mario Carneiro (Nov 17 2019 at 01:14):

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

#### Mario Carneiro (Nov 17 2019 at 01:14):

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 (Nov 17 2019 at 01:16):

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 (Nov 17 2019 at 01:19):

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 (Nov 17 2019 at 01:48):

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 (Nov 17 2019 at 01:50):

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 (Nov 17 2019 at 01:57):

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 (Nov 17 2019 at 02:01):

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 (Nov 17 2019 at 02:04):

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 (Nov 17 2019 at 02:05):

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 (Nov 17 2019 at 02:07):

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 (Nov 17 2019 at 02:10):

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 (Nov 17 2019 at 02:15):

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

#### Mario Carneiro (Nov 17 2019 at 02:17):

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 (Nov 17 2019 at 02:21):

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.

#### Kevin Buzzard (Nov 17 2019 at 02:33):

@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 (Nov 17 2019 at 02:34):

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 (Nov 17 2019 at 02:37):

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

#### Mario Carneiro (Nov 17 2019 at 02:38):

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

#### Mario Carneiro (Nov 17 2019 at 02:39):

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

#### Kevin Buzzard (Nov 17 2019 at 02:40):

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

#### Kevin Buzzard (Nov 17 2019 at 02:41):

that would be an interesting project

#### Mario Carneiro (Nov 17 2019 at 02:41):

I mean metamath the language doesn't have type inference

#### Mario Carneiro (Nov 17 2019 at 02:41):

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

#### Kevin Buzzard (Nov 17 2019 at 02:42):

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

#### Kevin Buzzard (Nov 17 2019 at 02:42):

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

#### Mario Carneiro (Nov 17 2019 at 02:43):

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 (Nov 17 2019 at 02:43):

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

#### Mario Carneiro (Nov 17 2019 at 02:44):

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

#### Kevin Buzzard (Nov 17 2019 at 02:45):

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

#### Mario Carneiro (Nov 17 2019 at 02:45):

a metavariable standing for a proof of a known expression

#### Mario Carneiro (Nov 17 2019 at 02:46):

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

#### Kevin Buzzard (Nov 17 2019 at 02:46):

Are you talking about expr?

#### Kevin Buzzard (Nov 17 2019 at 02:46):

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

#### Kevin Buzzard (Nov 17 2019 at 02:46):

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

#### Mario Carneiro (Nov 17 2019 at 02:46):

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

right

#### Mario Carneiro (Nov 17 2019 at 02:47):

sure, that's how almost every theorem prover works

#### Mario Carneiro (Nov 17 2019 at 02:48):

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 (Nov 17 2019 at 02:51):

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 (Nov 17 2019 at 02:53):

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 (Nov 18 2019 at 08:38):

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

#### Johan Commelin (Nov 18 2019 at 08:40):

@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 (Nov 18 2019 at 08:42):

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 (Nov 18 2019 at 08:43):

What is a good example...

#### Johan Commelin (Nov 18 2019 at 08:43):

Let me see if I can parse PNT

#### Johan Commelin (Nov 18 2019 at 08:46):

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

#### Johan Commelin (Nov 18 2019 at 08:46):

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

#### Mario Carneiro (Nov 18 2019 at 08:47):

it stands for metamath proof explorer, unicode version

#### Mario Carneiro (Nov 18 2019 at 08:48):

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

#### Mario Carneiro (Nov 18 2019 at 08:48):

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

#### Mario Carneiro (Nov 18 2019 at 08:49):

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 (Nov 18 2019 at 08:51):

Aha, I see

Last updated: May 09 2021 at 23:10 UTC