Can you add logical operations for predicates?

[Atalay-Ileri]

As far as I can see, AND, OR, NOT and FORALL is missing for predicates. Can you add them so I can combine predicates?

[tchajed]

forall makes sense to me so I just added it. The other connectives are quite awkward to work with in separation logic, so I'd rather not have them in the library if there's no real support for using them. Why do you need them?

[pseudohuman92]

One simple example is possible results of a Write operation. If it fails, disk contents aft the given address stays the same, if it succeeds content changes.

If you don't want to include them, I can fork and extend the library. Automation may not be as good as native support but it can work.

[tchajed]

You can express that particular example within separation logic - exists! v', [v' = v0 \/ v' = v] * a |-> v' would be the postcondition of Write(a, v).

The types are all transparent, so you can actually just define your own connectives for predicates on top. You just have to wrap your predicate (of type (A -> option V) -> Prop) in the mkPred constructor.