Zulip Chat Archive

Stream: new members

Topic: Simplifying equal types


view this post on Zulip Devon Richards (Jan 13 2021 at 04:55):

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.

view this post on Zulip Hanting Zhang (Jan 13 2021 at 05:16):

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

view this post on Zulip Devon Richards (Jan 13 2021 at 05:35):

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.

view this post on Zulip Devon Richards (Jan 13 2021 at 05:43):

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.

view this post on Zulip Eric Wieser (Jan 13 2021 at 08:24):

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

view this post on Zulip Eric Wieser (Jan 13 2021 at 08:26):

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


Last updated: May 11 2021 at 14:11 UTC