Zulip Chat Archive

Stream: new members

Topic: Improving injectivity proof

Danila Kurganov (Mar 05 2020 at 16:20):

Hi, I've proved that the composition of two injective functions is itself injective, but I'd like to see if I can improve on my proof; the paper version is much more slick IMO and I want to know if I can make my Lean more paper-like. Here is the code:

def injective {X : Type} {Y : Type} (f : X → Y) : Prop :=
∀ a b : X, f a = f b → a = b


theorem injective_comp2 {X Y Z : Type} (f : X → Y) (g : Y → Z) :
  injective f → injective g → injective (g ∘ f) :=

begin
  intros injf injg,
  unfold injective at *,
  intros c d,

  intro lefty,
  unfold function.comp at *,

  have intermediary : f c = f d,
  apply injg,
  exact lefty,

  apply injf,
  exact intermediary,
end

Now usually (after some explaining) I'd just do g ∘ f a = g ∘ f b → g(f(a)) = g(f(b)) → f(a) = f(b) → a = b, thinking in terms of injectivity in one-direction instead of bouncing back-and-forth with have statements. Is there anyway I can do this for the above theorem?

Johan Commelin (Mar 05 2020 at 16:22):

I don't know if this is what you want, but you can remove all the unfold statements

Johan Commelin (Mar 05 2020 at 16:24):

Once you've done that, the have statement becomes redundant...

Danila Kurganov (Mar 05 2020 at 16:31):

How does have become redundant here?

(I do see though that the unfold isn't of use in the backend)

Johan Commelin (Mar 05 2020 at 16:32):

Because your have is equal to the goal. So you might as well prove it directly.

Danila Kurganov (Mar 05 2020 at 16:37):

Oh wow that's neat!

theorem injective_comp3 {X Y Z : Type} (f : X → Y) (g : Y → Z) :
  injective f → injective g → injective (g ∘ f) :=

begin
  intros injf injg,
  intros c d,

  intro lefty,
  apply injf,
  apply injg,
  exact lefty,

end