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
[Merged by Bors] - refactor(data/matrix/basic): work around leanprover/lean4#2042 #18696
Conversation
This adjust definitions such that everything is well-behaved in the case that things are unfolded. For each such definition, a lemma is added that replaces the equation lemma. While this just adds `_apply` noise in Lean 3, it is necessary when porting to Lean 4 as there the equation lemma is not generated in the way that we want.
LGTM. I think the procedure for searching for maintainer merge |
🚀 Pull request has been placed on the maintainer queue by j-loreaux. |
bors merge |
This adjust definitions such that everything is well-behaved in the case that things are unfolded. For each such definition, a lemma is added that replaces the equation lemma. Before this PR, we used ```lean def transpose (M : matrix m n α) : matrix n m α | x y := M y x ``` which has the nice behavior (in Lean 3 only) of `rw transpose` only unfolding the definition when it is of the applied form `transpose M i j`. If `dunfold transpose` is used then it becomes the undesirable `λ x y, M y x` in both Lean versions. After this PR, we use ```lean def transpose (M : matrix m n α) : matrix n m α := of $ λ x y, M y x -- TODO: set as an equation lemma for `transpose`, see mathlib4#3024 @[simp] lemma transpose_apply (M : matrix m n α) (i j) : transpose M i j = M j i := rfl ``` This no longer has the nice `rw` behavior, but we can't have that in Lean4 anyway (leanprover/lean4#2042). It also makes `dunfold` insert the `of`, which is better for type-safety. This affects * `matrix.transpose` * `matrix.row` * `matrix.col` * `matrix.diagonal` * `matrix.vec_mul_vec` * `matrix.block_diagonal` * `matrix.block_diagonal'` * `matrix.hadamard` * `matrix.kronecker_map` * `pequiv.to_matrix` * `matrix.circulant` * `matrix.mv_polynomial_X` * `algebra.trace_matrix` * `algebra.embeddings_matrix` While this just adds `_apply` noise in Lean 3, it is necessary when porting to Lean 4 as there the equation lemma is not generated in the way that we want. This is hopefully exhaustive; it was found by looking for lines ending in `matrix .*` followed by a `|` line
Pull request successfully merged into master. Build succeeded: |
This adjust definitions such that everything is well-behaved in the case that things are unfolded. For each such definition, a lemma is added that replaces the equation lemma. Before this PR, we used
which has the nice behavior (in Lean 3 only) of
rw transpose
only unfolding the definition when it is of the applied formtranspose M i j
. Ifdunfold transpose
is used then it becomes the undesirableλ x y, M y x
in both Lean versions. After this PR, we useThis no longer has the nice
rw
behavior, but we can't have that in Lean4 anyway (leanprover/lean4#2042). It also makesdunfold
insert theof
, which is better for type-safety.This affects
matrix.transpose
matrix.row
matrix.col
matrix.diagonal
matrix.vec_mul_vec
matrix.block_diagonal
matrix.block_diagonal'
matrix.hadamard
matrix.kronecker_map
pequiv.to_matrix
matrix.circulant
matrix.mv_polynomial_X
algebra.trace_matrix
algebra.embeddings_matrix
While this just adds
_apply
noise in Lean 3, it is necessary when porting to Lean 4 as there the equation lemma is not generated in the way that we want.This is hopefully exhaustive; it was found by looking for lines ending in
matrix .*
followed by a|
line