Zulip Chat Archive

Stream: new members

Topic: basic lean commands


view this post on Zulip Pedro Castilho (Nov 05 2020 at 03:17):

hi, am trying to get more familiar with ⟨⟩ operator, I know it can be used for "and.intro", but I can't get the reason of the x in ⟨x, h6, h5⟩ to show y ∈ f '' (A ∪ B), why isn't ⟨h6, h5⟩ enough?

have h4 : x  A, from h.left,
        have h5 : f x = y, from h.right,
        have h6 : x  A  B, from or.inl h4,
        show y  f '' (A  B), from x, h6, h5⟩)

view this post on Zulip Yury G. Kudryashov (Nov 05 2020 at 03:24):

y ∈ f '' (A ∪ B) unfolds to ∃ x, x ∈ A ∧ f x = y

view this post on Zulip Yury G. Kudryashov (Nov 05 2020 at 03:25):

So, ⟨x, h6, h5⟩ unfolds to something like Exists.intro x (and.intro h6 h5)

view this post on Zulip Pedro Castilho (Nov 05 2020 at 03:27):

ah, that makes sense, thx @Yury G. Kudryashov

view this post on Zulip Pedro Castilho (Nov 05 2020 at 03:29):

do you have any references to the ⟨⟩ syntax? it looks really nice in proofs and I wanted to get a better feel for it

view this post on Zulip Yury G. Kudryashov (Nov 05 2020 at 03:30):

If Lean knows the expected type of an expression and this type has exactly one constructor, then ⟨...⟩ applies this constructor.

view this post on Zulip Pedro Castilho (Nov 05 2020 at 03:31):

that's really cool thanks

view this post on Zulip Yury G. Kudryashov (Nov 05 2020 at 03:31):

And you can write ⟨a, ⟨b, c⟩⟩ as ⟨a, b, c⟩. Note that you can't write ⟨⟨a, b⟩, c⟩ as ⟨a, b, c⟩.

view this post on Zulip Bryan Gin-ge Chen (Nov 05 2020 at 03:34):

I linked to a few mentions of the angle bracket notation in #TPiL in this thread.

view this post on Zulip Pedro Castilho (Nov 05 2020 at 03:40):

oh, that's really helpful @Bryan Gin-ge Chen

view this post on Zulip Pedro Castilho (Nov 05 2020 at 03:42):

i have been in leans Zulip community for a couple of weeks and I have to say that its a really great one, you guys are super helpful

view this post on Zulip Pedro Castilho (Nov 05 2020 at 03:42):

thx again for all the help

view this post on Zulip Pedro Castilho (Nov 05 2020 at 03:44):

and I hope soon enough I can help other around here hehehe

view this post on Zulip Bryan Gin-ge Chen (Nov 05 2020 at 03:44):

Happy to have you around, Pedro!

view this post on Zulip Eduardo Vianna (Nov 06 2020 at 01:06):

I'm having doubts when prooving an example image.png
I used the "assume x" hoping to do a universal introduction (to prove ∀ (x : B), v1 x = v2 x and consequently v1 = v2), but it is not working and I can't figure why!
Here's the type mismatch notification lean gives me at this marked "show":
"type mismatch at application
(λ (this : ∀ (x : B), v1 x = v2 x), this) h
term
h
has type
v1 x = v2 x
but is expected to have type
∀ (x : B), v1 x = v2 x"

view this post on Zulip Mario Carneiro (Nov 06 2020 at 01:15):

#backticks

view this post on Zulip Bryan Gin-ge Chen (Nov 06 2020 at 01:15):

You'll need to use function extensionality, which is funext.

view this post on Zulip Mario Carneiro (Nov 06 2020 at 01:16):

brian is right, you need funext $ assume x, ... instead of assume x, ...

view this post on Zulip Bryan Gin-ge Chen (Nov 06 2020 at 01:19):

Here's a working proof:

open function

example (A B : Type) (u : A  B) (v1 : B  A) (v2 : B  A)
  (h1 : left_inverse v1 u) (h2 : right_inverse v2 u) : v1 = v2 :=
funext $ assume x,
  have h : v1 x = v2 x, from
  calc
    v1 x = v1 (u (v2 x)) : by rw h2
    ... = v2 x : by rw h1,
  show v1 x = v2 x, from h

By the way, it's much easier for us to help if you copy+paste a #mwe; screenshots are hard to work off of.


Last updated: May 16 2021 at 20:13 UTC