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

[Matthew Daggitt]

Thanks everyone for their replies. In particular, thank you for András and
Jesper for pointing out I was forgetting about the implicit arguments!
Cheers,
Matthew

On Sun, Nov 8, 2020 at 1:16 AM Jesper Cockx <Jesper at sikanda.be> wrote:

> 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 (https://github.com/cedille), but Agda
> does not have such a notion.
>
> -- Jesper
>
> On Sat, Nov 7, 2020 at 3:46 PM András Kovács <puttamalac at gmail.com> wrote:
>
>> 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
>>>
>> _______________________________________________
>> 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/20201109/e4f94893/attachment.html>