Zulip Chat Archive

Stream: maths

Topic: should this be dec_trivial?


view this post on Zulip Kevin Buzzard (Nov 18 2018 at 15:26):

example (n : ℕ) : n > 0 → n ≤ 6 → fact n < 3 ^ n := dec_trivial -- fails

I do 6 case splits and dec_trivial seems to be able to handle the arithmetic, but I can't do it all in one go. I sometimes run into these. How is one supposed to diagnose what has happened and fix it?

view this post on Zulip Chris Hughes (Nov 18 2018 at 15:27):

Revert n, and put n \le 6 before 0<n

view this post on Zulip Kevin Buzzard (Nov 18 2018 at 15:28):

Thanks Chris.

view this post on Zulip Kevin Buzzard (Nov 18 2018 at 15:28):

I see, so forall n : nat, n <= X -> P n works, and I just need to ensure I'm in this format.

view this post on Zulip Mario Carneiro (Nov 18 2018 at 15:58):

sigh... why the horrible case split proofs?

view this post on Zulip Mario Carneiro (Nov 18 2018 at 15:58):

you could reason it instead

view this post on Zulip Kevin Buzzard (Nov 18 2018 at 15:58):

I don't really know what you're saying

view this post on Zulip Kevin Buzzard (Nov 18 2018 at 15:59):

or even if you're talking to me

view this post on Zulip Kevin Buzzard (Nov 18 2018 at 15:59):

But my job is to solve the problems I set, in Lean

view this post on Zulip Mario Carneiro (Nov 18 2018 at 15:59):

if you had to prove that theorem by hand I am sure you wouldn't evaluate 6 factorials

view this post on Zulip Kevin Buzzard (Nov 18 2018 at 15:59):

and the problem is "for which positive integers n is n! < 3^n"

view this post on Zulip Mario Carneiro (Nov 18 2018 at 16:00):

you can prove that it's true for 5 and stop because monotonicity

view this post on Zulip Kevin Buzzard (Nov 18 2018 at 16:00):

ha ha

view this post on Zulip Kevin Buzzard (Nov 18 2018 at 16:00):

I'm not sure it's that easy

view this post on Zulip Kevin Buzzard (Nov 18 2018 at 16:00):

n! and 3^n are changing in different ways

view this post on Zulip Kevin Buzzard (Nov 18 2018 at 16:00):

and things get weird at n=3

view this post on Zulip Kevin Buzzard (Nov 18 2018 at 16:00):

I think I have to check all 6

view this post on Zulip Kevin Buzzard (Nov 18 2018 at 16:01):

dec_trivial times out for 7 :-/

view this post on Zulip Kevin Buzzard (Nov 18 2018 at 16:01):

(hence the norm_num approach, which was also troublesome -- see other thread)


Last updated: May 12 2021 at 07:17 UTC