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

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
>

Attachment: Test.thy
Description: Test.thy



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