invalid apply tactic

Stream: new members

[Paul van Wamelen]

I'm getting

failed to unify
  k ∣ multiset.count q (factors' a0 hz)
with
  k ∣ multiset.count q (factors' a0 hz)

from this:

import ring_theory.unique_factorization_domain

noncomputable theory
open_locale classical

variables {α : Type*}

namespace associates
local attribute [instance] associated.setoid

open_locale add_monoid

lemma multiset_mul (s : multiset α) {k : ℕ} :
  (∀(a : α), k ∣ multiset.count a s) → ∃(u : multiset α), s = k • u := by sorry

open unique_factorization_domain associated lattice
variables [integral_domain α] [unique_factorization_domain α] [decidable_eq (associates α)]

-- set_option pp.all true
theorem power_of_count' (a0 : α) (hz : a0 ≠ 0) (k : ℕ)
  (hp : ∀ (p : {a // irreducible a}), k ∣ multiset.count p (factors' a0 hz))
  : ∃u, (factors' a0 hz) = k • u :=
begin
  apply multiset_mul (factors' a0 hz),
  intro q,
  apply hp q,
end

I'm sure the set_option pp.all true is telling me what is wrong, but I haven't been able to figure it out. Something to do with decidable_eq (associates α)?

[Kevin Buzzard]

You have put open_locale classical and that deals with all the decidable nonsense at once so you should probably remove the decidable_eq instance later

[Kevin Buzzard]

You shouldn't need it

[Paul van Wamelen]

Removing either open_locale classical or variable [decidable_eq (associates α)] still gives me errors...

[Kevin Buzzard]

OK you're going to have to talk to someone who knows what's going on. This isn't a mathematical problem, this is some sort of decidability problem. One of the terms contains

<           classical.prop_decidable
<             (@eq.{u_1+1}
<                (@subtype.{u_1+1}
<                   (@associates.{u_1} α
<                      (@ring.to_monoid.{u_1} α
<                         (@domain.to_ring.{u_1} α (@integral_domain.to_domain.{u_1} α _inst_1))))
<                   (λ
<                    (a :
<                      @associates.{u_1} α

and the other contains

>           @subtype.decidable_eq.{u_1}
>             (@associates.{u_1} α
>                (@ring.to_monoid.{u_1} α (@domain.to_ring.{u_1} α (@integral_domain.to_domain.{u_1} α _inst_1))))
>             (λ
>              (x :
>                @associates.{u_1} α
>                  (@ring.to_monoid.{u_1} α (@domain.to_ring.{u_1} α (@integral_domain.to_domain.{u_1} α _inst_1)))),
>                @irreducible.{u_1}
>                  (@associates.{u_1} α
>                     (@ring.to_monoid.{u_1} α (@domain.to_ring.{u_1} α (@integral_domain.to_domain.{u_1} α _inst_1))))
>                  (@comm_monoid.to_monoid.{u_1}
>                     (@associates.{u_1} α

Something has been decided in two different ways here.

[Kevin Buzzard]

The usual way around this is to use convert instead of apply. This works:

import ring_theory.unique_factorization_domain

--noncomputable theory
open_locale classical

variables {α : Type*}

namespace associates
--local attribute [instance] associated.setoid

open_locale add_monoid

lemma multiset_mul (s : multiset α) {k : ℕ} :
  (∀(a : α), k ∣ multiset.count a s) → ∃(u : multiset α), s = k • u := by sorry

open unique_factorization_domain associated lattice
variables [integral_domain α] [unique_factorization_domain α]

set_option pp.all true
theorem power_of_count' (a0 : α) (hz : a0 ≠ 0) (k : ℕ)
  (hp : ∀ (p : {a // irreducible a}), k ∣ multiset.count p (factors' a0 hz))
  : ∃u, (factors' a0 hz) = k • u :=
begin
  apply multiset_mul (factors' a0 hz),
  intro q,
  convert hp q,
end

end associates

[Kevin Buzzard]

The reason this works is because of this:

instance foo (P : Prop) : subsingleton (decidable P) := by apply_instance

decidable P is unfortunately a Type, i.e. it's data, and Lean managed to construct two terms of that type which weren't definitionally equal, so it couldn't unify them. However the example above shows that even though decidable P is a type, it's a subsingleton, which means that any two terms of that type are equal anyway. convert knows about this subsingleton trickery, and rw doesn't, so convert wins. In general you can use convert to close a goal when you have created a term (in this case hp q) which is equal to the goal modulo subsingleton types.

[Paul van Wamelen]

Wow, I'm glad I asked. I would NEVER have figured that out! Thanks Kevin!

[Kevin Buzzard]

I learnt lean by trying to do mathematics in it and asking whenever I got stuck

[Kevin Buzzard]

Independent of the convert solution there's still the question of how it happened, which is beyond me but certainly not beyond some people here.

[Reid Barton]

These things happen because there is no reason they should not happen :shrug:

[Reid Barton]

I guess you said how, not why

[Kevin Buzzard]

Yes I guess

[Kevin Buzzard]

I could envisage a rewrite failing for reasons like this, and convert being harder to apply because it's a subterm

[Kevin Buzzard]

Then what?

[Kevin Buzzard]

All solutions I can think of are ugly

[Kevin Buzzard]

Where's the tactic which replaces every instance of decidable anything in the entire local context by the one coming from classical?

[Jalex Stark]

is this morally what one wants from open_locale classical? to add a simp lemma that looks like decidable _ -\iff classical._? (where that _ is the instance you were gesturing at?)

[Kevin Buzzard]

Yeah maybe that's the way to do it? I'm not an expert at simp

[Reid Barton]

A more drastic version of this would be

lemma flatten_subsingleton {α : Type*} [subsingleton α] (h : α) :
  h = classical.choice ⟨h⟩ :=
subsingleton.elim _ _

But often these subsingletons will appear in places where they are hard to rewrite, I guess.