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

[Carette, Jacques]

I’m going to discourage you from going down this road.

Here’s an analogy: you are trying to show that the ‘bit patterns’ that represent values of two different types are the same. While this can be true, and can be a useful truth (for optimizing computations), it isn’t necessarily a good notion of ‘equality’. Which you yourself recognize.

Whenever I’ve been in the same situation (and it happened a lot in the early days of the work on the Pi reversible language), the eventual resolution usually involved having some type have 2 indices instead of 1, even though the indices were provably equal. And that was indeed the crux: the indices were merely propositionally equal, not definitionally equal. [Permutations, I see you!].  Of course, your setting might be entirely different.

In any case, if you persist down this road, I’d encourage you to see it as a “bit pattern are the same”, i.e. an issue of syntactic representation, rather than being about equality.

Jacques

From: Agda <agda-bounces at lists.chalmers.se> On Behalf Of Matthew Daggitt
Sent: November 7, 2020 3:26 AM
To: Agda mailing list <agda at lists.chalmers.se>
Subject: [Agda] General notion of equality for syntactically equal objects with different types from the same datatype family?

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201107/78cc2ce4/attachment.html>