[Agda] General notion of equality for syntactically equal objects with different types from the same datatype family?

[András Kovács]

>
> Note `inject₁` doesn't change the syntactic form of `i`, only it's type.


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.

Matthew Daggitt <matthewdaggitt at gmail.com> ezt írta (időpont: 2020. nov.
7., Szo, 9:26):

> Hi everyone,
>  I'm trying to prove something a lemma that looks something like:
> ```agda
> open import Data.Fin
> open import Data.Nat
> open import Relation.Binary.PropositionalEquality
>
> toℕ-inject₁ : ∀ {n} {i : Fin n} → toℕ (inject₁ i) ≡ toℕ i
> toℕ-inject₁ = {!!}
> ```
> 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:
> ```
> import Relation.Binary.HeterogeneousEquality as H using (_≅_)
>
> toℕ-cong : ∀ {m n} {i : Fin m} {j : Fin n} → i ≅ j → toℕ i ≡ toℕ j
> toℕ-cong H.refl = refl
>
> inject₁-≅ : ∀ {n} (i : Fin n) → inject₁ i  ≅ i
> inject₁-≅ zero    = H.refl
> inject₁-≅ (suc i) = H.cong suc (inject₁-≅ i)
> ```
> 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.
>
> 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...
> Cheers,
> Matthew
> _______________________________________________
> 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/20201107/c8e1b235/attachment.html>