Alexandra Graß (Sep 01 2023 at 12:09): Alexandra Graß (Sep 01 2023 at 12:09):I'm currently trying to define two mutual recursive (partial) functions. I'm also using (domintros).
Everything worked out fine until I introduced the line let d_new = if wn then d_old ⊔ d_new else d_old ⊓ d_new in (or operators similar to inf and sup). Proving pattern completeness and pattern compatibility still works out fine. But the keyword functionis now highlighted in red and shows the following error
Tactic failed
The error(s) above occurred for the goal statement⌂:
[...]
I tried to construct a minimal working example but didn't manage to reproduce the error in less complex definitions. And as most of the code is not mine, I can't publish the whole definition. Still hoping the error is so trivial that you guys can help me nonetheless. Is there a problem with the termination proof? Or something else?
Any hints are highly appreciate. Thanks in advance :)
Alexandra Graß (Sep 04 2023 at 09:05):Update: I managed to construct a minimal working example and the problem is neither with mutual recursion nor partial functions (?). Here's the code snippet:
function foo :: "nat ⇒ bool ⇒ nat" where
"foo old expand = (
let tmp = if old < 100 then old + 1 else old in
let new = if expand then old ⊔ tmp else old ⊓ tmp in
if new = old then
if expand then
foo new False
else
new
else
foo new expand)"
by pat_completeness auto
Key idea: There's a monotonically increasing function (in this case if old < 100 then old + 1 else old. old+1 works as well, but then the example would never terminate, which is not what I'm aiming for). There's two phases. First the expand phase where results are always chosen by means of sup. As soon as a fixed point is reached, the algorithm switches to a second phase where values are now combined via inf (which is trivial in this example and should terminate right away as new = old in the first iteration).
Again, keyword function is underlined all red and the following error ist displayed:
Tactic failed
The error(s) above occurred for the goal statement⌂:
⟦⋀old expand x xa.
⟦x = (if old < 100 then old + 1 else old);
xa = (if expand then old ⊔ x else old ⊓ x); xa = old;
expand⟧
⟹ P (xa, False) (old, expand);
⋀old expand x xa.
⟦x = (if old < 100 then old + 1 else old);
xa = (if expand then old ⊔ x else old ⊓ x); xa ≠ old⟧
⟹ P (xa, expand) (old, expand)⟧
⟹ foo_rel ≤ P
What's the issue with my definition? Potential nontermination in case the algorithm is called with expand set to False? (Which is sth I never intend to do.)
Mathias Fleury (Sep 04 2023 at 09:18):Here is a version that fails, but only needs Main:
function (sequential) foo :: "nat set ⇒ bool ⇒ nat set" where
"foo old expand = (
let new = old ∩ old in
if new = old then
foo new expand
else
foo new expand)"
by pat_completeness auto
I think that the way forward here is to write on the mailing list (I am not sure who feels responsible for the function package, but you have a higher chance on the mailing list)
Alexandra Graß (Sep 04 2023 at 09:34):Interesting, thanks for the example! Just realized there's no need for the 2nd param. In a nutshell:
function (sequential) foo :: "nat set ⇒ nat set" where
"foo old = (
let new = old ∩ old in
if new = old then
foo new
else
foo new)"
by pat_completeness auto
does show the Tactic failed error, but
function (sequential) foo :: "nat set ⇒ nat set" where
"foo old = (
let new = old ∩ old in
if new = old then
foo old ∩ old
else
foo new)"
by pat_completeness auto
does not. Replacing new in any of the other lines does not fix the problem.
Edit: Other trivial operations such as old ∪ {} do the job (i.e. invoking the error) as well, btw.
Alexandra Graß (Sep 04 2023 at 09:35):I'll discuss this on the mailing list :)
Last updated: Apr 27 2024 at 16:16 UTC