Zulip Chat Archive

Stream: general

Topic: cast woes


Kevin Buzzard (May 25 2018 at 10:05):

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 (May 25 2018 at 10:05):

What am I doing wrong?

Kevin Buzzard (May 25 2018 at 10:05):

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

Kevin Buzzard (May 25 2018 at 10:06):

I tried to be really precise:

Kevin Buzzard (May 25 2018 at 10:06):

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 (May 25 2018 at 10:06):

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

Kevin Buzzard (May 25 2018 at 10:06):

I switched pp.all off and got swamped.

Chris Hughes (May 25 2018 at 10:07):

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

Kevin Buzzard (May 25 2018 at 10:07):

You're right Chris.

Kevin Buzzard (May 25 2018 at 10:07):

Do you know why what I tried is failing?

Chris Hughes (May 25 2018 at 10:09):

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 (May 25 2018 at 10:10):

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

Mario Carneiro (May 25 2018 at 10:25):

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

Kevin Buzzard (May 26 2018 at 09:32):

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 (May 26 2018 at 09:33):

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

Kevin Buzzard (May 26 2018 at 09:33):

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

Kevin Buzzard (May 26 2018 at 09:35):

pmod is standard LaTeX notation

Mario Carneiro (May 26 2018 at 09:36):

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

Kevin Buzzard (May 26 2018 at 09:36):

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 (May 26 2018 at 09:36):

Oh --

Kevin Buzzard (May 26 2018 at 09:36):

this was forced upon you somehow?

Kevin Buzzard (May 26 2018 at 09:36):

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

Kevin Buzzard (May 26 2018 at 09:37):

the MOD stuff

Mario Carneiro (May 26 2018 at 09:37):

I'm not even sure the notation is worth it

Kevin Buzzard (May 26 2018 at 09:37):

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

Kevin Buzzard (May 26 2018 at 09:38):

The notation is what mathematicians want

Mario Carneiro (May 26 2018 at 09:38):

it's a parsing thing

Kevin Buzzard (May 26 2018 at 09:38):

We are sticklers for notation

Kevin Buzzard (May 26 2018 at 09:38):

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

Mario Carneiro (May 26 2018 at 09:40):

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

Kevin Buzzard (May 26 2018 at 09:40):

it enables you to write uncluttered calc proofs

Kevin Buzzard (May 26 2018 at 09:40):

so it's definitely better than no notation

Kevin Buzzard (May 26 2018 at 09:40):

but it still looks funny

Kevin Buzzard (May 26 2018 at 09:40):

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

Kevin Buzzard (May 26 2018 at 09:41):

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

Mario Carneiro (May 26 2018 at 09:41):

I never tried it, but I think chris did

Kevin Buzzard (May 26 2018 at 09:41):

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

Kevin Buzzard (May 26 2018 at 09:41):

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

Chris Hughes (May 26 2018 at 09:43):

What funny MOD stuff?

Kevin Buzzard (Jan 23 2019 at 10:34):

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 (Jan 23 2019 at 10:34):

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 (Jan 23 2019 at 14:58):

(deleted)

Simon Hudon (Jan 23 2019 at 23:53):

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


Last updated: Dec 20 2023 at 11:08 UTC