Simplifying equal types

Stream: new members

[Devon Richards]

I'm writing a function def concat {m n : ℕ} (s : fin m → α) (t : fin n → α) : fin (m + n) → α and I start by splitting on the case that m = 0. Is there a good way for me to get it to accept t as the result? Ultimately what I'm trying to do is make it simpler to work with the definition when trying to prove things about it. Currently when I do split_ifs I get a value of _.mpr t ⟨i, _⟩ which I'm not sure how to deal with.

[Hanting Zhang]

You can do cases n, which does induction by splitting into a base case m = 0 and the inductive step.

[Devon Richards]

I ended up being able to refactor concat so that I only have to check if m is zero since I can usually get a contradiction there, and instead of checking if n=0 I introduce an element of ⟨i, hi⟩ : fin (m + n) and have an if/else on whether h : i < m in which case it case it can just return s ⟨i, h⟩ which simplified much more usefully.

[Devon Richards]

And I could actually go further and completely remove the equal to zero checks for both variables so the only if expression is on i < m. Guess this makes a good lesson on making sure my definitions are correct.

[Eric Wieser]

There's a docs#sum_fin_sum_equiv or similar that mostly implements your concat

[Eric Wieser]

sum.cases s t \comp sum_fin_sum_equiv.symm is your function I think