Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Formal algorithms in Isabelle - is it OK to sp...


view this post on Zulip Email Gateway (Mar 20 2021 at 19:00):

From: Alex Meyer <alex153@outlook.lv>
I am digesting specification of quicksort https://isabelle.in.tum.de/library/HOL/HOL-Imperative_HOL/Imperative_Quicksort.html and I have question:

is it OK (acceptable by AFP standards) to specify algorithm as definition (e.g. swap) or is it strongly required that the final algorithm is specified as function (e.g. quicksort)?

According to tutorial, definition is not for recursive functions and it does not create proof obligation for termination. As I can see from the example, then Isabelle can still prove lemmas and theorms about definitions (maybe with additional assumptions).

So - as I understand: if the formalized algorithm is expected to be partially correct only (without the proof of termination) then it is OK that Isabelle theory specifies this algorithm (and its relevant sub-algorithms) as definition and proves theorems about this definition that resembles the partial correctness proofs.

So - the specification of some algorithm as function is required only in the case when total correctnes should be proved.

And just for clarification: is it really true, that the fun/function keyword requires that the specification of the function with fun/function is recursive, i.e., that the specified function should appear in the right hand side for at least one pattern-matching-clause? As can be understood from the tutorials then fun/function is for recursive definitions specifically, but nonetheless, Isabelle allows to write:

function two_integer_max_case :: "nat ⇒ nat ⇒ nat" where
"two_integer_max_case a b = (case a > b of True ⇒ a | False ⇒ b)"
by pat_completeness auto
termination by auto

And Isabelle also provides suggestions for the proof. But maybe it is just misleading - one should not expect that such function can be defined in such way...

Alex

view this post on Zulip Email Gateway (Mar 20 2021 at 19:46):

From: Jakub Kądziołka <kuba@kadziolka.net>
On Sat Mar 20, 2021 at 7:59 PM CET, Alex Meyer wrote:

I am digesting specification of quicksort https://isabelle.in.tum.de/library/HOL/HOL-Imperative_HOL/Imperative_Quicksort.html and I have question:

is it OK (acceptable by AFP standards) to specify algorithm as definition (e.g. swap) or is it strongly required that the final algorithm is specified as function (e.g. quicksort)?

According to tutorial, definition is not for recursive functions and it does not create proof obligation for termination. As I can see from the example, then Isabelle can still prove lemmas and theorms about definitions (maybe with additional assumptions).

So - as I understand: if the formalized algorithm is expected to be partially correct only (without the proof of termination) then it is OK that Isabelle theory specifies this algorithm (and its relevant sub-algorithms) as definition and proves theorems about this definition that resembles the partial correctness proofs.

Alex,

you seem to have a fundamental misunderstanding of what's happening
here. On the level of the logic, 'fun' and 'function' are strictly
generalizations of 'definition'. When Isabelle doesn't require a
termination proof, that's because it's trivial, not because the problem
of termination is ignored.

In fact, termination isn't only required for total correctness, but also
for logical consistency. Consider:

function foo where
"foo x = (¬ foo x)"
by pat_completeness auto
termination sorry

theorem False
proof -
have *: "a = (¬ a) ⟹ False" for a
by simp
show False by (fact *[OF foo.simps])
qed

When both 'definition' and 'fun' accept a formula, the difference comes
down to how proof automation will treat your function (by default) —
if you 'fun foo', the defining formula will become a fact named
foo.simps. As the name suggests, it will be added to the simpset and the
simplifier will unfold it by default. By contrast, for a
'definition foo', the fact is called foo_def and isn't added to the
simpset.

I presume that the reason the tutorial says that 'fun' should only be
used for recursive definitions, is that if you use it for non-recursive
ones, your intermediate goals will get needlessly large, and thus not
very readable.

After all, if a function is defined by pattern matching and a subformula
of the goal matches that pattern, then unfolding the application is
probably a good idea.

function two_integer_max_case :: "nat ⇒ nat ⇒ nat" where
"two_integer_max_case a b = (case a > b of True ⇒ a | False ⇒ b)"
by pat_completeness auto
termination by auto

In light of the above, function definitions with proofs this trivial
should really use the 'fun' keyword instead. Indeed, use 'function' only
when 'fun' is having trouble with the termination proof.

And just for clarification: is it really true, that the fun/function keyword requires that the specification of the function with fun/function is recursive, i.e., that the specified function should appear in the right hand side for at least one pattern-matching-clause?

As you've demonstrated, this is not the case. In fact, there are
situations where a function is non-recursive, and yet 'fun' is a better
tool for the job than 'definition'. Consider

fun pred :: "nat => nat" where
"pred 0 = 0" |
"pred (S n) = n"

Defining this function with 'definition' would require an explicit
'case' expression.

Hope that helps,
Jakub Kądziołka


Last updated: Mar 29 2024 at 04:18 UTC