-
Notifications
You must be signed in to change notification settings - Fork 193
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Define matrices as functions #1982
Comments
@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. |
It might still work out well, replacing 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 The current approach isn't that bad, just requiring frequent use of |
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.
The text was updated successfully, but these errors were encountered: