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

A few more comments:

1. This rule is somewhat weaker than P.coinduct, because I've omitted the case "\/ P xs'", which coinductive automatically adds. You can re-add it if you replace

  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)

and adjust the proof accordingly.

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





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