Zulip Chat Archive

Stream: new members

Topic: invalid apply tactic


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

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

view this post on Zulip Kevin Buzzard (May 02 2020 at 21:21):

You shouldn't need it

view this post on Zulip Paul van Wamelen (May 02 2020 at 22:55):

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

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

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

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

view this post on Zulip Paul van Wamelen (May 03 2020 at 00:23):

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

view this post on Zulip Kevin Buzzard (May 03 2020 at 00:25):

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

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

view this post on Zulip Reid Barton (May 03 2020 at 00:29):

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

view this post on Zulip Reid Barton (May 03 2020 at 00:29):

I guess you said how, not why

view this post on Zulip Kevin Buzzard (May 03 2020 at 00:31):

Yes I guess

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

view this post on Zulip Kevin Buzzard (May 03 2020 at 00:32):

Then what?

view this post on Zulip Kevin Buzzard (May 03 2020 at 00:32):

All solutions I can think of are ugly

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

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

view this post on Zulip Kevin Buzzard (May 03 2020 at 08:39):

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

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