Zulip Chat Archive

Stream: new members

Topic: Cryptic error message

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

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

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

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