*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, Manuel Eberl <eberlm at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] coinduct_upto for coinductive predicates*From*: Andrei Popescu <A.Popescu at mdx.ac.uk>*Date*: Mon, 7 Nov 2016 11:58:08 +0000*Accept-language*: en-GB, en-US*Authentication-results*: spf=none (sender IP is ) smtp.mailfrom=A.Popescu@mdx.ac.uk;*In-reply-to*: <2eac3394-b7da-ba90-7c18-0d4ad64145a5@inf.ethz.ch>*References*: <27160336-b7c8-8f83-117b-5258ea78da6e@in.tum.de>, <2eac3394-b7da-ba90-7c18-0d4ad64145a5@inf.ethz.ch>*Spamdiagnosticmetadata*: NSPM*Spamdiagnosticoutput*: 1:99*Thread-index*: AQHSONz1o/SKReAAJ0euxqjLWbQVXaDNZHMAgAACuok=*Thread-topic*: [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**

**References**:**[isabelle] coinduct_upto for coinductive predicates***From:*Manuel Eberl

**Re: [isabelle] coinduct_upto for coinductive predicates***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] yet another simplifier question
- Next by Date: [isabelle] Isabelle2016-1-RC2 cartouche vs quotation mark ML_file
- Previous by Thread: Re: [isabelle] coinduct_upto for coinductive predicates
- Next by Thread: Re: [isabelle] coinduct_upto for coinductive predicates
- Cl-isabelle-users November 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list