Email Gateway (Aug 18 2022 at 16:01): Email Gateway (Aug 18 2022 at 16:01):From: Joachim Breitner <mail@joachim-breitner.de>
Dear Brian,
I have been working some more with HOLCF (although my supervisers warned
me that I might run into difficulties or make life harder for me...),
and I have some suggestions and some questions. I hope you don’t mind me
accosting them to you, and remember that these really are only
suggestions, not requests :-)
First I noticed that I tend to have a lot of admissibility statements to
proof. With the lemmas provided in Adm.thy, this is usually not a big
problem. I wonder if it would be sensible to take a similar approach
than taken with cont2cont: I.e. have a ruleset adm2adm that I can amend,
so that I can just use "apply (intros adm2adm)" without listing all my
custon adm rules, and be done in most cases. Or possibly "apply (intros
adm2adm cont2cont)", if some rules involve continuity claims, such as
this one I wrote:
lemma adm_single_valued:
assumes "cont (λx. f x)"
shows "adm (λx. single_valued (f x))"
using assms
unfolding single_valued_def
by (intro adm_lemmas adm_not_mem cont2cont adm_subst[of f])
My next question is about pattern matching in fixrec equations. At the
moment, fixrec only supports very few constructors in patterns, and the
Discr constructor is not supported. Therefore, I have only one equation
with a large case expression then, which makes the .induct rule
relatively unpleasant to work with (compared with, e.g., the function
package). I’d be glad if I could use the Discr constructor in patterns,
and I’d be even more pleased if arbitrary patterns can be used inside
the Discr constructor.
And finaly, I’d like to have some advice. I tried to proof a statement
"P f" about the function f defined by fixrec, using f.induct. I noticed
that it would be easier if I know "Q f", so I proved that (again using
f.induct). Turning back to the proof of "P f", I found out that the
lemma "Q f" is useless, as in the inductive proof of "P f" I am not
working with f, but rather an approximation.
I worked around it by proving P and Q simultaneously in one induction,
but the proof is becoming illegibly convoluted.
Is there maybe a cleaner and more idiomatic way of handing such a case?
I’m afraid that if I continue this way, in the end all statements of my
projects will be proven in one huge induct rule. And Isabelle is already
moving slowly inside the induct proof.
Thanks for your support,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 16:01):From: Brian Huffman <brianh@cs.pdx.edu>
On Tue, Sep 7, 2010 at 1:11 PM, Joachim Breitner
<mail@joachim-breitner.de> wrote:
Dear Brian,
I have been working some more with HOLCF (although my supervisers warned
me that I might run into difficulties or make life harder for me...),
and I have some suggestions and some questions. I hope you don’t mind me
accosting them to you, and remember that these really are only
suggestions, not requests :-)First I noticed that I tend to have a lot of admissibility statements to
proof. With the lemmas provided in Adm.thy, this is usually not a big
problem. I wonder if it would be sensible to take a similar approach
than taken with cont2cont: I.e. have a ruleset adm2adm that I can amend,
so that I can just use "apply (intros adm2adm)" without listing all my
custon adm rules, and be done in most cases. Or possibly "apply (intros
adm2adm cont2cont)", if some rules involve continuity claims, such as
this one I wrote:
lemma adm_single_valued:
[...]
Hi Joachim,
You can easily create your own named rulesets using the Named_Thms ML
functor, like this:
ML {*
structure Adm2Adm = Named_Thms
(
val name = "adm2adm"
val description = "admissibility intro rule"
)
*}
setup Adm2Adm.setup
This defines a dynamic theorem list called "adm2adm", as well as an
attribute called "adm2adm" that will add a theorem to the list. You
can then populate the ruleset with pre-existing rules from Adm.thy
using a declare statement:
declare <names of adm rules> [adm2adm]
My next question is about pattern matching in fixrec equations. At the
moment, fixrec only supports very few constructors in patterns, and the
Discr constructor is not supported. Therefore, I have only one equation
with a large case expression then, which makes the .induct rule
relatively unpleasant to work with (compared with, e.g., the function
package). I’d be glad if I could use the Discr constructor in patterns,
and I’d be even more pleased if arbitrary patterns can be used inside
the Discr constructor.
You can extend fixrec by associating match combinators with new
constructors, using the Fixrec.add_matchers ML command. To see how to
do this, look at my latest update to List_Cpo.thy, where I set up Nil
and Cons to work with fixrec:
http://isabelle.in.tum.de/repos/isabelle/rev/3989b2b44dba
Unfortunately this won't work for all constructors -- fixrec has some
hard-wired assumptions about the kinds of constructors it will work
with. For one, it assumes that the arguments to the constructor will
all have types in class cpo. This means that the "Discr" and "Def"
constructors won't work, because their argument types are generally
not cpos.
I'd like to relax this restriction, but doing so would require
rewriting fixrec's pattern-match compiler, which I don't really have
time to do right now -- I need to finish my dissertation first!
And finaly, I’d like to have some advice. I tried to proof a statement
"P f" about the function f defined by fixrec, using f.induct. I noticed
that it would be easier if I know "Q f", so I proved that (again using
f.induct). Turning back to the proof of "P f", I found out that the
lemma "Q f" is useless, as in the inductive proof of "P f" I am not
working with f, but rather an approximation.I worked around it by proving P and Q simultaneously in one induction,
but the proof is becoming illegibly convoluted.Is there maybe a cleaner and more idiomatic way of handing such a case?
I’m afraid that if I continue this way, in the end all statements of my
projects will be proven in one huge induct rule. And Isabelle is already
moving slowly inside the induct proof.
I'm afraid that with the foo.induct rules currently produced by
fixrec, you're probably stuck doing the simultaneous inductions.
Fortunately it is possible to create a stronger induction rule, but
unfortunately fixrec does not generate such a rule for you. (It's on
my long list of things to do after I finish my degree :)
Here's how fixrec currently generates its induction rules: When you
define a recursive constant "foo :: 'a", fixrec builds a functional
"foo_rec :: 'a => 'a", and defines foo as its least fixed-point: "foo
== fix$(LAM f. foo_rec f)".
Then fixrec uses the "fix_ind" lemma to generate an induction rule for foo:
lemma fix_ind:
assumes "adm P" and "P \<bottom>" and "!!x. P x ==> P (F$x)"
shows "P (fix$F)"
The problem is that fix_ind is weaker than it could be. Here is a
stronger form of induction for least fixed-points that could be used
instead:
lemma
assumes "adm P" and "!!n. P (iterate n$F$\<bottom>)"
shows "P (fix$F)"
So here's what I'd like fixrec to do: In addition to defining "foo
== fix$(LAM f. foo_rec f)", also define another nat-indexed sequence
of approximations to foo: "foo_chain n == iterate n$(LAM f. foo_rec
f)$\<bottom>". Then it could generate an unfolding rule:
"foo_chain (Suc n) = foo_rec (foo_chain n)"
and a strong induction rule:
"adm P ==> (!!n. P (foo_chain n)) ==> P foo"
I think such a rule would allow you to prove separate lemmas about
foo_chain, and re-use them inside later inductions. This way you could
avoid having to do those big simultaneous inductions you complained
about. Even without automation from fixrec, it might be worthwhile to
define the extra constant and prove the extra rules manually.
Thanks for your support,
Joachim
Thanks for your interest in HOLCF!
Hope this helps,
Email Gateway (Aug 18 2022 at 16:02):From: Joachim Breitner <mail@joachim-breitner.de>
Dear Brian,
I’d like to try that, but here, the symbol "foo_rec" is not known. And
looking at src/HOLCF/Tools/fixrec.ML (without understanding much), I can
not find a string ending in "rec" anywhere. The _def theorems generated
by fixrec seem to contain the equations of my functions directly. Are
you sure that the _rec symbol is actually generated?
Thanks,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 16:03):From: Brian Huffman <brianh@cs.pdx.edu>
Sorry, I guess what I said was a bit misleading. There is no "foo_rec"
constant. I only meant "foo_rec" to stand for the functional (a
possibly large lambda term) of which "foo" is the least fixed-point.
Maybe a more explicit example will my suggestion more clear.
domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
fixrec repeat :: "'a -> 'a llist" where "repeat$a = LCons$a$(repeat$a)"
These lemmas are generated by fixrec:
repeat_def: "repeat == fix$(LAM r a. LCons$a$(r$a))"
repeat.unfold: "repeat = (LAM a. LCons$a$(repeat$a))"
repeat.simps: "repeat$a = LCons$a$(repeat$a)"
repeat.induct: "adm P ==> P \<bottom> ==> (!!x. P x ==> P (LAM a.
LCons$a$(x$a))) ==> P repeat"
And I would suggest that you also define
repeat_chain :: "nat => 'a -> 'a llist"
"repeat_chain n == iterate n$(LAM r a. LCons$a$(r$a))$\<bottom>"
and prove the lemmas
"repeat_chain (Suc n) = (LAM a. LCons$a$(repeat_chain n$a))"
"adm P ==> (!!n. P (repeat_chain n)) ==> P repeat"
Email Gateway (Aug 18 2022 at 16:03):From: Joachim Breitner <mail@joachim-breitner.de>
Hi Brian,
ah, I see. Although it would be nice to have the foo_chain defined, in
my case, it would be too ugly (the lambda-term I’d have to copy’n’paste
would just be too ugly large :-). I’ll try to work with one big
induction proof now.
But thanks for the suggestion.
Greetings,
Joachim
signature.asc
Last updated: Apr 20 2024 at 08:16 UTC