unfold `<`

Stream: new members

[Chris M]

I have a goal

1 goal
T : Type u_1,
P : T → Prop,
h : FinT T,
h : Π (t : T), decidable (P t),
assum : 0 < sumpred P (count T)
⊢ ∃ (t : T), P t

in the context:

lemma qimpE (T:Type*) (P:T → Prop) [h:FinT T] [h:∀t, decidable (P t)]: nat.zero < (sumpred P (count T))  → ∃t:T, P t :=
begin
    intros assum,

end
```
I want to expand the definition of the `<` inside `assum`. `dunfold < at assum` doesn't work, I presume because `<` is notation, not a defined term. What is the best way to go about this?

[Kenny Lau]

don't unfold!

[Kenny Lau]

what's your maths proof, and does it involve unfolding <?

[Chris M]

Well, tbh, my mental definition of a<b is \exists c, a+c=b \and c\neq 0, so that was what I was going for. I have since found out that that is not how it's defined in lean. Under that assumption yes it did involve unfolding <.

[Chris M]

Kenny Lau said:

don't unfold!

Why do you say this?

[Kenny Lau]

Because the word "definition" in maths is not the same as in Lean

[Kenny Lau]

"definition" in Lean should be better translated as "implementation" in maths, since there can only be one definition in Lean, but in maths one thing can have a lot of definitions

[Kenny Lau]

"definition" in maths would be "definitional lemmas" in Lean, and I can assure you that one exists for this definition you proposed

[Kenny Lau]

docs#exists_pos_add_of_lt

[Kenny Lau]

so for example in Lean I might define three to be 3, and then prove that 2 + 1 is an equivalent definition, i.e. prove a lemma saying that three = 2 + 1

[Kenny Lau]

I will even prove that three = 3 as a separate lemma just to discourage people from ever unfolding three

[Kenny Lau]

docs#def (this link doesn't work: how do I find all the lemmas containing def?)

[Chris M]

I see. Thanks :)

By the way I had trouble figuring out how to use exists_pos_add_of_lt. It gives me an error unknown identifier 'exists_pos_add_of_lt'. Clearly I should first open some namespace but I'm not sure how to figure out which one.

[Mario Carneiro]

I usually type exists_pos_add_of_lt and find the one I want in the ctrl-space dropdown

[Mario Carneiro]

I would guess it is nat.exists_pos_add_of_lt

[Kevin Buzzard]

#check exists_pos_add_of_lt ctrl-space says it's in the root namespace (I have import tactic at the top of my file though)