Re: [isabelle] coinduct_upto for coinductive predicates

Hi Manuel,

I am sorry for the headache. But since you've come this far, I suggest giving the proof reuse idea another chance (at some point).  :-)

Here is what my previously stated facts (1)-(3) become for your simple example (theory also attached). The only considered operation here is g, but the closure can potentially have any set of operations (including the constant s). Notice how (3) is the mother of all interesting facts -- and how everything else is absolute routine. Looking into what most people call "the low level", e.g., the operators behind (co)inductive definitions, can be rewarding for reducing proof complexity.

theory Test

coinductive P :: "int stream ? bool" where
  "P xs ? x ? 0 ? P (x ## xs)"

definition F :: "(int stream ? bool) ? int stream ? bool" where
"F X xs ? ?xs' x. xs = x ## xs' ? X xs' ? x ? 0"

lemma F_mono: "mono F"
unfolding mono_def F_def by blast

(* Note: *) lemma P: "P = gfp F"
unfolding HOL.nitpick_unfold F_def ..

corec (friend) g :: "int stream ? int stream" where
  "g x = (shd x + 1) ## g (stl x)"

inductive g_closure ::
"(int stream ? bool) ? int stream ? bool" for X where
 embed: "X xs ? g_closure X xs"
|step: "g_closure X xs ? g_closure X (g xs)"

(* The following three facts are all trivial: *)
lemma g_closure_mono:
assumes "X ? Y"
shows "g_closure X ? g_closure Y"
  fix xs assume "g_closure X xs"
  thus "g_closure Y xs"
  using assms by (induct) (auto intro: g_closure.intros)

lemma g_closure_ext: "X ? g_closure X"
  by (auto intro: embed)

lemma g_closure_idem: "g_closure (g_closure X) = g_closure X"
  {fix xs assume "g_closure (g_closure X) xs"
   hence "g_closure X xs"
     by (induction) (auto intro: g_closure.intros)
  thus ?thesis
  by (simp add: antisym g_closure_ext predicate1I)

(* The *only* non-routine fact: *)
lemma 3: "g_closure (F X) ? F (g_closure X)"
proof clarify
  fix xs
  assume "g_closure (F X) xs"
  thus "F (g_closure X) xs"
  apply induct
  using F_def embed apply auto[1]
  by (smt F_def g.code g_closure.step stream.sel)

lemma 1: (* Follows routinely from 3 *)
assumes "X ? F (g_closure X)"
shows "X ? gfp F"
  note g_closure_mono[OF assms]
  also have "g_closure (F (g_closure X)) ? F (g_closure (g_closure X))"
  using 3 by simp
  also have "... = F (g_closure X)" unfolding g_closure_idem ..
  finally have "g_closure X ? F (g_closure X)" .
  with gfp_upperbound have "g_closure X ? gfp F" by auto
  thus ?thesis by(auto intro: g_closure.intros)

lemma P_coinduct_upto_g: (* is just the concrete version on 1 *)
assumes *: "X xs"
and step: "?xs. X xs ? ?xs' x. xs = x ## xs' ? g_closure X xs' ? x ? 0"
shows "P xs"
  using 1 assms unfolding P F_def using predicate1I by blast

(* Follows routinely from 1 and 3: *)
lemma g_closure_P: "g_closure P ? P"
unfolding P apply(rule 1) unfolding g_closure_idem
apply(subst gfp_unfold[OF F_mono]) using 3 .

(* An immediate consequence of g_closure_P *)
lemma 2: "P xs ? P (g xs)"
using g_closure_P by (auto intro: g_closure.intros)



From: Manuel Eberl <eberlm at>
Sent: 08 November 2016 10:48
To: Andrei Popescu; cl-isabelle-users at
Subject: Re: [isabelle] coinduct_upto for coinductive predicates

I think this probably answers my question.

I have decided not to look into this any further at the moment, seeing
as 1. it gives me a headache, 2. I have working proofs for now and 3.
I'm quite eager to continue my formalisation elsewhere.

Thanks a lot for your help (also to Andreas). I still have no idea what
I actually did with these closures, but the proofs went relatively
smoothly and everything works out.



Attachment: Test.thy
Description: Test.thy

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.