## Stream: new members

### Topic: basics

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


#### Kenny Lau (Dec 26 2019 at 06:31):

the last line should be:

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


#### Kenny Lau (Dec 26 2019 at 06:31):

and.intro : ∀ {a b : Prop}, a → b → a ∧ b


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

#### Kenny Lau (Dec 26 2019 at 06:32):

show_p h is the first input

#### Kenny Lau (Dec 26 2019 at 06:32):

show_q_or_r h is the second input

Thanks

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


#### Patrick Massot (Dec 26 2019 at 20:01):

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

#### Patrick Massot (Dec 26 2019 at 20:01):

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

#### Iocta (Dec 26 2019 at 20:03):

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

#### Patrick Massot (Dec 26 2019 at 20:04):

This defaults to regular parentheses, hence explicit arguments.

#### Patrick Massot (Dec 26 2019 at 20:04):

Switch to variables {p q r : Prop}.

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

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


#### Iocta (Dec 26 2019 at 20:16):

Oh I see. Thank you all.

#### Patrick Massot (Dec 26 2019 at 20:16):

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

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

Yep, got it.

#### Iocta (Jan 07 2020 at 22:09):

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

#### Aria Miuk (Jan 07 2020 at 22:10):

That should be id.

Thanks

#### Iocta (Jan 07 2020 at 22:14):

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

#### Simon Hudon (Jan 07 2020 at 22:19):

Yes. Do you want to prove it yourself?

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

#### Iocta (Jan 07 2020 at 22:36):

No luck. How do I get p into context?

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

#### Aria Miuk (Jan 07 2020 at 22:46):

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

#### Iocta (Jan 07 2020 at 23:04):

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

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

#### Iocta (Jan 07 2020 at 23:37):

No I'm back where I started :-)

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

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

#### Aria Miuk (Jan 07 2020 at 23:41):

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

#### Aria Miuk (Jan 07 2020 at 23:42):

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

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


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

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

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

#### Iocta (Jan 08 2020 at 00:52):

I'll meditate on this. Thanks.

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


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

#### 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 :=
_


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


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


#### Kevin Buzzard (Jan 08 2020 at 04:17):

import tactic

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


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


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


#### Kenny Lau (Jan 08 2020 at 08:03):

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

Thanks

#### Iocta (Jan 08 2020 at 08:15):

Is it possible to prove unnotnot without classical?

no

#### Kenny Lau (Jan 08 2020 at 08:24):

it's equivalent to em

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

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

Alright

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


#### Chris Hughes (Jan 12 2020 at 19:56):

You can fill in the underscore

ok

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

#### Kenny Lau (Jan 12 2020 at 19:59):

example : true :=
false.elim _


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

#### Iocta (Jan 12 2020 at 20:03):

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

#### Kevin Buzzard (Jan 12 2020 at 20:05):

search for yourself using the search bar at the top.

ah I see

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


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

Thanks.

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

#### Iocta (Jan 14 2020 at 06:11):

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

#### Iocta (Jan 18 2020 at 05:48):

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

#### Iocta (Jan 18 2020 at 05:57):

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


nope

#### Kenny Lau (Jan 18 2020 at 06:05):

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

#### Iocta (Jan 18 2020 at 06:09):

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

#### Iocta (Jan 18 2020 at 06:11):

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

#### Mario Carneiro (Jan 18 2020 at 06:22):

You just write

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


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


#### Mario Carneiro (Jan 18 2020 at 06:23):

or

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


#### Iocta (Jan 18 2020 at 06:46):

Oh, easy. Thanks.

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

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

#### Iocta (Jan 18 2020 at 07:45):

(m in the example)

#### Iocta (Jan 18 2020 at 07:49):

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

#### Iocta (Jan 18 2020 at 07:49):

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

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


Aha

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

#### Iocta (Jan 18 2020 at 08:12):

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

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

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

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

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

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

#### Kevin Buzzard (Jan 18 2020 at 10:08):

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

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

#### 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 ∈ ∅} = ∅


ouch

#### Cerek Hillen (he) (W2'20) (Jan 19 2020 at 00:50):

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

#### Kevin Buzzard (Jan 19 2020 at 00:50):

It's hidden too deep in the term.

#### Kevin Buzzard (Jan 19 2020 at 00:50):

try ext first

#### Kevin Buzzard (Jan 19 2020 at 00:50):

You can't rewrite under a lambda.

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

#### Kevin Buzzard (Jan 19 2020 at 00:51):

Alternatively you could try simp only [mem_empty_eq]

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

#### Cerek Hillen (he) (W2'20) (Jan 19 2020 at 00:52):

I am a mathematician

Hahaha, well thank you all the same :happy:

#### Kevin Buzzard (Jan 19 2020 at 00:52):

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

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

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

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

#### Kevin Buzzard (Jan 19 2020 at 00:56):

After ext the rewrites do work.

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

#### Cerek Hillen (he) (W2'20) (Jan 19 2020 at 00:58):

thank you for your help :)

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


#### Cerek Hillen (he) (W2'20) (Jan 19 2020 at 01:10):

thanks again Kevin!

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

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


#### Iocta (Jan 19 2020 at 01:44):

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


How to write this?

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


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


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

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


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


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

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

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

#### Bryan Gin-ge Chen (Jan 19 2020 at 19:08):

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

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

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

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

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

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

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

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

#### Cerek Hillen (he) (W2'20) (Jan 19 2020 at 19:56):

On it :slight_smile:

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

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