Dependent equalities

Stream: general

[Trebor Huang]

Consider this type

inductive DEq {α : Sort _} {β : α → Sort _} :
  ∀ (x y : α), β x → β y → Prop
  | rfl : DEq x x u u

theorem DEq.to_HEq : DEq x y u v → HEq u v
  | .rfl => HEq.rfl

theorem HEq.to_DEq {u : α} {v : β} : HEq u v → DEq (β := id) _ _ u v
  | .rfl => DEq.rfl

theorem DEq.fst : DEq x y u v → x = y
  | .rfl => Eq.refl _

theorem DEq.snd : (p : DEq x y u v) → p.fst.subst u = v
  | .rfl => Eq.refl _

This can be regarded as a compromise between Eq and HEq, potentially having the benefits of both. Is this tried out anywhere in mathlib?

[Kyle Miller]

This shows up in an indirect way in things like docs#simple_graph.walk.copy and docs#quiver.hom.cast where rather than having a separate inductive type, there's some syntactic way of writing down the concept with explicit equalities on indices. (These are both with two indices rather than your DEq's one index on β.)

[Kyle Miller]

The DEq type can also be written in another form using just existentials and Eq:

theorem DEq_iff (β : α → Sort _) (x y : α) (u : β x) (v : β y) :
  DEq x y u v ↔ ∃ (h : x = y), h.subst u = v := by
  constructor
  · intro h
    cases h
    exact ⟨rfl, rfl⟩
  · intro h
    cases h
    subst_vars
    constructor

[Kyle Miller]

The nice thing about DEq-like relations (and this cast pattern for homs/walks) is that they preserve the equality on the index. This is much more powerful than just working with HEq, which only remembers equality on the whole type. You can't recover index equalities from type equalities in general.

[Kyle Miller]

A design question then is whether you have a DEq type (well, one for every number of indices you might have) or instead work with the ∃ (h : x = y), h.subst u = v form more directly (and define a special subst for your type so that simp lemmas don't put things into an inconvenient form involving subst of an entire type rather than just the indices). The second way seems to be convenient to work with, but I have no idea if it would be better to pursue the first way.

[Kyle Miller]

One point against developing DEq is that HEq is sufficient if you have index equalities hanging around:

theorem DEq_iff' (β : α → Sort _) (x y : α) (u : β x) (v : β y) :
  x = y → (DEq x y u v ↔ HEq u v) := by
  intro h
  cases h
  constructor
  · intro h
    cases h
    rfl
  · intro h
    cases h
    constructor

[Eric Wieser]

I explored this a little in #10712

[Kyle Miller]

I have an experiment in this branch from a couple years ago for this but for two-index types (walks in graphs). Rather than a new inductive type, heqi ( "heterogeneous equality that equates indices") is defined as a plain Prop.