Zulip Chat Archive

Stream: new members

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


Lawrence Lin (Nov 16 2022 at 19:41):

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 (Nov 16 2022 at 19:43):

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

Lawrence Lin (Nov 16 2022 at 19:43):

let me try!

Johan Commelin (Nov 16 2022 at 19:44):

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

Lawrence Lin (Nov 16 2022 at 19:44):

truncated subtraction?

Lawrence Lin (Nov 16 2022 at 19:44):

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 (Nov 16 2022 at 19:45):

(an error)

Lawrence Lin (Nov 16 2022 at 19:47):

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

Johan Commelin (Nov 16 2022 at 19:48):

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

Lawrence Lin (Nov 16 2022 at 19:48):

oooh sure let me try

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

Lawrence Lin (Nov 16 2022 at 19:48):

yep!
thanks

Johan Commelin (Nov 16 2022 at 19:49):

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

Lawrence Lin (Nov 16 2022 at 19:50):

yea, i tried that too

Lawrence Lin (Nov 16 2022 at 19:51):

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 (Nov 16 2022 at 19:51):

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

Johan Commelin (Nov 16 2022 at 19:51):

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

Johan Commelin (Nov 16 2022 at 19:51):

Apparently it does!

Lawrence Lin (Nov 16 2022 at 19:52):

both int and nat do!

Lawrence Lin (Nov 16 2022 at 19:52):

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

Johan Commelin (Nov 16 2022 at 19:52):

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

Johan Commelin (Nov 16 2022 at 19:52):

It will typeset as .

Lawrence Lin (Nov 16 2022 at 19:52):

mhm i see
what does that do?

Johan Commelin (Nov 16 2022 at 19:52):

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

Lawrence Lin (Nov 16 2022 at 19:52):

the statement magically works now o.o

Johan Commelin (Nov 16 2022 at 19:53):

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

Johan Commelin (Nov 16 2022 at 19:53):

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

Lawrence Lin (Nov 16 2022 at 19:53):

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

Lawrence Lin (Nov 16 2022 at 19:54):

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

Johan Commelin (Nov 16 2022 at 19:54):

The 2nd is a bit more readable and predictable.

Lawrence Lin (Nov 16 2022 at 19:54):

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

Lawrence Lin (Nov 16 2022 at 19:54):

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

Eric Wieser (Nov 16 2022 at 20:16):

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 (Nov 16 2022 at 20:19):

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".


Last updated: Dec 20 2023 at 11:08 UTC