fib_mono

Stream: new members

[Julian Külshammer]

In the file about Fibonacci numbers in mathlib there is the following lemma:

lemma fib_mono {n m : ℕ} (n_le_m : n ≤ m) : fib n ≤ fib m :=
by { induction n_le_m with m n_le_m IH, { refl }, { exact (le_trans IH fib_le_fib_succ) }}

I would have expected the following statement instead under the same name:

lemma fib_mono' : monotone fib :=
begin
  apply monotone_of_monotone_nat,
  apply fib_le_fib_succ,
end

Is there a reason why one should be preferred over the other (or to have both)? As far as I can see monotone_of_monotone_nat basically has the same proof as the first one, it is just more general.

[Johan Commelin]

@Julian Külshammer The code for fib might be very old. I don't know, but I can imagine it's one of the first things one tries in a new theorem prover.

[Johan Commelin]

So it probably predates the monotone predicate

[Kevin Buzzard]

If the proof is apply, apply then I would expect to see this in mathlib:

lemma fib_mono' : monotone fib :=
monotone_of_monotone_nat $ λ _, fib_le_fib_succ

[Eric Wieser]

I think a PR to change the statement would probably be accepted and appreciated, although I can't speak for the maintainers

[Johan Commelin]

yup, I think such a PR is fine (-;

[Julian Külshammer]

PR created, #5776

[Johan Commelin]

reviewed (-;

[Eric Wieser]

Should every monotone lemma be tagged with mono?

[Bryan Gin-ge Chen]

Good question. I don't think the mono tactic is used much, but maybe we should. cc: @Simon Hudon

[Simon Hudon]

Yes you can mark monotone lemmas as mono. That lets the mono tactic use your lemma when trying to prove ≤ goals