attribute [class] nat.prime in data.padics.padic_norm has awkward side effects
#1601
Labels
Comments
|
There is another option. I haven't thought it through yet, but I'd love to see it smashed to pieces. Crazy idea: We throw away the |
|
Just realized I never commented on this, and should, because I'm guilty of introducing
|
|
I think I agree with your suggested order. If nobody beats me to it, I might start the refactor in two weeks time. |
Closed
7 tasks
|
#2511 is my attempt to address this issue. It doesn't touch the padics yet, but that would be the immediate next step. |
bors bot
pushed a commit
that referenced
this issue
Apr 24, 2020
…c search (#2511) This PR introduces the class `fact P := P` for `P : Prop`, which is a way to inject elementary propositions into the type class system. This desing is inspired by @cipher1024 's https://gist.github.com/cipher1024/9bd785a75384a4870b331714ec86ad6f#file-zmod_redesign-lean. We use this to endow `zmod p` with a `field` instance under the assumption `[fact p.prime]`. As a consequence, the type `zmodp` is no longer needed, which removes a lot of duplicate code. Besides that, we redefine `zmod n`, so that `n` is a natural number instead of a *positive* natural number, and `zmod 0` is now definitionally the integers. To preserve computational properties, `zmod n` is not defined as quotient type, but rather as `int` and `fin n`, depending on whether `n` is `0` or `(k+1)`. The rest of this PR is adapting the library to the new definitions (most notably quadratic reciprocity and Lagrange's four squares theorem). Future work: Refactor the padics to use `[fact p.prime]` instead of making `nat.prime` a class in those files. This will address #1601 and #1648. Once that is done, we can clean up the mess in `char_p` (where the imports are really tangled) and finally get some movement in #1564.
|
#2519 has now been merged, so I consider this issue fixed. |
anrddh
pushed a commit
to anrddh/mathlib
that referenced
this issue
May 15, 2020
…c search (leanprover-community#2511) This PR introduces the class `fact P := P` for `P : Prop`, which is a way to inject elementary propositions into the type class system. This desing is inspired by @cipher1024 's https://gist.github.com/cipher1024/9bd785a75384a4870b331714ec86ad6f#file-zmod_redesign-lean. We use this to endow `zmod p` with a `field` instance under the assumption `[fact p.prime]`. As a consequence, the type `zmodp` is no longer needed, which removes a lot of duplicate code. Besides that, we redefine `zmod n`, so that `n` is a natural number instead of a *positive* natural number, and `zmod 0` is now definitionally the integers. To preserve computational properties, `zmod n` is not defined as quotient type, but rather as `int` and `fin n`, depending on whether `n` is `0` or `(k+1)`. The rest of this PR is adapting the library to the new definitions (most notably quadratic reciprocity and Lagrange's four squares theorem). Future work: Refactor the padics to use `[fact p.prime]` instead of making `nat.prime` a class in those files. This will address leanprover-community#1601 and leanprover-community#1648. Once that is done, we can clean up the mess in `char_p` (where the imports are really tangled) and finally get some movement in leanprover-community#1564.
anrddh
pushed a commit
to anrddh/mathlib
that referenced
this issue
May 16, 2020
…c search (leanprover-community#2511) This PR introduces the class `fact P := P` for `P : Prop`, which is a way to inject elementary propositions into the type class system. This desing is inspired by @cipher1024 's https://gist.github.com/cipher1024/9bd785a75384a4870b331714ec86ad6f#file-zmod_redesign-lean. We use this to endow `zmod p` with a `field` instance under the assumption `[fact p.prime]`. As a consequence, the type `zmodp` is no longer needed, which removes a lot of duplicate code. Besides that, we redefine `zmod n`, so that `n` is a natural number instead of a *positive* natural number, and `zmod 0` is now definitionally the integers. To preserve computational properties, `zmod n` is not defined as quotient type, but rather as `int` and `fin n`, depending on whether `n` is `0` or `(k+1)`. The rest of this PR is adapting the library to the new definitions (most notably quadratic reciprocity and Lagrange's four squares theorem). Future work: Refactor the padics to use `[fact p.prime]` instead of making `nat.prime` a class in those files. This will address leanprover-community#1601 and leanprover-community#1648. Once that is done, we can clean up the mess in `char_p` (where the imports are really tangled) and finally get some movement in leanprover-community#1564.
cipher1024
pushed a commit
to cipher1024/mathlib
that referenced
this issue
Mar 15, 2022
…c search (leanprover-community#2511) This PR introduces the class `fact P := P` for `P : Prop`, which is a way to inject elementary propositions into the type class system. This desing is inspired by @cipher1024 's https://gist.github.com/cipher1024/9bd785a75384a4870b331714ec86ad6f#file-zmod_redesign-lean. We use this to endow `zmod p` with a `field` instance under the assumption `[fact p.prime]`. As a consequence, the type `zmodp` is no longer needed, which removes a lot of duplicate code. Besides that, we redefine `zmod n`, so that `n` is a natural number instead of a *positive* natural number, and `zmod 0` is now definitionally the integers. To preserve computational properties, `zmod n` is not defined as quotient type, but rather as `int` and `fin n`, depending on whether `n` is `0` or `(k+1)`. The rest of this PR is adapting the library to the new definitions (most notably quadratic reciprocity and Lagrange's four squares theorem). Future work: Refactor the padics to use `[fact p.prime]` instead of making `nat.prime` a class in those files. This will address leanprover-community#1601 and leanprover-community#1648. Once that is done, we can clean up the mess in `char_p` (where the imports are really tangled) and finally get some movement in leanprover-community#1564.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
A side effect of making
nat.primeinto a class is that you can no longer revert anat.prime phypothesis that came from the left of the colon, or (more likely) revertpitself, in order tosubstit, for example.data.padics.padic_normhasattribute [class] nat.prime, so that the primality ofpcan be taken as a type class argument to most of the functions in the file. But this means that if, for example, you importdata.padics.padic_normindata.zmod.quadratic_reciprocity, then some of the proofs there will break because they rely onsubsting parameters that are known to be prime. Now adding that import is not that likely, but it could happen (#1564) that some random module thatdata.zmod.quadratic_reciprocityimports gains an import of something else that importsdata.padics.padic_norm. It's probably possible to refactor things in this case to avoid the problematic transitive import, but that just pushes the issue down the road.Two obvious possible solutions:
local attribute [class] nat.primeindata.padics.padic_norm, and make its users do the same.attribute [class] nat.primeby moving it to the definition ofnat.prime, and fix all the proofs that break as a result.The text was updated successfully, but these errors were encountered: