Re: [isabelle] induction for mutually recursive functions



Hi Alex,

That you for your message. Changing the function definition to
the curried version helped. After this change I got
the proof obligations that I expected.

I managed already to prove the theorem by instantiating the
induction theorems manually, but it was very cumbersome,
and I needed to prove the same facts 3 times.

Regarding my initial definition, it still does not seem provable.
The conditions na = n; 0 = k; 0 = s cannot be discharged.
If you look at the second subgoal, the situation is even worse
because one would need to prove k = k+1. Maybe there is an error
in applying the induction when the functions have tuples
as parameters.

Best regards,

Viorel

On 9/7/11 1:21 AM, Alexander Krauss wrote:
Hi Viorel,

I have the following mutually recursive function definition

function
init_fun :: "nat => nat * nat * nat"
and loop_fun :: "nat * nat * nat => nat * nat * nat"
and final_fun :: "nat * nat * nat => nat * nat * nat"
where
"init_fun n = loop_fun (n, 0, 0)" |
"loop_fun (n, k, s) = (if k < n then loop_fun (n, k + 1, s + k + 1)
else if k = n then final_fun (n, k, s)
else (n, k, s))"|

"final_fun (n, k, s) = (n, k, s)"

by pat_completeness auto
termination
apply (relation "measure (% x. case x of Inl n => n + 3 | Inr (Inl (n,
k, s)) => n - k + 2 | Inr (Inr (n, k, s)) => n - k + 1)")
by auto

Asumming that Testa, Testb, Testc, and Test are defined I want to prove by
(mutual) induction:

theorem TestInduction:
"Testa n ==> Test (init_fun n)"
"Testb n k s ==> Test (loop_fun (n, k, s))"
"Testc n k s ==> Test (final_fun (n, k, s))"

If I try

apply (induct n and "(n, k, s)" and "(n, k, s)" rule:
init_fun_loop_fun_final_fun.induct)

I get something that is unprovable:

1. [| [| na = n; 0 = k; 0 = s; Testb n k s|] ==> Test (loop_fun (n, k,
s)); Testa na |] ==> Test (init_fun na)
2. ...
3. ...

I would expect something like:

1. [| [| Testb na 0 0|] ==> Test (loop_fun (na, 0, 0)); Testa na |] ==>
Test (init_fun na)
2. ...
3. ...

that I can prove using the definition of the Test predicates.

The two versions are actually equivalent, so one should be provable when the other is. Unfortunately, the equation "na = n" seems to be oriented in an unfortunate way, such that the simplifier does not help you here...

Note that here you are relying on a feature of the induct method to do induction over non-variable terms, which introduces equations on the fly (which you already see in the simplified form; if you add (no_simp) after "induct", you see where they come from).

You can avoid this situation altogether by using currying instead of tuple arguments in your function definition, which is generally recommended:

function
  init_fun :: "nat => nat * nat * nat"
  and loop_fun :: "nat => nat => nat => nat * nat * nat"
  and final_fun :: "nat => nat => nat => nat * nat * nat"
  where
    "init_fun n = loop_fun n 0 0" |
    "loop_fun n k s = (if k < n then loop_fun n (k + 1) (s + k + 1)
                             else if k = n then final_fun n k s
                             else (n, k, s))"|

    "final_fun n k s = (n, k, s)"

by pat_completeness auto
termination
apply (relation "measure (% x. case x of Inl n => n + 3 | Inr (Inl (n, k, s)) => n - k + 2 | Inr (Inr (n, k, s)) => n - k + 1)")
  by auto


theorem TestInduction:
  "Testa n ==>  Test (init_fun n)"
  "Testb n k s ==> Test (loop_fun n k s)"
  "Testc n k s ==> Test (final_fun n k s)"
apply (induct n and n k s and n k s rule: init_fun_loop_fun_final_fun.induct)



Hope this helps...

Alex







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.