exercise 2 on ch3

Stream: new members

[Dave]

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]

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

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

[Dave]

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

[Marc Huisinga]

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

[Kevin Buzzard]

Yes, you have been undone by the missing colon.

[Dave]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Marc Huisinga]

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]

Yes I think you're right.

[Dave]

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]

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]

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]

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]

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

[Marc Huisinga]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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

[Dave]

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]

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

[Marc Huisinga]

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

[Dave]

fair fair

[Bryan Gin-ge Chen]

^ see also Mario's paper

[Dave]

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?

[Dave]

^ see also Mario's paper

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