## Stream: new members

### Topic: exercise 2 on ch3

#### Dave (Jun 11 2019 at 02:38):

I seem to have completed the exercise, but only through pattern recognition and some guesswork. Could someone explain to me why this works?

 variables (p q : Prop) example (h : ¬(p ↔ ¬p)) := begin intros, apply iff.intro, exact h, apply false.elim, end --assume hw : p ↔ ¬ p, --show false, from h hw 

I wrote 2 proofs- one with tactics and one without. The one without seems like cheating, but shouldn't lean see that? Why did it work? Also when clicking around the commas in the tactics proof there seem to be special moments when lean creates multiple goals that are somehow identical (?) and then later they vanish. Specifically, this happens on the second line after  begin. Some clarification on this would be great. I want to be able to appreciate odd proofs like this (if it even is a proof...).

#### Bryan Gin-ge Chen (Jun 11 2019 at 03:00):

That example is a bit weird, you should be trying to prove this instead:

variables (p q : Prop)
example  : ¬(p ↔ ¬p) := sorry


#### Dave (Jun 11 2019 at 03:02):

thanks- I was afraid I wrote it wrong to begin with... I should remember not to write it like I did then.

#### Marc Huisinga (Jun 11 2019 at 07:25):

the proof felt like cheating because it was cheating - you assumed what you were trying to prove.
parameters, like h, are hypotheses.

#### Kevin Buzzard (Jun 11 2019 at 07:26):

Yes, you have been undone by the missing colon.

#### Dave (Jun 11 2019 at 18:03):

the proof felt like cheating because it was cheating - you assumed what you were trying to prove.
parameters, like h, are hypotheses.

Precisely. Now I think I have proven it, but I don't understand how the  assume  tactic works.

 example : ¬(p ↔ ¬p) :=
begin
intro h,
cases h,
let hp: p, from h_mpr
(assume hp: p,
have hnp : ¬ p, from h_mp hp,
show false, from hnp hp),
show false , from (h_mp hp) hp,
end


I seems to work within the parenthesis and I can then apply h_mpr on what "resolves" to be  hp: p  . It seems that what is within parenthesis is the "construction" of such a hypothesis, but it looks very odd. Is this correct?

Also why can't I use  assume  outside of the parentheses? I imagine it is something like a "namespace" issue, but maybe some elaboration would be helpful.

Additionally, lean seems to complain whenever assume is used outside of these parentheses, saying it expected a let statement. I figure this is some of lean's advanced pattern matching at work, but it seems bizarre that it can guess what you should write, but still allows you to either fail or write things some alternate, equivalent way. I imagine an explanation of the assume question above will help explain this situation too.

Thank you.

#### Kevin Buzzard (Jun 11 2019 at 18:09):

Is this correct?

It compiles, so it's correct in that sense. I don't think I ever use assume. I rewrote your proof the way I would probably have written it.

variable (p : Prop)

example : ¬(p ↔ ¬p) :=
begin
intro h,
cases h,
have hp: p,
{ apply h_mpr,
intro hp,
have hnp : ¬ p := h_mp hp,
exact hnp hp
},
exact (h_mp hp) hp
end


#### Kevin Buzzard (Jun 11 2019 at 18:09):

It's exactly the same proof, but I don't ever use from or assume.

#### Kevin Buzzard (Jun 11 2019 at 18:10):

You use let at some point but that's for defining data (stuff whose type is in Type). You can use have to make proofs (stuff whose type is in Prop).

#### Dave (Jun 11 2019 at 18:13):

You use let at some point but that's for defining data (stuff whose type is in Type). You can use have to make proofs (stuff whose type is in Prop).

Thank you for this clarification and the rewritten proof. I was thinking of let as in the let of regular math proofs. Your proof is much nicer and uses tactics in the way I imagine one is supposed to.

#### Kevin Buzzard (Jun 11 2019 at 18:13):

Here's the same proof again in term mode:

example : ¬(p ↔ ¬p) := λ ⟨h_mp, h_mpr⟩, have hp : p := h_mpr (λ hp, h_mp hp hp), h_mp hp hp


#### Marc Huisinga (Jun 11 2019 at 18:13):

assume is not a tactic, afaik assume a : b, c is merely syntactic sugar for λ a : b, c, i.e. it is just syntax to define a function without a name (also known as anonymous function, or just "lambda") in term mode.
so to understand why your code doesn't work without the brackets, you need to understand how precedence works in lambda calculus (or at least its implementation in lean).
essentially, lambda terms always capture everything until the very end. i.e. λ a, b c d e f g will be read as (λ a, b c d e f g)

#### Kevin Buzzard (Jun 11 2019 at 18:14):

The whole "assume, from" stuff is some sort of half way house which I never came to terms with.

#### Marc Huisinga (Jun 11 2019 at 18:15):

as far as i understand it it's really just a bunch of syntactic sugar for lambdas in term mode and their corresponding type annotations

#### Kevin Buzzard (Jun 11 2019 at 18:15):

Yes I think you're right.

#### Dave (Jun 11 2019 at 18:16):

assume is not a tactic,

And here's the answer to my other doubt. Wonderful! So I should simply use \lambda whenever I would have used assume. This connection was very useful!

Also it seems I more or less proved this by accident! How fortunate...

#### Dave (Jun 11 2019 at 18:17):

The whole "assume, from" stuff is some sort of half way house which I never came to terms with.

Again reassuring since it seems you've gotten quite far along the road without needing to!

#### Kevin Buzzard (Jun 11 2019 at 18:18):

I did absolutely everything in tactic mode for ages, and then slowly got to grips with term mode. But I had a maths background and knew nothing about lambdas.

#### Reid Barton (Jun 11 2019 at 18:19):

The whole "assume, from" stuff is some sort of half way house which I never came to terms with.

Again reassuring since it seems you've gotten quite far along the road without needing to!

Yes, for example there is no such thing as "assume, from"

#### Kevin Buzzard (Jun 11 2019 at 18:19):

ha ha, just shows you how little I know about it :-)

#### Marc Huisinga (Jun 11 2019 at 18:19):

at this point it's maybe a good idea to post something some other people and i made at @Sebastian Ullrich 's institute for teaching untyped lambda calculus, maybe it helps a little.
https://pp.ipd.kit.edu/lehre/misc/lambda-ide/Wavelength.html

you can reduce lambda terms and step through the reduction by yourself if you like.
there's no proper tutorial yet because i never got around to turning this into a full blown "tutorial on the lambda calculus", but it might be helpful for visualizing stuff and giving students something to play with.
some of the "exercises" are randomly generated, so don't take that too seriously.
edit: oh, also, the share button doesn't work because the institute didn't want to enable the corresponding database ;)

#### Dave (Jun 11 2019 at 18:19):

I did absolutely everything in tactic mode for ages, and then slowly got to grips with term mode. But I had a maths background and knew nothing about lambdas.

I share such a combination, so I'll likely keep asking you questions

#### Dave (Jun 11 2019 at 18:21):

at this point it's maybe a good idea to post something some other people and i made at Sebastian Ullrich 's instute for teaching untyped lambda calculus, maybe it helps a little.

I will look into this now!

#### Dave (Jun 11 2019 at 18:21):

and thanks again :) - hilarious bit about the share button. I like that you've kept it anyway

#### Kevin Buzzard (Jun 11 2019 at 18:23):

If you're a mathematician you can just do it this way:

variable (p : Prop)

open classical

attribute [instance] prop_decidable

example : ¬(p ↔ ¬p) :=
begin
by_cases h : p,
{ -- p is true
simp [h]
},
{ -- p is false
simp [h]
}
end


#### Dave (Jun 11 2019 at 18:26):

If you're a mathematician you can just do it this way:

I kept running into a wall because my brain is hardwired classically and that proof is what I kept trying to recreate. The exercise wanted us to try it otherwise though, which was kind of challenging.

#### Kevin Buzzard (Jun 11 2019 at 18:27):

Yeah. Figuring out all those constructive exercises is fun, interesting, difficult, kind of cool, and then it turns out that it's completely irrelevant because you just open classical anyway.

#### Dave (Jun 11 2019 at 18:28):

lol irl- I figured as much would be the case. :joy:

#### Kevin Buzzard (Jun 11 2019 at 18:28):

(at least if you're formalising the sort of stuff I'm formalising -- YMMV)

#### Dave (Jun 11 2019 at 18:31):

hmm, well I think you do number theory so not exactly, but do you know if there are computability things in lean? I'd like to see those and maybe get a better feel for lean through that. Otherwise I guess I have the task of formalizing it first...? (Or perhaps you just haven't heard of it and it's out there)

#### Kevin Buzzard (Jun 11 2019 at 18:32):

I'm not the best person to talk to about computability.

fair fair

#### Dave (Jun 11 2019 at 18:33):

wow thanks, this is awesome (and also recent!).
The turing machine file seems to be 1.7k lines of code... wow?