Zulip Chat Archive

Stream: new members

Topic: fin succ proof coercing to `n + 1`


Yakov Pechersky (Jul 28 2020 at 19:46):

Is there some fin n coercion lemma that is missing? Or should I be using fin.cast_succ? In the following proof. I don't know how to remove % (n + 1) even if I have a hypothesis of i < n.

import tactic.linarith

example {n : } (i : fin n) : ((i : fin (n + 1)) + 1) = i.succ :=
begin
  cases i with i h,
  induction i with k hk,
  simp [fin.succ],
  cases n, linarith, refl,
  cases n, linarith,
  simp [fin.succ],
  /-
  case nat.succ, nat.succ
  k n : ℕ,
  hk : ∀ (h : k < n.succ), ↑⟨k, h⟩ + 1 = ⟨k, h⟩.succ,
  h : k.succ < n.succ
  ⊢ ↑k + 1 + 1 = ⟨k.succ.succ, _⟩
  -/
  sorry,
end

Yakov Pechersky (Jul 28 2020 at 20:15):

Even this is confusing me. I'm unable to use h with hi.

example (i n : ) (h : i < n) : (i : fin (n + 1)).val = i :=
begin
  induction i with i hi,
  simp,
  sorry,
end

Kevin Buzzard (Jul 28 2020 at 20:48):

I don't think you need induction to prove this. There's bound to be a lemma in the library saying that if i<j then i%j=i, it will be called mod_lt or something

Jalex Stark (Jul 28 2020 at 20:50):

the code you posted doesn't say anything about %

Kevin Buzzard (Jul 28 2020 at 20:53):

Addition on fin uses % IIRC

Johan Commelin (Jul 28 2020 at 20:59):

I would avoid the cast from nat to fin (n+1). It isn't "nice" (imho)

Johan Commelin (Jul 28 2020 at 21:00):

But if you really need to, you can do it. The file zmod.lean will show you how to deal with it.

Jalex Stark (Jul 28 2020 at 21:03):

I had to guess that the lemma I wanted started with fin.coe_. I spent about a minute trying other things before making this guess.

example (i n : ) (h : i < n) : (i : fin (n + 1)).val = i :=
begin
  apply fin.coe_coe_of_lt, linarith,
end

Last updated: Dec 20 2023 at 11:08 UTC