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