*To*: 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 20:11:31 +0000*Accept-language*: en-GB, en-US*Authentication-results*: spf=none (sender IP is ) smtp.mailfrom=A.Popescu@mdx.ac.uk;*In-reply-to*: <8155fe9a-4580-292f-810b-3e83ea583b21@in.tum.de>*References*: <27160336-b7c8-8f83-117b-5258ea78da6e@in.tum.de> <2eac3394-b7da-ba90-7c18-0d4ad64145a5@inf.ethz.ch> <ffdc69e0-3dae-31d8-1452-91afb1a77fa2@in.tum.de> <AM3PR01MB1313214A7E11EF6FDE1308AAB7A70@AM3PR01MB1313.eurprd01.prod.exchangelabs.com>, <8155fe9a-4580-292f-810b-3e83ea583b21@in.tum.de>*Spamdiagnosticmetadata*: NSPM*Spamdiagnosticoutput*: 1:99*Thread-index*: AQHSONz1o/SKReAAJ0euxqjLWbQVXaDNZHMAgABc0ICAABlCEoAABmkAgAAHgqg=*Thread-topic*: [isabelle] coinduct_upto for coinductive predicates

OK, let me see if I understand what you have here. I will speak in terms of sets since it will be nicer for the concepts involved here (but it works the same for predicates). Essentially, you have a set of operations on a type T. (In your case, T is 'a llist * (real->real) * scale.) For any set X on that type, let Cl(X) be the closure of X under the operations. (This is essentially your ms_closure). You also have a predicate (is_expansion_aux) defined coinductively, i.e., as gfp F, where F : T set -> T set is a monotonic operator. Your up-to coinduction rule says: (1) For all X, X <= F (Cl X) implies X <= gfp F. On the other hand, you prove that "gfp F" is closed under each of the operations, i.e.: (2) for each n-ary operation f and all x, if x is in (gfp F)^n then "f x" is in "gfp F". And the question is whether you can use aspects of (1) to prove (2), as opposed to replicating proofs -- is this correct? I don't think (2) follows from (1). However, for proving (1) you typically need something stronger, namely (something at least as strong as) the following "distributive law": (3) For all X, Cl (F X /\ X) <= F (Cl X) (where /\ is intersection) So if from (1) you can extract (3) as a lemma, you can reuse (3) for proving (2): (2) is immediately implied by Cl (gfp F) <= gfp F, which in turn follows from (1) and (3): To prove Cl (gfp F) <= gfp F, by (1) it suffices that Cl (gfp F) <= F (Cl (Cl (gfp F))), i.e., Cl (gfp F) <= F (Cl (gfp F)). The last is true by (3): Cl (gfp F) = Cl (F(gfp F) /\ gfp F) <= F(Cl (gfp F)). I preferred to use an algebraic language since I find it clearest. Of course, for your concrete problem you will not have to invoke F explicitly, but inline everything inside (co)induction. Andrei ________________________________ From: Manuel Eberl <eberlm at in.tum.de> Sent: 07 November 2016 19:01 To: cl-isabelle-users at lists.cam.ac.uk Cc: Andrei Popescu Subject: Re: [isabelle] coinduct_upto for coinductive predicates Hallo Andrei, yes, but the new coinduction rule doesn't help with that; I can do the same proof using the old one: lemma P_s: assumes "P xs" shows "P( g xs)" using assms apply(coinduction arbitrary: xs) by (smt P.cases embed g.code stream.sel(1) stream.sel(2)) It is a bit difficult to illustrate my problem because my actual predicate is quite complicated, but the above minimal example is so trivial that it is difficult to see what my point is. Anyway, I attached my theory. The relevant coinductive predicate is "is_expansion_aux". The corresponding closure predicate is "ms_closure". The coinduct_upto theorem is "is_expansion_aux_coinduct_upto". Note that the coinduct_upto theorem contains a lengthy proof for the ms_closure_add case involving the friendly ms_plus_aux function. Later, when I want to prove "is_expansion_aux_add", I have to do pretty much the same proof again. I wonder if there is some way to get rid of that duplication. Cheers, Manuel

**Follow-Ups**:**Re: [isabelle] coinduct_upto for coinductive predicates***From:*Manuel Eberl

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

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

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

**Re: [isabelle] coinduct_upto for coinductive predicates***From:*Andrei Popescu

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

- Previous by Date: Re: [isabelle] coinduct_upto for coinductive predicates
- Next by Date: Re: [isabelle] Isabelle2016-1-RC1 processing theories twice
- 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