## Stream: new members

### Topic: Cryptic error message

#### Bhavik Mehta (Dec 12 2019 at 23:12):

invalid apply tactic, failed to unify
geom_series (1 + 1) (kU + 1) * 1 + 1 = (1 + 1) ^ (kU + 1)
with
geom_series (1 + 1) (kU + 1) * 1 + 1 = (1 + 1) ^ (kU + 1)


Here's the code:

  example (U : finset (fin n)) (hU : U ≠ ∅) : sum U (λ (x : fin n), 2 ^ x.val) < 2^((max' U hU).1+1) :=
begin
set kU := (max' U hU).1,
have r: geom_series (1+1) (kU + 1) * 1 + 1 = (1+1)^(kU+1),
apply geom_sum_mul_add 1 (kU + 1),

end


#### Simon Hudon (Dec 12 2019 at 23:14):

Some of the implicit arguments are probably different. Try adding set_option pp.implicit true before your lemma. It will show you the implicit arguments

#### Bhavik Mehta (Dec 12 2019 at 23:16):

The error message says

invalid apply tactic, failed to unify
@geom_series ℕ nat.semiring (1 + 1) (kU + 1) * 1 + 1 = (1 + 1) ^ (kU + 1)
with
@geom_series ℕ nat.semiring (1 + 1) (kU + 1) * 1 + 1 = (1 + 1) ^ (kU + 1)


now...

#### Kevin Buzzard (Dec 12 2019 at 23:16):

Then try setting pp.all true

#### Reid Barton (Dec 12 2019 at 23:17):

or try convert instead of apply

#### Bhavik Mehta (Dec 12 2019 at 23:18):

or try convert instead of apply

Hmmm... Now my goal is nat.has_pow = monoid.has_pow

Nice!

#### Kevin Buzzard (Dec 12 2019 at 23:19):

So the issue is that the powers you're using are different

#### Kevin Buzzard (Dec 12 2019 at 23:19):

You can rewrite a lemma saying they're equal first

#### Bhavik Mehta (Dec 12 2019 at 23:19):

I was intending everything to be for nats though - that's why there's .1s around

#### Kevin Buzzard (Dec 12 2019 at 23:20):

The various ^s are being treated differently

#### Kevin Buzzard (Dec 12 2019 at 23:20):

It's notation for more than one thing

#### Kevin Buzzard (Dec 12 2019 at 23:21):

We can't fix it because the bad one is in core

#### Kevin Buzzard (Dec 12 2019 at 23:21):

So we lemmad our way around it

#### Bhavik Mehta (Dec 12 2019 at 23:22):

If I understand correctly though, ^ is overloaded using typeclasses, but changing the type to example (U : finset (fin n)) (hU : U ≠ ∅) : sum U (λ (x : fin n), (2 : ℕ) ^ (x.val : ℕ)) < (2 : ℕ)^((max' U hU).1+1 : ℕ) :=  still doesn't fix it

#### Kevin Buzzard (Dec 12 2019 at 23:22):

Nat is a monoid and maybe the geom series lemma uses monoid.pow

#### Kevin Buzzard (Dec 12 2019 at 23:22):

It's overloaded in a worse sense than eg +

#### Kevin Buzzard (Dec 12 2019 at 23:22):

It's two typeclasses

#### Kevin Buzzard (Dec 12 2019 at 23:23):

You're using nats so one is a nat.pow

Ah I see

#### Kevin Buzzard (Dec 12 2019 at 23:23):

And you're using monoids so one is a monoid.pow

#### Kevin Buzzard (Dec 12 2019 at 23:23):

And there's a lemma which says they're the same which you can rewrite before you do your apply

#### Kevin Buzzard (Dec 12 2019 at 23:24):

The fix is to delete nat.pow but it's in core so we can't

#### Kevin Buzzard (Dec 12 2019 at 23:24):

I mean the fix is to delete that notation

#### Bhavik Mehta (Dec 12 2019 at 23:26):

Do you have an idea where this lemma is? library_search can't find it

#### Kevin Buzzard (Dec 12 2019 at 23:26):

In Algebra.group_power maybe?

#### Reid Barton (Dec 12 2019 at 23:26):

it's probably eta expanded like x^n = x^n

#### Bhavik Mehta (Dec 12 2019 at 23:32):

It's two typeclasses

Where are the two typeclasses? I can only see has_pow...

#### Bhavik Mehta (Dec 12 2019 at 23:33):

In Algebra.group_power maybe?

I found nat.pow_eq_pow, but still not much luck

#### Bhavik Mehta (Dec 12 2019 at 23:33):

Finally managed, thanks both

Last updated: May 16 2021 at 05:21 UTC