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 22 2024 at 08:21 UTC