replace goal with definition

Stream: general

[Leonard Wiechmann]

This is something I run into again and again:
Given a goal of some "non-trivial" form (eg: A <= B for A B : set α),
how do I make lean tell me what the goal means?

as in: how to replace the goal with its definition without knowing what the definition is?
I've tried all kinds of rws/applys, but can't seem to figure out what <= is supposed to mean. Lean surely knows. How do I make it tell me? The very useful go to definition feature only shows me the definition of class has_le, not the instance.

[Yaël Dillies]

You can inspect in the goal in the infoview what has_le instance it is.

[Johan Commelin]

@Leonard Wiechmann In the case of notation, this can be a bit tricky. But if you have foo x y z, then you can do unfold foo to unfold the definition.

[Johan Commelin]

With notation, you can use widgets in the infoview, like Yaël says, if you are using VSCode.

[Johan Commelin]

Just click on the ≤ and drill down the popup windows. The popup windows also have buttons that allow you to "go to definition".

[Leonard Wiechmann]

I'm not quite sure what it's trying to tell me :thinking:
image.png

[Yaël Dillies]

Click on preorder.to_has_le. That's the next step.

[Leonard Wiechmann]

oh boy
image.png

[Leonard Wiechmann]

unfold got rid of the notation, but I still don't have a "useful" goal:
image.png

[Johan Commelin]

That was a wrong turn :wink: In the second box, click on the third subitem

[Johan Commelin]

Leonard Wiechmann said:

I've tried all kinds of intros/rws/applys, but can't seem to figure out what <= is supposed to mean.

Did you try intros x hx?

[Leonard Wiechmann]

yep. I can only introduce one thing. (A : set \a)

[Alex J. Best]

You can also do this with simp

example {T R : set ℕ} : T ≤ R :=
begin
  simp [(≤)],
  simp [(⊆)],
  simp [set.subset],
end

[Reid Barton]

The <= is whatever partial instance your function takes!

[Reid Barton]

You should just delete that

[Leonard Wiechmann]

Alex J. Best said:

You can also do this with simp

that's very useful, thanks!

[Leonard Wiechmann]

Reid Barton said:

The <= is whatever partial instance your function takes!

I had a feeling, that was the issue.
But without it, I'm having trouble getting is_smallest to choose the right partial order.
image.png

[Reid Barton]

that's because Lean has no idea what you mean

[Leonard Wiechmann]

yeah, I'm just giving it a function. It can't really know what I mean. So I have to tell it somehow.

[Reid Barton]

You should help it by giving a type annotation (and help us by copying and pasting text not screenshots)

[Leonard Wiechmann]

sorry, I wanted to include the error messages

def is_smallest {α : Type} [partial_order α] (a : α): Prop :=
  ∀ x, a <= x

lemma powerset_empty_smallest {α : Type}
  : is_smallest (λ x, false) := sorry

[Reid Barton]

The normal way to write the argument of is_smallest is (∅ : set α)

[Leonard Wiechmann]

Reid Barton said:

The normal way to write the argument of is_smallest is (∅ : set α)

oooooh, that's what emptyc is for!
ok, is_smallest (∅ : set α) isn't giving me an error so far.
let's see if I can make the proof work.
thanks!

[Leonard Wiechmann]

ok, got it working! all of that notation is nice to look at, but really obfuscates what the hypotheses and the goal actually mean.
thanks everyone!

[Kevin Buzzard]

The reason that using "canonical" notation is important, is that this is what all the simp lemmas are designed to use, and simp works up to syntactic equality so it matters.

[Mario Carneiro]

Leonard Wiechmann said:

sorry, I wanted to include the error messages

The usual way I include error messages in code snippets is to put them in comments immediately after the failing command