# 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
imports
Main
"~~/src/HOL/Library/BNF_Corec"
"~~/src/HOL/Library/Stream"
begin

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"
proof
fix xs assume "g_closure X xs"
thus "g_closure Y xs"
using assms by (induct) (auto intro: g_closure.intros)
qed

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

lemma g_closure_idem: "g_closure (g_closure X) = g_closure X"
proof-
{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)
qed

(* 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)
qed

lemma 1: (* Follows routinely from 3 *)
assumes "X ? F (g_closure X)"
shows "X ? gfp F"
proof-
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)
qed

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)

end

Andrei

________________________________
From: Manuel Eberl <eberlm at in.tum.de>
Sent: 08 November 2016 10:48
To: Andrei Popescu; cl-isabelle-users at lists.cam.ac.uk
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.

Cheers,

Manuel
```

Attachment: Test.thy
Description: Test.thy

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