Zulip Chat Archive

Stream: new members

Topic: exercise 2 on ch3


view this post on Zulip 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...).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:26):

Yes, you have been undone by the missing colon.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 18:09):

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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 18:15):

Yes I think you're right.

view this post on Zulip 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...

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 18:19):

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

view this post on Zulip 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 ;)

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Dave (Jun 11 2019 at 18:21):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Dave (Jun 11 2019 at 18:28):

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

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 18:28):

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

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 18:32):

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

view this post on Zulip Marc Huisinga (Jun 11 2019 at 18:32):

there's this https://github.com/leanprover-community/mathlib/tree/master/src/computability

view this post on Zulip Dave (Jun 11 2019 at 18:33):

fair fair

view this post on Zulip Bryan Gin-ge Chen (Jun 11 2019 at 18:33):

^ see also Mario's paper

view this post on Zulip Dave (Jun 11 2019 at 18:33):

there's this https://github.com/leanprover-community/mathlib/tree/master/src/computability

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

view this post on Zulip Dave (Jun 11 2019 at 18:34):

^ see also Mario's paper

oh thanks for this too! I have a lot of reading to do then :)


Last updated: May 09 2021 at 20:11 UTC