+Int≡+ #1028
+Int≡+ #1028
Conversation
| ℤ→Int+Int≡+ : ∀ (n m : ℤ) → (ℤ→Int n) +Int (ℤ→Int m) ≡ ℤ→Int (n + m) | ||
| ℤ→Int+Int≡+ (pos zero) m = | ||
| (ℤ→Int (pos zero)) +Int (ℤ→Int m) | ||
| ≡⟨ sym (pos0+ (ℤ→Int m)) ⟩ |
There was a problem hiding this comment.
I'd suggest indenting the reasoning lines with a different number of spaces to improve readability.
There was a problem hiding this comment.
Hm, I changed the formatting into something else entirely, because it felt nicer. Lemme know what you think and if you want a specific different one then tell me what it should be.
|
I also privated a lot of the PR after all, I think they are pretty irrelevant. |
| where | ||
| posℤ→Int+Int≡+ : ∀ (n : ℕ) (m : ℤ) → (ℤ→Int (pos n)) Int.+ (ℤ→Int m) ≡ ℤ→Int ((pos n) + m) | ||
| posℤ→Int+Int≡+ zero m = | ||
| (ℤ→Int (pos zero)) Int.+ (ℤ→Int m) ≡⟨ |
There was a problem hiding this comment.
That's too funky of a notation wrt. the rest of the library. I feel better with seperate lines for ≡ steps, with differing indentation. Also, it's not consistent with +'≡+
There was a problem hiding this comment.
Better now? Or is this not what you had in mind?
I also fixed the other series of equalities, I completely forgot it was there before. ^^"
| predℤ→Int (posneg i) = refl | ||
|
|
||
| ℤ→Int+Int≡+ : ∀ (n m : ℤ) → (ℤ→Int n) Int.+ (ℤ→Int m) ≡ ℤ→Int (n + m) | ||
| ℤ→Int+Int≡+ n m = (ℤelim (λ n → ∀ (m : ℤ) → (ℤ→Int n) Int.+ (ℤ→Int m) ≡ ℤ→Int (n + m)) posℤ→Int+Int≡+ negsucℤ→Int+Int≡+ n) m |
There was a problem hiding this comment.
I think a name containing something like 'IsHom+' would be better.
And then this fact should be exported as well (maybe even as an homomorphism of abelian groups - that might fit in better somewhere else though).
There was a problem hiding this comment.
Kinda related to the other comment – shouldn't we care about the equality (rather than homomorphism) of abelian groups, as in that the base sets are equal and the operations are equal? I believe we can recover a traditional homomorphism (well, iso-) from this quite easily and it seems conceptually simpler when they are literally equal.
I definitely might be missing some performance issues with this though, I have no idea how these work here.
Oh, to be clear, I am quite happy to change it, but I would also like to understand all this better and adjust my approach for the future. ^^"
There was a problem hiding this comment.
Just to be clear: The equality you proved is exactly the statement that the map ℤ→Int is a homomorphism with respect to +. As you suspect, the performance of a homomorphism proof extracted from an equality of groups is not going to be great, so we should export this one separately.
Regarding conventions, it would be better to turn the equality around. In general, we try to write equations like this in a "evaluating/simplifying/normalizing direction" (meaning f(x+y)=f(x)+f(y) for a homomorphism or x*(y+z)=x*y+x*z for distributivity). This is not a well defined term and there is no reason to do it this way -- it is just about having a convention people can remember.
There was a problem hiding this comment.
Right, the thing I wrote about "iso-" was just silly, sorry. Anyway, exported, renamed, and flipped.
I also rebased this, but in the meantime another thing got merged so that was a tad pointless.
|
Thanks! Looks all good to me now -> will merge if CI is happy. |
This is more of a warmup, since I actually want
·Int≡·(useful to proveQuoQ≡HITQI think?). But this might also prove useful to prove that, so no effort wasted.I'm aware of some problems with this, but I'm not sure how to fix them, so I'll be grateful for any comments.
asimports still cause conflicts I think?).Isoare ok or if there is a better way of doing a similar thing. Similarly, exportingisoIntℤmight be controversial?private, but I'm not sure what the best way of achieving this is –privateis kinda obvious, but I think I've also seen some unnamed modules? What should I do with this?