-
Notifications
You must be signed in to change notification settings - Fork 242
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
Added Z mod n as Fin #2073
Added Z mod n as Fin #2073
Conversation
I'm hoping that #1923 will soon be merged, after which it might be easier to consider the 'carry' case of successor/addition in terms of the |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Other things to think about:
_+ℕ_
also has a (admittedly trivial) left identity. We should have this proven.- How do these operations interact with addition of
ℕ
andℤ
? - Can you define a
_+ℤ_
? What laws does it have? - Is
_+_
associative? Commutative? It should be both. - Can you define a corresponding notion of multiplication modulo n? What laws does it have? When does that have an inverse?
src/Data/Fin/Mod.agda
Outdated
_+_ : Fin m → Fin n → Fin n | ||
i + j = toℕ i ℕ+ j | ||
|
||
_+‵_ : Fin n → Fin n → Fin n |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is this ever necessary over _+_
? A lot of the time Agda should be able to unify the two dimensions.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It could be necessary if someone wants a more restrictive version.
This is one example:
agda-stdlib/src/Function/Base.agda
Line 134 in 78e11bd
_∘′_ : (B → C) → (A → B) → (A → C) |
_+‵_ = _+_ | ||
|
||
_-_ : Fin n → Fin n → Fin n | ||
i - j = i + opposite j |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This suggests that opposite
is an inverse function for _+_
(which I agree it should be). Can you prove this?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Again, for a possible alternative (re-)definition of opposite
, see also #1923
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Now, it is with the alternative re-definition.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Except that there's still an asymmetry. _+_
has heterogeneous sizes but _-_
is homogeneous?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I made it assymmetric.
Thanks @Taneb for the reinforcement... I'd previously held off asking about proofs that |
I think I will wait for #1923 to be merged to redefine all my solutions. |
If you are going to wait for another PR to merge: suggest that you
Good luck, and thanks in advance! Something along these lines has been missing for a long time now. |
Would it be possible to prove one big theorem that any results that hold about ℤ under the mod n equivalence relation also hold of this |
@laMudri for that we'd need a definition of the mod n equivalence relation. I've been behind-the-scenes working on one but keep convincing myself I have the wrong definition for it. Currently working on one in terms of ring ideals - this would let us get, for example, the ring of polynomials over the integers modulo x^2 + x + 1 with the same code. But I don't think this PR needs to wait for that! |
PR #1923 now successfully merged. |
@jamesmckinna , I have already made the modifications to the code using #1923 . |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks @guilhermehas, I've done a little bit of refactoring and have a couple of more comments. I'll have another go over it at the start of next week.
Sorry it's taking so long, it's nearly there I think!
src/Data/Fin/Mod/Properties.agda
Outdated
+-identityʳ : .{{ _ : NonZero n }} → RightIdentity zeroFromNonZero _+_ | ||
+-identityʳ {suc n} i rewrite +ℕ-identityʳ {m = toℕ i} {n} _ = fromℕ<-toℕ _ (toℕ≤pred[n] _) | ||
|
||
induction : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This should be moved to a new file Data.Fin.Mod.Induction
(i.e. along the lines of https://github.com/agda/agda-stdlib/blob/master/src/Data/Fin/Induction.agda).
Also I think this proof should be strengthened. Surely this should hold for any exists j . P j
, not just P zero
?
src/Data/Fin/Properties.agda
Outdated
@@ -68,6 +68,9 @@ private | |||
nonZeroIndex : Fin n → ℕ.NonZero n | |||
nonZeroIndex {n = suc _} _ = _ | |||
|
|||
zeroFromNonZero : .⦃ _ : ℕ.NonZero n ⦄ → Fin n | |||
zeroFromNonZero {n = suc _} = zero |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Anyone have any bright ideas for what this could be called? @jamesmckinna etc?
It should also live in Data.Fin.Base
I think?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
So, the abandoned #1847 , tackling #1686 , called this concept "homogeneous zero" (and its friend "homogeneous successor", on the model of n : Nat, i : Fin n
being a 'homogeneous' telescope; of course, the {{NonZero n}}
precondition spoils things, but hey ;-)), and gave it the terrible name zero\'
in the PR.
👍 to its being in Data.Fin.Base
, as in that PR.
Better name(s): hzero
? zeroNZ
? zero⁺
?
I ran out of mental strength/inspiration working on that PR, and I find it slightly hard to revisit the discussion/thought processes again now...
src/Data/Fin/Mod.agda
Outdated
zero ℕ+ i = i | ||
suc n ℕ+ i = sucMod (n ℕ+ i) | ||
|
||
_+_ : Fin m → Fin n → Fin n |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you give me an example of a use-case of this operation? Seems a little unnatural to me adding together two numbers of different mods and arbitrarily returning the result mod the right one?
And why does _-_
return the result mod the left one?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Don't really know why I still have open review comments, but I've updated in response to @MatthewDaggitt 's comment, plus a new CHANGELOG
snafu I found.
src/Data/Fin/Mod.agda
Outdated
suc : Fin n → Fin n | ||
suc {ℕ.suc n} i with i ≟ fromℕ n | ||
... | yes _ = zero | ||
... | no i≢n = hs i≢n |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Consider the following alternative definition (which doesn't actually use the view; but simulates its effect, in the same way as the definition of Data.Fin.Base.opposite
:
suc : Fin n → Fin n
suc {n = ℕ.suc ℕ.zero} zero = zero
suc {n = ℕ.suc n@(ℕ.suc _)} zero = Fin.suc zero
suc {n = ℕ.suc n@(ℕ.suc _)} (Fin.suc i) with suc {n} i
... | zero = zero
... | j@(Fin.suc _) = Fin.suc j
for which one may then prove injectivity, and the view-related inversions, as follows:
suc[fromℕ]≡zero : ∀ n → suc (fromℕ n) ≡ zero
suc[fromℕ]≡zero ℕ.zero = refl
suc[fromℕ]≡zero (ℕ.suc n) rewrite suc[fromℕ]≡zero n = refl
suc[fromℕ]≡zero⁻¹ : (i : Fin (ℕ.suc n)) → (suc i ≡ zero) → i ≡ fromℕ n
suc[fromℕ]≡zero⁻¹ {n = ℕ.zero} zero _ = refl
suc[fromℕ]≡zero⁻¹ {n = ℕ.suc _} (Fin.suc i) _ with zero ← suc i in eq
= cong Fin.suc (suc[fromℕ]≡zero⁻¹ i eq)
suc[inject₁]≡suc[j] : (j : Fin n) → suc (inject₁ j) ≡ Fin.suc j
suc[inject₁]≡suc[j] zero = refl
suc[inject₁]≡suc[j] (Fin.suc j) rewrite suc[inject₁]≡suc[j] j = refl
suc[inject₁]≡suc[j]⁻¹ : (i : Fin (ℕ.suc n)) {j : Fin n} →
(suc i ≡ Fin.suc j) → i ≡ inject₁ j
suc[inject₁]≡suc[j]⁻¹ zero {zero} = λ _ → refl
suc[inject₁]≡suc[j]⁻¹ (Fin.suc i) {j} with suc i in eqᵢ
... | zero rewrite eqᵢ = λ ()
... | Fin.suc p rewrite eqᵢ = λ eq → begin
Fin.suc i ≡⟨ cong Fin.suc (suc[inject₁]≡suc[j]⁻¹ i eqᵢ) ⟩
inject₁ (Fin.suc p) ≡⟨ cong inject₁ (Fin.suc-injective eq) ⟩
inject₁ j ∎ where open ≡-Reasoning
suc-injective : {i j : Fin n} → suc i ≡ suc j → i ≡ j
suc-injective {n = n} {i} {j} eq with suc i in eqᵢ | suc j in eqⱼ
... | zero | zero
= trans (suc[fromℕ]≡zero⁻¹ i eqᵢ) (sym (suc[fromℕ]≡zero⁻¹ j eqⱼ))
... | Fin.suc p | Fin.suc q
= begin
i ≡⟨ suc[inject₁]≡suc[j]⁻¹ i eqᵢ ⟩
inject₁ p ≡⟨ cong inject₁ (Fin.suc-injective eq) ⟩
inject₁ q ≡⟨ sym (suc[inject₁]≡suc[j]⁻¹ j eqⱼ) ⟩
j ∎ where open ≡-Reasoning
src/Data/Fin/Mod.agda
Outdated
+-identityˡ : LeftIdentity {ℕ.suc n} zero _+_ | ||
+-identityˡ _ = refl | ||
|
||
+ℕ-identityʳ : ∀ {n′} (let n = ℕ.suc n′) → m ℕ.≤ n → toℕ (m ℕ+ zero {n}) ≡ m |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The proof of this seems very fiddly, but I admit I'm finding it harder to do better, even for the alternative definition of suc
. Hmmm...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is this lemma not also provable in the case n = ℕ.zero
? By inversion of the hypothesis m ℕ.≤ n
, we would obtain m = ℕ.zero
, and then the proof is simply refl
... or am I missing something?
UPDATED: it seems I might be, after banging my head against your proof for a while...
src/Data/Fin/Properties.agda
Outdated
@@ -68,6 +68,9 @@ private | |||
nonZeroIndex : Fin n → ℕ.NonZero n | |||
nonZeroIndex {n = suc _} _ = _ | |||
|
|||
zeroFromNonZero : .⦃ _ : ℕ.NonZero n ⦄ → Fin n | |||
zeroFromNonZero {n = suc _} = zero |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
So, the abandoned #1847 , tackling #1686 , called this concept "homogeneous zero" (and its friend "homogeneous successor", on the model of n : Nat, i : Fin n
being a 'homogeneous' telescope; of course, the {{NonZero n}}
precondition spoils things, but hey ;-)), and gave it the terrible name zero\'
in the PR.
👍 to its being in Data.Fin.Base
, as in that PR.
Better name(s): hzero
? zeroNZ
? zero⁺
?
I ran out of mental strength/inspiration working on that PR, and I find it slightly hard to revisit the discussion/thought processes again now...
CHANGELOG.md
Outdated
+ℕ-identityʳ-toℕ : m ℕ.≤ n → toℕ (m ℕ+ zero {n}) ≡ m | ||
+ℕ-identityʳ : ∀ m≤n → m ℕ+ zero ≡ fromℕ< (s≤s m≤n) | ||
+-identityʳ : .⦃ NonZero n ⦄ → RightIdentity zeroFromNonZero _+_ | ||
induction : ∀ P → P zero → (P i → P (sucMod i)) → ∀ i → P i |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think that this has now moved to Data.Fin.Mod.Induction
?
I added all of your suggestions if I am not missing anything. |
Having now worked extensively on #2257 (and using it to sketch an implementation of |
The library committee met, and decided that this is not the design that we wish to go with. Thank you very much for your efforts, but we regretfully must close this. |
In
Data.Integer.DivMod
, there are already some properties of Z mod n, but in this pull request, it is represented as Fin n.