Zulip Chat Archive

Stream: new members

Topic: Composing surjections, proof using pattern matching


Martin C. Martin (Aug 04 2022 at 21:02):

The first exercise in Chapter 8 of Theorem proving in Lean is "Use pattern matching to prove that the composition of surjective functions is surjective:

open function

universes u v w
variables {α : Type u} {β : Type v} {γ : Type w}

lemma surjective_comp {g : β  γ} {f : α  β}
  (hg : surjective g) (hf : surjective f) :
surjective (g  f) := sorry

Here's what I have, which is incomplete, and I feel like I'm barking up the wrong tree:

lemma surjective_comp {g : β  γ} {f : α  β}
  (hg : surjective g) (hf : surjective f) :
surjective (g  f)
| c := exists.elim (hg c)
  (assume b hgb, exists.elim (hf b) (assume a hfa, exists.intro a sorry))

I just used the pattern matching to get c, can it be used for more of the proof? Can the proof be simplified further, hopefully leveraging the pattern matching in a way I'm not seeing, but otherwise using tactics or something?

Alex J. Best (Aug 04 2022 at 23:40):

Here's a pattern matching solution, no idea what is intended:

lemma surjective_comp {g : β  γ} {f : α  β}
  (hg : surjective g) (hf : surjective f) :
surjective (g  f)
| x := match hg x with
       | y, hy := match hf y with
                    | z, hz := z, by rw [ hy,  hz]⟩
                    end
       end

BTW most of this answer was generated by github copilot! I pretty much wrote half of the first line only, I have no idea if that means this is written somewhere already or if it is just very smart

Martin C. Martin (Aug 05 2022 at 01:22):

Alex J. Best said:

BTW most of this answer was generated by github copilot! I pretty much wrote half of the first line only, I have no idea if that means this is written somewhere already or if it is just very smart

Perhaps copilot is the new stack overflow. :) Thanks Alex.


Last updated: Dec 20 2023 at 11:08 UTC