Efficiently unfolding notation

Stream: new members

[Keefer Rowan]

How is one supposed to unfold notation that comes from type classes? E.g. :

theorem not_mem_mem_compl {α : Type u} (x : α) (S : set α)  (h : ¬ (x ∈ S)) : x ∈ (- S) :=
begin
    sorry
end

I want to be able to unfold the notation -S using the definition of compl, so I would write unfold compl. This doesn't work, as I need to also tell it to unfold has_neg.neg, as the - notation is given for compl as an instance of the type class has_neg. Is there a better way to do this than unfold has_neg.neg compl? I want to be able to think of the notation as an abbreviation for compl, but here it is demanding an extra step. It doesn't seem similar steps are necessary for the notation + on nat, which is introduced the same way, with has_add. Is there an attribute I can give something so that unfold knows to incorporate has_neg?

[Reid Barton]

Three backticks and then a newline

[Keefer Rowan]

Thanks, fixed it.

[Reid Barton]

I think you also need these two steps to unfold + on nats, no?

[Reid Barton]

Or maybe the difference is + has an equational lemma which is phrased in terms of the notation?

[Reid Barton]

Because you probably only want to unfold + when you're also applying one of the two defining equations.

[Keefer Rowan]

Why does this work?

example : (1 + 0 = 1):=
begin
    refl,
end

[Reid Barton]

Because refl works up to definitional equality

[Reid Barton]

Er, well okay the exact reason is a bit complicated

[Reid Barton]

If you said exact rfl, then the reason would be that exact works up to definitional equality

[Keefer Rowan]

How does refl know to access has_add.add while unfold and dunfold doesn't?

[Reid Barton]

refl doesn't know anything about has_add

[Reid Barton]

refl says: the goal is equality, so I'll supply eq.rfl as the proof term

[Reid Barton]

and eq.rfl : 1 + 0 = 1, so Lean is happy

[Reid Barton]

In order to check this eq.rfl : 1 + 0 = 1, Lean knows that + is notation for has_add.add and it knows how to reduce has_add.add applied to the has_add instance for nat to get nat.add, and then how to unfold nat.add to its definition in terms of nat.rec, and then how to reduce nat.rec applied to 0, etc. But this is all happening outside the tactic layer.

[Reid Barton]

On the other hand, unfold means: replace the named thing with its definition (possibly applying equational lemmas).

[Reid Barton]

You didn't give an example involving + and unfold, so it's not analogous.

[Keefer Rowan]

So in some sense refl is "smarter" or has access to more stuff than unfold' (but as you say it's all happening outside of tactic layer). So refl can figure out definitions that unfold` can't without being fed them explicitly?

[Reid Barton]

If anything, refl is dumber.

[Reid Barton]

There are several layers at work here, and several different notions of equality.

[Keefer Rowan]

And your point about not having an example of + and unfold is fair; you made me realize why I thought you didn't need the two unfolding steps for nat, which was wrong, but that led to the question about refl.

[Reid Barton]

If you don't mind, whenever you say refl, I'll pretend you said exact rfl, since that cuts out an irrelevant step (deciding which kind of reflexivity to use).

[Keefer Rowan]

I think I'm getting the general picture now. My final question about this topic is how you would prove the (trivial) theorem above:

theorem not_mem_mem_compl {α : Type u} (x : α) (S : set α)  (h : ¬ (x ∈ S)) : x ∈ (- S)

[Reid Barton]

exact is a tactic that uses the term you give it to close the goal. The term only has to match the goal up to definitional equality, which means up to unfolding anything that needs unfolding.

[Keefer Rowan]

Noting that

def compl (s : set α) : set α :=
{a | a ∉ s}

[Reid Barton]

Well, one way is just := h

[Reid Barton]

or := by exact h--this takes advantage of definitional equality

[Keefer Rowan]

Ok, because everything holds definitionally, exact can figure it out.

[Reid Barton]

alternatively, there is probably already a lemma which says precisely this

[Reid Barton]

Probably named something like mem_compl or mem_compl_iff

[Reid Barton]

Using that is better practice in principle, since it insulates you from the specific definition of compl

[Keefer Rowan]

Yeah, I just wanted an example. Thanks for your help! I think (most of) my confusion has been resolved. And your last comment makes sense.

[Kevin Buzzard]

In the natural number game, zero_add is a theorem which is proved by induction, but add_zero can be proved by refl. Definitional equality is not mathematical, in some sense; it depends on exactly how an object is defined, rather than the way a mathematician thinks about it (where there might be several different definitions of one thing, all equivalent).