cast woes

Stream: general

[Kevin Buzzard]

import data.int.basic data.nat.cast

#check int.mod_add_mod -- ∀ (m n k : ℤ), (m % n + k) % n = (m + k) % n
-- #check nat.mod_add_mod -- unknown identifier
-- so let's create it

-- note:
#check int.of_nat_mod -- ∀ (m n : ℕ), ↑m % ↑n = int.of_nat (m % n)

theorem nat.mod_add_mod : ∀ (m n k : ℕ), (m % n + k) % n = (m + k) % n :=
begin
  intros m n k,
  apply int.of_nat_inj,
  rw ←int.of_nat_mod,
  rw ←int.of_nat_mod,
  rw nat.cast_add -- fails
  /-
  rewrite tactic failed, did not find instance of the pattern in the target expression
  ↑(?m_4 + ?m_5)
state:
m n k : ℕ
⊢ ↑(m % n + k) % ↑n = ↑(m + k) % ↑n
  -/
  sorry
end

[Kevin Buzzard]

What am I doing wrong?

[Kevin Buzzard]

I found a "hole" in mathlib -- but am failing to fix it.

[Kevin Buzzard]

I tried to be really precise:

[Kevin Buzzard]

have H1 := @nat.cast_add ℤ _ _ (m % n) k,
  /-
  H1 : ↑(m % n + k) = ↑(m % n) + ↑k
  ⊢ ↑(m % n + k) % ↑n = ↑(m + k) % ↑n
  -/

  -- rw H1, -- fails
  /-
  rewrite tactic failed, did not find instance of the pattern in the target expression
  ↑(m % n + k)
state:
m n k : ℕ,
H1 : ↑(m % n + k) = ↑(m % n) + ↑k
⊢ ↑(m % n + k) % ↑n = ↑(m + k) % ↑n
  -/

[Kevin Buzzard]

I switched notation off and the rewrite still looked like it should work

[Kevin Buzzard]

I switched pp.all off and got swamped.

[Chris Hughes]

int.coe_nat_add is the correct lemma, rather than nat.cast_add I think

[Kevin Buzzard]

You're right Chris.

[Kevin Buzzard]

Do you know why what I tried is failing?

[Chris Hughes]

Because cast is a coercion into a general ring, whereas there's a seperately defined coercion fromnat to int, probably because it's in core, but cast is is in mathlib

[Chris Hughes]

Also, of_nat is a more natural function to use as the coercion than cast which just does 1 + 1 + 1 ...

[Mario Carneiro]

You can probably use nat.modeq to prove this one, there are more modeq theorems than there are theorems about mod

[Kevin Buzzard]

You can probably use nat.modeq to prove this one, there are more modeq theorems than there are theorems about mod

My eyes are opened!

[Kevin Buzzard]

I had somehow ruled out this MOD stuff as "another way of setting up the theory, which I didn't use".

[Kevin Buzzard]

I've always thought that MOD notation was horrible, by the way.

[Kevin Buzzard]

pmod is standard LaTeX notation

[Mario Carneiro]

there were technical reasons I couldn't use parens and lowercase

[Kevin Buzzard]

I think using LaTeX as a guide is a good idea. I'm really familiar with LaTeX notation and it still occasionally confuses me that \equiv is not equiv

[Kevin Buzzard]

Oh --

[Kevin Buzzard]

this was forced upon you somehow?

[Kevin Buzzard]

I had no idea! I just thought it was a wacky design decision

[Kevin Buzzard]

the MOD stuff

[Mario Carneiro]

I'm not even sure the notation is worth it

[Kevin Buzzard]

This wasn't the fault of some labour-saving tactic was it?

[Kevin Buzzard]

The notation is what mathematicians want

[Mario Carneiro]

it's a parsing thing

[Kevin Buzzard]

We are sticklers for notation

[Kevin Buzzard]

That's why I mentioned it -- it looks funny to mathematicians because there is already standard notation

[Mario Carneiro]

It's probably better than no notation, but even as it is it's a bit problematic

[Kevin Buzzard]

it enables you to write uncluttered calc proofs

[Kevin Buzzard]

so it's definitely better than no notation

[Kevin Buzzard]

but it still looks funny

[Kevin Buzzard]

To be honest I've never used it -- I assume it can be used in calc proofs

[Kevin Buzzard]

I'm giving a talk on this stuff in about 10 hours

[Mario Carneiro]

I never tried it, but I think chris did

[Kevin Buzzard]

Maybe it's about time I learnt how it worked.

[Kevin Buzzard]

@Chris Hughes how did you learn that funny MOD stuff?

[Chris Hughes]

What funny MOD stuff?

[Kevin Buzzard]

I have generally got the hang of how to handle casts now. The point of view which I want to push amongst the UGs is that even though yes it's annoying that natural numbers aren't actually real numbers, simp should do all the translating for you. But here's an example where I couldn't make it work:

import data.real.basic

example (M : ℕ) (H : 0 < M + 1) : (0 : ℝ) < M + 1 :=
begin
  simp [H],
  -- ⊢ 0 < 1 + ↑M
  -- gaargh
  -- simp at H, -- won't change it to 0 < 1 + M
  sorry
end

Applying simp to nat M + 1 doesn't change it, but applying simp to real M + 1 changes it to 1 + M and this somehow means Lean loses track.

[Kevin Buzzard]

I know I can use some cast_lt or whatever, but this is exactly what I am trying to avoid. simp is usually good at these.

[Andrew Ashworth]

(deleted)

[Simon Hudon]

I recommend finding the simp lemma responsible for this (probably something like real.add_comm) and declare in your file local attribute [-simp] real.add_comm