Zulip Chat Archive

Stream: new members

Topic: composite of injectives


view this post on Zulip Jakob Scholbach (Jan 31 2021 at 14:45):

I am working through §3 of the mathematics in lean tutorial. I am stuck with the composition of injectivity.

open function

-- BEGIN
variables {α : Type*} {β : Type*} {γ : Type*}
variables {g : β  γ} {f : α  β}

example (injg : injective g) (injf : injective f) :
  injective (λ x, g (f x)) :=
begin
  intro x1,
  intro x2,
  dsimp,
  apply injg (injf),
end

I am not quite able to find the right syntax for saying : apply injg to f(x1) and f(x2 (in the last line of the proof). How is this done? Thanks!

view this post on Zulip Adam Topaz (Jan 31 2021 at 14:55):

You can apply them separately

view this post on Zulip Adam Topaz (Jan 31 2021 at 15:03):

Oh you probably need to introduce another thing, saying that g (f x1) = g (f x2), with the goal x1 = x2. Then you can apply injf, then apply injg, etc

view this post on Zulip Patrick Massot (Jan 31 2021 at 15:35):

Yes, if you want to do it fully backward then:

example (injg : injective g) (injf : injective f) :
  injective (λ x, g (f x)) :=
begin
  intro x1,
  intro x2,
  intro h,
  apply injf,
  apply injg,
  exact h,
end

view this post on Zulip Patrick Massot (Jan 31 2021 at 15:39):

I don't know how much was explained in MIL at the point you are reading, but note that nothing in Lean forces you to write such an inscrutable proof script that looks like nothing you would write on paper. You can perfectly write:

example (injg : injective g) (injf : injective f) :
  injective (λ x, g (f x)) :=
begin
  assume (x₁ x₂ : α) (h : g (f x₁) = g (f x₂)),
  show x₁ = x₂,
  have fact : f x₁ = f x₂, from injg h,
  exact injf fact,
end

view this post on Zulip Kevin Buzzard (Jan 31 2021 at 15:56):

Alternatively you can go full inscrutable:

open function

-- BEGIN
variables {α : Type*} {β : Type*} {γ : Type*}
variables {g : β  γ} {f : α  β}

example (injg : injective g) (injf : injective f) :
  injective (λ x, g (f x)) :=
λ x₁ x₂ h, injf $ injg h

view this post on Zulip Kevin Buzzard (Jan 31 2021 at 15:57):

This way makes it clearer that a proof is just a function.

view this post on Zulip Eric Wieser (Jan 31 2021 at 16:04):

Nah, I think full inscrutable is

example (injg : injective g) (injf : injective f) :
  injective (g  f) :=
λ x₁ x₂, @@injf  @@injg

view this post on Zulip Jakob Scholbach (Jan 31 2021 at 19:24):

Ah, thanks -- I was missing the exact h in Patrick's solution. It is nice to know that there are less readable :) versions of this, too. I am currently at the level where I try to write down the proof as slowly as possible, because it gives me more safety what the prover does at each point. In the lambda-calculus notation I find it much less clear what is going on, so at best I am able to compress a several-lines-proof a posteriori into a single-line-proof.

view this post on Zulip Kevin Buzzard (Jan 31 2021 at 19:28):

λ x₁ x₂ h, injf $ injg h, known less brutally as λ x₁ x₂ h, injf (injg h), is a proof that gfg\circ f is injective. Here's how to read it. It is supposed to be a function which takes three inputs, namely two elements x1x_1 and x2x_2 of α\alpha and a proof h that g(f(x1))=g(f(x2))g(f(x_1))=g(f(x_2)), and spits out a proof that x1=x2x_1=x_2 (proofs and elements are both "things" in type theory, so functions can eat proofs as well as elements). So the claim now is that injf (injg h) is a proof that x1=x2x_1=x_2. And you can see that it is: injg is a function which takes in a proof that g(a)=g(b)g(a)=g(b) and returns a proof that a=ba=b, and so injg h is a proof that f(x1)=f(x2)f(x_1)=f(x_2). And injf takes a proof that f(x1)=f(x2)f(x_1)=f(x_2) and returns a proof that x1=x2x_1=x_2.

view this post on Zulip Kevin Buzzard (Jan 31 2021 at 19:31):

Note also that Patrick's tactic proof literally just reads the terms in λ x₁ x₂ h, injf (injg h), in that order, so it is just literally building the function piece by piece. This is why the "backwards" argument (using injectivity of f before injectivity of g) is so natural to computer scientists, because that's how they build the function.


Last updated: May 16 2021 at 05:21 UTC