# 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 from`nat`

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