Re: [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



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