Zulip Chat Archive

Stream: general

Topic: refl power


view this post on Zulip Patrick Massot (May 13 2020 at 13:43):

At https://github.com/leanprover-community/tutorials/issues/11, @Dan Stanescu asks why rw is so powerful. I know that part of the answer is it calls refl, by I don't understand why refl works when the relevant lemma doesn't seem to be tagged.

import data.nat.basic

open nat

-- The following lemma is not tagged refl
#check @dvd_refl
/- dvd_refl : ∀ {α : Type*} [comm_semiring α] (a : α), a ∣ a -/

example (n : ) : n  n := by refl

view this post on Zulip Patrick Massot (May 13 2020 at 13:45):

Note that you cannot replace by refl with rfl here

view this post on Zulip Gabriel Ebner (May 13 2020 at 13:50):

It is tagged?

-- #print dvd_refl
@[refl, simp, priority 100]
theorem dvd_refl :  {α : Type u} [_inst_1 : comm_semiring α] (a : α), a  a :=

view this post on Zulip Kenny Lau (May 13 2020 at 13:52):

(deleted)

view this post on Zulip Patrick Massot (May 13 2020 at 13:53):

Ok, so someone added this attribute far away from the lemma itself (presumably in mathlib)

view this post on Zulip Patrick Massot (May 13 2020 at 13:53):

I should have used #print instead of "Go to definition"

view this post on Zulip Johan Commelin (May 13 2020 at 13:53):

I'm about to move that definition out of core

view this post on Zulip Patrick Massot (May 13 2020 at 13:54):

It even sounds familiar. I think this is not the first time I meet this issue actually.

view this post on Zulip Johan Commelin (May 13 2020 at 13:54):

And when I say "I", of course I mean "Johan, with an enormous amount of help from Gabriel"

view this post on Zulip Patrick Massot (May 13 2020 at 13:55):

https://github.com/leanprover-community/mathlib/blob/master/src/algebra/ring.lean#L156


Last updated: May 08 2021 at 03:17 UTC