Continued Thoughts on Collections

[DavePearce]

This is a continuation of #236 (which was a continuation of #218).

With the further development of wycs into a standalone theorem prover, there are now some more interesting options available for handling collections. In essence, I now believe there are two competing solutions:

1) Have an underlying theory of sets, and build explicit quantified constraints on top of them. For example:

• Set Representation Base: {x,y} {= xs
• Map Representation Adds: forall { (i,x),(j,y) } in xs | x != y || i == j }
• List Representation Adds: forall { (i,x) in xs | 0 <= i && i < |xs| }

2) Have entirely separate theories for sets, maps and lists. For example:

• Set Representation: {x,y} {= xs
• Map Representation: {i=>x,j=>y} {= xs
• List Representation: [i=>x,j=>y] {= xs

The latter would then need some explicit rules for checking the explicit constraints from before. One of the difficulties with this approach is handling unions of collections properly [however, it is possible I think]. There would also be a fair amount of repetition between the rules for e.g. transitive closure, least upper bound, etc.

[DavePearce]

This is moot now since the verifier is being reworked.