Email Gateway (Aug 22 2022 at 14:34): Email Gateway (Aug 22 2022 at 14:34):From: Manuel Eberl <eberlm@in.tum.de>
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
Test.thy
Email Gateway (Aug 22 2022 at 14:34):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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:
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.
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.
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
Email Gateway (Aug 22 2022 at 14:34):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
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
Test.thy
Email Gateway (Aug 22 2022 at 14:35):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
thanks for the explanation. I think I now managed to define the closure
that I need and prove the corresponding coinduct_upto rule.
I noticed that during the proof of this rule, I essentially needed to
prove that all the friendly functions in the closure preserve the
inductive predicate, i.e. in terms of the example theory from earlier, I
needed to prove some generalised version of "P s ==> P (g s)".
I then thought that once I have proven the coinduct_upto rule, I should
be able to easily derive the fact "P s ==> P (g s)" from that, but I
cannot see how. If I want to prove "P s ==> P (g s)", do I really have
to do all the proof work again?
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 14:35):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Manuel,
You can use Andreas's rule to prove that fact for any xs:
lemma P_s: assumes "P xs" shows "P( g xs)"
using assms apply(coinduction arbitrary: xs rule: P_coinduct_upto_g)
by (smt P.cases embed g.code stream.sel(1) stream.sel(2))
(and, of course, you can also use it to immediately prove P(s), your original motivation)
Andrei
Email Gateway (Aug 22 2022 at 14:35):From: Manuel Eberl <eberlm@in.tum.de>
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
Bar.thy
Email Gateway (Aug 22 2022 at 14:35):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
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
Email Gateway (Aug 22 2022 at 14:35):From: Manuel Eberl <eberlm@in.tum.de>
I think this probably answers my question.
I have decided not to look into this any further at the moment, seeing
as 1. it gives me a headache, 2. I have working proofs for now and 3.
I'm quite eager to continue my formalisation elsewhere.
Thanks a lot for your help (also to Andreas). I still have no idea what
I actually did with these closures, but the proofs went relatively
smoothly and everything works out.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 14:36):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Manuel,
I am sorry for the headache. But since you've come this far, I suggest giving the proof reuse idea another chance (at some point). :-)
Here is what my previously stated facts (1)-(3) become for your simple example (theory also attached). The only considered operation here is g, but the closure can potentially have any set of operations (including the constant s). Notice how (3) is the mother of all interesting facts -- and how everything else is absolute routine. Looking into what most people call "the low level", e.g., the operators behind (co)inductive definitions, can be rewarding for reducing proof complexity.
theory Test
imports
Main
"~~/src/HOL/Library/BNF_Corec"
"~~/src/HOL/Library/Stream"
begin
coinductive P :: "int stream ? bool" where
"P xs ? x ? 0 ? P (x ## xs)"
definition F :: "(int stream ? bool) ? int stream ? bool" where
"F X xs ? ?xs' x. xs = x ## xs' ? X xs' ? x ? 0"
lemma F_mono: "mono F"
unfolding mono_def F_def by blast
(* Note: *) lemma P: "P = gfp F"
unfolding HOL.nitpick_unfold F_def ..
corec (friend) g :: "int stream ? int stream" where
"g x = (shd x + 1) ## g (stl x)"
inductive g_closure ::
"(int stream ? bool) ? int stream ? bool" for X where
embed: "X xs ? g_closure X xs"
|step: "g_closure X xs ? g_closure X (g xs)"
(* The following three facts are all trivial: *)
lemma g_closure_mono:
assumes "X ? Y"
shows "g_closure X ? g_closure Y"
proof
fix xs assume "g_closure X xs"
thus "g_closure Y xs"
using assms by (induct) (auto intro: g_closure.intros)
qed
lemma g_closure_ext: "X ? g_closure X"
by (auto intro: embed)
lemma g_closure_idem: "g_closure (g_closure X) = g_closure X"
proof-
{fix xs assume "g_closure (g_closure X) xs"
hence "g_closure X xs"
by (induction) (auto intro: g_closure.intros)
}
thus ?thesis
by (simp add: antisym g_closure_ext predicate1I)
qed
(* The only non-routine fact: *)
lemma 3: "g_closure (F X) ? F (g_closure X)"
proof clarify
fix xs
assume "g_closure (F X) xs"
thus "F (g_closure X) xs"
apply induct
using F_def embed apply auto[1]
by (smt F_def g.code g_closure.step stream.sel)
qed
lemma 1: (* Follows routinely from 3 *)
assumes "X ? F (g_closure X)"
shows "X ? gfp F"
proof-
note g_closure_mono[OF assms]
also have "g_closure (F (g_closure X)) ? F (g_closure (g_closure X))"
using 3 by simp
also have "... = F (g_closure X)" unfolding g_closure_idem ..
finally have "g_closure X ? F (g_closure X)" .
with gfp_upperbound have "g_closure X ? gfp F" by auto
thus ?thesis by(auto intro: g_closure.intros)
qed
lemma P_coinduct_upto_g: (* is just the concrete version on 1 *)
assumes *: "X xs"
and step: "?xs. X xs ? ?xs' x. xs = x ## xs' ? g_closure X xs' ? x ? 0"
shows "P xs"
using 1 assms unfolding P F_def using predicate1I by blast
(* Follows routinely from 1 and 3: *)
lemma g_closure_P: "g_closure P ? P"
unfolding P apply(rule 1) unfolding g_closure_idem
apply(subst gfp_unfold[OF F_mono]) using 3 .
(* An immediate consequence of g_closure_P *)
lemma 2: "P xs ? P (g xs)"
using g_closure_P by (auto intro: g_closure.intros)
end
Andrei
Test.thy
Last updated: Apr 25 2024 at 16:19 UTC