Zulip Chat Archive

Stream: new members

Topic: basics


view this post on Zulip Iocta (Dec 26 2019 at 05:19):

Why does this fail, and how to fix it?

def show_p : (p  q)  (p  r)  p :=
  (assume h: (p  q)  (p  r),
  show p,
  from or.elim h
  and.left
  and.left
)

def show_q_or_r : (p  q)  (p  r)  q  r :=
(assume h: (p  q)  (p  r),
  show q  r,
  from or.elim h
  (λ z, or.inl  (and.right z))
  (λ z, or.inr (and.right z))
)

example : (p  q)  (p  r)  p  (q  r) :=
(assume h: (p  q)  (p  r) ,
show p  (q  r),
from and.intro ((show_p h )  (show_q_or_r h))
)

view this post on Zulip Kenny Lau (Dec 26 2019 at 06:31):

the last line should be:

from and.intro (show_p h) (show_q_or_r h)

view this post on Zulip Kenny Lau (Dec 26 2019 at 06:31):

and.intro :  {a b : Prop}, a  b  a  b

view this post on Zulip Kenny Lau (Dec 26 2019 at 06:32):

and.intro is a function that takes a proof of a and a proof of b and gives a proof of a ∧ b

view this post on Zulip Kenny Lau (Dec 26 2019 at 06:32):

show_p h is the first input

view this post on Zulip Kenny Lau (Dec 26 2019 at 06:32):

show_q_or_r h is the second input

view this post on Zulip Iocta (Dec 26 2019 at 07:57):

Thanks

view this post on Zulip Iocta (Dec 26 2019 at 19:59):

Hm it's not quite that? Doesn't compile.

def show_p : (p  q)  (p  r)  p :=
  (assume h: (p  q)  (p  r),
  show p,
  from or.elim h
  and.left
  and.left
)

def show_q_or_r : (p  q)  (p  r)  q  r :=
(assume h: (p  q)  (p  r),
  show q  r,
  from or.elim h
  (λ z, or.inl  (and.right z))
  (λ z, or.inr (and.right z))
)

example : (p  q)  (p  r)  p  (q  r) :=
(assume h: (p  q)  (p  r) ,
show p  (q  r),
from and.intro (show_p h )  (show_q_or_r h)
)

view this post on Zulip Patrick Massot (Dec 26 2019 at 20:01):

How do you declare your variables p, q and r?

view this post on Zulip Patrick Massot (Dec 26 2019 at 20:01):

You seem to use them implicitly, hence they should appear between curly brackets.

view this post on Zulip Iocta (Dec 26 2019 at 20:03):

I have variables p q r : Prop at the top of the page.

view this post on Zulip Patrick Massot (Dec 26 2019 at 20:04):

This defaults to regular parentheses, hence explicit arguments.

view this post on Zulip Patrick Massot (Dec 26 2019 at 20:04):

Switch to variables {p q r : Prop}.

view this post on Zulip Iocta (Dec 26 2019 at 20:11):

That works. How should my code be if I wanted to keep the variables p q r : Prop?

view this post on Zulip Bryan Gin-ge Chen (Dec 26 2019 at 20:15):

You have to provide all explicit parameters to the function show_p, so your last example should look like this:

example : (p  q)  (p  r)  p  (q  r) :=
(assume h: (p  q)  (p  r) ,
show p  (q  r),
from and.intro (show_p p q r h )  (show_q_or_r p q r h)
)

view this post on Zulip Iocta (Dec 26 2019 at 20:16):

Oh I see. Thank you all.

view this post on Zulip Patrick Massot (Dec 26 2019 at 20:16):

That kind of verbosity is precisely what implicit arguments are meant to deal with.

view this post on Zulip Patrick Massot (Dec 26 2019 at 20:17):

(of course you're free to use them or not, I only want to make sure you understand the point).

view this post on Zulip Iocta (Dec 26 2019 at 20:18):

Yep, got it.

view this post on Zulip Iocta (Jan 07 2020 at 22:09):

Is there a built-in function \lambda h, h?

view this post on Zulip Aria Miuk (Jan 07 2020 at 22:10):

That should be id.

view this post on Zulip Iocta (Jan 07 2020 at 22:11):

Thanks

view this post on Zulip Iocta (Jan 07 2020 at 22:14):

Is it possible to do this without classical? example : ¬(p ↔ ¬p) := sorry

view this post on Zulip Simon Hudon (Jan 07 2020 at 22:19):

Yes. Do you want to prove it yourself?

view this post on Zulip Aria Miuk (Jan 07 2020 at 22:20):

Yes it is provable. Think about how to get p into context and the definition of not.

view this post on Zulip Iocta (Jan 07 2020 at 22:36):

No luck. How do I get p into context?

view this post on Zulip Bryan Gin-ge Chen (Jan 07 2020 at 22:37):

Have you been able to get ¬p into the goal? Remember that this is actually p → false.

view this post on Zulip Aria Miuk (Jan 07 2020 at 22:46):

Strat with intros contra (or \lambda contra, _) and see how one magically conjures hypotheses :).

view this post on Zulip Iocta (Jan 07 2020 at 23:04):

I'm missing something. I can't find anything shaped like p or p \to false.

view this post on Zulip Aria Miuk (Jan 07 2020 at 23:06):

You're on the right path. You're looking for something p \to false. Can you prove it?

view this post on Zulip Iocta (Jan 07 2020 at 23:37):

No I'm back where I started :-)

view this post on Zulip Aria Miuk (Jan 07 2020 at 23:38):

Look at your contradictory hypothesis, (p ↔ ¬p). You "win" once you either know p, or not p. Agreed? (As this then leads to contradiction.)

view this post on Zulip Aria Miuk (Jan 07 2020 at 23:40):

So then surely the only way to prove this is to either know p or not p. There is bound to be no other way.

view this post on Zulip Aria Miuk (Jan 07 2020 at 23:41):

So choose one, whichever you prefer. And formulate: have h : p, { ... }. (Or the other one.)

view this post on Zulip Aria Miuk (Jan 07 2020 at 23:42):

Can you prove either of these? What happens if you attempt?

view this post on Zulip Iocta (Jan 08 2020 at 00:31):

I want to do something like or.elim hp, but I can't figure out how to make hp.

example : ¬(p  ¬p) :=
λ c,
have hp: p, from _,
show false, from _

view this post on Zulip Iocta (Jan 08 2020 at 00:35):

If hp then hnp, and absurd hp hnp. And vice versa. But how do I state either of those hypotheses?

view this post on Zulip Aria Miuk (Jan 08 2020 at 00:37):

So you need to prove p. Surely your only hypothesis is c. Let's use it. c.2 gives us not p -> p, we apply it to get the conclusion not p. So far so good?

view this post on Zulip Bryan Gin-ge Chen (Jan 08 2020 at 00:38):

Here's another transcript of my thoughts as I work through the start of this one "automatically" (in the style of this previous post).

We start out with a single underscore and let Lean tell us what's missing:

-- (1)
example (p : Prop) : ¬(p  ¬p) :=
_
/- p : Prop
⊢ ¬(p ↔ ¬p) -/

Here and below, I'll just quote the part of the error message(s) that shows the hypotheses in the context and the goal. Since ¬(p ↔ ¬p) is the same as (p ↔ ¬p) → false, which is a function type, we should be able to make progress by introducing a lambda:

-- (2a)
example (p : Prop) : ¬(p  ¬p) :=
λ h, _
/- p : Prop,
h : p ↔ ¬p
⊢ false -/

Note that p ↔ ¬p is the same as (p → ¬p) ∧ (¬p → p) so we could proceed by using h.1 and h.2. However, I'll redo this step by making use of Lean's pattern-matching syntax to split h into two hypotheses:

-- (2b)
example (p : Prop) : ¬(p  ¬p) :=
λ h1, h2, _
/- p : Prop,
_x : p ↔ ¬p,
_fun_match : (p ↔ ¬p) → false,
h1 : p → ¬p,
h2 : ¬p → p
⊢ false -/

Aside from h1 and h2 there's some other junk in the context related to the pattern-matching; I won't show it again below. Now, how do we make progress towards the goal of false? Now we realize that h1 : p → ¬p is short for h1 : p → p → false. Since passing two parameters to h1 will yield false, we should try replacing the underscore with h1 _ _:

-- (3)
example (p : Prop) : ¬(p  ¬p) :=
λ h1, h2, h1 _ _
/- h1 : p → ¬p,
h2 : ¬p → p
⊢ p -/
/- h1 : p → ¬p,
h2 : ¬p → p
⊢ p -/

There are now two error messages because there are two underscores. Since I'm only intending to show a few more steps, from here on out I'm only going to show the error message corresponding to the first underscore. How do we make progress towards p there? Well, note that h2 : ¬p → p is a function which takes one parameter and returns p, so let's replace the underscore with h2 _:

-- (4)
example (p : Prop) : ¬(p  ¬p) :=
λ h1, h2, h1 (h2 _) _
/- h1 : p → ¬p,
h2 : ¬p → p
⊢ ¬p -/

Hey, here's the goal of ¬p we hinted at! Now what? Well, naïvely, we might apply h1 again, since it ends in ¬p. However, if you try this, you'll see that continuing this way won't work (try it, what happens?). What should we do instead? Well, if we instead observe that ¬p is the same as p → false, we can alternatively introduce another lambda here:

-- (5)
example (p : Prop) : ¬(p  ¬p) :=
λ h1, h2, h1 (h2 (λ h3, _)) _
/- h1 : p → ¬p,
h2 : ¬p → p,
h3 : p
⊢ false -/

Now we have p in the context, as desired! I'll leave the rest to you, but one final hint. Our goal is false again. Last time we saw this (step (3)), we replaced the underscore with h1 _ _. You should try doing this again. You'll end up in a state with 3 underscores / errors, but there's now something in the context which will let you close two of them right away...

You can fill in the last underscore very similarly.

When you get to the end, you'll notice that in blindly "chasing underscores" we end up with quite a bit of duplication. We could have avoided this by naming some terms with have statements, and it's worth refactoring the proof along those lines. Then you might start again from scratch and try to write a version of the proof with the have statements from the beginning.

view this post on Zulip Iocta (Jan 08 2020 at 00:52):

I'll meditate on this. Thanks.

view this post on Zulip Iocta (Jan 08 2020 at 01:51):

The basic version looks like

example (p : Prop) : ¬(p  ¬p) :=
λ (|h1, h2|),
(h1
  (h2 (λ hp, absurd hp (h1 hp)))
  (h2 (λ hp, absurd hp (h1 hp)))
)

Is this less redundant, or is it the same thing?

example (p : Prop) : ¬(p  ¬p) :=
λ (|h1, h2|),
have hnp : ¬p, from (λ hp', absurd hp' (h1 hp')),
have hp: p, from (h2 hnp),
show false, from (absurd hp hnp)

view this post on Zulip Bryan Gin-ge Chen (Jan 08 2020 at 02:27):

Well, absurd itself is short for a certain proof term... do you know how absurd is proved?

view this post on Zulip Kenny Lau (Jan 08 2020 at 02:40):

@Iocta maybe try this more general theorem:

theorem Curry's_paradox (p q : Prop) : (p  (p  q))  q :=
_

view this post on Zulip Iocta (Jan 08 2020 at 03:17):

example (p : Prop) : ¬(p  ¬p) :=
λ (|h1, h2|),
have hnp : ¬p, from (λ hp', (h1 hp')  hp'),
have hp: p, from (h2 hnp),
show false, from hnp hp

view this post on Zulip Iocta (Jan 08 2020 at 03:27):

theorem Curry's_paradox (p q : Prop) : (p  (p  q))  q :=
λ (|h1, h2|),
have hp : p, from (h2 (λ hp', h1 hp' hp')),
show q, from (h1 hp hp)

view this post on Zulip Kevin Buzzard (Jan 08 2020 at 04:17):

import tactic

theorem Curry's_paradox (p q : Prop) : (p  (p  q))  q := by tauto!

view this post on Zulip Iocta (Jan 08 2020 at 08:00):

Why's this wrong? How to fix it?

open classical

lemma unnotnot : ¬¬p  p :=
λ hnnp, or.elim (em p) id (λ hnp, false.elim (absurd hnp hnnp))


example : ¬(p  q)  ¬p  ¬q :=
λ h, or.elim (em p)
(λ hp,
have hnq : ¬q, from (by_contradiction (λ hnnq, h (and.intro hp (unnotnot hnnq)))),
  show _, from or.inr
)
or.inl

view this post on Zulip Kenny Lau (Jan 08 2020 at 08:02):

or.inr should be or.inr hnq:

open classical

variables {p q : Prop}

lemma unnotnot : ¬¬p  p :=
λ hnnp, or.elim (em p) id (λ hnp, false.elim (absurd hnp hnnp))


example : ¬(p  q)  ¬p  ¬q :=
λ h, or.elim (em p)
(λ hp,
have hnq : ¬q, from (by_contradiction (λ hnnq, h (and.intro hp (unnotnot hnnq)))),
  show _, from or.inr hnq
)
or.inl

view this post on Zulip Kenny Lau (Jan 08 2020 at 08:03):

the type of or.inr is unified with ¬q → ¬p ∨ ¬q

view this post on Zulip Iocta (Jan 08 2020 at 08:10):

Thanks

view this post on Zulip Iocta (Jan 08 2020 at 08:15):

Is it possible to prove unnotnot without classical?

view this post on Zulip Kenny Lau (Jan 08 2020 at 08:24):

no

view this post on Zulip Kenny Lau (Jan 08 2020 at 08:24):

it's equivalent to em

view this post on Zulip Iocta (Jan 09 2020 at 09:07):

When I have \not p in context and p in goal, is there something I should be saying to myself?

view this post on Zulip Kenny Lau (Jan 09 2020 at 09:10):

if you can prove the goal, then you can prove false; so maybe aim to prove false instead

view this post on Zulip Iocta (Jan 09 2020 at 09:10):

Alright

view this post on Zulip Iocta (Jan 12 2020 at 19:54):

Can I fill this underscore, or am I down the wrong path?

example : ¬(p  q)  p  ¬q :=
λ h,
have notq : ¬q, from (λ hq', (h (λ hp, hq'))),
and.intro
(or.elim (em p) id (λ hnp, _))
notq

view this post on Zulip Chris Hughes (Jan 12 2020 at 19:56):

You can fill in the underscore

view this post on Zulip Iocta (Jan 12 2020 at 19:58):

ok

view this post on Zulip Iocta (Jan 12 2020 at 19:58):

Is it possible to get into situations where I wouldn't be able to fill in the underscore, but where the overall claim is true?

view this post on Zulip Kenny Lau (Jan 12 2020 at 19:59):

example : true :=
false.elim _

view this post on Zulip Bryan Gin-ge Chen (Jan 12 2020 at 20:00):

There was another example at the very end of this reply to one of your questions (step 2R).

view this post on Zulip Iocta (Jan 12 2020 at 20:03):

how do I find conversations I've been involved in on zulip?

view this post on Zulip Kevin Buzzard (Jan 12 2020 at 20:05):

search for yourself using the search bar at the top.

view this post on Zulip Iocta (Jan 12 2020 at 20:06):

ah I see

view this post on Zulip Iocta (Jan 13 2020 at 01:06):

This example works but it's quite long. Did I miss some opportunity to simplify?

variables p q : Prop

theorem contrap : (p  q)  (¬q  ¬p) :=
λ h hnq hp, hnq (h hp)


open classical

lemma unnotnot : ¬¬p  p :=
λ hnnp, or.elim (em p) id (λ hnp, false.elim (absurd hnp hnnp))

lemma notnot : p  ¬¬p :=
λ hp hnp, hnp hp

theorem ncontrap : ( ¬p  ¬q)  (q  p) :=
λ np2nq hq,
or.elim (em p)
id
(λ hnp,  (absurd (np2nq hnp)   (notnot _ hq)))


lemma contrapositive_not : ¬(p  q)  ¬(¬q  ¬p) :=
λh h',
or.elim (em q)
(λ hq,
  have nnp2nnq : _, from (contrap _ _ h'),
  have p2q : p  q, from
  (λ hp,
    have hq: _,
    from unnotnot _ (nnp2nnq (notnot _ hp)), hq),
  absurd p2q h)
(λ hnq,
  have hnp: ¬p, from h' hnq,
  have p2q: p  q, from ncontrap _ _ h',
  have false' : _, from h p2q,
  false')


example : ¬(p  q)  p  ¬q :=
λ h,
have hnq : ¬q, from (λ hq', (h (λ hp, hq'))),
and.intro
(or.elim (em p) id (λ hnp,
have h' : _, from contrapositive_not _ _ h,
(false.elim (h' (λ hnq', hnp)))))
hnq

view this post on Zulip Reid Barton (Jan 13 2020 at 01:27):

This looks a lot more complicated than necessary. In particular, you shouldn't need to use em again to fill in the underscore.
In the context of the underscore, you know not p and also not (p -> q). But not p is p -> false, and from false you can prove q, so you get p -> q, which contradicts not (p -> q).

view this post on Zulip Iocta (Jan 13 2020 at 04:17):

Thanks.

view this post on Zulip Kevin Buzzard (Jan 13 2020 at 07:23):

Of course you can also prove all of these basic logic statements with one line using tactics, and most if not all of them will already be proved in lean or mathlib already. If you're interested in seeing very short proofs you can read the proofs in the library

view this post on Zulip Iocta (Jan 14 2020 at 06:11):

I'm still working through the tutorial, haven't got to tactics yet.

view this post on Zulip Iocta (Jan 18 2020 at 05:48):

I'm confused about the forall syntax. How do you fill this? def prime (n : ℕ) : Prop := sorry

view this post on Zulip Iocta (Jan 18 2020 at 05:57):

def nondivisible (n : ) : Prop :=
  forall m : , (and.intro (m > 1) (m < n) )  not (divides m n)

nope

view this post on Zulip Kenny Lau (Jan 18 2020 at 06:05):

and.intro (hp : p) (hq : q) is a proof of p and q

view this post on Zulip Iocta (Jan 18 2020 at 06:09):

How do I take an m : \N such that 1 < m < nas an argument?

view this post on Zulip Iocta (Jan 18 2020 at 06:11):

I guess I could say or.elim (em 1 < m) but that seems roundabout

view this post on Zulip Mario Carneiro (Jan 18 2020 at 06:22):

You just write

  forall m : , 1 < m < n  not (divides m n)

view this post on Zulip Mario Carneiro (Jan 18 2020 at 06:23):

except that doesn't actually work, but this does:

  forall m : , (and (m > 1) (m < n) )  not (divides m n)

view this post on Zulip Mario Carneiro (Jan 18 2020 at 06:23):

or

  forall m : , m > 1  m < n  not (divides m n)

view this post on Zulip Iocta (Jan 18 2020 at 06:46):

Oh, easy. Thanks.

view this post on Zulip Iocta (Jan 18 2020 at 07:44):

def prime (n : ) : Prop :=
forall m : , and (m > 1) (m < n)  not (divides m n)

variable m: 

example : Prop :=
forall n : , (n > 2)   k : ,  (and (eq (k + m) n) (and (prime k) (prime m)))

What's the quantifier on m?

view this post on Zulip Iocta (Jan 18 2020 at 07:44):

compared to forall n : ℕ, (n > 2) → ∃ k : ℕ, ∃m : ℕ, (and (eq (k + m) n) (and (prime k) (prime m)))

view this post on Zulip Iocta (Jan 18 2020 at 07:45):

(m in the example)

view this post on Zulip Iocta (Jan 18 2020 at 07:49):

Oh I see, we're taking it as an argument.

view this post on Zulip Iocta (Jan 18 2020 at 07:49):

Why doesn't it complain that it doesn't match Prop then?

view this post on Zulip Mario Carneiro (Jan 18 2020 at 07:53):

When you refer to a variable, it automatically adds the variable binder to the definition, as if you had written

example (m : ) : Prop :=
forall n : , (n > 2)   k : ,  (and (eq (k + m) n) (and (prime k) (prime m)))

view this post on Zulip Iocta (Jan 18 2020 at 08:01):

Aha

view this post on Zulip Iocta (Jan 18 2020 at 08:11):

Given

def divides (m n : ) : Prop :=  k, m * k = n

How do I check whether divides 3 6?

view this post on Zulip Iocta (Jan 18 2020 at 08:12):

#check/#eval/#print don't seem to do it

view this post on Zulip Mario Carneiro (Jan 18 2020 at 08:14):

You need to prove the predicate is decidable first, which amounts to giving a decision procedure. In most programming languages, for example, you decide m | n by testing if m % n = 0

view this post on Zulip Mario Carneiro (Jan 18 2020 at 08:14):

Luckily, we've already gone to the trouble to do this, but you have to use the built-in divides relation to get this

view this post on Zulip Alex J. Best (Jan 18 2020 at 08:16):

Once you have a decidable proposition #eval to_bool (divides 3 6) will display either tt or ff

view this post on Zulip Mario Carneiro (Jan 18 2020 at 08:16):

Note that by the syntactic form of the expression (an exists over natural numbers of a basic proposition) it is not obviously decidable. For example Goldbach's conjecture can also be written in this form but it's an open question if this is a decidable proposition

view this post on Zulip Kevin Buzzard (Jan 18 2020 at 10:06):

With inbuilt divides, it just works: #eval to_bool (3 ∣ 6) -- tt. Note that this is \| not |.

view this post on Zulip Kevin Buzzard (Jan 18 2020 at 10:08):

example (a b : ℕ) : decidable (a ∣ b) := by apply_instance -- already inbuilt

view this post on Zulip Kevin Buzzard (Jan 18 2020 at 10:12):

def prime (n : ) : Prop :=
forall m : , and (m > 1) (m < n)  not (divides m n)

There is notation which makes this more readable for mathematicians, right?

def prime (n : ) : Prop :=
 m : , m > 1  m < n  ¬ (divides m n)

But Mario's suggestion of currying it and writing m > 1 → m < n → ¬ (divides m n) is better for functional languages because it's easier to work with; typically m>1 comes from one proof and m<n comes from another, and if you curry it then you don't need to apply the and.intro

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 00:49):

sorry if this is out of place (new to lean and to the community :happy:) but i've been searching all over the docs and can't find an answer. i'm trying to rewrite with rw mem_empty_eq, and receiving the following error:

rewrite tactic failed, did not find instance of the pattern in the target expression
  ?m_2 ∈ ∅
state:
α : Type,
A : set α
⊢ {a : α | a ∈ A ∧ a ∈ ∅} = ∅

view this post on Zulip Kevin Buzzard (Jan 19 2020 at 00:50):

ouch

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 00:50):

i would think that a ∈ ∅ is sufficient to rewrite?

view this post on Zulip Kevin Buzzard (Jan 19 2020 at 00:50):

It's hidden too deep in the term.

view this post on Zulip Kevin Buzzard (Jan 19 2020 at 00:50):

try ext first

view this post on Zulip Kevin Buzzard (Jan 19 2020 at 00:50):

You can't rewrite under a lambda.

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 00:51):

ah! that makes sense. is that just to protect against accidentally rewriting already-bound terms?

view this post on Zulip Kevin Buzzard (Jan 19 2020 at 00:51):

Alternatively you could try simp only [mem_empty_eq]

view this post on Zulip Kevin Buzzard (Jan 19 2020 at 00:51):

I have no idea why it makes sense, I am a mathematician. I just know the workarounds.

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 00:52):

I am a mathematician

Hahaha, well thank you all the same :happy:

view this post on Zulip Kevin Buzzard (Jan 19 2020 at 00:52):

mem_empty_eq is definitionally true, so you could just write show {a : α | a ∈ A ∧ false} = ∅

view this post on Zulip Kevin Buzzard (Jan 19 2020 at 00:54):

but then you probably won't be able to rewrite and_false on the next line, you'll perhaps have to do ext in the end if you want to prove this by hand. Did you try simp?

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 00:54):

yeah, simp goes through the entire proof for me. i'm trying to get a better handle on lean by doing some introductory exercises on an undergrad abstract algebra textbook i found

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 00:55):

i got it to work with simp only [...] for both the mem_empty_eq and and_false steps. i'm going to try with ext to get more experience with that too

view this post on Zulip Kevin Buzzard (Jan 19 2020 at 00:56):

After ext the rewrites do work.

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 00:58):

yep, although only on the rhs of the iff, i can show that forall a. a \not \in ... with a iff_false, and then i can map that to the set being \emptyset maybe?

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 00:58):

thank you for your help :)

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 01:10):

after many hours of syntax errors, i'm proud to say i've shown... A ∩ ∅ = ∅ :face_palm:

lemma intersection_empty (α : Type) (A : set α) :
        A ∩ ∅ = ∅ :=
        begin
            rw inter_def,
            ext a,
            rw mem_set_of_eq,
            repeat {rw mem_empty_eq},
            rw and_false,
        end

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 01:10):

thanks again Kevin!

view this post on Zulip Daniel Keys (Jan 19 2020 at 01:30):

@Cerek Hillen (he) (W2'20) Hey Cerek, that doesn't work for me, do you need to include or open some stuff?

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 01:31):

yeah! i have the following at the top of my .lean file:

import data.set.basic
import data.nat.basic
import logic.basic

open set
open nat

view this post on Zulip Iocta (Jan 19 2020 at 01:44):

example : (x :α, p x)  α :=
λ h, exists.elim h, _

How to write this?

view this post on Zulip Bryan Gin-ge Chen (Jan 19 2020 at 02:07):

@Iocta The answer depends on the type of α:

import logic.basic

variables (α : Prop)

example (p : α  Prop) : (x :α, p x)  α :=
λ h, exists.elim h (λ x h', x)

variables (β : Type*)

noncomputable example (p : β  Prop) : (x :β, p x)  β :=
λ h, exists.classical_rec_on h (λ x h', x)

view this post on Zulip Bryan Gin-ge Chen (Jan 19 2020 at 02:10):

@Cerek Hillen (he) (W2'20) Maybe you already know this, but just to be sure, your intersection_empty is also known as set.inter_empty in mathlib. You can find this out if you import tactic and then use library_search:

lemma intersection_empty (α : Type) (A : set α) :
        A   =  := by library_search

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 02:37):

Cerek Hillen (he) (W2'20) Maybe you already know this, but just to be sure, your intersection_empty is also known as set.inter_empty in mathlib. You can find this out if you import tactic and then use library_search:

lemma intersection_empty (α : Type) (A : set α) :
        A   =  := by library_search

I was aware, but thank you! I'm looking to get a better handle on Lean by going through proofs manually

view this post on Zulip Patrick Massot (Jan 19 2020 at 08:06):

@Cerek Hillen (he) (W2'20) your proof works but it breaks many abstraction barriers. You know too much about how sets are implemented, and know too many lemmas about them. Maybe try:

example (α : Type) (A : set α) : A   =  :=
begin
  ext a,
  split,
  { rintro ha, ha',
    assumption },
  { intro h,
    exfalso,
    assumption },
end

view this post on Zulip Patrick Massot (Jan 19 2020 at 08:08):

Another useful exercise from the opposite of the style spectrum is to understand the following proof term:

example (α : Type) (A : set α) : A   =  :=
set.ext $ λ a, ⟨λ h, h', h', λ h, false.elim h

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 19:02):

I'm just recently learning about the axiomatic description of set theory, so bear with me. When you say I know too much about how sets are implemented / too many lemmas about them, do just mean that it's generally better to provide proofs that don't rely on operators' definitions & facts about them?

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 19:03):

Or just that in this situation, since it's a base-level proof about the union identity, that it's better to prove it without knowledge of constructions and proofs that one would prove with the result itself?

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 19:06):

Also another introductory question, say I have the following 2 hypotheses:

h : ∀ (x : α), x ∈ A → x ∈ B,
a : α

Intuitively I should be able to construct a hypothesis that states a ∈ A → a ∈ B, but how would I actually do that?

view this post on Zulip Bryan Gin-ge Chen (Jan 19 2020 at 19:08):

h a has type a ∈ A → a ∈ B.

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 19:09):

oh! i didn't realize that \forall operators actually presented themselves as functions, or function-adjacent thing

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 19:09):

i get the sense that i'm using the word wrong so far as lean is concerned

view this post on Zulip Bryan Gin-ge Chen (Jan 19 2020 at 19:18):

Well, the way I would phrase it (which might be a little off still...) is that the forall "creates" a dependent function type, thus something whose type is a forall (like h) is a function. (The section of TPiL I linked talks about "Pi" types, see this section for why forall and Pi are the same).

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 19:37):

Ah ok, that makes sense--it's like in a type theoretic mathematical system where you'd say a thing is true iff there exists a function of the type A -> true (or A -> 1 i guess technically)

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 19:38):

but since forall describes a property of some thing, it's just equivalent to some A -> Prop, except you have to provide some a : A

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 19:38):

my only knowledge of type theory is the introductory section of Homotopy Type Theory so some of my intuitions might be off

view this post on Zulip Kevin Buzzard (Jan 19 2020 at 19:50):

You should probably read the first few sections of theorem proving in Lean, I think you'll find it very enlightening

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 19 2020 at 19:56):

On it :slight_smile:

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 23 2020 at 14:29):

Thanks for pointing me towards Theorem Proving in Lean, Kevin. I'm finding it a big help. NN game focuses a lot on rewrite rules so Chapt 3 has been really good about getting a sense for constructive proofs

view this post on Zulip Cerek Hillen (he) (W2'20) (Jan 23 2020 at 14:30):

(at least the early parts of NN Game)


Last updated: May 17 2021 at 22:15 UTC