<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">Dear Peter,<div class=""><br class=""></div><div class="">Agda often doesn’t like pattern matching or rewriting on type equalities where the same variable appears in both sides.</div><div class=""><br class=""></div><div class="">To get around this issue, it helps to use heterogeneous equality. The standard library defines a general version, but here’s a type specific to `Fin` that should be easier to understand.</div><div class=""><br class=""></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;" class=""><div class=""><div class="">data _≈_ {m} : ∀ {n} → Fin m → Fin n → Set where</div></div><div class=""><div class=""> reflexive : {i j : Fin m} → i ≡ j → i ≈ j</div></div><div class=""><div class=""><br class=""></div></div><div class=""><div class="">cong-suc : ∀ {m n} {i : Fin m} {j : Fin n} → i ≈ j → suc i ≈ suc j</div></div><div class=""><div class="">cong-suc (reflexive p) = reflexive (cong suc p)</div></div></blockquote><div class=""><div class=""><br class=""></div></div><div class="">You can see how it’s possible to write `i ≈ j` even when `i` and `j` are from finite sets of different sizes. Now an analogous theorem to yours is easy to prove.</div><div class=""><br class=""></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;" class=""><div class=""><div class="">inject+0n : ∀ {n : ℕ} (fn : Fin n) → inject+ 0 fn ≈ fn</div></div><div class=""><div class="">inject+0n {zero} ()</div></div><div class=""><div class="">inject+0n {suc n} zero rewrite n+0=n n = reflexive refl</div></div><div class=""><div class="">inject+0n {suc n} (suc fn) = cong-suc (inject+0n fn)</div></div></blockquote><div class=""><br class=""></div><div class="">Notice the rewrite on `n+0=n n` to convince Agda that it is valid to introduce the `reflexive` constructor.</div><div class=""><br class=""></div><div class="">We can retrieve propositional equality like this:</div><div class=""><br class=""></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;" class=""><div class=""><div class="">≈-n≡m : ∀ {m n} {i : Fin m} {j : Fin n} → i ≈ j → m ≡ n</div></div><div class=""><div class="">≈-n≡m (reflexive _) = refl</div></div><div class=""><div class=""><br class=""></div></div><div class=""><div class="">≈-to-≡ : ∀ {m n} {i : Fin m} {j : Fin n} (p : i ≈ j) → subst Fin (≈-n≡m p) i ≡ j</div></div><div class=""><div class="">≈-to-≡ (reflexive p) = p</div></div><div class=""><div class=""><br class=""></div></div><div class=""><div class="">inject+0n′ : ∀ {n : ℕ} (fn : Fin n) → subst Fin (≈-n≡m (inject+0n fn)) (inject+ 0 fn) ≡ fn</div></div><div class=""><div class="">inject+0n′ fn = ≈-to-≡ (inject+0n fn)</div></div></blockquote><div class=""><br class=""></div><div class="">I hope this helps!</div><div class=""><br class=""></div><div class="">-Bradley</div><div class=""><br class=""></div><div class=""><div><blockquote type="cite" class=""><div class="">On 21 Feb 2018, at 16:36, Peter Thiemann <<a href="mailto:thiemann@informatik.uni-freiburg.de" class="">thiemann@informatik.uni-freiburg.de</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="">Dear list,<br class=""><br class="">I’m stuck with a proof involving the Fin module from the standard library.<br class="">I need to use Data.Fin.inject+ and the last definition is the lemma that I need.<br class="">However, when I try to solve the first hole by pattern matching on the argument of coerce list this:<br class=""><br class="">inject+0n {suc n} zero with finn=n+0 n<br class="">... | p = {!!}<br class=""><br class="">But then I cannot destruct p because its type is <br class="">p : Fin n ≡ Fin (n + 0)<br class=""><br class="">That ought to be fixable with a rewrite, but all alternatives I tried were rejected by Agda.<br class=""><br class="">-Peter<br class=""><br class=""><br class="">%%%%%%%%%%%%<br class="">module Lemmas where<br class=""><br class="">open import Data.Fin hiding (_+_ ; _≤_)<br class="">open import Data.Nat<br class="">open import Relation.Binary.PropositionalEquality<br class=""><br class=""><br class="">-- about Fin and Nat<br class="">n=n+0 : (n : ℕ) → n ≡ n + 0<br class="">n=n+0 zero = refl<br class="">n=n+0 (suc n) = cong suc (n=n+0 n)<br class=""><br class="">n+0=n : (n : ℕ) → n + 0 ≡ n<br class="">n+0=n zero = refl<br class="">n+0=n (suc n) = cong suc (n+0=n n)<br class=""><br class="">m=n=>finm=finn : ∀ {m n : ℕ} → m ≡ n → Fin m ≡ Fin n<br class="">m=n=>finm=finn refl = refl<br class=""><br class="">finn=n+0 : (n : ℕ) → Fin n ≡ Fin (n + 0)<br class="">finn=n+0 n = m=n=>finm=finn (n=n+0 n)<br class=""><br class="">coerce : ∀ {A B : Set} → A ≡ B → A → B<br class="">coerce refl x = x<br class=""><br class="">inject+0n : ∀ {n : ℕ} (fn : Fin n) → inject+ 0 fn ≡ coerce (finn=n+0 n) fn<br class="">inject+0n {zero} ()<br class="">inject+0n {suc n} zero = {!!}<br class="">inject+0n {suc n} (suc fn) = {!!}<br class="">%%%%%%%%%%%%<br class=""><br class="">_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class="">https://lists.chalmers.se/mailman/listinfo/agda<br class=""></div></div></blockquote></div><br class=""></div></body></html>