Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Derive bounded sets from extended nat


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Dec 05 2021 at 23:19 UTC