How to prove val_succ_eq_succ_val

Stream: general

[Johan Commelin]

This feels almost defeq to me. But I am stumped how to prove this:

lemma val_succ_eq_succ_val (j : fin n) : j.succ.val = j.val.succ := sorry

[Sean Leather]

lemma val_succ_eq_succ_val {n : ℕ} (j : fin n) : j.succ.val = j.val.succ :=
by cases j; simp [fin.succ]

[Johan Commelin]

Aaaahaaa.

[Patrick Massot]

I think we should add this sentence to our bluff toolbox. Instead of saying "the following is trivial", as we always do, we could say "the following is almost defeq".

[Patrick Massot]

People may think we are a bit weird (at least until proof assistant manage to take over the world).

[Patrick Massot]

But it won't be worse than all those students who took Kevin's exam on Monday and will get as their only explanation for poor grade: this doesn't type check.

[Patrick Massot]

Actually I'm reading this because I procrastinate writing a referee report. I should send "this paper does not type check" and be done with it

[Kevin Buzzard]

I have taken off many points for solutions which don't type-check.

[Kevin Buzzard]

I ask them what P_4(X) is, and many people tell me that it is 8cos(theta)^4-8cos(theta)^2+1

[Kevin Buzzard]

[P_n(X) satisfies P_n(cos(theta))=cos(n.theta)]

[Patrick Massot]

Right now I'm staring at some wlog without filling in the proof obligation in that paper I need to referee

[Kevin Buzzard]

One student wrote down the answer and said it was true "by symmetry"

[Kevin Buzzard]

and I thought "hmm, I don't think that will work in Lean"

[Kevin Buzzard]

but at least it typechecks

[Reid Barton]

Replying to the original question; alternatively

by cases j; refl

which shows how almost-defeq it really is

[Johan Commelin]

@Mario Carneiro Should this be in mathlib?

[Johan Commelin]

And the analogue for pred.

[Johan Commelin]

More generally: should I just create PR's for such small additions, or is it too trivial for that?

[Mario Carneiro]

Small additions are fine, since they are focused and usually don't have dependency problems they are easy to review. I think it is not a good idea to have a lower bound on "too trivial" because then you have to find other things to do in the PR or forget about your little fix. It's rules like that that make typos like αdditive persist in lean core for so long

[Mario Carneiro]

I would call the theorem succ_val though

[Johan Commelin]

Done: https://github.com/leanprover/mathlib/pull/138