Stream: Beginner Questions

Topic: Split if/case in induction rule

Christian Zimmerer (Apr 20 2024 at 13:48):

Say I have a function

fun f :: "'a list => 'a list" where
"f [] = []"
"f (x#xs) = (if P x then x # f (g xs) else x # f (h xs))"

How can I get an induction rule that creates individual cases for P x and ~P x respectively?

Manuel Eberl (Apr 20 2024 at 14:23):

You'll have to prove it yourself:

lemma f_induct [case_names Nil Cons1 Cons2]:
  assumes "Q []"
  assumes "⋀x xs. P x ⟹ Q (g xs) ⟹ Q (x # xs)"
  assumes "⋀x xs. ¬P x ⟹ Q (h xs) ⟹ Q (x # xs)"
  shows   "Q xs"
  using assms f.induct by metis

You can also prove such induction rules from scratch using the induction_schema tactic:

lemma f_induct [case_names Nil Cons1 Cons2]:
  assumes "Q []"
  assumes "⋀x xs. P x ⟹ Q (g xs) ⟹ Q (x # xs)"
  assumes "⋀x xs. ¬P x ⟹ Q (h xs) ⟹ Q (x # xs)"
  shows   "Q xs"
  using assms
  apply induction_schema
    using list.exhaust_sel apply blast
    apply (rule wf_measure[of length])
     apply auto
    done

Lastly, you can also write the function with explicit different cases from the beginning and the generated induction rule will be the one you want. The downside is that code generation will not work anymore (at least not by itself; you'll have to prove the original function definition as a separate code equation):

function f :: "'a list => 'a list" where
  "f [] = []"
| "P x ⟹ f (x#xs) = x # f (g xs)"
| "¬P x ⟹ f (x # xs) = x # f (h xs)"
  using list.exhaust_sel apply blast
  apply auto
  done
termination by lexicographic_order

thm f.induct

lemma f_code [code]:
  "f [] = []"
  "f (x # xs) = (if P x then x # f (g xs) else x # f (h xs))"
  by auto

Christian Zimmerer (Apr 20 2024 at 15:20):

Thank you very much. Sadly, it seems like this is not trivial for the function that I am working with, so I'll have to stick to the ugly induction scheme.

Yong Kiam (Apr 20 2024 at 16:12):

if you think you'll use the induction principle with the split cases multiple times, it might be worth proving it once and for all (first one @Manuel Eberl suggested)

Christian Zimmerer (Apr 23 2024 at 21:36):

I did it :>

Last updated: Dec 21 2024 at 16:20 UTC