## Stream: Proof Ground

### Topic: [PG 2019] Fold

#### Jakub Kądziołka (Jun 22 2021 at 23:15):

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?

#### Manuel Eberl (Jun 23 2021 at 09:30):

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
``````

#### Manuel Eberl (Jun 23 2021 at 09:30):

Actually, pretty sure it was Peter who wrote this.

Last updated: Dec 07 2023 at 16:21 UTC