Zulip Chat Archive

Stream: general

Topic: definitional equalities


view this post on Zulip Thorsten Altenkirch (Sep 23 2020 at 17:33):

Ok, I have been converted. I am going to use definitional equations like:

def notb : bool  bool
| tt := ff
| ff := tt

theorem notb_1 : notb tt = ff := rfl
theorem notb_2 : notb ff = tt := rfl

Are they generated automatically? Exactly what is the naming convention?

This means I am not going to use simp but always rw instead?

view this post on Zulip Johan Commelin (Sep 23 2020 at 17:39):

@[simp] theorem notb_1 would make simp rw along that theorem when possible.

view this post on Zulip Johan Commelin (Sep 23 2020 at 17:39):

And the mathlib name convention would be to call it notb_tt and notb_ff

view this post on Zulip Thorsten Altenkirch (Sep 23 2020 at 17:45):

Ok, but they are not generated automagically?

view this post on Zulip Johan Commelin (Sep 23 2020 at 17:50):

Nope, I don't think so.

view this post on Zulip Johan Commelin (Sep 23 2020 at 17:52):

But we have an attribute @[simps] that you can stick in front of a definition, and it will generate simp lemmas for you. At the moment it doesn't handle inductive definitions, like you gave. It only handles projections out of record types. But it's only lack of human time and energy... in principle we can have the automagic generation like you wish for.

view this post on Zulip Reid Barton (Sep 23 2020 at 17:52):

They are, use #print prefix notb to see them

view this post on Zulip Johan Commelin (Sep 23 2020 at 17:52):

Oooh, cool. But they aren't tagged @[simp], right?

view this post on Zulip Reid Barton (Sep 23 2020 at 17:54):

ah, no

view this post on Zulip Rob Lewis (Sep 23 2020 at 17:56):

Putting @[simp] def notb : ... does that, or something equivalent, no?

view this post on Zulip Mario Carneiro (Sep 23 2020 at 18:46):

definitional equations like this are usually marked @[simp], and as rob says you can just put @[simp] on the definition to mark the equation lemmas as simp lemmas

view this post on Zulip Scott Morrison (Sep 23 2020 at 23:28):

(with the proviso that as the pattern matches become more complicated, the generated equation lemmas become more ... surprising!)


Last updated: May 08 2021 at 04:14 UTC