## Stream: new members

### Topic: Coercion between nat and rat

#### Patrick Stevens (Jun 28 2020 at 13:43):

How was I able to prove this obviously untrue statement? By which I mean, how can I phrase the statement I wanted?

lemma bad (b p : nat) : (b : ℚ) / (p : ℚ) = (((b : ℕ) / (p : ℕ)) : ℚ) := rfl

This is Obviously False: 1/2 is 1/2 in the rationals and 0 in the naturals. How do I phrase bad in such a way that rfl doesn't prove it and instead I need to add the hypothesis that p divides b?

#### Reid Barton (Jun 28 2020 at 13:46):

Type inference is outside in.

#### Reid Barton (Jun 28 2020 at 13:46):

(Generally speaking.)

#### Patrick Stevens (Jun 28 2020 at 13:51):

I hoped I'd be able to completely override the type inference algorithm by specifying the types of everything - I presume the problem is that the right-hand / has implicitly upcasted its two explicitly nat inputs. How can I stop it doing that? I ask because I have the following:

lemma r (p : nat) (p_prime : nat.prime p) (b : nat) (b_nonzero : b ≠ 0) (dvd : p ∣ b) : (padic_val_nat p b) - 1 = (padic_val_nat p (b / p)) :=
begin
let e := @padic_val_rat.div p p_prime b p (nat.cast_ne_zero.mpr b_nonzero) (nat.cast_ne_zero.mpr (nat.prime.ne_zero p_prime)),
rw @padic_val_rat.padic_val_rat_self p (nat.prime.one_lt p_prime) at e,
rw ← @padic_val_rat_of_nat p b at e,
--have s : (b : ℚ) / (p : ℚ) = (((b : ℕ) / (p : ℕ)) : ℚ) := rfl,
--rw ← @padic_val_rat_of_nat p (b / p) at e,
end


In scope is a term of type padic_val_rat p (↑b / ↑p) = ↑(padic_val_nat p b) - 1, and I know padic_val_rat_of_nat can turn the left-hand side into a padic_val_nat (it's currently talking about padic_val_rat) if I can make that b / p term appear as an upcasted natural, rather than a rational

#### Mario Carneiro (Jun 28 2020 at 13:53):

there should be a theorem nat.cast_div (but there probably isn't right now)

#### Reid Barton (Jun 28 2020 at 13:55):

The way to write your statement is something like (untested)
lemma bad (b p : nat) : (b / p : ℚ) = (b / p : ℕ)

:up:

#### Patrick Stevens (Jun 28 2020 at 16:07):

Writing either of these functions is by a large margin the hardest thing I've experienced in Lean. My approach must be completely wrong, because it feels like Lean is fighting me as hard as it can in a way I've never experienced from a computer. It would be a lot easier if I could simply prevent it from doing any coercion locally, because then at least I could easily control what types anything had!

theorem cast_dvd {α : Type*} [semiring α] [has_div α] (m n : ℕ) (n_dvd : n ∣ m) (n_nonzero : n ≠ 0) : ((m / n : ℕ) : α) = m / n :=
begin
induction m with m ind_m,
{ cases n,
{ trivial },
have r : ↑(n.succ) ≠ 0 := nat.cast_ne_zero.mpr n_nonzero,
have s : ↑n + 1 ≠ 0, by simp,
norm_num,
sorry,
},
{ sorry, },
end

lemma thing (p : nat) (p_prime : nat.prime p) (b : nat) (b_nonzero : b ≠ 0) (dvd : p ∣ b) : (padic_val_nat p (b / p)) = (padic_val_nat p b) - 1 :=
begin
let e := @padic_val_rat.div p p_prime b p (nat.cast_ne_zero.mpr b_nonzero) (nat.cast_ne_zero.mpr (nat.prime.ne_zero p_prime)),
rw @padic_val_rat.padic_val_rat_self p (nat.prime.one_lt p_prime) at e,
rw ← @padic_val_rat_of_nat p b at e,
rw <- @cast_dvd ℚ _ _ b p dvd (nat.prime.ne_zero p_prime) at e,
rw <- @padic_val_rat_of_nat at e,
have r : 1 ≤ padic_val_nat p b, by sorry, -- I can do that one
-- this is nonsense
let e : @coe ℕ ℤ _ _ = ↑(padic_val_nat p b : ℤ) - (1 : ℤ) := @nat.cast_sub ℤ _ _ 1 (padic_val_nat p b) r,
sorry,
end


#### Mario Carneiro (Jun 28 2020 at 16:26):

You can always control coercion by putting more type ascriptions in, or putting \u directly in the term where you want the coercion to appear

#### Mario Carneiro (Jun 28 2020 at 16:28):

in particular you can use double type ascription like ((x + y : nat) : int) to make sure a coercion gets inserted between the type ascriptions

#### Mario Carneiro (Jun 28 2020 at 16:30):

cast_dvd is not true in the generality you have stated for it

#### Mario Carneiro (Jun 28 2020 at 16:30):

the division on alpha has nothing to do with the algebraic structure

#### Mario Carneiro (Jun 28 2020 at 16:35):

Here's a true version of your theorem (possibly not maximally general)

theorem cast_dvd {α : Type*} [field α] (m n : ℕ) (n_dvd : n ∣ m) (n_nonzero : (n:α) ≠ 0) : ((m / n : ℕ) : α) = m / n :=
begin
rcases n_dvd with ⟨k, rfl⟩,
have : n ≠ 0, {rintro rfl, simpa using n_nonzero},
rw nat.mul_div_cancel_left _ (nat.pos_iff_ne_zero.2 this),
rw [nat.cast_mul, mul_div_cancel_left _ n_nonzero],
end


#### Mario Carneiro (Jun 28 2020 at 16:43):

Maybe this will help you for the second part:

lemma thing (p : nat) (p_prime : nat.prime p) (b : nat) (b_nonzero : b ≠ 0) (dvd : p ∣ b) : (padic_val_nat p (b / p)) = (padic_val_nat p b) - 1 :=
begin
let e := @padic_val_rat.div p p_prime b p (nat.cast_ne_zero.mpr b_nonzero) (nat.cast_ne_zero.mpr (nat.prime.ne_zero p_prime)),
rw @padic_val_rat.padic_val_rat_self p (nat.prime.one_lt p_prime) at e,
rw ← @padic_val_rat_of_nat p b at e,
rw <- @cast_dvd ℚ _ b p dvd (nat.cast_ne_zero.2 \$ nat.prime.ne_zero p_prime) at e,
rw <- @padic_val_rat_of_nat at e,
apply int.coe_nat_inj,
rw [e, int.coe_nat_sub], {simp},
sorry,
end


#### Mario Carneiro (Jun 28 2020 at 16:50):

You also don't have to provide as many arguments to the rewrites if you do them from left to right:

lemma thing (p : nat) (p_prime : nat.prime p) (b : nat) (b_nonzero : b ≠ 0) (dvd : p ∣ b) : (padic_val_nat p (b / p)) = (padic_val_nat p b) - 1 :=
begin
apply int.coe_nat_inj,
have b0' : (b:ℚ) ≠ 0 := nat.cast_ne_zero.2 b_nonzero,
have p0' : (p:ℚ) ≠ 0,
{ rw nat.cast_ne_zero, exact nat.prime.ne_zero p_prime },
haveI : fact (nat.prime p) := p_prime,
rw [padic_val_rat_of_nat, cast_dvd _ _ dvd p0',
padic_val_rat.div p b0' p0',
sorry,
end


@Patrick Stevens

#### Kevin Buzzard (Jun 28 2020 at 19:25):

You just have to learn the knack. lemma bad (b p : nat) : (b : ℚ) / (p : ℚ) = (((b : ℕ) / (p : ℕ)) : ℚ) := rfl works because Lean knows the RHS is a rational so it deduces that / is rat.div and then it coerces b and p into Q before doing the division. You need to tell Lean the division is still happening in nat, that's what it guesses incorrectly.

#### Patrick Stevens (Jun 28 2020 at 21:33):

Thanks all, I'll stare at these

#### Kevin Buzzard (Jun 28 2020 at 21:34):

It took me a while. You go from outside in. I used to be forever checking types when I was doing this the first time

#### Patrick Stevens (Jun 29 2020 at 07:36):

This is what I mean when I say I don't know how to control the type of anything: I have not yet found any type annotations I can place on the last line while retaining an expression that type-checks, and I don't know what types the things on the left or right hand side of f are. When I hover over them in the Lean widget, it tells me it's coercing to Z, but when I try and annotate anything as being in Z, the nat.cast_sub stops compiling, with an error message that tells me two identical terms are not equal. (Obviously the terms aren't identical - one of them has been coerced to a different type than the other. But I have no idea what those types are.)

import data.nat.prime
import data.nat.multiplicity
import tactic
import ring_theory.multiplicity

theorem cast_dvd {α : Type*} [field α] (m n : ℕ) (n_dvd : n ∣ m) (n_nonzero : (n:α) ≠ 0) : ((m / n : ℕ) : α) = m / n :=
begin
rcases n_dvd with ⟨k, rfl⟩,
have : n ≠ 0, {rintro rfl, simpa using n_nonzero},
rw nat.mul_div_cancel_left _ (nat.pos_iff_ne_zero.2 this),
rw [nat.cast_mul, mul_div_cancel_left _ n_nonzero],
end

lemma padic_val_nat_of_quot (p : nat) (p_prime : nat.prime p) (b : nat) (b_nonzero : b ≠ 0) (dvd : p ∣ b) : (padic_val_nat p (b / p)) = (padic_val_nat p b) - 1 :=
begin
let e := @padic_val_rat.div p p_prime b p (nat.cast_ne_zero.mpr b_nonzero) (nat.cast_ne_zero.mpr (nat.prime.ne_zero p_prime)),
rw @padic_val_rat.padic_val_rat_self p (nat.prime.one_lt p_prime) at e,
rw ← @padic_val_rat_of_nat p b at e,
rw <- @cast_dvd ℚ _ b p dvd (nat.cast_ne_zero.mpr (nat.prime.ne_zero p_prime)) at e,
rw <- @padic_val_rat_of_nat at e,
have r : 1 ≤ padic_val_nat p b := by sorry, -- I can do this

have f : ↑(padic_val_nat p b - 1) = ↑(padic_val_nat p b) - ↑1 := @nat.cast_sub ℤ _ _ _ _ r,
end


The aim is to append these lines to get a u that type-checks, but currently f.symm is of the wrong type (although the error message does not help me work out what that type is):

  have s : (padic_val_nat p b : ℤ) - ↑1 = ↑(padic_val_nat p b) - 1, by congr,
rw <- s at e,
let u := eq.trans e (f.symm),


#### Patrick Stevens (Jun 29 2020 at 07:40):

Ah, I found an unhelpful type annotation I can place without breaking things: I can note that either of the 1s is a nat. But that doesn't tell me what anything has been coerced to.

#### Scott Morrison (Jun 29 2020 at 08:11):

I don't have long to look at this now, but the fact that you are writing ↑ by hand seems like a bad idea. Always write (x : T) when you want to make coercions.

#### Scott Morrison (Jun 29 2020 at 08:12):

What do you want f to say?

#### Patrick Massot (Jun 29 2020 at 08:16):

When I copy-paste your code I get unknown identifier 'padic_val_nat'.

Hmm... I don't!

#### Patrick Massot (Jun 29 2020 at 08:18):

Oops, I needed to restart Lean after updating.

#### Patrick Massot (Jun 29 2020 at 08:19):

Now I can ask "What do you want f to say?".

#### Scott Morrison (Jun 29 2020 at 08:20):

So if you replace the last line with

  have f : ((padic_val_nat p b - 1 : ℕ) : ℤ) = (padic_val_nat p b : ℤ) - ((1 : ℕ) : ℤ) := by convert @nat.cast_sub ℤ _ _ _ _ r,


#### Scott Morrison (Jun 29 2020 at 08:20):

you at least get a manageable error message

#### Patrick Massot (Jun 29 2020 at 08:20):

But at least I can finish the proof: exact_mod_cast e.

:-)

#### Scott Morrison (Jun 29 2020 at 08:22):

I would advise trusting in Patrick's answer, but if you want to dig deeper you'll have to work out why there are two different ways the coercion is happening. :-(

#### Scott Morrison (Jun 29 2020 at 08:22):

The unsolved goal from my last line is coe_base = nat.cast_coe, ... which isn't a good sign!

#### Patrick Massot (Jun 29 2020 at 08:38):

I did a bit of cleanup, but now I should work instead:

import data.nat.prime
import data.nat.multiplicity
import tactic
import ring_theory.multiplicity

theorem cast_dvd {α : Type*} [field α] {m n : ℕ} (n_dvd : n ∣ m) (n_nonzero : (n:α) ≠ 0) : ((m / n : ℕ) : α) = m / n :=
begin
rcases n_dvd with ⟨k, rfl⟩,
have : n ≠ 0, {rintro rfl, simpa using n_nonzero},
rw nat.mul_div_cancel_left _ (nat.pos_iff_ne_zero.2 this),
rw [nat.cast_mul, mul_div_cancel_left _ n_nonzero],
end

@[norm_cast]
theorem cast_dvd_char_zero {α : Type*} [field α] [char_zero α ] {m n : ℕ} (n_dvd : n ∣ m) : ((m / n : ℕ) : α) = m / n :=
begin
by_cases hn : n = 0,
{ subst hn,
simp },
exact cast_dvd n_dvd (nat.cast_ne_zero.mpr hn),
end

lemma padic_val_nat_of_quot {p : ℕ} (p_prime : nat.prime p) {b : ℕ} (b_nonzero : b ≠ 0) (dvd : p ∣ b) :
(padic_val_nat p (b / p)) = (padic_val_nat p b) - 1 :=
begin
haveI : fact p.prime := p_prime,
have e := padic_val_rat.div p (nat.cast_ne_zero.mpr b_nonzero) (nat.cast_ne_zero.mpr (nat.prime.ne_zero p_prime)),
have r : 1 ≤ padic_val_nat p b := sorry, -- I can do this
exact_mod_cast e,
end


#### Patrick Stevens (Jun 29 2020 at 11:50):

Scott Morrison said:

I don't have long to look at this now, but the fact that you are writing ↑ by hand seems like a bad idea. Always write (x : T) when you want to make coercions.

Ah OK, thanks - I was essentially copy-pasting out of the goal window at that point; just wanted to construct terms that I could rw` by to make progress

#### Patrick Stevens (Jun 29 2020 at 11:51):

Thanks again all, I will stare harder at these examples

#### Kevin Buzzard (Jun 29 2020 at 11:59):

I often find myself deleting arrows which I've cut and pasted from goal windows

Last updated: Dec 20 2023 at 11:08 UTC