preferred proof

Stream: new members

[Joseph O]

Which proof is more preferred to level 7 of the Function World in nng?
Mine:

example (P Q F : Type) : (P → Q) → ((Q → F) → (P → F)) :=
begin
  intros f r p,
  have q : Q := f p,
  apply (r q),
end

or the given solution

example (P Q F : Type) : (P → Q) → ((Q → F) → (P → F)) :=
begin
  intro f,
  intro h,
  intro p,
  apply h,
  apply f,
  exact p,
end

Im curious to know, as I want to prove it in the more idiomatic way.

[Junyan Xu]

example (P Q F : Type) : (P → Q) → ((Q → F) → (P → F)) := λ f g, g ∘ f

[Arthur Paulino]

The given solution is better for didactic purposes IMO. It's easier to see the goal changing little by little

[Patrick Johnson]

Junyan Xu said:

example (P Q F : Type) : (P → Q) → ((Q → F) → (P → F)) := λ f g, g ∘ f

You can even use flip (∘). I don't recommend it to someone who is learning Lean via NNG.

[Junyan Xu]

Both λ f g, g ∘ f or flip (∘) could be mathlib-idiomatic depending on whether the author knows the existence of flip. It's not the usual way one would solve NNG levels, but I think it does no harm to learn alternative (ways of writing) proofs after one comes up with their own proof(s).

[Junyan Xu]

Also, in mathlib one would omit the extraneous parentheses:
example (P Q F : Type) : (P → Q) → (Q → F) → P → F := flip (∘)

[Kevin Buzzard]

I'm not claiming any of the "official" solutions are idiomatic, I'm just claiming they compile.

[Mario Carneiro]

I believe the mathib idiomatic way would be:

example {P Q F : Sort*} (f : P → Q) (g : Q → F) (x : P) : F := g (f x)

[Joseph O]

Junyan Xu said:

example (P Q F : Type) : (P → Q) → ((Q → F) → (P → F)) := λ f g, g ∘ f

How does that work, nng didn’t really teach that