Email Gateway (Jan 18 2021 at 10:03): Email Gateway (Jan 18 2021 at 10:03):From: "Kruse, Kevin" <kevin.kruse@rwth-aachen.de>
Hi,
I’m trying to execute the following code snippet:
value "(∀n::nat. (enat n) ≤ (4::enat) ⟶ (n≤6))"
To do this, I use the following code abbreviation, which transforms the universal quantifier into an bounded set (for the non-infinite case):
lemma bounded_enat_exec [code_abbrev]:"(if ((x::enat)=∞) then (∀n. P n)
else ((∀n∈{0..(the_enat(x))}. P n))) = (∀n::nat. enat n ≤ (x::enat) ⟶ P n)"
sorry
However, I can’t explain the behavior of Isabelle: If I’m writing e.g. “False” in the first if branch (which should never be entered), the code will execute (but the lemma is not provable). If I’m writing what I stated above, the code won’t execute (Error, that nat is not enumerable).
Is there an explanation, why this happens? (… and hopefully a solution?)
All the best,
Kevin
Email Gateway (Jan 18 2021 at 10:25):From: Manuel Eberl <eberlm@in.tum.de>
Code generation happens statically, so if you cannot generate code for
the "False" branch, you cannot generate code for the whole thing. Even
if the branch can never be entered in practice.
What you can do is to use Code.abort in the False branch. Basically,
Code.abort s f is defined to be equal to f () but does not generate
code for f. Instead, whenever Code.abort is encountered at run time, you
get an exception with the message s.
For your case, this works:
lemma bounded_enat_exec [code_unfold]:
"(∀n::nat. enat n ≤ x ⟶ P n) =
(if (x::enat) = ∞ then Code.abort STR ''infinite'' (λ_. ∀n∈UNIV. P n)
else (∀n∈{0..the_enat x}. P n))"
by auto
definition P :: "enat ⇒ bool" where "P x = (∀n::nat. enat n ≤ x ⟶ x ^ 2
= x)"
value "P 1"
I'm a bit puzzled why it doesn't work with just "∀n. P n" instead of
"∀n∈UNIV. P n". Perhaps one of our code generation experts can comment
on this (I CC'ed Florian).
Manuel
smime.p7s
Email Gateway (Jan 18 2021 at 22:06):From: Kevin Kruse <kevin.kruse@rwth-aachen.de>
Hi Manuel, thanks for the explanation/hint!
All the best
Kevin
Last updated: Jul 15 2022 at 23:21 UTC