Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jalex Stark (Jul 28 2020 at 20:50):

the code you posted doesn't say anything about %

view this post on Zulip Kevin Buzzard (Jul 28 2020 at 20:53):

Addition on fin uses % IIRC

view this post on Zulip Johan Commelin (Jul 28 2020 at 20:59):

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

view this post on Zulip 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.

view this post on Zulip 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: May 13 2021 at 18:26 UTC