<div dir="ltr"><div>Indeed, expanding the implicit arguments you get `zero {n} : Fin (suc n)` and `zero {suc n} : Fin (suc (suc n))`, which are definitely not syntactically equal. There exist languages that have a notion of "equality up to erasure" such as Cedille (<a href="https://github.com/cedille">https://github.com/cedille</a>), but Agda does not have such a notion.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Nov 7, 2020 at 3:46 PM András Kovács <<a href="mailto:puttamalac@gmail.com">puttamalac@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Note `inject₁` doesn't change the syntactic form of `i`, only it's type.</blockquote><div><br></div><div>This is not correct. Inject1 changes the implicit Nat indices in Fin constructors. There is no notion of equality which is more "syntactic" than definitional equality. If two terms are not equal by refl, they are not syntactically equal. </div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Matthew Daggitt <<a href="mailto:matthewdaggitt@gmail.com" target="_blank">matthewdaggitt@gmail.com</a>> ezt írta (időpont: 2020. nov. 7., Szo, 9:26):<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">Hi everyone,<br><div> I'm trying to prove something a lemma that looks something like:</div><div>```agda</div><div>open import Data.Fin</div><div>open import Data.Nat</div><div>open import Relation.Binary.PropositionalEquality</div><div><br></div><div>toℕ-inject₁ : ∀ {n} {i : Fin n} → toℕ (inject₁ i) ≡ toℕ i<br>toℕ-inject₁ = {!!}</div><div>```</div><div>Note `inject₁` doesn't change the syntactic form of `i`, only it's type. In this simple case it is easy enough to prove inductively, but I've currently got a harder case where `inject₁` is more complicated. So I was thinking about using heterogeneous equality and generalising this to something of the form:</div><div>```</div><div>import Relation.Binary.HeterogeneousEquality as H using (_≅_)<br></div><div><br></div><div>toℕ-cong : ∀ {m n} {i : Fin m} {j : Fin n} → i ≅ j → toℕ i ≡ toℕ j<br>toℕ-cong H.refl = refl<br></div><div><br></div><div>inject₁-≅ : ∀ {n} (i : Fin n) → inject₁ i  ≅ i<br></div><div>inject₁-≅ zero    = H.refl<br>inject₁-≅ (suc i) = H.cong suc (inject₁-≅ i)<br></div><div>```</div><div>The problem is of course that the two cases of `inject₁-≅` don't type check as the two sides don't have the same type. Examining the first case, we want to assert that `zero : Fin n` and `zero : Fin (suc n)` are equal. In heterogeneous equality, despite working for terms of different types, the constructor `refl` can only be applied when those two types can be proved to be propositionally equal.</div><div><br></div><div>I suspect I'm going to have to define a custom notion of equality over `Fin`, but I just thought I'd check that there isn't a more general notion of equality out there that I could use that I'm missing? It's probably a silly question, as a purely syntactic notion of equality that entirely ignores the types seems very unlikely to be undefinable. But I thought perhaps the fact that they belonged to the same datatype might give some wriggle room...</div><div>Cheers,</div><div>Matthew</div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>