Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Base case in termination proof..

Email Gateway (Aug 22 2022 at 13:05):

From: Daniel Horne <d.horne@danielhorne.co.uk>
I have the following function:

function (domintros) index:: "int ⇒ int" where
"index a = (if (a<0) then (index (a+5)) else (a mod 5))"

and have been trying to prove the result is always >=0 and <= 4. Ran
into a bit of trouble and after some investigation found that it was
because Isabelle couldn't automatically prove termination..

The intention is to prove that this condition is true for all ints, so I
need to prove "∀ a. index_dom a".

Print_theorems gives the following:

index.cases: (⋀a. ?x = a ⟹ ?P) ⟹ ?P
index.domintros: (?a < 0 ⟹ index_dom (?a + 5)) ⟹ index_dom ?a
index.pelims: index ?x = ?y ⟹ index_dom ?x ⟹ (⋀a. ?x = a ⟹ ?y = (if a
< 0 then index (a + 5) else a mod 5) ⟹ index_dom a ⟹ ?P) ⟹ ?P
index.pinduct: index_dom ?a0.0 ⟹ (⋀a. index_dom a ⟹ (a < 0 ⟹ ?P (a +
5)) ⟹ ?P a) ⟹ ?P ?a0.0
index.psimps: index_dom ?a ⟹ index ?a = (if ?a < 0 then index (?a +
5) else ?a mod 5)

with which I've managed to prove this inductive rule:

lemma ddda: "index_dom a ⟹ index_dom (a-5)"
apply(induction a rule:index.pinduct)
apply(simp add:index.domintros)
done

Which is well and good for negative numbers as long as I have an
appropriate base case. I'd been thinking of doing
1: index_dom (a) /\ a<5 /\ a>=0 as a base case. Can do for each
individual value of a, as it's a small enough range
2: index_dom a ⟹ index_dom (a-5) to extend over negative numbers
3: a >= 0 ==> index_dom a ==> index_dom a+5 to extend over positives
using cyclic nature of mod operation.

The problem is that I don't see any way in the theorems that mention
index_dom that I could establish index_dom 0, for example.
I can assume it and succeed in calculating the result - which would be
sufficient to prove to a human that it terminates for that value, but I
don't know how I'd mechanise that reasoning.

Any clues?

Email Gateway (Aug 22 2022 at 13:05):

From: Lars Hupel <hupel@in.tum.de>
Hi Daniel,

if you use the "function" command, Isabelle doesn't even attempt to
prove termination. Only the "fun" command performs automatic proofs
(which fail in this case, however).

If your function is total (it is), you can use the "termination" command
to establish a termination proof.

Here's how it works for your example:

termination index
by (relation "measure (λn. nat (- n))") auto

As you can see, you just have to specify a suitable measure function
under which the function arguments decrease on each call. The rest is
automatic.

You can then use the total induction rule for your lemmas:

lemma "index n ≥ 0"
by (induct n rule: index.induct) auto

lemma "index n ≤ 4"
by (induct n rule: index.induct) auto

Cheers
Lars

Email Gateway (Aug 22 2022 at 13:05):

From: Daniel Horne <d.horne@danielhorne.co.uk>
On 03/04/2016 22:16, Lars Hupel wrote:

Hi Daniel,

and have been trying to prove the result is always >=0 and <= 4. Ran
into a bit of trouble and after some investigation found that it was
because Isabelle couldn't automatically prove termination..
if you use the "function" command, Isabelle doesn't even attempt to
prove termination. Only the "fun" command performs automatic proofs
(which fail in this case, however).

Yes. I initially tried defining it as fun, but switched it over to
function when one of the automatic proofs failed, and had auto do the
completeness proof like this:

function (domintros) index:: "int ⇒ int" where
"index a = (if (a<0) then (index (a+5)) else (a mod 5))"
apply(auto)
done

If your function is total (it is), you can use the "termination" command
to establish a termination proof.

Here's how it works for your example:

termination index
by (relation "measure (λn. nat (- n))") auto

As you can see, you just have to specify a suitable measure function
under which the function arguments decrease on each call. The rest is
automatic.

Ah. I did see in the "Defining Recursive Functions in Isabelle/HOL"
manual that fun is equivalent to function with "termination by
lexicographic_order".
Somehow I completely missed the section "the relation method" section
further down the same page.

Thanks for the assist.

Last updated: Nov 21 2024 at 12:39 UTC