Zulip Chat Archive

Stream: new members

Topic: term style equivalent to `use`


view this post on Zulip Kevin Doran (Mar 29 2020 at 11:26):

I am trying to write a term-style solution to @Kevin Buzzard's maths challenges. I'm a little stuck on #4, with the following progress (and tactic solution included at the bottom for comparison):

import data.real.basic

open function

theorem challenge4
 (X Y Z : Type)
 (f : X  Y)
 (g : Y  Z) :
surjective (g  f)  surjective g :=
assume h₁,
assume z,
 have h₂ : y : Y, g y = z, from exists.elim (h₁ z)
 (assume (x : X) (hh₁ : (g  f) x = z),
   have hh₂ : g (f x) = z, from hh₁, -- I'm not sure how to create a variable, y : Y, using f x.
   --exists.intro (f x) hh₂
   sorry),
 h₂

theorem challenge4_tactic
 (X Y Z : Type)
 (f : X  Y)
 (g : Y  Z) :
surjective (g  f)  surjective g :=
begin
 intro h,
 intro z,
 cases h z with a ha,
 use f a,
 assumption,
end

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 11:27):

Oh yeah, I can never do those crazy assume have proofs either. Why not just go full lambda-calculus?

view this post on Zulip Patrick Massot (Mar 29 2020 at 11:29):

let y := f x in exists.intro y hh₂

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 11:29):

You can replace the sorry with ⟨f x, hh₂⟩

view this post on Zulip Kevin Doran (Mar 29 2020 at 11:33):

Kevin Buzzard said:

Oh yeah, I can never do those crazy assume have proofs either. Why not just go full lambda-calculus?

The downside of starting with the fantastic "Logic and Proof" website is that my understanding is currently rooted pretty exclusively in assume proofs.

view this post on Zulip Kevin Doran (Mar 29 2020 at 11:33):

Patrick Massot said:

let y := f x in exists.intro y hh₂

Thanks! That's what I needed. I didn't know of let ... in.

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 11:40):

Kevin Doran said:

The downside of starting with the fantastic "Logic and Proof" website is that my understanding is currently rooted pretty exclusively in assume proofs.

Are you the kind of person who understands those big fractions with Gamma ⊢ x : P on the top and bottom?

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 11:40):

All I know is that you don't have to have a clue about those to use Lean.

view this post on Zulip Kevin Doran (Mar 30 2020 at 00:47):

I'm trying to follow that path! The assume have proofs get out of hand quickly.


Last updated: May 10 2021 at 17:39 UTC