Salvatore Francesco Rossetta (Mar 10 2024 at 15:12): Salvatore Francesco Rossetta (Mar 10 2024 at 15:12):Hi, I have "no code equation" on this function:
fun f_ex :: "nat ⇒ nat" where "f_ex n = n - 1"
function loop_ex ::
"nat ⇒ nat"
where
"r = 0 ⟹loop_ex r = r" |
"¬(r = 0) ⟹ loop_ex r = loop_ex (f_ex r)"
by auto
termination by (relation "measure (λr. r)")
(auto)
because I have to prove subgoals.
But how should I structure the proof? Is there some guide I can follow? I could not find anything even though I am sure there's something somewhere in the doc. Proving these subgoals is enough to generate code or there is some additional step?
Also, some of them have "Auto solve_direct", like:
Auto solve_direct: subgoal #3 can be solved directly with
BNF_Greatest_Fixpoint.neq_eq_eq_contradict: ?t ≠ ?u ⟹ ?s = ?t ⟹ ?s = ?u ⟹ ?P
How do I correctly insert this in my proof?
John Hughes (Mar 10 2024 at 17:06):I don't know the answer to most of what you ask, but if you've used "try" and gotten that "auto solve_direect" thing, you could try instead using try0: when it finds a simple answer, it gives it to you in a form you can just paste, which is nice . Here's what your proof looks like when I insert that try0:
image.png
Mathias Fleury (Mar 10 2024 at 17:18):What do you mean by "generate code"? Using the code generator? If so, no. You need to have an equation like :
lemma [code]: ‹loop_ex r = (if r = 0 then r else loop_ex (f_ex r))›
by (cases r) auto
value ‹loop_ex 5›
https://isabelle.in.tum.de/dist/Isabelle2023/doc/functions.pdf
Salvatore Francesco Rossetta (Mar 10 2024 at 18:11):Mathias Fleury said:
What do you mean by "generate code"? Using the code generator? If so, no. You need to have an equation like :
lemma [code]: ‹loop_ex r = (if r = 0 then r else loop_ex (f_ex r))› by (cases r) auto value ‹loop_ex 5›
I mean to solve the error "no code equation", which means that Isabelle cannot generate code for the function right? I have to "help" through [code], right?
Mathias Fleury (Mar 10 2024 at 18:13):Yes
Salvatore Francesco Rossetta (Mar 13 2024 at 11:40):Mathias Fleury said:
Yes
It works. Also, I have my measure inside a record and with some additional calculations and it works, however I have an error when i try to change a field of the same record:
fun a_seat :: "my_rec ⇒ my_rec" where
"a_seat r =
let win = max_v (fv rec) (p rec) in
(div r⦇p := win⦈)⦇ns := ns r - 1⦈"
function loop_o ::
"my_rec ⇒ my_rec"
where
"ns r = 0 ⟹ loop_o r = r" |
"¬(ns r = 0) ⟹ loop_o r = loop_o (a_seat r)"
by auto
termination by (relation "measure (λr. ns r)")
(auto simp add: lemma1)
lemma [code]: ‹loop_o r = (if ns r = 0 then r else loop_o (a_seat r))›
by (cases r) auto
In "a_seat" if I add ⦇p := win⦈ I have a failed subgoal error but if I add ⦇p := [ ]⦈ it's working, so clearly the problem is calling the function. Should I add some lemma? I mean, if I am changing another field, why this influences the measure?
PS: lemma1 is to prove that ns (a_seat r) < ns r
Mathias Fleury (Mar 14 2024 at 10:18):… where do you have an error?
Mathias Fleury (Mar 14 2024 at 10:19):My crystal ball says that the answer is
by (cases r)(auto simp: Let_def)
Mathias Fleury (Mar 14 2024 at 10:19):but it is a wild guess
Salvatore Francesco Rossetta (Mar 14 2024 at 10:43):Mathias Fleury said:
My crystal ball says that the answer is
by (cases r)(auto simp: Let_def)
Actually, it is on the
termination by (relation "measure (λr. ns r)")
(auto simp add: lemma1)
(lemma1 is working)
Mathias Fleury (Mar 14 2024 at 10:45):and (auto simp add: Let_def lemma1)? (you have not provided enough context for me to try this out…)
Salvatore Francesco Rossetta (Mar 14 2024 at 12:02):Mathias Fleury said:
and
(auto simp add: Let_def lemma1)? (you have not provided enough context for me to try this out…)
I was not giving also lemma1 because i tried to reduce the example to make it less messy and get to the problem. But adding Let_def should have worked fine. Thanks!
Last updated: Apr 28 2024 at 04:17 UTC