Zulip Chat Archive

Stream: new members

Topic: Cryptic error message


view this post on Zulip Bhavik Mehta (Dec 12 2019 at 23:12):

Can anyone give suggestions about this error message?

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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Kevin Buzzard (Dec 12 2019 at 23:16):

Then try setting pp.all true

view this post on Zulip Reid Barton (Dec 12 2019 at 23:17):

or try convert instead of apply

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 12 2019 at 23:18):

Nice!

view this post on Zulip Kevin Buzzard (Dec 12 2019 at 23:19):

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

view this post on Zulip Kevin Buzzard (Dec 12 2019 at 23:19):

You can rewrite a lemma saying they're equal first

view this post on Zulip Bhavik Mehta (Dec 12 2019 at 23:19):

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

view this post on Zulip Kevin Buzzard (Dec 12 2019 at 23:20):

The various ^s are being treated differently

view this post on Zulip Kevin Buzzard (Dec 12 2019 at 23:20):

It's notation for more than one thing

view this post on Zulip Kevin Buzzard (Dec 12 2019 at 23:21):

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

view this post on Zulip Kevin Buzzard (Dec 12 2019 at 23:21):

So we lemmad our way around it

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 12 2019 at 23:22):

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

view this post on Zulip Kevin Buzzard (Dec 12 2019 at 23:22):

It's overloaded in a worse sense than eg +

view this post on Zulip Kevin Buzzard (Dec 12 2019 at 23:22):

It's two typeclasses

view this post on Zulip Kevin Buzzard (Dec 12 2019 at 23:23):

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

view this post on Zulip Bhavik Mehta (Dec 12 2019 at 23:23):

Ah I see

view this post on Zulip Kevin Buzzard (Dec 12 2019 at 23:23):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 12 2019 at 23:24):

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

view this post on Zulip Kevin Buzzard (Dec 12 2019 at 23:24):

I mean the fix is to delete that notation

view this post on Zulip Bhavik Mehta (Dec 12 2019 at 23:26):

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

view this post on Zulip Kevin Buzzard (Dec 12 2019 at 23:26):

In Algebra.group_power maybe?

view this post on Zulip Reid Barton (Dec 12 2019 at 23:26):

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

view this post on Zulip Bhavik Mehta (Dec 12 2019 at 23:32):

It's two typeclasses

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

view this post on Zulip Bhavik Mehta (Dec 12 2019 at 23:33):

In Algebra.group_power maybe?

I found nat.pow_eq_pow, but still not much luck

view this post on Zulip Bhavik Mehta (Dec 12 2019 at 23:33):

Finally managed, thanks both


Last updated: May 16 2021 at 05:21 UTC