[Agda] subst puzzle

[Andreas Nuyts]

Hi,

This also works. It's longer than Paolo's solution, but more self-contained:

    module SubstPuzzle where

    open import Data.Nat -- using (ℕ; _+_; zero)
    open import Data.Fin using (Fin; zero; suc; splitAt)
    open import Relation.Binary.PropositionalEquality -- using (_≡_; subst)
    open import Data.Sum -- using (inj₁)
    open import Function

    suc-inj : {j k : ℕ} (p : (ℕ ∋ suc j) ≡ suc k) → j ≡ k
    suc-inj {j} {.j} refl = refl

    subst-zero : {j k : ℕ} (p : suc j ≡ suc k) → subst Fin p zero ≡ zero
    subst-zero {j} {.j} refl = refl

    subst-suc : {j k : ℕ} (p : suc j ≡ suc k) (m : Fin j) → subst Fin p
    (suc m) ≡ suc (subst Fin (suc-inj p) m)
    subst-suc {j} {.j} refl m = refl

    splitAtSuc : (j k : ℕ) (m : Fin (j + k)) (n : Fin j) (p : splitAt j
    m ≡ inj₁ n) → (splitAt (suc j) (suc m) ≡ inj₁ (suc n))
    splitAtSuc j k m n p = cong (map suc id) p

    lemma : (k : ℕ) (m : Fin k) (p : k ≡ k + 0) → splitAt k (subst Fin p
    m) ≡ inj₁ m
    lemma zero () p
    lemma (suc k) zero p = cong (splitAt (suc k)) (subst-zero p)
    lemma (suc k) (suc m) p = trans
                                 (cong (splitAt (suc k)) (subst-suc p m))
                                 (splitAtSuc k zero (subst Fin (suc-inj
    p) m) m (lemma k m (suc-inj p)))


Best regards,
Andreas

On 02.03.21 08:39, Paolo Capriotti wrote:
> March 1, 2021 9:54 pm:
>> Here is a self-contained puzzle that has me stumped. I'm sure there are
>> lemmas in Relation.Binary.PropositionalEquality.Properties that ought to
>> apply, but I just can't see it.  Ideas?
> Here is my attempt:
> https://gist.github.com/pcapriotti/32358d5b89e72459608651e6030886de
>
> I find the easiest way to prove an equality of elements of Fin n is to just convert them to natural numbers, prove the equality there, then using injectivity of toℕ.
>
> Best,
> Paolo
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210302/2cf8e04b/attachment.html>