CODEWITHSUNDEEP
isabellecoinduction
david streader
david streader

Reputation: 589

in isabelle what format of goal is required to pertorm coinduction

Hi I am a novice trying to learn how to use coinduction in isabelle. I have been looking at HOL/Datatype_Examples/Process.thy (Andrei Popescu) 2012. As 2019 Isabelle is much improved (and not because of any personal skill) I have simplified the proof but still can not understand why they decided to make the first step.

The working simplified proof is

lemma solution_PROC[simp]: "solution sys (PROC p) = p"
proof-
  {fix q assume "q = solution sys (PROC p)" (* How did they know to do this! *)
   hence "p = q"
   proof (coinduct rule: process.coinduct)
     case (Eq_process process process')
     then show ?case
       by simp 
   qed
 }
  thus ?thesis by metis
qed

My failed naive approach was:

lemma solution_PROCFail: " p  = solution sys (PROC p)"
proof (coinduct rule: process.coinduct) (* look up  process.coinduct and 
            you can see the extra goal forced by the misalignment*)  
  case Eq_process
  then show ?thesis  (* cannot solve*)
qed

Two questions:

  1. is the syntax {fix q assume "q = solution sys (PROC p)" .....} old syntax for a local lemma?

And more importantly 2. How will I know when to try this technique?

many thanks david

Upvotes: 2

Views: 107

Answers (1)

Mathias Fleury
Mathias Fleury

Reputation: 2261

  1. The syntax is equivalent to

    have ‹p = q› if ‹q = solution sys (PROC p)› for q
  using that by (coinduct rule: process.coinduct) simp

in

{fix q assume "q = solution sys (PROC p)" (* How did they know to do this! *)
   hence "p = q"
   proof (coinduct rule: process.coinduct)
     case (Eq_process process process')
     then show ?case
       by simp 
   qed
 }

{} opens a new block (with locales variables and locale assumptions), and assume introduces a local assumption. The blocks exports a theorem of the form ?q2 = solution sys (PROC p) ⟹ p = ?q2.

You should probably read an Isar tutorial (like the Concrete Semantics, not the isar-ref) to know about these very useful constructs.

  1. The idea is that you need an assumption that involves the coinductive predicate. I would describe the technique as a standard work-around in Isabelle, since (co)induction sometimes looses links between variables.

  2. lemma solution_PROCFail: " p  = solution sys (PROC p)"
proof (coinduct rule: process.coinduct) (* look up  process.coinduct and 
        you can see the extra goal forced by the misalignment*)  
  case Eq_process
  then show ?thesis  (* cannot solve*)
qed

fails because the case/show generated is garbage (that happens, look at the state panel).

Upvotes: 1

Related Questions