Email Gateway (Aug 22 2022 at 10:54): Email Gateway (Aug 22 2022 at 10:54):From: Johannes Hölzl <hoelzl@in.tum.de>
Am Dienstag, den 18.08.2015, 21:23 +0200 schrieb Esseger:
If ?f is simple enough, it suffices to do
have "incseq ?f" by ...
moreover have "⋀i. AE x in M. 0 ≤ ?f i x" by ...
moreover have "⋀i. ?f i ∈ borel_measurable M" by ...
ultimately have "(∫⇧+ x. (SUP i. ?f i x) ∂M) = (SUP i. integral⇧N M (?f
i))" using nn_integral_monotone_convergence_SUP_AE_incseq by forcewhich has no need for additional notations, and in which the flow of
ideas is clear. Unfortunately, when ?f starts being complicated, force
does not succeed.
Lars already mentioned the use of proof-blocks. But in this specific
case it should also be possible to use
by (rule nn_integral_monotone_convergence_SUP_AE_incseq)
directly to prove the last have. "force" needs to find the instantiation
for the theorem provided by using, which gets difficult for big
terms ?f.
The proof block has one advantage: you can concentrate on the
non-automatic part and hope that everything else works automatic.
nn_integral_monotone_convergence_SUP_AE_incseq is a good example:
usually 0 <= f x and the measurability proof work automatic (the later
hopefully when the measurability assumptions are annotated with
[measurable]). Then you can write:
have "(∫⇧+ x. (SUP i. ?f i x) ∂M) = (SUP i. integral⇧N M (?f i))"
proof (rule nn_integral_monotone_convergence_SUP_AE_incseq)
show "incseq ?f" by ...
qed auto
2) In the middle of proofs, once a lot of context was fixed, I needed to
do inductive constructs. But I did not find how to define recursive
functions in the middle of a proof, so I had to define a helper function
outside of the body of the proof. This is not satisfactory since this
helper function is completely useless (and impossible to understand)
outside of the context of the proof, and should really not be in the
global namespace.
Yes, this is very unfortunate. In my experience for analysis simple
inductive definitions are not enough (i.e. the rec_nat or rec_list etc
mentioned by others). For more complicated constructions there are also
the choice theorems: choice, dependent_nat_choice, or
dependendent_wf_choice (for a well-founded definition).
Email Gateway (Aug 22 2022 at 10:55):From: Tobias Nipkow <nipkow@in.tum.de>
On 18/08/2015 22:40, Larry Paulson wrote:
A lot is missing, for sure. Contributions definitely welcome!
Very much so! If you (Esseger) happen to have a teaching position, consider
student projects in this area.
Tobias
Larry Paulson
On 18 Aug 2015, at 20:23, Esseger <esseger@free.fr> wrote:
I would say the main problem is precisely to formalize the results (say, a little bit of functional analysis and spectral theory...)
Email Gateway (Aug 22 2022 at 10:55):From: Lars Noschinski <noschinl@in.tum.de>
I agree with the suggestions of Johannes and Lars. You might also try
something along the lines of
by (force intro: nn_integral_monotone_convergence_SUP_AE_incseq)
or
by (intro nn_integral_monotone_convergence_SUP_AE_incseq) (auto ...)
This is often useful, if you don't want to spell out all of the
assumptions automatically.
-- Lars
Email Gateway (Aug 22 2022 at 11:11):From: Esseger <esseger@free.fr>
Dear Isabelle users,
I played recently with Isabelle/HOL, to see if it was possible to
formally prove a nice mathematical theorem I have recently established.
My conclusion is that the system is excellent, since mathematicians with
almost no computer science background can use it, but there are still
too many missing mathematical bricks (which, hopefully, will be covered
with time) for research mathematics. In any case, it was a lot of fun,
and very interesting. I will certainly come back later to it, to add
more results to what I have already proved.
Along the way, I stumbled across some difficulties. I solved them in a
non-satisfactory way, so I wanted to ask if there are better practices:
1) In the middle of proofs, I often needed to prove statements of the
form "!!n. P n", by induction, or by case analysis.
I proved them as follows:
have "!!n. P n"
proof -
fix n
show "P n"
proof (induction n)
...
qed
qed
This looks like too much boilerplate, and from the mathematical point of
view it is definitely not the right thing to fix n before doing an
induction (in which n is varying). So, is there a better way? Something like
have "!!n. P n"
proof (?????, induction n)
...
qed
2) In the middle of proofs, once a lot of context was fixed, I needed to
do inductive constructs. But I did not find how to define recursive
functions in the middle of a proof, so I had to define a helper function
outside of the body of the proof. This is not satisfactory since this
helper function is completely useless (and impossible to understand)
outside of the context of the proof, and should really not be in the
global namespace.
So, is there a way to define recursive functions inside a proof?
3) In an Isar proof, is there a way to refer to previous statements in
an OF clause? More specifically, consider
have *: "P" by auto
have "Q" using foo[OF *] by auto
where P is some complicated statement. I would like to write this as
have "P" by auto
then have "Q" using foo[OF this] by auto
But this fails. Is there a way to make it work, replacing "this" by
something else?
Same thing with "moreover" statements: is it possible to write something
like:
have "P1" by auto
moreover have "P2" by auto
moreover have "P3" by auto
ultimately have "Q" using foo[OF this-1, OF this-2, OF this-3] by auto
Two additional comments:
4) "theorem", "lemma" and "corollary" are available, but it seems that
most theories use "lemma" 99% of the time. Maybe adding "proposition"
(and maybe "example") would help a little bit to have a bigger scale of
statements, for more expressiveness.
5) When I knew that some statement foo would be helpful to prove a
property P, I would write
have "P" using foo
and then call sledgehammer on it. Very often, I would get results of the
form:
proof reconstruction failed: "by (metis bar)"
Most of the time, "by (metis foo bar)" would do the job, so I guess the
problem is an excessive minimization, assuming wrongly that "using foo
by (metis bar)" is the same as "by (metis foo bar)"...
Any comment welcome!
Esseger
Email Gateway (Aug 22 2022 at 11:11):From: Larry Paulson <lp15@cam.ac.uk>
Quite a lot in your question! But to answer this bit, you can refer to the theorem P as P.
Incidentally, I also vote for “proposition”. I gather that to a mathematician, a proposition is a routine but interesting result, while a lemma is a stepping-stone that is of no interest in its own right.
Larry Paulson
Email Gateway (Aug 22 2022 at 11:11):From: Lars Hupel <hupel@in.tum.de>
Dear Esseger,
I played recently with Isabelle/HOL, to see if it was possible to
formally prove a nice mathematical theorem I have recently established.
My conclusion is that the system is excellent, since mathematicians with
almost no computer science background can use it, but there are still
too many missing mathematical bricks (which, hopefully, will be covered
with time) for research mathematics. In any case, it was a lot of fun,
and very interesting. I will certainly come back later to it, to add
more results to what I have already proved.
that is nice to hear! The community is always interested in use cases and
feedback from non-computer-scientists.
1) In the middle of proofs, I often needed to prove statements of the
form "!!n. P n", by induction, or by case analysis.
I proved them as follows:have "!!n. P n"
proof -
fix n
show "P n"
proof (induction n)
...
qed
qed
Try this instead:
{
fix n
show "P n"
proof (induction n)
...
qed
}
The effect will be the roughly same: You will have proven the predicate
"P" for all arguments. As a general rule of thumb: Avoid the "!!"
quantifier on the right-hand side of an implication.
(The formal description of these "proof blocks" is in Sec 6.1.2 of
<https://isabelle.in.tum.de/dist/Isabelle2015/doc/isar-ref.pdf>.)
This looks like too much boilerplate, and from the mathematical point of
view it is definitely not the right thing to fix n before doing an
induction (in which n is varying).
I think your intuition about what the phrase "fix a variable" means in
Isabelle is not accurate. In this example, you merely introduce a variable
into the scope, so that the system knows about it. You could also leave
the "fix n" off, which will make Isabelle/jEdit render the variable
distinctly to alert you that you're using something unknown.
2) In the middle of proofs, once a lot of context was fixed, I needed to
do inductive constructs. But I did not find how to define recursive
functions in the middle of a proof, so I had to define a helper function
outside of the body of the proof. This is not satisfactory since this
helper function is completely useless (and impossible to understand)
outside of the context of the proof, and should really not be in the
global namespace.So, is there a way to define recursive functions inside a proof?
No, but there's a different solution. You can write it like this:
context begin
private fun helper where ...
lemma bla
... use helper ...
end
After the end of the context block, the "helper" function is inaccessible.
See also Sec 5.2 of the aforementioned manual.
Hope that helps.
Lars
Email Gateway (Aug 22 2022 at 11:11):From: Tobias Nipkow <nipkow@in.tum.de>
On occasion I have used the primitive recursion operator that comes with each
data type. This way you can defined a recursive function nonrecursively.
However, the result tends to be obscure.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 11:11):From: Lars Noschinski <noschinl@in.tum.de>
On 18.08.2015 18:26, Esseger wrote:
Dear Isabelle users,
I played recently with Isabelle/HOL, to see if it was possible to
formally prove a nice mathematical theorem I have recently established.
My conclusion is that the system is excellent, since mathematicians with
almost no computer science background can use it, but there are still
too many missing mathematical bricks (which, hopefully, will be covered
with time) for research mathematics. In any case, it was a lot of fun,
and very interesting. I will certainly come back later to it, to add
more results to what I have already proved.
Thanks a lot for the feedback! May I ask what you used as learning
resources?
If you want to build on some missing result, which you do want to
formalize, it is sometimes an option to just assume the result (using a
locale).
Along the way, I stumbled across some difficulties. I solved them in a
non-satisfactory way, so I wanted to ask if there are better practices:1) In the middle of proofs, I often needed to prove statements of the
form "!!n. P n", by induction, or by case analysis.
I proved them as follows:have "!!n. P n"
proof -
fix n
show "P n"
proof (induction n)
...
qed
qed
I would state this as
{ fix n have "P n"
proof (induction n)
..
qed
}
which admittedly is still a bit boilerplatey. In the next Isabelle
release, it might be possible to write 'have "P n" for n' instead.
2) In the middle of proofs, once a lot of context was fixed, I needed to
do inductive constructs. But I did not find how to define recursive
functions in the middle of a proof, so I had to define a helper function
outside of the body of the proof. This is not satisfactory since this
helper function is completely useless (and impossible to understand)
outside of the context of the proof, and should really not be in the
global namespace.So, is there a way to define recursive functions inside a proof?
Unfortunately, you cannot use primrec or fun inside a proof. If you want
primitive recursion on datatypes, you can use the recursion function
defined by the datatype package. E.g., for a list datatype defined as
datatype 'a mylist = My_Nil | My_Cons 'a "'a mylist"
you could use
def mylen == "rec_mylist 0 (λx' xs' rec. rec + 1)"
to define a recursive length function inside a proof. There is also the
whileOption combinator (from ~~/src/HOL/Library/While_Combinator).
3) In an Isar proof, is there a way to refer to previous statements in
an OF clause? More specifically, considerhave *: "P" by auto
have "Q" using foo[OF *] by autowhere P is some complicated statement. I would like to write this as
have "P" by auto
then have "Q" using foo[OF this] by autoBut this fails. Is there a way to make it work, replacing "this" by
something else?
In most cases, I would use the \<open>P\<close> syntax suggested by
Larry. "this" is only bound before the have, you could write
have "P" by auto
with foo[OF this] have "Q" by auto
(keep in mind that "then" abbreviates "from this" and "with ..."
abbreviates "from ... this".
Same thing with "moreover" statements: is it possible to write something
like:have "P1" by auto
moreover have "P2" by auto
moreover have "P3" by auto
ultimately have "Q" using foo[OF this-1, OF this-2, OF this-3] by auto
I don't know a nice syntax for this. For me this is not an
often-occurring situation, so I wonder if writing the proof differently
would help. Do you have an example?
Note that many proof tools work better if lemmas are used in a more
directed fashion, e.g. as simp, intro, elim, ... rules.
Most of the time, "by (metis foo bar)" would do the job, so I guess the
problem is an excessive minimization, assuming wrongly that "using foo
by (metis bar)" is the same as "by (metis foo bar)"...
Indeed, there are some subtle differences between these two statements,
that sledgehammer does not fully deal with. Jasmin (the sledgehammer
author) is aware of this problem.
-- Lars
Email Gateway (Aug 22 2022 at 11:11):From: Manuel Eberl <eberlm@in.tum.de>
As other people have already said here: no. You can, however, define a
recursive function within a locale that has the same fixes as the place
in your proof where you want to define the function and the assumes the
relevant facts. You can then just interpret that locale in your proof.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 11:11):From: Esseger <esseger@free.fr>
Very nice, thanks a lot!
Email Gateway (Aug 22 2022 at 11:11):From: Esseger <esseger@free.fr>
Le 18/08/2015 19:22, Lars Noschinski a écrit :
On 18.08.2015 18:26, Esseger wrote:
Thanks a lot for the feedback! May I ask what you used as learning
resources?
"Programming and Proving in Isabelle/HOL" was invaluable to start. The
tutorial on locales was also very useful.
On the other hand, the
Isabelle/Isar Reference Manual was essentially of no use to me (too many
informations, probably). But I mostly understood things by looking at
code in the HOL library, and HOL-Multivariate_Analysis.
If you want to build on some missing result, which you do want to
formalize, it is sometimes an option to just assume the result (using a
locale).
I would say the main problem is precisely to formalize the results (say,
a little bit of functional analysis and spectral theory...)
3) In an Isar proof, is there a way to refer to previous statements in
an OF clause? More specifically, considerhave *: "P" by auto
have "Q" using foo[OF *] by autowhere P is some complicated statement. I would like to write this as
have "P" by auto
then have "Q" using foo[OF this] by autoBut this fails. Is there a way to make it work, replacing "this" by
something else?In most cases, I would use the \<open>P\<close> syntax suggested by
Larry. "this" is only bound before the have, you could writehave "P" by auto
with foo[OF this] have "Q" by auto
nice, thanks. The problem with P is when P is really complicated. Then
it is more efficient to give a name to "P", say:
have i: "P"
have "Q" using foo[OF i] by auto
But I don't like giving names to equations if it is not necessary, as
more notations are always a burden on the reader.
Same thing with "moreover" statements: is it possible to write something
like:have "P1" by auto
moreover have "P2" by auto
moreover have "P3" by auto
ultimately have "Q" using foo[OF this-1, OF this-2, OF this-3] by autoI don't know a nice syntax for this. For me this is not an
often-occurring situation, so I wonder if writing the proof differently
would help. Do you have an example?
Take for instance the following lemma (from
Probability/Nonnegative_Lebesgue_Integration.thy):
lemma nn_integral_monotone_convergence_SUP_AE_incseq:
assumes f: "incseq f" "⋀i. AE x in M. 0 ≤ f i x" and borel: "⋀i. f i
∈ borel_measurable M"
shows "(∫⇧+ x. (SUP i. f i x) ∂M) = (SUP i. integral⇧N M (f i))"
To use this lemma, you typically need to check his three assumptions,
and all of them are nontrivial. If ?f is some complicated expression to
which I want to apply the above lemma, I will typically do:
have i: "incseq ?f" by ...
have ii: "⋀i. AE x in M. 0 ≤ ?f i x" by ...
have iii: "⋀i. ?f i ∈ borel_measurable M" by ...
have "(∫⇧+ x. (SUP i. ?f i x) ∂M) = (SUP i. integral⇧N M (?f i))" by
(rule nn_integral_monotone_convergence_SUP_AE_incseq[OF i, OF ii, OF iii])
I don't really like this syntax because I have to give names to
equations (more notations are always more confusing), and because it
does not illustrate directly that the last statement is deduced from the
previous ones.
If ?f is simple enough, it suffices to do
have "incseq ?f" by ...
moreover have "⋀i. AE x in M. 0 ≤ ?f i x" by ...
moreover have "⋀i. ?f i ∈ borel_measurable M" by ...
ultimately have "(∫⇧+ x. (SUP i. ?f i x) ∂M) = (SUP i. integral⇧N M (?f
i))" using nn_integral_monotone_convergence_SUP_AE_incseq by force
which has no need for additional notations, and in which the flow of
ideas is clear. Unfortunately, when ?f starts being complicated, force
does not succeed.
Best,
Esseger
Email Gateway (Aug 22 2022 at 11:11):From: Lars Hupel <hupel@in.tum.de>
In these cases I usually employ a subproof:
have "(∫⇧+ x. (SUP i. ?f i x) ∂M) = (SUP i. integral⇧N M (?f i))"
proof (rule nn_integral_monotone_convergence_SUP_AE_incseq)
show "incseq ?f" by ...
next
...
qed
However, this is largely a matter of taste.
Cheers
Lars
Email Gateway (Aug 22 2022 at 11:12):From: Larry Paulson <lp15@cam.ac.uk>
A lot is missing, for sure. More complex analysis is on the way for the next release, along with the Stone-Weierstraß theorem, etc. Contributions definitely welcome!
Larry Paulson
Last updated: Apr 19 2024 at 12:27 UTC