# Re: [isabelle] coinduct_upto for coinductive predicates

```Hi guys,

Nice uniform description, Andreas!  We should have this for friends and other "up-to" operators at some point.

(Coq has a tool for "up-to" coinduction called Paco -- they are ahead of us on coinduction but behind us corecursion.)

Btw, here is my more ad hoc solution, which also illustrates the currently available friend structural corecursion -- theory also attached. Please pardon my unpolished scripts. Essentially, I follow "s" wherever it unfolds, which suggests a generalization.

corec s_gen :: "int â int stream" where
"s_gen i = i ## g (s_gen i)"

inductive gs :: "int stream  â bool" where
s_gen: "i â 0 â gs (s_gen i)"
|g: "gs xs â gs (g xs)"

(* Can use the existing structural friend corecursion here: *)
lemma s_gen_s: "s = s_gen 0"
proof-
{fix xs ys assume "xs = s â ys = s_gen 0" hence "xs = ys"
apply (coinduct rule: s_gen.corec.coinduct)
using s.unique s_gen.code s_gen.cong_refl by force
}
thus ?thesis by auto
qed

lemma gs_shd:
assumes "gs xs" shows "shd xs â 0"
using assms apply (induct) by (subst s_gen.code) auto

lemma gs_stl:
assumes "gs xs" shows "gs (stl xs)"
using assms apply (induct)
by (subst s_gen.code) (auto intro: gs.intros)

lemma P_gs: assumes "gs xs" shows "P xs"
using assms proof (coinduct rule: P.coinduct)
case (P xs)
thus ?case proof cases
case (s_gen i) thus ?thesis apply(intro exI[of _ "g (s_gen i)"] exI[of _ i])
apply simp apply (subst s_gen.code) by (auto intro: gs.intros)
next
case (g xss) thus ?thesis
apply(intro exI[of _ "g (stl xss)"] exI[of _ "shd xss + 1"])
apply simp apply (subst g.code)
by (auto intro: gs.intros  gs_stl simp: gs_shd)
qed
qed

lemma P_s: "P s"
by (simp add: s_gen s_gen_s  P_gs)

Best,

Andrei

________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
Sent: 07 November 2016 11:35
To: Manuel Eberl; cl-isabelle-users at lists.cam.ac.uk
Subject: Re: [isabelle] coinduct_upto for coinductive predicates

Hi Manuel,

You have to manually derive a coinduction up-to rule for your coinductive predicates.
BNF_Corec only proves coinduction up-to rules for equality. User-defined predicates are
not supported and probably will not be in the foreseeable future, because one would need a
lot of properties of the predicate. I've sketched the derivation of such an coinduction
up-to rule for your unary predicate P and the friend g below. It roughly corresponds to
what the BNF_Corec package does internally. Basically, you first define a closure operator
for the set of friends that you are interested in and then prove the upto rule by
coinduction with a nested induction on the closure.

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

lemma P_coinduct_upto_g:
assumes *: "X xs"
and step: "âxs. X xs â âx xs'. xs = x ## xs' â g_closure X xs' â 0 â x"
shows "P xs"
proof -
from * have "g_closure X xs" by(rule g_closure.intros)
then show ?thesis
proof(coinduction arbitrary: xs)
case (P xs)
then have "âx xs'. xs = x ## xs' â g_closure X xs' â 0 â x"
proof induction
case (embed xs)
from step[OF embed] show ?case by(auto)
next
case (step xs)
then show ?case
by(subst g.code)(auto intro: g_closure.step)
qed
then show ?case by blast
qed
qed

1. This rule is somewhat weaker than P.coinduct, because I've omitted the case "\/ P xs'",

from * have "g_closure X xs" by(rule g_closure.intros)

with

from * have "g_closure (%xs. X xs \/ P xs) xs" by(rule g_closure.intros)

2. You may want to include SCons as another intro rule for g_closure such that SCons is
treated as a friend. The problem there is that SCons does not in general preserve the
coinductive predicate P, but only if the new head is non-negative. That means that you
need a separate closure predicate for every coinductive predicate. This is also one of the
reasons why there's no support for user-defined coinductive predicates yet.

3. If you use friends in the context of the constructor guard for your corecursive
definitions, then you want to have an even stronger coinduction rule, namely

lemma P_coinduct_upto_g:
assumes *: "X xs"
and step: "âxs. X xs â
g_closure (%xs. âx xs'. xs = x ## xs' â g_closure X xs' â 0 â x) xs"
shows "P xs"

You can derive that one from mine above by another induction.

Hope this helps,
Andreas

On 07/11/16 10:52, Manuel Eberl wrote:
> Hallo,
>
> I have a coinductive predicate P and I want to show that "P s" holds, where "s" is a
> corecursively-defined stream whose definition uses a friendly function, i.e. something
> like "s = 0 ## g s" where g is friendly. (see also attached theory)
>
> The problem is that P.coinduct then only allows me to use "P s" in the coinduction proof,
> but I need "P (g s)". I suppose what I really need here is something like "coinduction up
> to friends for coinductive predicates"; from what I read, something like this is already
> available for "normal" coinduction w.r.t. equality.
>
> How do I do something like this? (my actual coinductive predicate is, of course, much more
> complicated than this, so working with "normal" coinduction w.r.t. equality is not an option)
>
> Cheers,
>
> Manuel
>

```

Attachment: Test.thy
Description: Test.thy

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