Zulip Chat Archive

Stream: new members

Topic: unfold `<`


view this post on Zulip Chris M (Nov 03 2020 at 16:18):

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?

view this post on Zulip Kenny Lau (Nov 03 2020 at 16:19):

don't unfold!

view this post on Zulip Kenny Lau (Nov 03 2020 at 16:20):

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

view this post on Zulip Chris M (Nov 03 2020 at 16:24):

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

view this post on Zulip Chris M (Nov 03 2020 at 16:24):

Kenny Lau said:

don't unfold!

Why do you say this?

view this post on Zulip Kenny Lau (Nov 03 2020 at 16:25):

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

view this post on Zulip Kenny Lau (Nov 03 2020 at 16:25):

"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

view this post on Zulip Kenny Lau (Nov 03 2020 at 16:26):

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

view this post on Zulip Kenny Lau (Nov 03 2020 at 16:27):

docs#exists_pos_add_of_lt

view this post on Zulip Kenny Lau (Nov 03 2020 at 16:28):

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

view this post on Zulip Kenny Lau (Nov 03 2020 at 16:28):

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

view this post on Zulip Kenny Lau (Nov 03 2020 at 16:30):

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

view this post on Zulip Chris M (Nov 03 2020 at 17:04):

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.

view this post on Zulip Mario Carneiro (Nov 03 2020 at 17:07):

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

view this post on Zulip Mario Carneiro (Nov 03 2020 at 17:07):

I would guess it is nat.exists_pos_add_of_lt

view this post on Zulip Kevin Buzzard (Nov 03 2020 at 18:15):

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


Last updated: May 10 2021 at 19:16 UTC