<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
Hi,<br>
<br>
This also works. It's longer than Paolo's solution, but more
self-contained:<br>
<br>
<blockquote>module SubstPuzzle where<br>
<br>
open import Data.Nat -- using (ℕ; _+_; zero)<br>
open import Data.Fin using (Fin; zero; suc; splitAt)<br>
open import Relation.Binary.PropositionalEquality -- using (_≡_;
subst)<br>
open import Data.Sum -- using (inj₁)<br>
open import Function<br>
<br>
suc-inj : {j k : ℕ} (p : (ℕ ∋ suc j) ≡ suc k) → j ≡ k<br>
suc-inj {j} {.j} refl = refl<br>
<br>
subst-zero : {j k : ℕ} (p : suc j ≡ suc k) → subst Fin p zero ≡
zero<br>
subst-zero {j} {.j} refl = refl<br>
<br>
subst-suc : {j k : ℕ} (p : suc j ≡ suc k) (m : Fin j) → subst Fin
p (suc m) ≡ suc (subst Fin (suc-inj p) m)<br>
subst-suc {j} {.j} refl m = refl<br>
<br>
splitAtSuc : (j k : ℕ) (m : Fin (j + k)) (n : Fin j) (p : splitAt
j m ≡ inj₁ n) → (splitAt (suc j) (suc m) ≡ inj₁ (suc n))<br>
splitAtSuc j k m n p = cong (map suc id) p<br>
<br>
lemma : (k : ℕ) (m : Fin k) (p : k ≡ k + 0) → splitAt k (subst Fin
p m) ≡ inj₁ m<br>
lemma zero () p<br>
lemma (suc k) zero p = cong (splitAt (suc k)) (subst-zero p)<br>
lemma (suc k) (suc m) p = trans<br>
(cong (splitAt (suc k)) (subst-suc p
m))<br>
(splitAtSuc k zero (subst Fin (suc-inj
p) m) m (lemma k m (suc-inj p)))<br>
</blockquote>
<br>
Best regards,<br>
Andreas<br>
<br>
<div class="moz-cite-prefix">On 02.03.21 08:39, Paolo Capriotti
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:1614670450.ja9x5xymbp.astroid@avocado.none">
<pre class="moz-quote-pre" wrap="">March 1, 2021 9:54 pm:
</pre>
<blockquote type="cite">
<pre class="moz-quote-pre" wrap="">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?
</pre>
</blockquote>
<pre class="moz-quote-pre" wrap="">
Here is my attempt:
<a class="moz-txt-link-freetext" href="https://gist.github.com/pcapriotti/32358d5b89e72459608651e6030886de">https://gist.github.com/pcapriotti/32358d5b89e72459608651e6030886de</a>
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
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>