What is wrong with this Isabelle proof?

Question

This pattern generator produces a list with a given number at a given position, all other values are zero.

fun pattern_one_value :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat list" where
"pattern_one_value _   _    _   0   = []" |
"pattern_one_value pos pos1 val lng = 
    (if pos = pos1 then val else 0) # (pattern_one_value pos (pos1 + 1) val (lng - 1))"

The following lemma is aimed to prove that generated lists contain the right value at the given position.

lemma pattern_one_value_check [simp]: "∀pos val. pos < lng ⟹ pattern_one_value pos 0 val lng ! pos = val"
    proof(induct lng)
        case 0         then show ?case by simp
    next
        case (Suc lng) then show ?case by auto
    qed

It seems to be a correct proof; however, changing val in the cons expression of the generator function into an arbitrary number like (if pos = pos1 then 7 else 0) # ..., the proof still holds because both the base and the induction hypothesis are false. Where am I wrong? Thanks for any help.

user9716869 user9716869 · Accepted Answer · 2020-05-13T20:22:25

It seems to be a correct proof; however, changing val in the cons expression of the generator function into an arbitrary number like (if pos = pos1 then 7 else 0) # ..., the proof still holds because both the base and the induction hypothesis are false. Where am I wrong?

I believe that the problem is related to an attempt to treat HOL's universal quantifier ∀ as equivalent to Pure's universal quantifier ⋀. Effectively, it is possible to prove anything from the premise of the theorem pattern_one_value_check, as stated in your question. Indeed:

lemma pattern_one_value_check'[simp]:
  "(∀pos val::nat. pos < (lng::nat)) = False"
  by auto

lemma pattern_one_value_check''[simp]: 
  "(∀pos val::nat. pos < (lng::nat)) ⟹ P"
  by auto

I believe that you meant to use Pure's universal quantification in the statement of the theorem, e.g.

lemma pattern_one_value_check [simp]: 
  "⋀pos val. pos < lng ⟹ pattern_one_value pos 0 val lng ! pos = val"
proof(induct lng)
  case 0 then show ?case by simp
next
  case (Suc lng) then show ?case sorry
qed

In fact, even this is not necessary. The following theorem, once proven, will appear in the context as identical to the one stated above:

lemma pattern_one_value_check' [simp]: 
  "pos < lng ⟹ pattern_one_value pos 0 val lng ! pos = val"
proof(induct lng)
  case 0 then show ?case by simp
next
  case (Suc lng) then show ?case sorry
qed

If you seek a more detailed explanation, see Section 2.1 in Isar-ref and the document "Programming and Proving in Isabelle/HOL", both are part of the official documentation.

As a side note, I have to mention that, perhaps, there is an easier way to define pattern_one_value. In this case, the proof of pattern_one_value_check also seems to be easier:

definition pattern_one_value :: "nat ⇒ nat ⇒ nat ⇒ nat list"
  where "pattern_one_value val pos len = list_update (replicate len 0) pos val"

lemma pattern_one_value_check:
  assumes "pos < len" 
  shows "pattern_one_value val pos len ! pos = val"  
  using assms unfolding pattern_one_value_def
  apply(induct len)
  subgoal by auto
  subgoal by (metis length_replicate nth_list_update)
  done

What is wrong with this Isabelle proof?

1 Answers