I'm trying to do the "Fold" problem from Proof Ground 2019. I did the first 4/6 theorems, but I am confused as to what was intended. The description states:

Using the universal property, prove that

`filter`

and`fold_left`

can be rewritten as a fold.

However, I do not use the universal property for this at all. In fact, I am confused as to how it's useful. Instead, I simply instantiate the existentials manually:

```
lemma filter_with_fold:
fixes p :: "'a ⇒ bool"
shows "∃a g. (∀xs. filter p xs = foldr g xs a)"
apply (rule exI[of _ "[]"])
apply (rule exI[of _ "λx ys. if p x then x # ys else ys"])
apply (rule allI)
subgoal for xs
apply (induction xs)
by auto
done
```

Is it just poor wording of the problem, or is there a clever solution I'm not seeing?

Well, that's how *Sledgehammer Squad* did it (the team consisting of @Peter Lammich and me):

```
lemma filter_with_fold:
fixes p :: "'a ⇒ bool"
shows "∃a g. (∀xs. filter p xs = foldr g xs a)"
apply (rule exI[where x="[]"])
apply (rule exI[where x="λx xs. if p x then x#xs else xs"])
apply clarify
apply (rule universal_property_foldI2)
apply auto
done
```

Actually, pretty sure it was Peter who wrote this.

Last updated: Dec 07 2023 at 16:21 UTC