Stream: Beginner Questions

Topic: "using assms"

Maximilian Vollath (Jun 13 2024 at 15:34):

Most proofs have the line "using assms" in the definition of the lemma. But just for my understanding, how can I refer to the assumptions if I don't use this line, when the context is modified? Here's an example. (The function merge_distinct_aux merges two lists xs and acc while skipping over duplicate elements. The auxiliary variable seen keeps track of the elements that were already seen and typically "seen = set acc".)

This works:

lemma merge_distinct_aux_distinct:
  assumes "distinct acc" and "set acc ⊆ seen"
  shows "distinct (merge_distinct_aux xs seen acc)"
  using assms
proof (induct xs arbitrary: acc seen)
  case Nil
  thus ?case by simp

But if I remove "using assms" and move it here "thus ?case using assms by simp", it doesn't work because acc is arbitrary now. If I remove the arbitrary statement, this part of the proof works again. But is there a proper way to refer to the assumptions if I keep arbitrary?

lemma merge_distinct_aux_distinct:
  assumes "distinct acc" and "set acc ⊆ seen"
  shows "distinct (merge_distinct_aux xs seen acc)"
proof (induct xs)
  case Nil
  thus ?case using assms by simp

Yong Kiam (Jun 13 2024 at 15:36):

I would suggest first to look carefully at what you get out of the induction here.

when you write using assms in this context, you're actually carrying out a very different induction (where assms is part of IH that you will need to prove)

  using assms
proof (induct xs arbitrary: acc seen)

Maximilian Vollath (Jun 13 2024 at 15:46):

Oooooh now it makes sense to me, thank you, I see the difference in the output. And I thought it was just a simplification so you wouldn't have to reference the assumptions every time.

So what is the difference to defining the lemma like so then?
"⟦ distinct acc; set acc ⊆ seen ⟧ ⟹ distinct (merge_distinct_aux xs seen acc)"

Yong Kiam (Jun 13 2024 at 15:46):

I think that's identical to both lemmas

Yong Kiam (Jun 13 2024 at 15:48):

oh wait no sorry, that's identical to this:

lemma foo:
shows   "distinct acc ⟹ set acc ⊆ seen ⟹ distinct (merge_distinct_aux xs seen acc)"

which is almost the same as baking in using assms directly

Maximilian Vollath (Jun 13 2024 at 16:07):

Alright, thank you!

Last updated: Dec 21 2024 at 16:20 UTC