Show that some specific typcasts/coercions are trivial

Stream: new members

[Thomas Preu]

How would I go about showing this:

example (n : ℕ) [NeZero n] (k : ℕ) (h : n = k + 1) (i : Fin n):
  @Nat.cast (Fin n) Fin.instNatCast (@Fin.val (k + 1) (@Nat.cast (Fin (k + 1)) Fin.instNatCast (@Fin.val n i))) = i := by
  sorry

---

A bit of background in order that it does not look completely arbitrary.
I am trying to formally prove a high school problem as an exercise. As an intermediate step I want to show

theorem lemmaD {n: ℕ} [NeZero n] (ha: 2 ≤ n) (x: Fin n → ℝ)
  (hb: ∀ i, x i > 0)
  (hc: (i : Fin n) → (x i = 1 + 1 / (x (i + 1)))) :
  ∀ i : Fin n, (∏ j : Fin i, ((- (1 : ℝ)) * (x (j + 1)) * (x (j + 2)))) * (x 0 - x 1) = (x i - x (i + 1)) := by sorry

To use Fin.induction I need to explicitly rewrite n as a successor, which I could do. What I accomplished is (sorry are just to shorten the exposition):

have h01 : n = k + 1 := by sorry
have h02 : Fin n = Fin (k + 1) := by simp[h01]
have ck : ∀ i : Fin (k + 1), (∏ j : Fin i, ((- (1 : ℝ)) * (x (j + 1)) * (x (j + 2)))) * (x 0 - x 1) = (x i - x (i + 1)) := by sorry -- here I use Fin.induction

As a next step I want to apply ck, but when I do as in

intro i -- in the context of showing lemmaD, i is of type Fin n and not Fin (k + 1)
have cki := ck i

I get that cki does not make direct use of i, but rather reroutes it through several type casts. Now I need to get rid of them. The one making up my questions goes through four steps and is the most cumbersome of several such beasts appearing in cki.

[Aaron Liu]

don't do all these casts

[Aaron Liu]

don't use Fin.instNatCast

[Aaron Liu]

try subst h01

[Thomas Preu]

Did not know about subst - need to research its use - thanks.

[Thomas Preu]

Using

have cn := h01 ▸ ck
intro i
rw[cn]

avoids the most horrible coercions, but I am still left with some. These are easily dealt with simp:

example (n : ℕ) [NeZero n] (k : ℕ) (h : n = k + 1) (i : Fin n):
  @Nat.cast (Fin n) Fin.instNatCast (@Fin.val n i) = i := by
  simp

Out of curiosity I would still like to know how to resolve my original question - although I can go on without knowing.

[Kevin Buzzard]

It's not difficult, if you're making the transition between maths and lean, to ask all sorts of horrible questions which are mathematically trivial but very difficult to do formally. That doesn't necessarily mean that it's worth answering them. The trick is to learn how best to write your ideas in Lean's dependent type theory to make them as easy to do in lean as they are to do on paper. For example instead of taking a product over j in Fin i (a totally different thing to Fin n) and then immediately trying to treat it as being in Fin n, why not take a product over j in the relevant subset of Fin n (because then j will be in Fin n from the start).

[Aaron Liu]

Thomas Preu said:

Out of curiosity I would still like to know how to resolve my original question - although I can go on without knowing.

unfortunately I can't get your statement to compile

[Kevin Buzzard]

In mathematics you have all kinds of implicit identifications going on in your head which you very quickly learn are explicit and sometimes very fiddly identifications in lean. You strongly want to minimise the amount of explicit casting you're doing because casts get in the way and are often not necessary.

[Kevin Buzzard]

I wonder whether you should be using Fin n at all, to be honest. Why not just index the x_i by the natural numbers and only talk about natural numbers?