confused on what's happening here... N and Z?

Stream: new members

[Lawrence Lin]

Hi, everyone! I'm trying to write some lean stuff, but I'm getting a weird error.

import tactic
import geom_sum

example (a m n : ℕ) : (nat.gcd (a^m - 1) (a^n - 1)) = a^(nat.gcd m n) - 1 :=
begin
rw mul_geom_sum a m,
end

and the error is
failed to synthesize type class instance for
a m n : ℕ
⊢ ring ℕ
state:
a m n : ℕ
⊢ (a ^ m - 1).gcd (a ^ n - 1) = a ^ m.gcd n - 1

how do I resolve this? I'm assuming i need to turn my a into an integer, but i'm not sure how to do it.

[Johan Commelin]

If you change the ℕ into ℤ and the nat.gcd into int.gcd, would that help?

[Lawrence Lin]

let me try!

[Johan Commelin]

- on natural numbers means truncated subtraction. So it probably is not exactly what you want.

[Lawrence Lin]

truncated subtraction?

[Lawrence Lin]

import tactic
import geom_sum

example (a m n : ℤ) : (int.gcd (a^m - 1) (a^n - 1)) = a^(int.gcd m n) - 1 :=
begin
rw mul_geom_sum a m,
end

gives me failed to synthesize type class instance for
a m n : ℤ
⊢ has_pow ℤ ℤ

[Lawrence Lin]

(an error)

[Lawrence Lin]

looked up truncated subtraction. i think ik what it means now, like m - n for m < n would give 0

[Johan Commelin]

Btw, with #backticks you can typeset codeblocks on Zulip to get syntax highlighting and such.

[Lawrence Lin]

oooh sure let me try

type mismatch at application
  pow a
term
  a
has type
  ℤ
but is expected to have type
  ℕ

[Lawrence Lin]

yep!
thanks

[Johan Commelin]

Ooh, I guess only a should have become a ℤ. But m and n should still be ℕ.

[Lawrence Lin]

yea, i tried that too

[Lawrence Lin]

import tactic
import geom_sum

example (a : ℤ) (m n : ℕ) : (int.gcd (a^m - 1) (a^n - 1)) = a^(nat.gcd m n) - 1 :=
begin
  /- rw mul_geom_sum a m, -/
  sorry,
end

the left hand side of my statement is okay! but... the right hand side isn't.
it spits out this error

type mismatch at application
  pow a
term
  a
has type
  ℤ
but is expected to have type
  ℕ

[Lawrence Lin]

doesn't matter if i do try int.gcd or nat.gcd for it :')

[Johan Commelin]

Huh, does docs#int.gcd spit out a natural number?

[Johan Commelin]

Apparently it does!

[Lawrence Lin]

both int and nat do!

[Lawrence Lin]

which does make sense, after all... hmm...

[Johan Commelin]

Ok, write \u in front of the left-hand-side

[Johan Commelin]

It will typeset as ↑.

[Lawrence Lin]

mhm i see
what does that do?

[Johan Commelin]

Alternatively, you can write (int.gcd (a^m - 1) (a^n - 1) : ℤ)

[Lawrence Lin]

the statement magically works now o.o

[Johan Commelin]

↑ is a "coercion". It turns something of type X into something of type Y whenever that makes sense.

[Johan Commelin]

For a suitable value of "whenever that makes sense".

[Lawrence Lin]

i see!
would it be better style to use \u or (left hand side : Z)

[Lawrence Lin]

since i suspect \u might break sometimes... and you can't tell exactly what it wants to become!

[Johan Commelin]

The 2nd is a bit more readable and predictable.

[Lawrence Lin]

alright! i'll be using that then. thanks for your help!

[Lawrence Lin]

i'm going to go try and prove this c:

[Eric Wieser]

The 2nd is a bit more readable and predictable.

I don't agree with it being more predictable; certainly not to newcomers. Consider

def foo (m n : ℕ) : ℚ := (m + n : ℤ)

which actually means

#print foo
-- def foo : ℕ → ℕ → ℚ := λ (m n : ℕ), ↑(↑m + ↑n)

In general the two syntaxes are not directly interchangeable

[Eric Wieser]

The most predictable spelling would probably be:

def foo (m n : ℕ) : ℚ := ↑(↑m + ↑n : ℤ)

where ↑ means "do a coercion", and : ℤ means "here's a hint about what you're supposed to coerce to".