Stream: Beginner Questions

Topic: recursive function proving

Salvatore Francesco Rossetta (Mar 25 2024 at 10:10):

Hi, I am writing a lemma (it's a simplified version of my real function, so don't mind the function itself too much)

fun func1:: "char list list ⇒ char list list ⇒ char list list" where
"func1 [] w = w" |
"func1 (px # p) w =
        func1 p (if px = ''y'' then (w @ [px])
                                   else w)"

lemma lemma1:
  fixes
    ps::"char list list" and
    sw::"char list list"
  assumes "px ∉ set sw"
  assumes "px ≠ ''y''"
  shows "px ∉ set (func1 ps sw)"
proof (induction ps)
  case Nil
  then show ?case using assms by simp
next
  case (Cons a ps)
  show ?case
  proof(cases "a = ''y''")
    case True
    have "func1 (a # ps) sw = func1 ps (if a = ''y'' then (sw @ [a])
                                   else sw)"
      by simp
    then have "... = func1 ps (sw @ [a])" using True by simp
    then have "px ∉ set (func1 ps sw @ [a])" ? ? ?
    then show ?thesis sorry
  next
    case False
    have "func1 (a # ps) sw = func1 ps (if a = ''y'' then (sw @ [a])
                                   else sw)" by simp
    then have "... = func1 ps sw" using False by simp
    then have "px ∉ set (func1 (a # ps) sw)"
      using assms local.Cons by simp
    then show ?thesis by simp
  qed

I should end the True case, where I get a list sw @ [a] different from the one of the IH (only sw). In the False case, since a is not appended, I easily managed to finish it. But how can I do it if my list is changing, even if I know that the thesis is holding (trivially, i know that px ∉ set (sw @ [a]))? Is the induction principle okay to prove the lemma or I have to change it? I hope I was clear

Manuel Eberl (Mar 25 2024 at 10:16):

You have to tell the induction method that sw is allowed to change during the induction, using the arbitrary parameter:

using assms
proof (induction ps arbitrary: sw)

Generally, when you want to prove something about a recursively-defined function defined with the fun/function command, it is best to use the induction rule that comes with the function, because that way the induction directly follows the recursion pattern of the function, which typically leads to much smoother proofs. In your case, the proof becomes fully automatic:

lemma lemma1:
  assumes "px ∉ set sw" and "px ≠ ''y''"
  shows "px ∉ set (func1 ps sw)"
  using assms by (induction ps sw rule: func1.induct) auto

Manuel Eberl (Mar 25 2024 at 10:17):

Note however that it's important to chain the assumptions into the induction as well (at least the first one), since it contains sw and sw is allowed to change. If you don't do that, you will have the assumption px ∉ set sw for the "old" value of sw, but inside your induction you will be talking about a different sw, so it won't work.

Manuel Eberl (Mar 25 2024 at 10:19):

Also, it is usually not necessary to use explicit fixes declarations and give type annotations for all the variables in your theorem. Usually, type inference can figure it all out. Annotations are only necessary when you want to restrict polymorphism. Or sometimes you need fixes declarations if you use defines declarations as well.

Manuel Eberl (Mar 25 2024 at 10:21):

Also note that you can prove something much stronger about your function, namely lemma "func1 ps sw = sw @ filter (λx. x = ''y'') ps".

Last updated: Apr 28 2024 at 08:19 UTC