## Stream: new members

### Topic: invalid apply tactic

#### Paul van Wamelen (May 02 2020 at 20:30):

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

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 (May 02 2020 at 21:21):

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 (May 02 2020 at 21:21):

You shouldn't need it

#### Paul van Wamelen (May 02 2020 at 22:55):

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

#### Kevin Buzzard (May 02 2020 at 23:35):

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 (May 02 2020 at 23:41):

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

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 (May 02 2020 at 23:45):

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 (May 03 2020 at 00:23):

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

#### Kevin Buzzard (May 03 2020 at 00:25):

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

#### Kevin Buzzard (May 03 2020 at 00:27):

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 (May 03 2020 at 00:29):

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

#### Reid Barton (May 03 2020 at 00:29):

I guess you said how, not why

Yes I guess

#### Kevin Buzzard (May 03 2020 at 00:31):

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

Then what?

#### Kevin Buzzard (May 03 2020 at 00:32):

All solutions I can think of are ugly

#### Kevin Buzzard (May 03 2020 at 00:33):

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

#### Jalex Stark (May 03 2020 at 01:09):

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 (May 03 2020 at 08:39):

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

#### Reid Barton (May 03 2020 at 09:36):

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.

Last updated: May 13 2021 at 18:26 UTC