Email Gateway (Aug 18 2022 at 18:19): Email Gateway (Aug 18 2022 at 18:19):From: Alexander Krauss <krauss@in.tum.de>
Hi Viorel,
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
Email Gateway (Aug 18 2022 at 18:19):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
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
Email Gateway (Aug 18 2022 at 18:27):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,
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:
[| [| na = n; 0 = k; 0 = s; Testb n k s|] ==> Test (loop_fun (n, k,
s)); Testa na |] ==> Test (init_fun na)
...
I would expect something like:
[| [| Testb na 0 0|] ==> Test (loop_fun (na, 0, 0)); Testa na |] ==>
Test (init_fun na)
...
that I can prove using the definition of the Test predicates.
Best regards,
Viorel Preoteasa
Last updated: Apr 25 2024 at 08:20 UTC