## Stream: general

### Topic: definitional equalities

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

#### Johan Commelin (Sep 23 2020 at 17:39):

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

#### Johan Commelin (Sep 23 2020 at 17:39):

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

#### Thorsten Altenkirch (Sep 23 2020 at 17:45):

Ok, but they are not generated automagically?

#### Johan Commelin (Sep 23 2020 at 17:50):

Nope, I don't think so.

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

#### Reid Barton (Sep 23 2020 at 17:52):

They are, use #print prefix notb to see them

#### Johan Commelin (Sep 23 2020 at 17:52):

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

ah, no

#### Rob Lewis (Sep 23 2020 at 17:56):

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

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

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