## Stream: new members

### Topic: preferred proof

#### Joseph O (Apr 24 2022 at 02:02):

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 (Apr 24 2022 at 02:09):

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


#### Arthur Paulino (Apr 24 2022 at 02:12):

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

#### Patrick Johnson (Apr 24 2022 at 03:55):

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 (Apr 24 2022 at 04:06):

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 (Apr 24 2022 at 04:08):

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

#### Kevin Buzzard (Apr 24 2022 at 07:23):

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

#### Mario Carneiro (Apr 24 2022 at 07:26):

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 (Apr 24 2022 at 12:15):

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

Last updated: Dec 20 2023 at 11:08 UTC