Equality between indexed types

Stream: lean4

[Scott Godwin]

Is there a general pattern for handling equality of two terms of an indexed type where the indexes are not definitionally equal but are propositionally equal? The equality can't be stated since they aren't definitionally equal, and trying to do rewrites in the definition itself introduces a lot of Eq.mp/Eq.mpr which makes reasoning about them extremely hard in my experience. I can try to come up with an example, but I've run into this a lot and just wanted to see if there's an agreed upon approach.

I know in Agda, for example, you can state rewrite rules for propositional equality and then you can state the equality since they will unify.

[Shreyas Srinivas]

Are you looking for coercions by any chance? There is the Coe typeclass if that is the case.

[Johan Commelin]

There is also HEq, which is a heterogeneous equality.

[Scott Godwin]

Here is a highly contrived example that illustrates what I mean:

inductive Foo : Nat → Type where
  | foo : (n : Nat) → Foo n

def bar {n : Nat} : Foo n → Foo n → Type := sorry

def baz {m n : Nat} (f₁ : Foo (m + n)) (f₂ : Foo (n + m)) : bar f₁ f₂ := sorry

In the definition of baz itself, I can't call bar f₁ f₂ because their indexes are not definitionally equal, but they are propositionally equal.

Shreyas Srinivas said:

Are you looking for coercions by any chance? There is the Coe typeclass if that is the case.

I haven't actually used Coe before, but it doesn't seem like it's appropriate in this situation?

Johan Commelin said:

There is also HEq, which is a heterogeneous equality.

Sometimes you can do that, but like the example above, I don't see how you'd use it.

[Henrik Böving]

I don't know myself how to make proper use of HEq but you can go like so if you want:

inductive Foo : Nat → Type where
  | foo : (n : Nat) → Foo n

def bar {n : Nat} (lhs : Foo n) (rhs : Foo m) (h : n = m) : Prop := lhs = h ▸ rhs

def baz {m n : Nat} (f₁ : Foo (m + n)) (f₂ : Foo (n + m)) : bar f₁ f₂ (Nat.add_comm _ _) := sorry

or alternatively:

inductive Foo : Nat → Type where
  | foo : (n : Nat) → Foo n

def bar {n : Nat} (lhs : Foo n) (rhs : Foo n) : Prop := lhs = rhs

def baz {m n : Nat} (f₁ : Foo (m + n)) (f₂ : Foo (n + m)) : bar f₁ ((Nat.add_comm _ _) ▸ f₂)  := sorry

[Shreyas Srinivas]

Coercions will work well for this example. You need to define coercions for Foo (n+m) and Foo (m+n). Alternatively in this particular case Nat.add_comm _ _ \t term also helps

[Shreyas Srinivas]

(Replace \t with the Unicode variant)

[Kevin Buzzard]

Rather than using the coercion framework people usually get around this by writing a bespoke wrapper for Eq.rec and training the simplifier on it. See for example docs#category_theory.eq_to_hom in the lean 3 category theory library; it produces a morphism A -> B from a proof of A=B.

This issue is a standard thorn in the side of dependent type theory

[Shreyas Srinivas]

You might also like to see how Fin n works.

[Shreyas Srinivas]

docs4#Fin

[Scott Godwin]

Thanks for the responses. I'll admit that when casting starts getting involved, I start getting a bit lost. It obviously makes sense to do it, but then I run into situations where I need to give a term of an indexed type SomeType (... a ... ) but I instead I have something like SomeType (... (Eq.mp _ a) ...) and I'm just not sure how to proceed. For example, this is the actual error message I'm stuck on (trying to prove strong normalization of the STLC as an exercise):

type mismatch
  h
has type
  HereditarilyNormalizing
    (Expr.application
      (applicationᵣ fs
        (Eq.mpr
          (_ :
            (Γ ⊢ arrowᵣ (Ty.arrow f.τ τ') (List.map (fun f => f.τ) fs)) =
              (Γ ⊢ arrowᵣ τ' (List.map (fun f => f.τ) fs ++ [f.τ])))
          (Eq.mpr
            (_ :
              (Γ ⊢ arrowᵣ τ' (List.map (fun f => f.τ) fs ++ [f.τ])) =
                (Γ ⊢ List.foldr (fun τ' τ => Ty.arrow τ' τ) (Ty.arrow f.τ τ') (List.map (fun f => f.τ) fs)))
            (Eq.mp
              (_ :
                (Γ ⊢ arrowᵣ τ' (List.map (fun f => f.τ) (fs ++ [f]))) =
                  (Γ ⊢
                    List.foldr (fun τ' τ => Ty.arrow τ' τ) (List.foldr (fun τ' τ => Ty.arrow τ' τ) τ' [f.τ])
                      (List.map (fun f => f.τ) fs)))
              (Expr.var
                (Eq.mpr
                  (_ :
                    (Γ ∋ arrowᵣ τ' (List.map (fun f => f.τ) (fs ++ [f]))) =
                      (Γ ∋ List.foldr (fun τ' τ => Ty.arrow τ' τ) τ' (List.map (fun f => f.τ) fs ++ [τ])))
                  (Eq.mpr
                    (_ :
                      (Γ ∋ List.foldr (fun τ' τ => Ty.arrow τ' τ) τ' (List.map (fun f => f.τ) fs ++ [τ])) =
                        (Γ ∋ List.foldr (fun τ' τ => Ty.arrow τ' τ) (Ty.arrow τ τ') (List.map (fun f => f.τ) fs)))
                    a)))))))
      e') : Type
but is expected to have type
  HereditarilyNormalizing (Expr.application (applicationᵣ fs (Expr.var a)) e') : Type

I'm sure it could be cleaned up significantly, but was just trying to get it to typecheck first. I don't really expect anyone to figure it out from that and I don't really know of a good way to create a MWE, just noting that my types become polluted with all these Eq.mp/Eq.mprs after doing these kinds of casts.

[Kyle Miller]

In addition to docs4#CategoryTheory.eqToHom, two other mathlib case studies in having functions to manipulate indices into the right form are docs4#SimpleGraph.Walk.copy and docs4#Quiver.Hom.cast

[Kyle Miller]

I didn't actually test this, but a way this design pattern could apply in this case is like so:

inductive Foo : Nat → Type where
  | foo : (n : Nat) → Foo n

def bar {n : Nat} : Foo n → Foo n → Type := sorry

def Foo.cast (f : Foo n) (h : n = m) : Foo m := h ▸ f

def baz {m n : Nat} (f₁ : Foo (m + n)) (f₂ : Foo (n + m)) : bar f₁ (f₂.cast (add_comm _ _)) := sorry

[Kyle Miller]

Unrestricted Eq.mpr/Eq.rec/etc. tend to be annoying to work with; having a wrapper helps constrain exactly what is being rewritten.

[Kyle Miller]

If you look in the SimpleGraph.Walk module, you can take a look at how helper lemmas for the wrapper are proved. You usually write lemmas where the index equalities are between variables (rather than arbitrary expressions), then start the proof with subst_vars. Many times then the proof of the helper lemmas is rfl after this.

[Eric Wieser]

docs#tensor_power.cast is another example. Note this is an example of it often being nicer not to just use the triangle.

[Eric Wieser]

(docs#fin.cast being the other main example of that pattern)

[Scott Godwin]

Thanks, I'll try defining cast and the corresponding lemmas on the related indexed types and see where that gets me.

[Scott Godwin]

Spent some time on this, defining all the cast lemmas etc and was able to get the proof to go through (or at least the part I was having trouble with, still have a couple more to go)! Thanks again for the help everyone!