0

There seems to be something about inductive predicates I don't understand since I keep getting issues with them. My most recent struggle is to understand case analysis with inductively defined predicates on ev from chapter 5 of the concrete semantics books.

Assume I am proving 

lemma
  shows "ev n ⟹ ev (n - 2)"

I've tried to start the proof immediately in Isabelle/HOL but it complains when I try or gives weird goals:

lemma
  shows "ev n ⟹ ev (n - 2)"
proof (cases)

which shows:

proof (state)
goal (2 subgoals):
 1. ⟦ev n; ?P⟧ ⟹ ev (n - 2)
 2. ⟦ev n; ¬ ?P⟧ ⟹ ev (n - 2)

which is not what I expected.

When I pass n to cases we instead induct on the definition of natural numbers (note other times it does the induction on ev correctly, see later example):

lemma
  shows "ev n ⟹ ev (n - 2)"
proof (cases n)

gives:

proof (state)
goal (2 subgoals):
 1. ⟦ev n; n = 0⟧ ⟹ ev (n - 2)
 2. ⋀nat. ⟦ev n; n = Suc nat⟧ ⟹ ev (n - 2)

which is not what I expected. Note however that the following DOES work (i.e. it inducts on ev not on natural numbers) even with n as a parameter:

lemma
  shows "ev n ⟹ ev (n - 2)"
proof -
  assume 0: "ev n"
  from this show "ev (n - 2)"
  proof (cases n)

I realize that there must be some magic about assuming ev n first and then stating to show ev (n-2) otherwise the error wouldn't occur.

I understand the idea of rule inversion (of arriving at a given fact to be proven in reverse, by analysis the cases that could have lead to it). For the "even" predicate the rule inversion is:

ev n ==> n = 0 ∨ (∃k. n = Suc (Suc k) ∧ ev k)

which makes sense based on the inductively defined predicate:

inductive ev :: "nat ⇒ bool" where
ev0: "ev 0" |
evSS: "ev n ⟹ ev (Suc (Suc n))"

but I don't understand. Why wouldn't directly doing the cases work? or why is this syntax invalid:

proof (cases ev)

or this:

proof (cases ev.case)

etc.

I think the crux is that at the heart I don't know when dealing with inductively define predicates if this induction is applied to the goal or the assumption, but from the writing on of the textbook:

The name rule inversion emphasizes that we are reasoning backwards: by which rules could some given fact have been proved?

I'd assume it's applying rule inversion to the goals since it says "by which rules could some given fact have been proved".

In addition, this example ev ==> ev (n-2) froom the book does not help because both the premise and conclusion have ev involved.

How is case analysis with rule inversion really working and why do we need to assume things first for Isabelle to give sensible goal for case analysis?

Charlie Parker
  • 5,884
  • 57
  • 198
  • 323
  • why does `thm nat.cases` not show anything? I would have expected to see something like this for proving `P n`. Subgoal 1) `[| x=0 |] ==> P x` subgoal 2) `/\ k. x=k+1 ==> P x `. Why doesn't it show that? (or something similar to that) – Charlie Parker May 21 '20 at 18:29

2 Answers2

2

Not sure I understand the entire question but this:

lemma
  shows "ev n ⟹ ev (n - 2)"
proof (cases)

Gives you:

proof (state)
goal (2 subgoals):
 1. ⟦ev n; ?P⟧ ⟹ ev (n - 2)
 2. ⟦ev n; ¬ ?P⟧ ⟹ ev (n - 2)

because Isabelle is splitting on the truth of ev n, i.e. either true or false. I believe the syntax you are looking for is:

proof (cases rule: ev.cases)

Which is how you tell Isabelle explicitly what rule it should use for a proof by cases.

Zoey Sheffield
  • 108
  • 4
  • why does `thm nat.cases` not show anything? I would have expected to see something like this for proving `P n`. Subgoal 1) `[| x=0 |] ==> P x` subgoal 2) `/\ k. x=k+1 ==> P x `. Why doesn't it show that? (or something similar to that) – Charlie Parker May 21 '20 at 18:29
  • what is the point of the word cases in your command if `rule ev.cases` does the same thing? – Charlie Parker May 21 '20 at 18:44
  • As noted [here](https://stackoverflow.com/questions/61921839/why-cant-i-make-my-cases-explicit-in-isabelle-when-the-proof-is-already-complet) cases does do some simplification which rule doesn't. Its also easier to read IMO. – Zoey Sheffield May 21 '20 at 18:58
  • Ben, I think there is still something weird going on when only doing `cases` since it doesn't split into the actual cases of the rules. For the syntax `cases` to work by itself without the explicit `cases rule: ev.cases` syntax, Isabelle doesn't actually split the assumption properly (unless you do an `assume ev n` in this case). Why is it? How does `cases` decide what to split into cases and what cases is the crux of my original question. – Charlie Parker May 22 '20 at 19:34
1

The way to do it is as the answer Ben Sheffield said:

proof (cases rule: ev.cases)

I also noticed that:

apply (rule ev.cases)

works, but I think it would be helpful to go through a small example to see the cases explicitly outlined:

Consider:

lemma "ev n ⟹ ev (n - 2)"

first inspect it's cases theorem:

thm ev.cases
⟦ev ?a; ?a = 0 ⟹ ?P; ⋀n. ⟦?a = Suc (Suc n); ev n⟧ ⟹ ?P⟧ ⟹ ?P

then it unifies the goal and introduces the new goals with the original assumptions and all the assumption for the cases. That is why there is a ev n in all of them.

  apply (rule ev.cases)

has goals:

proof (prove)
goal (3 subgoals):
 1. ev n ⟹ ev ?a
 2. ⟦ev n; ?a = 0⟧ ⟹ ev (n - 2)
 3. ⋀na. ⟦ev n; ?a = Suc (Suc na); ev na⟧ ⟹ ev (n - 2)

and you can do simp and proceed the proof as normal.

Charlie Parker
  • 5,884
  • 57
  • 198
  • 323