Add more Data.Rational.Properties#2996
Conversation
kleinreact
force-pushed
the
more-rational-properties
branch
from
0ab7060 to
e4da88b
Compare
| ↥p/↧p≡p (mkℚ -[1+ n ] d-1 prf) = cong (-_) (normalize-coprime prf) | ||
|
|
||
| ↥[i/1]≡i : (i : ℤ) → ↥ (i / 1) ≡ i | ||
| ↥[i/1]≡i i = begin |
There was a problem hiding this comment.
This feels like an awfully complicated proof for something so simple. I wonder if a "first principles" proof, by matching on i, would be simpler?
| where open ≡-Reasoning | ||
|
|
||
| ↧ₙ[i/1]≡1 : (i : ℤ) → ↧ₙ (i / 1) ≡ 1 | ||
| ↧ₙ[i/1]≡1 i = ℤ.+-injective $ begin |
There was a problem hiding this comment.
Possibly the same here.
| n/g≢0 = ℕ.≢-nonZero (ℕ.n/gcd[m,n]≢0 n n {{gcd≢0 = g≢0}}) | ||
|
|
||
| gcd[n,n]≡n : ∀ n → ℕ.gcd n n ≡ n | ||
| gcd[n,n]≡n n rewrite sym (ℕ.*-identityʳ n) |
There was a problem hiding this comment.
We tend not to use rewrite in stdlib. Also this lemma should go in to Data.Nat.GCD.
| p*g≢0 = ℕ.m*n≢0 p (ℕ.gcd qₙ r) | ||
|
|
||
| lemma : ∀ n → (p ℕ.* n) ℕ./ ℕ.gcd (p ℕ.* qₙ) (p ℕ.* r) ≡ n ℕ./ ℕ.gcd qₙ r | ||
| lemma n = trans (ℕ./-congʳ $ sym $ ℕ.c*gcd[m,n]≡gcd[cm,cn] p qₙ r) |
There was a problem hiding this comment.
an equational proof would be more readable here
| (ℕ.m*n/m*o≡n/o p n $ ℕ.gcd qₙ r) | ||
|
|
||
| proof : ∀ q → (+ p ℤ.* q) / (p ℕ.* r) ≡ q / r | ||
| proof (+ qₙ) rewrite sym (ℤ.pos-* p qₙ) = *-cancelˡ-/-helper qₙ |
There was a problem hiding this comment.
Please make these explicit instead of using rewrite
|
|
||
| ↥≡ : (↥ pᵢ ℤ.* ↧ qⱼ ℤ.+ ↥ qⱼ ℤ.* ↧ pᵢ) ℤ.* gcd[j,n] ℤ.* gcd[i,n] | ||
| ≡ (i ℤ.+ j) ℤ.* + n | ||
| ↥≡ rewrite ℤ.*-distribʳ-+ gcd[j,n] (↥ pᵢ ℤ.* ↧ qⱼ) (↥ qⱼ ℤ.* ↧ pᵢ) |
There was a problem hiding this comment.
most definitely needs to be done equationally!
| ------------------------------------------------------------------------ | ||
| -- Properties of _*_ and _/_ | ||
|
|
||
| *-cancelˡ-/ : ∀ p {q r} .{{_ : ℕ.NonZero r}} .{{_ : ℕ.NonZero (p ℕ.* r)}} → |
There was a problem hiding this comment.
Others may disagree, but I find this kind of quantification annoying, especially when you will have to explicitly plumb in the derived instance p≢0 immediately below.
I know that it is to ensure that the typechecker is OK with the well-formedness of (+ p ℤ.* q) / (p ℕ.* r), but I would personally find it more mathematically plausible (even if more ugly/unwieldy) to write
| *-cancelˡ-/ : ∀ p {q r} .{{_ : ℕ.NonZero r}} .{{_ : ℕ.NonZero (p ℕ.* r)}} → | |
| *-cancelˡ-/ : ∀ p {q r} .{{_ : ℕ.NonZero r}} .{{_ : ℕ.NonZero p}} (let instance _ = ℕ.m*n≢0 p r) → |
or even to lift all of this prefix out as part of a module _ ... declaration.
3 participants
I needed the following common properties over normalized rationals for some proofs, but found them to be missing in the library.
Hence, my proposal to add them with this PR.