# Zulip Chat Archive

## 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
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 (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
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 (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

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

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

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

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: Dec 20 2023 at 11:08 UTC