Proof of associativity law for type-level set
Asked Answered
U

0

3

I'm trying to prove that type-level function Union is associative, but I'm not sure how it should be done. I proved right identity and associativity laws for type-level append function and right identity for union:

data SList (i :: [k]) where
  SNil :: SList '[]
  SSucc :: SList t -> SList (h ': t)

appRightId :: SList xs -> xs :~: (xs :++ '[])
appRightId SNil       = Refl
appRightId (SSucc xs) = case appRightId xs of Refl -> Refl

appAssoc
  :: SList xs
  -> Proxy ys
  -> Proxy zs
  -> (xs :++ (ys :++ zs)) :~: ((xs :++ ys) :++ zs)
appAssoc SNil       _  _  = Refl
appAssoc (SSucc xs) ys zs = case appAssoc xs ys zs of Refl -> Refl

cong :: a :~: b -> f a :~: f b
cong Refl = Refl

unionRightId :: SList xs -> AsSet xs :~: Union xs '[]
unionRightId xs = case cong (appRightId xs) of Refl -> Refl

but I don't get how to prove that union is associative.

Unilateral answered 25/11, 2017 at 11:47 Comment(4)
Leaving aside convincing the compiler of your proof, do you know how to prove that the operation should be associative on paper? (And here I don't mean the mathematical "set union" operation, but the one actually defined here: doing a sort, then deduplicating. And of course the requisite lemma that the operation implemented by the name Sort is a sort.) For a complex proof like this, that seems like an absolutely critical first step.Prendergast
@DanielWagner is right, but I might go a bit further. Sorting is generally more complicated than merging, so you might be better off representing sets as sorted lists, with sortedness evidence.Heall
@DanielWagner I'm actually a noob in proving things. First two proofs I took from this answer and right identity proof is super easy, so I was able to prove it by myself. BTW my final goal is to have an indexed free monad, like the one in the linked answer, only with Sets instead of Lists.Unilateral
@Heall do you mean on value level (singleton)?Unilateral

© 2022 - 2024 — McMap. All rights reserved.