I am reading Software Foundations, chapter Logic. See here. There is an informal exercise that asks:
Are there any important properties of the function
forallbwhich are not captured by this specification?
Here are the relevant types:
forallb: (?X -> bool) -> list ?X -> bool All: (?T -> Prop) -> list ?T -> Prop forallb_true_iff: forall (X : Type) (test : X -> bool) (l : list X), forallb' test l = true <-> All (fun x : X => test x = true) l
I have proven this theorem with two variants of
forallb that process the list in either usual or reverse order. So, the order of evaluation is not captured.
- Is this the «important property» the book hints at?
- How hard would it be to formally prove that
forallbexactly up to the order of evaluation?