Zulip Chat Archive

Stream: general

Topic: refl failure without intros


Oliver Nash (Feb 06 2020 at 20:57):

Is there an easy explanation for why the following fails if I drop the intros from the proof of map_mul?

universes u v w

variables {α : Type u} {β : Type v} {γ : Type w} [monoid β] [comm_monoid γ]

@[to_additive]
lemma hom_prod (s : finset α) (b : β) (g : α  β →* γ) :
  s.prod (λ a, g a b) = (s.prod g) b :=
begin
let evb : (β →* γ)  γ := λ h, h b,
haveI : is_monoid_hom evb := {
  map_one := rfl,
  map_mul := by { intros, refl, }, },
rw finset.prod_hom s evb,
end

Oliver Nash (Feb 06 2020 at 21:00):

The error I see if I replace map_mul := by { intros, refl, } with map_mul := rfl is:

type mismatch at field 'map_mul'
  rfl
has type
  ?m_2 = ?m_2
but is expected to have type
  ∀ (x y : β →* γ), evb (x * y) = evb x * evb y

Patrick Massot (Feb 06 2020 at 21:00):

Why would it work?

Oliver Nash (Feb 06 2020 at 21:01):

Erm, good question!

Patrick Massot (Feb 06 2020 at 21:02):

in

example :  n : , n = n :=
begin
  sorry
end

would you expect refl to close the goal?

Patrick Massot (Feb 06 2020 at 21:02):

hint: you shouldn't.

Oliver Nash (Feb 06 2020 at 21:02):

Oh dear, I would have expected it to close that goal :embarrassed:

Oliver Nash (Feb 06 2020 at 21:03):

Thank you for providing such a simplified example. Is there a simple explanation for when I should expect refl to work, or somewhere I should look to read more?

Patrick Massot (Feb 06 2020 at 21:03):

You should expect it to work when the goal is x = x, maybe in disguise.

Oliver Nash (Feb 06 2020 at 21:03):

Till now I had regarded it as a way to close goals that are just definitional equalities once you unfold sufficiently (or something along those lines).

Patrick Massot (Feb 06 2020 at 21:04):

Yes, exactly.

Oliver Nash (Feb 06 2020 at 21:04):

Right, that has been my approximate understanding.

Patrick Massot (Feb 06 2020 at 21:04):

And ∀ n : ℕ, n = n is not of that form.

Oliver Nash (Feb 06 2020 at 21:04):

But I'm fairly sure it has been able to succeed in the past when there was a universal qualifier "in the way".

Oliver Nash (Feb 06 2020 at 21:04):

Understood, perhaps my memory misleads me.

Oliver Nash (Feb 06 2020 at 21:05):

Hmm, I suppose it does. There does not seem to be anything more to this.

Oliver Nash (Feb 06 2020 at 21:05):

Thank you!

Patrick Massot (Feb 06 2020 at 21:06):

If you are frustrated to have to type two tactics to close this goal you can probably try tauto

Oliver Nash (Feb 06 2020 at 21:07):

Right ho, I'll use that.

Patrick Massot (Feb 06 2020 at 21:07):

I hope Mario has a good zulip filtering preventing him from seeing such suggestions...

Oliver Nash (Feb 06 2020 at 21:08):

You mean my original message (which I now realise was perhaps wasting people's time) or the suggestion to use tauto?

Patrick Massot (Feb 06 2020 at 21:08):

Seriously, the right proof here is lambda _ _, rfl

Patrick Massot (Feb 06 2020 at 21:08):

I meant the suggestion to use tauto

Oliver Nash (Feb 06 2020 at 21:09):

Oh I see.

Patrick Massot (Feb 06 2020 at 21:09):

You are not wasting people's time. Everybody answering questions here is volunteer, and has been asking elementary questions before.

Oliver Nash (Feb 06 2020 at 21:09):

Well, I can believe tauto might be too heavyweight alright!

Oliver Nash (Feb 06 2020 at 21:10):

Thanks for the encouragement, and again for the clarifications.

Mario Carneiro (Feb 06 2020 at 21:24):

I like the proof \lam _, rfl

Mario Carneiro (Feb 06 2020 at 21:25):

Note that refl already has problems with guessing the number of arguments because it is equivalent to apply *refl where *refl is some reflexivity lemma

Mario Carneiro (Feb 06 2020 at 21:26):

and the apply bug causes issues in cases like le_refl when le is defined as a pi

Mario Carneiro (Feb 06 2020 at 21:26):

maybe this is your recollection

Oliver Nash (Feb 06 2020 at 21:38):

Thank you @Mario Carneiro I suspect this is the case. I appreciate this further information.

Jesse Michael Han (Feb 06 2020 at 22:09):

this is also by cc


Last updated: Dec 20 2023 at 11:08 UTC