search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.23k stars 185 forks source link

Define matrices as functions #1982

Open Alizter opened 1 month ago

Alizter commented 1 month ago

In #1979 it was mentioned that matrices might be better defined as functions from a finite domain. This would allow us to remove a lot of boiler plate in the matrix proofs. It should also be possible to characterize path types of matrices without funext since it should be provable for functions with finite domains.

In practice, this means we should redefine vectors as functions from a finite domain since matrices are defined in terms of vectors.

Alizter commented 1 month ago

@jdchristensen After thinking about this for a bit I actually don't think I know how to prove function extensionality for a finite domain. Even for the empty type, I don't know how to show two functions from the empty type are equal without assuming funext.

It would seem then if we wanted matrices to compute like this, then we will have to introduce funext everytime we prove something with an equality.

jdchristensen commented 1 month ago

It might still work out well, replacing = by == for statements about vectors and matrices. But it would be pretty radical, so I'm not sure if we want to go there. But so many operations on vectors are naturally expressed componentwise, and would then compute definitionally. map would just become postcomposition, and iterated map would definitionally commute with composition of functions. I guess a summary is that some = would have to be replaced by == (or use funext), while many others would be replaced by definitional equality.

I checked how the Coq standard library does it, and it uses the inductive family approach to defining vectors, which still has the property that nth doesn't definitionally commute with map.

The current approach isn't that bad, just requiring frequent use of rewrite entry_Build_Vector.