Isabelle: Proof on difference between 2 lists

Question

I am new to theorem proving and Isabelle. I am trying to prove a simple(?) theorem in Isabelle about lists.

Here is the theory:

theory Scratch
imports
  Main
  Option
  String
begin

fun list_difference :: "string list => string list => nat"
where
  "list_difference [] [] = 0"
| "list_difference [] x = length x"
| "list_difference x [] = length x"
| "list_difference (x#d1) (y#d2) = (if (x=y) then  list_difference d1 d2 else (1 + list_difference d1 d2))"

fun modify :: "string list ⇒ nat ⇒ string list"
where
"modify list n = list[n:=''somethingnew'']"

These are the supporting lemmas

lemma diff_zero [simp]:
shows "list_difference somelist somelist = 0"
apply(induct_tac somelist, auto)
done

lemma sub1 [simp]:
shows "modify [] 0 = []"
apply(auto)
done

lemma diff_zero_basecase [simp]:
shows "list_difference somelist (modify somelist 0) <= 1"
apply(induct_tac somelist, auto)
done

This the original theorem I am trying to prove

(*Description : modify will change only one or zero elements.. so diff should be <= 1*) <br>
lemma modification_lemma [simp]:
shows "list_difference somelist (modify somelist index) ≤ 1"
apply(induct_tac somelist, auto)
apply(cases index, auto)
oops

How do I proceed to prove this theorem?

My other question is how to proceed from these kind of situations generally when trying to prove theorems? I tried following Isabelle tutorials but I was not able to get general advice on this.

Answer 1

I give you a proof, and explain some basic techniques I've used to get results, but in a fairly mindless way. Someone else may want to provide an explanation that will give you a better understanding of the subject matter: induction involving nat and list.

I shortened some identifiers, and I put the whole theory in below. There are basically two free variables that are in the formulas that need proving, ls and idx.

So, for proof goals, in trying things, I was doing a lot of what I show next, or some variation, with maybe cases for induct:

(*MINDLESS_TECHNIQUE_1*)
apply(induct ls, auto)
apply(induct idx, auto)

At a certain point, auto was taking a long time, which meant it was maybe looping bad because of the simp rules you had in.

I eliminated the simp rules and inserted them only where needed, which got rid of auto looping.

That was the first point of progress, which got me to MINDLESS_TECHNIQUE_2, breaking out proof goals into a lemma, to be used with MINDLESS_TECHNIQUE_1, along with Sledgehammer.

At this point, for your modification_lemma, after using apply like above, I had 3 proof goals, and I used Sledgehammer to prove two of them. I then broke out the 3rd proof goal as shown below, which was easily proved with by(induct ls, auto).

Update: Using Alexander's tip to get to the same proof goal as the broke-out lemma above, I've added a proof, in the source below, where I unwrap the two bound variables. It's still an ugly solution, so maybe there's a better way than ending up with bound variables.

Using auto or simp_all as I do, the reason I can't mindlessly get the final result with by(induct ls, auto) is because variables idx and ls are bound by a meta-all, !!. They need to be unwrapped if no auto tool can do the proof-job (I guess), which clutters things up a lot.

theory c2
imports Main Option String
begin

fun list_diff :: "string list => string list => nat" where
  "list_diff [] [] = 0"
 |"list_diff [] x = length x"
 |"list_diff x [] = length x"
 |"list_diff (x#d1) (y#d2) = 
   (if (x=y) then list_diff d1 d2 else (1 + list_diff d1 d2))"

fun modify :: "string list => nat => string list" where
  "modify ls n = ls[n := ''abc'']"

lemma diff_zero:
  "list_diff ls ls = 0"
by(induct_tac ls, auto)

lemma sub1:
  "modify [] 0 = []"
by(auto)

lemma diff_zero_basecase:
  "list_diff ls (modify ls 0) <= 1"
by(induct_tac ls, auto simp add: diff_zero)

(*****************************************************************************)
lemma the_mindless_result_of_eliminating_simp_rules_and_breaking_out_goals:
  "(!!a ls. list_diff ls (ls[idx := ''abc'']) <= Suc 0 ==>
     list_diff (a # ls) 
     (case idx of 0 => ''abc'' # ls | Suc j => a # ls[j := ''abc'']) <= Suc 0) 
   ==> list_diff ls (ls[Suc idx := ''abc'']) <= Suc 0 ==>
         list_diff ls (ls[idx := ''abc'']) <= Suc 0"
by(induct ls, auto)

lemma modification_lemma:
  "list_diff ls (modify ls idx) <= 1"
apply(induct ls, auto)
apply(induct idx, auto)
apply(metis diff_zero le0)
apply(metis diff_zero) (*The goal I broke out to the above lemma.*)
by (metis the_mindless_result_of_eliminating_simp_rules_and_breaking_out_goals)

(*****************************************************************************)
(*Update: After the third 'apply', I can't mindlessly do 'by(induct ls, auto)', 
  because variables 'ls' and 'idx' are bound by '!!. If I use 'auto' like I 
  did, and I don't want to break out the proof goal, I need to unwrap the 
  variables 'idx' and 'ls, as shown below.*)

lemma unwrapping_variables:
  "list_diff ls (modify ls idx) <= 1"
apply(induct ls, simp_all)
apply(induct idx, simp_all)
apply(simp_all add: diff_zero)
proof-
  fix idx
show "!!ls. ((!!a ls. list_diff ls (ls[idx := ''abc'']) <= Suc 0 ==>
     list_diff (a # ls) 
     (case idx of 0 => ''abc'' # ls | Suc j => a # ls[j := ''abc'']) <= Suc 0) 
   ==> list_diff ls (ls[Suc idx := ''abc'']) <= Suc 0 ==>
         list_diff ls (ls[idx := ''abc'']) <= Suc 0)"
  proof-
    fix ls
  show "(!!a ls. list_diff ls (ls[idx := ''abc'']) <= Suc 0 ==>
     list_diff (a # ls) 
     (case idx of 0 => ''abc'' # ls | Suc j => a # ls[j := ''abc'']) <= Suc 0) 
   ==> list_diff ls (ls[Suc idx := ''abc'']) <= Suc 0 ==>
         list_diff ls (ls[idx := ''abc'']) <= Suc 0"
    by(induct ls, auto)
  qed
qed

thm unwrapping_variables

end