Stream: Beginner Questions

Topic: Trying to prove a complete induction

Alex Weisberger (Sep 13 2022 at 21:34):

I recently encountered a proof by complete induction in a book that I wanted to formalize using the less_induct induction rule. The proof is for a simple statement about terms in a programming language. Here's a stripped down version of the code and proof that exposes the issue that I'm seeing:

datatype small_term = suc small_term | zero

fun consts_st :: "small_term ⇒ small_term set" where
"consts_st zero = {zero}" |
"consts_st (suc t1) = consts_st t1"

fun size_st :: "small_term ⇒ nat" where
"size_st zero = 1" |
"size_st (suc t1) = (size_st t1) + 1"

fun depth_st :: "small_term ⇒ nat" where
"depth_st  zero = 1" |
"depth_st (suc t1) = (depth_st t1) + 1"

lemma "⟦depth_st t = d⟧ ⟹ card (consts_st t) ≤ size_st t"
proof (induction d rule: less_induct)
  case (less x)
  then show ?case
  proof (cases t)
    case (suc x1)
    then show ?thesis sorry
  next
    case zero
    then show ?thesis by simp
  qed
qed

The book suggests using the technique of using "induction on the depth of terms" to prove a property about all terms. Here, the property is that the number of constants in a term is always less than or equal to the size of the term (number of nodes in the AST).

The (suc x1) case is where I'm stuck. This case should be trivial to prove using the induction hypothesis, but since I'm in an inner proof the IH is not automatically present in the proof state at this point. So I tried explicitly assuming the IH:

proof (cases t)
    case (suc x1)
    from less.IH show ?thesis sorry

This brings the proof state at ?thesis to:

proof (prove)
using this:
  ?y < x ⟹ depth_st t = ?y ⟹ card (consts_st t) ≤ size_st t

goal (1 subgoal):
 1. card (consts_st t) ≤ size_st t

Because this case is inside of the outer complete induction case, I believe that ?y < x and depth_st t = ?y should already be known in this state, but they are not. Is there a way for me to pull in those facts into the inner proof?

Mathias Fleury (Sep 14 2022 at 04:15):

1. You are missing a generalization over t
2. You are missing the less.prems facts
3. from is not the same as with

Mathias Fleury (Sep 14 2022 at 04:15):

lemma "⟦depth_st t = d⟧ ⟹ card (consts_st t) ≤ size_st t"
proof (induction d arbitrary:t rule: less_induct)
  case (less x)
  then show ?case
  proof (cases t)
    case (suc x1)
    with less.IH less.prems show ?thesis by force
  next
    case zero
    then show ?thesis by simp
  qed
qed

Alex Weisberger (Sep 14 2022 at 12:25):

That’s exactly how I thought the proof should be written - thank you.

Is there any documentation about the rules that get introduced in cases like this? I forgot about less.prems, and I feel like there are other useful ones that get introduced that I don’t know about.

Lukas Stevens (Sep 14 2022 at 12:48):

The prems come from the premises that are piped into the inductive proof with using and the hyps are the assumptions of the inductive cases (i.e. they depend on the induction rule). The hyps should thus contain the IH (?). As for the .IH, I am not really sure.

Lukas Stevens (Sep 14 2022 at 13:36):

In any case, you can use print_theorems after case to see the theorems that are generated.

Last updated: Apr 24 2024 at 04:17 UTC