Zulip Chat Archive

Stream: maths

Topic: Coercions N->Z->Q->R->C


view this post on Zulip Kevin Buzzard (Aug 03 2018 at 16:41):

My students want to move freely between these five basic objects, sometimes because they have made poor design decisions but sometimes for genuine reasons. I figured I'd try to get to the bottom of why they were having problems.

import data.complex.basic

definition has_coe_NZ : has_coe   := by apply_instance
definition has_coe_NQ : has_coe   := by apply_instance
definition has_coe_NR : has_coe   := by apply_instance
definition has_coe_NC : has_coe   := by apply_instance
definition has_coe_ZQ : has_coe   := by apply_instance
definition has_coe_ZR : has_coe   := by apply_instance
definition has_coe_ZC : has_coe   := by apply_instance
-- definition has_coe_QR : has_coe ℚ ℝ := by apply_instance -- fails
noncomputable definition has_coe_QR : has_coe   := by apply_instance
-- definition has_coe_QC : has_coe ℚ ℂ := by apply_instance -- fails
noncomputable definition has_coe_QC : has_coe   := by apply_instance
definition has_coe_RC : has_coe   := by apply_instance

definition coe_NZ :    := has_coe_NZ.coe
definition coe_NQ :    := has_coe_NQ.coe
definition coe_NR :    := has_coe_NR.coe
definition coe_NC :    := has_coe_NC.coe
definition coe_ZQ :    := has_coe_ZQ.coe
definition coe_ZR :    := has_coe_ZR.coe
definition coe_ZC :    := has_coe_ZC.coe
noncomputable definition coe_QR :    := has_coe_QR.coe
noncomputable definition coe_QC :    := has_coe_QC.coe
definition coe_RC :    := has_coe_RC.coe

-- The ten theorems below are what I would like to access easily in Lean.
-- I don't know what to call them; the current names are just placeholders.

-- N to Z is never a problem
theorem NZQ (x : ) : coe_ZQ (coe_NZ x) = coe_NQ x := rfl
theorem NZR (x : ) : coe_ZR (coe_NZ x) = coe_NR x := rfl
theorem NZC (x : ) : coe_ZC (coe_NZ x) = coe_NC x := rfl

-- the problems start now
theorem ZQR (x : ) : coe_QR (coe_ZQ x) = coe_ZR x := sorry -- simp fails
theorem QRC (x : ) : coe_RC (coe_QR x) = coe_QC x := sorry -- simp fails
theorem ZRC (x : ) : coe_RC (coe_ZR x) = coe_ZC x := sorry -- simp fails

theorem NQR (x : ) : coe_QR (coe_NQ x) = coe_NR x := by rw [NZQ,ZQR,NZR]
theorem ZQC (x : ) : coe_QC (coe_ZQ x) = coe_ZC x := by rw [QRC,ZRC,ZQR]
theorem NQC (x : ) : coe_QC (coe_NQ x) = coe_NC x := by rw [NZC,NZQ,ZQC]
theorem NRC (x : ) : coe_RC (coe_NR x) = coe_NC x := by rw [NQC,QRC,NQR]

-- cool stuff my stuents constantly want to be able to do
example (x : ) : ((x : ) : ) = x := ZQR x
example (x : ) : let (y : ) := x in let (z : ) := y in z = x := ZQR x

Q1) Is there a good reason for the noncomputable coercions being noncomputable?

Q2) How do I prove the sorried coercion theorems?

Q3) What are the correct names for these theorems that enable me to cancel ↑↑ in these specific cases?

view this post on Zulip Gabriel Ebner (Aug 03 2018 at 17:05):

You need to use the right syntax, then everything works out of the box :smile:

theorem ZQR (x : ) : ((x : ) : ) = (x : ) := by simp
theorem QRC (x : ) : ((x : ) : ) = (x : ) := by simp
theorem ZRC (x : ) : ((x : ) : ) = (x : ) := by simp

view this post on Zulip Gabriel Ebner (Aug 03 2018 at 17:07):

You can use set_option trace.simplify.rewrite true to find the corresponding lemmas.

view this post on Zulip Kevin Buzzard (Aug 03 2018 at 17:19):

Oh many thanks Gabriel! I think I can take it from here

view this post on Zulip Chris Hughes (Aug 03 2018 at 17:41):

Q - > R is noncomputable, I'm guessing because it's defined to any field using division and the integer coercion and division is noncomputable on the reals. There is a computable function Q->R, the constant sequence, but that would be less general than the current Q coercion, and computable reals are useless anyway.

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:18):

"computable reals are useless anyway" -- maybe to you. But to a beginner, I think

def x :  := 1/2
/-
definition 'x' is noncomputable, it depends on 'real.division_ring'
-/

is very confusing. What's so noncomputable about 1/2?

view this post on Zulip Kenny Lau (Aug 04 2018 at 08:19):

I hear they have a computable division by positive numbers

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:20):

there is a manual coercion from Q if you really care about defining 1/2 computably, but the point is that it's not the object but the way it is defined that makes it noncomputable

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:20):

The default coercion from nat to int isn't the generic one from nat to any semiring, it's the constructor, and my understanding was that this decision was made for efficiency reasons.

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:21):

Is there a similar argument saying that the default coercion from Q to R should be the one that's staring you in the face rather than the generic one?

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:21):

i.e. the constant series

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:21):

These are implementation issues I guess, which I of course know nothing about in practice

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:22):

Short answer yes

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:23):

But this road leads to the same confusion as why int.coe_nat_* and nat.cast_* have parallel but apparently identical statements

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:24):

look ma, no noncomputable

import data.real.basic
def one_half : ℝ := real.of_rat (1/2)
theorem one_half_eq : one_half = 1/2 := by simp [one_half]

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:28):

But this road leads to the same confusion as why int.coe_nat_* and nat.cast_* have parallel but apparently identical statements

Right. And as you know I've been thinking about this recently (I'm trying to write some undergraduate example sheets which look like maths but are actually not hard to do in Lean for a beginner). A decision was made to not use the generic coercion, this then causes some issues like int.coe_nat... v nat.cast..., these are solved by the devs, the right simp lemmas are proved, people like me learn (in my case, yesterday) that if you use \u then everything should be fine, and then we move on. The devs could do the same for Q -> R, right? Chris seems to think there's no point because who cares about computable reals, but I'm suggesting that there might be a point which has something to do with efficiency somehow.

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:29):

this decision was made for efficiency reasons

Actually it's the opposite. Efficiency would dictate using real.of_rat because it has the more natural implementation, and is exponentially faster if you actually run it. The decision was made for uniformity of the library - in the lean 2 library we had all 10 coercions N->Z->Q->R->C and 10 sets of lemmas about them (plus some extras for the 15 ways to combine them), while the nat.cast approach requires only 4 coercions and sets of lemmas

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:31):

def one_half :  := real.of_rat (1/2)
theorem one_half_eq : one_half = 1/2 := by simp [one_half]

noncomputable def real_half :  := 1 / 2

example : one_half = real_half := by simp [one_half] -- fails

aargh. Lean why u hate me

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:31):

If you work with reals and don't want to be surprised by noncomputable markings, just put noncomputable theory at the top. It's not worth the digression for newbies

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:32):

Oh that's a good idea.

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:32):

you have to unfold both

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:33):

you have to unfold both

I know that rw won't unfold. simp is the same? If I had to simplify something, I think I'd be tempted to start unfolding right at the start.

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:34):

again, you should remember gabriel's advice from yesterday: simp cares about how you write things, so if you hide something behind a definition you can break some simp proofs

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:34):

yes exactly.

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:34):

simp will only unfold things you tell it to

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:34):

I feel like I really understand how to use rw now but I'm still getting the hang of simp. There is an art to all these things.

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:36):

I don't want to work with reals at all, it's just that the 250 people in front of me in October are all familiar with them (at some level -- at some other level they don't have a clue what they are, and don't have a clue that they don't know, but I don't mean that; I mean they're not scared of them). So it's very natural to use them whenever I want a random big set. They show up on the first example sheet. I've been looking back at my work from last October when I was working on my own example sheets. It took me 150 lines of code to prove that 1/2 : real wasn't an integer :-)

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:37):

I honestly think you can use Q for all those types of theorems and have a much better day

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:37):

I honestly believe you.

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:38):

I had a principle back then -- "don't change the example sheets; that would be a compromise"

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:38):

just say "there are some complications with using reals so we'll use Q for now" at the start of class and come back to it when you are ready (or not at all)

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:38):

https://github.com/kbuzzard/xena/blob/master/M1F/2016-17/example_sheets/exsht1.pdf

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:39):

Sheet 1 Q6 -- I was told "this is not possible in Lean because your sets are stupid"

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:39):

I had to start compromising pretty quickly

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:40):

Heh - I could show you how to define that using inductive types

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:40):

or trees

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:40):

https://github.com/kbuzzard/xena/blob/2bf7737bc0fbcd3943ddadfb513bd19c1eea14a3/xenalib/half_not_an_integer.lean#L116

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:41):

triumphant proof that 1/2 wasn't an integer, so I could do Q7 part (i)

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:41):

Kind of amazing that I didn't give up there and then

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:41):

to do example sheet 2 I had to write my own square root function

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:42):

it occurs to me that it is really easy to prove that over Q

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:42):

since 1/2 has denom 2 and integers have denom 1

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:42):

right

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:42):

import data.real.basic tactic.interactive

lemma rational_half_not_an_integer : ¬  n : , (1/2 : ) = n :=
begin
  -- proof by contradiction
  rintros n,Hn, -- n is an integer, Hn the proof that 1/2 = n
  -- goal is "false"
  have H := rat.coe_int_denom n, -- H says denominator of n is 1
  rw Hn at H, -- H now says denominator of 1/2 is 1...
  revert H,exact dec_trivial -- ...but denominator of 1/2 isn't 1.
end

lemma real_half_not_an_integer : ¬  n : , (1/2 : ) = n :=
begin
  rintro n,Hn, -- n is an integer, Hn the proof that it's 1/2
  apply rational_half_not_an_integer,
  existsi n,
  -- now our hypothesis is that 1/2 = n as reals, and we want to
  -- deduce 1/2 = n as rationals!
  -- This is possible by some messing around with coercionc
  -- from integers to rationals to reals.
  rw @rat.cast_inj  _ _,
  rw (show ((n : ) : ) = (n : ), by simp),
  rw Hn,
  simp
end

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:43):

Current version of 2018 proof

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:43):

no having to define my own floor function in sight!

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:43):

and a lot less than 150 lines too

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:44):

and Gabriel's proof right there at the end

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:44):

There is a name for that lemma

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:44):

you don't have to show by simp

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:44):

yes, I even looked it up

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:44):

as Gabriel suggested

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:45):

in fact did you know that whenever you use simp, you can actually replace it with lemmas which have names?

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:45):

;-)

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:46):

the advantage of simp is when there are a lot of lemmas, applied in complicated positions

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:46):

I am sort-of confused by this. I never know whether to write assumption or exact H27...

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:46):

when the theorem name is shorter than the statement I prefer rw

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:46):

...and I never know whether to write simp or to write simp and then look what it did and write that instead.

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:47):

Hmm, so maybe the answer is "it depends"

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:47):

I prefer exact H27 over assumption, indeed I rarely use assumption because it is longer, less descriptive, and possibly time consuming if it normalizes an irrelevant hypothesis

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:50):

This code above has a rather strange role to play. My current idea is to present the example sheet questions and at the top have a list of lemmas which the students might find helpful. This is example sheet 1 so I'll probably get a lot of people trying it; many will have given up by sheet 2. My plan as I say was to list useful lemmas at the top which they will need, and then hopefully they can prove all the parts of Q7 with rewrites and exact. One of the lemmas I was going to offer them was the proof that 1/2 wasn't an integer, because they need it for Q7(i). But I was going to say "don't worry about these lemmas, just assume them, however anyone interested in what is going on here might want to take a look at them". So I was thinking that the code above would only be seen by people who were interested in what Lean was doing but knew nothing about Lean at all; hence the comments everywhere and the decision to use simp instead of a lemma with a to-them-incomprehensible name

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:51):

My goal was to stick with R but to give them the lemmas they need and then to see how well they did.

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:52):

I was going to get my xena undergrads to test out the problems in Sept and report back.

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:52):

example of assumption going wrong:

example {p : Prop} (h1 : if 10^4 = 10^4 then true else true)
  (hp : p) : p := by assumption

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:52):

I will happily never use assumption again.

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:52):

except for those funny cases when you prove lots of cases at once after a semicolon

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:53):

a somewhat nicer form of assumption which you may not know is the french quotes ‹p›

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:53):

Whenever I see people using that I always figure that they should be doing something else

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:54):

I have started using the french quotes to refer to instances that I don't want to name, when I need to refer to them directly for some reason

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:54):

Actually I think that's not assumption going wrong

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:55):

example {p : Prop} (h1 : if 10^4 = 10^4 then true else true)
  (hp : p) : p :=
  begin

  end

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:55):

already times out

view this post on Zulip Kevin Buzzard (Aug 04 2018 at 08:55):

but I do believe you

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:55):

That is a recently discovered mystery for me

view this post on Zulip Mario Carneiro (Aug 04 2018 at 08:57):

@Sebastian Ullrich Do you know what preprocessing is done on the context before a begin end block and why? This also came up with the person who was trying to pattern match on a beta redex in the goal only to find it was already reduced before the tactic got to it

view this post on Zulip Mario Carneiro (Aug 04 2018 at 09:01):

this is a better example

example {n : ℕ} (h1 : (if 10^4 = 10^4 then 1 else 1) = 1)
  (hp : n = 1) : n = 1 := by assumption

view this post on Zulip Mario Carneiro (Aug 04 2018 at 09:02):

in the original example the timeout is because h1 has a type which is not obviously even a type, so it has to do the expensive evaluation to find out if it is a type

view this post on Zulip Mario Carneiro (Aug 04 2018 at 09:05):

Wow, even this times out

def q : Prop := if 10^4 = 10^4 then true else true
example (h : q) : q := h

view this post on Zulip Mario Carneiro (Aug 04 2018 at 09:05):

but example : q → q := id is okay

view this post on Zulip Mario Carneiro (Aug 04 2018 at 09:15):

Here is an example of an interesting partial reduction:

example : (λ x, x ∧ x) ((λ x, x) true) :=
by tactic.target >>= tactic.trace
-- (λ (x : Prop), x) true ∧ (λ (x : Prop), x) true

It looks like the goal has whnf applied first

view this post on Zulip Sebastian Ullrich (Aug 04 2018 at 18:04):

I wouldn't even know where to start looking for the whnf

view this post on Zulip Mario Carneiro (Aug 04 2018 at 18:15):

My guess is that it is making sure it is a sort first


Last updated: May 12 2021 at 08:14 UTC