composite of injectives

Stream: new members

[Jakob Scholbach]

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!

[Adam Topaz]

You can apply them separately

[Adam Topaz]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Eric Wieser]

Nah, I think full inscrutable is

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

[Jakob Scholbach]

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.

[Kevin Buzzard]

λ x₁ x₂ h, injf $ injg h, known less brutally as λ x₁ x₂ h, injf (injg h), is a proof that $g\circ f$ is injective. Here's how to read it. It is supposed to be a function which takes three inputs, namely two elements $x_1$ and $x_2$ of $\alpha$ and a proof h that $g(f(x_1))=g(f(x_2))$, and spits out a proof that $x_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 $x_1=x_2$. And you can see that it is: injg is a function which takes in a proof that $g(a)=g(b)$ and returns a proof that $a=b$, and so injg h is a proof that $f(x_1)=f(x_2)$. And injf takes a proof that $f(x_1)=f(x_2)$ and returns a proof that $x_1=x_2$.

[Kevin Buzzard]

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.