Zulip Chat Archive

Stream: new members

Topic: fib_mono


Julian Külshammer (Jan 16 2021 at 12:59):

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 (Jan 16 2021 at 13:10):

@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 (Jan 16 2021 at 13:10):

So it probably predates the monotone predicate

Kevin Buzzard (Jan 16 2021 at 13:11):

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 (Jan 16 2021 at 14:10):

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

Johan Commelin (Jan 16 2021 at 14:59):

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

Julian Külshammer (Jan 16 2021 at 15:11):

PR created, #5776

Johan Commelin (Jan 16 2021 at 15:11):

reviewed (-;

Eric Wieser (Jan 16 2021 at 15:37):

Should every monotone lemma be tagged with mono?

Bryan Gin-ge Chen (Jan 16 2021 at 15:45):

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

Simon Hudon (Jan 16 2021 at 15:59):

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


Last updated: Dec 20 2023 at 11:08 UTC