Coercion between nat and rat

Stream: new members

[Patrick Stevens]

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]

Type inference is outside in.

[Reid Barton]

(Generally speaking.)

[Patrick Stevens]

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]

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

[Reid Barton]

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

[Mario Carneiro]

:up:

[Patrick Stevens]

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

open padic_val_rat

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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',
    padic_val_rat.padic_val_rat_self p_prime.one_lt,
    int.coe_nat_sub, padic_val_rat_of_nat, int.coe_nat_one],
  sorry,
end

[Mario Carneiro]

@Patrick Stevens

[Kevin Buzzard]

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]

Thanks all, I'll stare at these

[Kevin Buzzard]

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]

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 data.padics.padic_norm
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]

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]

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]

What do you want f to say?

[Patrick Massot]

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

[Scott Morrison]

Hmm... I don't!

[Patrick Massot]

Oops, I needed to restart Lean after updating.

[Patrick Massot]

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

[Scott Morrison]

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]

you at least get a manageable error message

[Patrick Massot]

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

[Scott Morrison]

:-)

[Scott Morrison]

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]

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

[Patrick Massot]

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

import data.nat.prime
import data.nat.multiplicity
import data.padics.padic_norm
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)),
  rw padic_val_rat.padic_val_rat_self (nat.prime.one_lt p_prime) at e,
  have r : 1 ≤ padic_val_nat p b := sorry, -- I can do this
  exact_mod_cast e,
end

[Patrick Stevens]

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]

Thanks again all, I will stare harder at these examples

[Kevin Buzzard]

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