definitional equalities

Stream: general

[Thorsten Altenkirch]

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]

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

[Johan Commelin]

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

[Thorsten Altenkirch]

Ok, but they are not generated automagically?

[Johan Commelin]

Nope, I don't think so.

[Johan Commelin]

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]

They are, use #print prefix notb to see them

[Johan Commelin]

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

[Reid Barton]

ah, no

[Rob Lewis]

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

[Mario Carneiro]

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]

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