Conversation
Taneb
force-pushed
the
int-construction
branch
from
f0fafe4 to
5087388
Compare
| record _≃_ (i j : ℤ) : Set where | ||
| constructor mk≃ | ||
| field | ||
| eq : ℤ.minuend i ℕ.+ ℤ.subtrahend j ≡ ℤ.minuend j ℕ.+ ℤ.subtrahend i |
There was a problem hiding this comment.
First observation from Properties: use of sym to flip rewrites in the RHS of such equations... so suggest instead
| eq : ℤ.minuend i ℕ.+ ℤ.subtrahend j ≡ ℤ.minuend j ℕ.+ ℤ.subtrahend i | |
| eq : ℤ.minuend i ℕ.+ ℤ.subtrahend j ≡ ℤ.subtrahend i ℕ.+ ℤ.minuend j |
?
There was a problem hiding this comment.
The reason I did it this way was so that reflexivity is exactly refl. But you're right, that doesn't seem to be worth the tradeoff
| 1ℤ : ℤ | ||
| 1ℤ = 1 ⊖ 0 | ||
|
|
There was a problem hiding this comment.
Also:
| 1ℤ : ℤ | |
| 1ℤ = 1 ⊖ 0 | |
| 1ℤ : ℤ | |
| 1ℤ = 1 ⊖ 0 | |
| -1ℤ : ℤ | |
| -1ℤ = 0 ⊖ 1 |
There was a problem hiding this comment.
Easy enough, but does it pass the Fairbairn threshold? -1ℤ = - 1ℤ, after all
| infix 8 ⁻_ ⁺_ | ||
|
|
||
| ⁺_ : ℕ → ℤ | ||
| ⁺ n = n ⊖ 0 | ||
|
|
||
| ⁻_ : ℕ → ℤ | ||
| ⁻ n = 0 ⊖ n |
There was a problem hiding this comment.
The ⁻ symbol is in particular quite hard to discern as distinct form -. Would it be better to use Sign here (and reimplement the corresponding signAbs/SignAbs plumbing)?
There was a problem hiding this comment.
I mostly got annoyed at Agda not being able to tell if a section (x +_) was _+_ x or x (+_), so I wanted different symbols for them... the superscript-minus symbol is used in APL's number syntax for a negative, and that's what inspired the use of these here. I'm not attached to them, though.
| a ℕ.% n ℕ.+ 0 ≡⟨ ℕ.+-identityʳ (a ℕ.% n) ⟩ | ||
| a ℕ.% n ≡⟨ ℕ.m∸n+n≡m p ⟨ | ||
| a ℕ.% n ℕ.∸ b ℕ.% n ℕ.+ b ℕ.% n ∎ | ||
| ... | no b%n≰a%n = ≃-trans property′ $ mk≃ $ begin |
There was a problem hiding this comment.
Oh. Tempting to use a (Semi)Ring solver here?
There was a problem hiding this comment.
Do those work well when I'm using monus? Not that I ever really can manage to get them to work well for me...
| open import Data.Product.Base | ||
| open import Function.Base | ||
| open import Relation.Binary.PropositionalEquality | ||
|
|
There was a problem hiding this comment.
is it easier to derive each of these properties from the 'adjoint equivalence'/'graph relation' forms:
fromINT i ≡ j → i ≃ toINT j
i ≃ toINT j → fromINT i ≡ j(plus, perhaps, some additional lemmas to 'explain' these two graph relations)?
(I think even the congs follow from this, but I'd need to check that...)
There was a problem hiding this comment.
The second one is easy enough, it's hidden in my surjective proof. I'll have a go at the first one later.
As weak evidence that the congs don't follow from this: they're separate fields in the IsInverse structure in Function.Structures
JacquesCarette
left a comment
JacquesCarette
left a comment
There was a problem hiding this comment.
Some are requests for changes, some are suggestions.
I have quite a few more things I'd like simplified, but I feel that maybe I should do those myself as they require some level of experimenting.
| ... | yes _ = ℕ.≤-<-trans (ℕ.m∸n≤m (a ℕ.% n) (b ℕ.% n)) (ℕ.m%n<n a n) | ||
| ... | no b%n≰a%n = ℕ.∸-monoʳ-< {o = 0} (ℕ.m<n⇒0<n∸m (ℕ.≰⇒> b%n≰a%n)) (ℕ.≤-trans (ℕ.m∸n≤m (b ℕ.% n) (a ℕ.% n)) (ℕ.<⇒≤ (ℕ.m%n<n b n))) | ||
|
|
||
| property : a ⊖ b ≃ ⁺ remainder + quotient * ⁺ n |
There was a problem hiding this comment.
I wonder if we could do a giant "control inversion": the computation of remainder and quotient and this here property all do a case analysis on the same thing. Maybe we could case once and then return all 3 pieces of information?
| ; property = property | ||
| } | ||
| where | ||
| open ≡-Reasoning |
There was a problem hiding this comment.
Given that all of the reasoning below is done in a ℕ context and the +, *, etc of ℤ are never used, might it make sense to qualify ℤ and not ℕ instead? That would definitely shorten a lot of things.
| ((n ℕ.∸ (v ℕ.∸ w)) ℕ.+ x) ℕ.+ (v ℕ.+ (y ℕ.+ z)) ∎ | ||
| where | ||
| w = a ℕ.% n | ||
| x = a ℕ./ n ℕ.* n ℕ.+ b ℕ./ n ℕ.* 0 |
There was a problem hiding this comment.
can't the above proof be greatly simplified by first getting rid of those * 0 in x and y, and then reconstructing them later?
Also, isn't it the case that z + v = b ?
| fromINT-cong {a INT.⊖ b} {c INT.⊖ d} (mk≃ a+d≡c+b) = begin | ||
| a ⊖ b ≡⟨ m-n≡m⊖n a b ⟨ | ||
| + a - + b ≡⟨ cong (_- + b) (+-identityʳ (+ a)) ⟨ | ||
| (+ a + 0ℤ) - + b ≡⟨ cong (λ z → (+ a + z) - + b) (+-inverseʳ (+ d)) ⟨ |
There was a problem hiding this comment.
identity followed by inverse are exactly the (opposite direction) of the cancel lemmas.
| (+ a + 0ℤ) - + b ≡⟨ cong (λ z → (+ a + z) - + b) (+-inverseʳ (+ d)) ⟨ | ||
| (+ a + (+ d - + d)) - + b ≡⟨ cong (_- + b) (+-assoc (+ a) (+ d) (- + d)) ⟨ | ||
| (+ (a ℕ.+ d) - + d) - + b ≡⟨ cong (λ z → (+ z - + d) - + b) a+d≡c+b ⟩ | ||
| (+ (c ℕ.+ b) - + d) - + b ≡⟨ cong (_- + b) (+-assoc (+ c) (+ b) (- + d)) ⟩ |
There was a problem hiding this comment.
aren't these 2 lines some kind of middle4 ?
| (+ c + (+ b - + d)) - + b ≡⟨ cong (λ z → (+ c + z) - + b) (+-comm (+ b) (- + d)) ⟩ | ||
| (+ c + (- + d + + b)) - + b ≡⟨ cong (_- + b) (+-assoc (+ c) (- + d) (+ b)) ⟨ | ||
| ((+ c - + d) + + b) - + b ≡⟨ +-assoc (+ c - + d) (+ b) (- + b) ⟩ | ||
| (+ c - + d) + (+ b - + b) ≡⟨ cong₂ _+_ (m-n≡m⊖n c d) (+-inverseʳ (+ b)) ⟩ |
| pred : ℤ → ℤ | ||
| pred (a ⊖ b) = a ⊖ ℕ.suc b | ||
|
|
||
| 0ℤ : ℤ |
There was a problem hiding this comment.
I wonder if it would be useful to also have non-normalized 0 and 1, i.e. 0ℤn {n} = n ⊖ n with the n in the name being a super/sub-script? I think you are prematurely normalizing in places.
| ∣m+n-m+o∣≡∣n-o∣ zero n o = refl | ||
| ∣m+n-m+o∣≡∣n-o∣ (suc m) n o = ∣m+n-m+o∣≡∣n-o∣ m n o | ||
|
|
||
| ∣m+o-n+o∣≡∣m-n∣ : ∀ m n o → ∣ m + o - n + o ∣ ≡ ∣ m - n ∣ |
There was a problem hiding this comment.
maybe add parens in the lhs to make it easier to parse for humans?
|
The library always turns up surprising things: have you looked at |
|
Wow, I don't think I'd ever even noticed that module before! |
3 participants
Closes #2890 (eventually)
The proofs, while purely algebraic, are often very tedious, especially
*-cong.I've got basic arithmetic, ordering with addition, and divmod working!