Closed vikraman closed 10 months ago
Running into problems proving
Free
forCList
because of termination checking when I need to rewrite some terms withp
andq
when I am defining sharp forcomm
. Probably better if I proveFree
forSList
first, and transport the proof fromSList
toCList
I'm surprised, since you can prove swap from comm, and the proof of freeness should follow from just that, if you can show that SList is free. Maybe better to try and prove freeness for SList first.
Running into problem proving SList
's sharp is a homomorphism, Agda won't normalize stuff and I couldn't work it out, so I deleted everything and am trying to current strategy:
toFree
from SList
to FreeCMon
toFree
is a homsharp f
as FreeCMon.sharp f . toFree
sharp
is a homI guess we would need to prove two hom f
and g
would imply f . g
is a hom, hopefully this shouldn't be too hard to prove??
Running into problem proving
SList
's sharp is a homomorphism, Agda won't normalize stuff and I couldn't work it out, so I deleted everything and am trying to current strategy:1. Define a hom `toFree` from `SList` to `FreeCMon` 2. Prove `toFree` is a hom 3. Define `sharp f` as `FreeCMon.sharp f . toFree` 4. Prove `sharp` is a hom
I guess we would need to prove two hom
f
andg
would implyf . g
is a hom, hopefully this shouldn't be too hard to prove??
Yes homs are closed under composition, but I don't get why we need to do this?? Going to FreeCMon should be as hard as going to an arbitrary algebra Y, I'll play around with the code later tonight to see what the problem is.
Running into problem proving
SList
's sharp is a homomorphism, Agda won't normalize stuff and I couldn't work it out, so I deleted everything and am trying to current strategy:1. Define a hom `toFree` from `SList` to `FreeCMon` 2. Prove `toFree` is a hom 3. Define `sharp f` as `FreeCMon.sharp f . toFree` 4. Prove `sharp` is a hom
I guess we would need to prove two hom
f
andg
would implyf . g
is a hom, hopefully this shouldn't be too hard to prove??Yes homs are closed under composition, but I don't get why we need to do this??
When trying to prove sharp is a hom you get this hole 𝔜 .algebra (M.⊕ , (λ x₁ → i x₁ ♯)) ≡ (𝔉 .algebra (M.⊕ , i) ♯)
, it is not obvious how this would be done since you would have to deal with (λ x₁ → i x₁ ♯)
not being normalized I think?
Going to FreeCMon should be as hard as going to an arbitrary algebra Y, I'll play around with the code later tonight to see what the problem is.
It simplifies the definition of sharp a lot because I don't need to write a bunch of lemmas to convert from 𝔜 .algebra
to sharp
and vice versa. I'm currently running into some termination checking problem trying to prove toFree
is a hom right now but so far things are looking much cleaner.
Ok, the direct proof is this: https://github.com/vikraman/generalised-species/blob/master/set/MSet/Universal.agda#L77
Maybe first we need to cleanup all the noise coming from lookup and lists, using the dsl we tried to make in our last meeting? That will make the content of these lemmas clear...
What about lists and free monoids, does that also require going through freeMon
?
What about lists and free monoids, does that also require going through
freeMon
?
I'm not sure, it should be possible to define it without going thru FreeMon
but it would be very tedious because we have to spam those sharp
lemmas.
I'd imagine it probably would look something like this if we don't use FreeMon
: https://github.com/pufferffish/agda-symmetries/blob/3b2c0af334b0e7ec6578d43cc495f3403984e5eb/Cubical/Structures/Set/CMon/SList.agda
Running into problems proving
Free
forCList
because of termination checking when I need to rewrite some terms withp
andq
when I am defining sharp forcomm
. Probably better if I proveFree
forSList
first, and transport the proof fromSList
toCList