Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unable to generate code for ?P = (%x. True)

Email Gateway (Aug 18 2022 at 12:36):

From: Duraid Madina <duraid@kinoko.c.u-tokyo.ac.jp>
I was expecting a bool from the following, but instead got the error in the subject:

theory odd imports Primes begin

definition
  m_cond :: "nat => (nat => nat) => bool" where
  "m_cond n mf =
    ((ALL i. i <= n --> 0 < mf i) &
     (ALL i j. i <= n & j <= n & i ~= j
   --> gcd (mf i, mf j) = 1))"

value "m_cond 1 (%x. 3)"

Am I doing something evil here?

Duraid

Email Gateway (Aug 18 2022 at 12:37):

From: Tobias Nipkow <nipkow@in.tum.de>
Universal quantifiers are not executable. The only exception are bounded
quantifiers of the form "Q x : A" where A is one of two kinds of sets:
either a set interval, eg {0..n::nat}, or a set coming from a list, eg
"set xs". Formulas "ALL x. x < n --> ..." are not recognized as
executable. You have to rewrite them into the set interval form:

definition
m_cond :: "nat => (nat => nat) => bool" where
"m_cond n mf =
((ALL i : {0..n}. 0 < mf i) &
(ALL i : {0..n}. ALL j : {0..n}. i ~= j
--> gcd (mf i, mf j) = 1))"

Now

value "m_cond 1 (%x. 3)"

returns "false".

Note: you must import the theory "Executable_Set" for this to work!

Regards
Tobias

Duraid Madina wrote:

Email Gateway (Aug 18 2022 at 12:39):

From: Tobias Nipkow <nipkow@in.tum.de>
Here is how you would go about it if you wanted to make "ALL i<=n"
executable directly. You define your own recursive function all_upto,
prove that it behaves the same as ALL, and make that a code lemma that
replaces such bounded quantifiers by all_upto:

primrec all_upto :: "(nat bool) nat bool" where
"all_upto P 0 = P 0" |
"all_upto P (Suc n) = (P(Suc n) & all_upto P n)"

lemma all_Suc: "(ALL i<=Suc n. P i) = (P(Suc n) & (ALL i<=n. P i))"
by (auto simp:le_Suc_eq)

lemma [code unfold]: "(ALL i<=n. P i) = all_upto P n"
by (induct n) (simp_all add:all_Suc)

Now you don't need Executable_Set (and need to change m_cond only a little).

Regards
Tobias

PS If you want to extract efficient code, import Efficient_Nat: it
implements nat by int.

Duraid Madina wrote:

Email Gateway (Aug 18 2022 at 12:41):

From: Duraid Madina <duraid@kinoko.c.u-tokyo.ac.jp>
Many thanks - this is very good to know. I got over some hurdles, but soon
ran into existential quantifiers. My attempts to get these executable
failed, so I'd like to ask:

- What can be said in the case of making a 'SOME' executable?

- Suppose one has a lemma which proves a unique integer exists satisfiying
some properties, given some preconditions. How could one add an
appropriate "code lemma"? (To get, say, the function which returns the
unique integer when the preconditions are met and zero otherwise.)

Thanks again,

Duraid

Email Gateway (Aug 18 2022 at 12:41):

From: Tobias Nipkow <nipkow@in.tum.de>

Many thanks - this is very good to know. I got over some hurdles, but soon
ran into existential quantifiers.

EX is completely dual to ALL, also w.r.t. code generation.

- What can be said in the case of making a 'SOME' executable?

Tricky. Of course in general you cannot. But even if everything inside
the SOME is executable, non-uniqueness (esp for "SOME x. False") almost
always rule out replacing the some by a logically equivalent term. You
usually have to resort to extra-logical means. For example, in our Jinja
work we implemented "%S. SOME x. x : S" by the ML function "hd" on lists:

definition
some_elem :: "'a set => 'a"
"some_elem == (%S. SOME x. x : S)"

consts_code
"some_elem" ("hd")

The const_code statement is outside the logic and it is your
responsibility that hd is a correct implementation of some_elem!

- Suppose one has a lemma which proves a unique integer exists satisfiying
some properties, given some preconditions. How could one add an
appropriate "code lemma"? (To get, say, the function which returns the
unique integer when the preconditions are met and zero otherwise.)

In that case I would avoid working with SOME in the first place. Use
THE. And if you want to generate code: don't even use THE, define the
function explicitly. For example, if the element can be found by a
search over some interval:

fun search where
"search i j = (if i<j then if p i then f i else search (i+1) j else 0)"

Then prove that search has the properties you want and use search where
you would have used SOME.

Tobias

Thanks again,

Duraid

On Tue, Nov 04, 2008 at 11:47:24AM +0100, Tobias Nipkow wrote:

Universal quantifiers are not executable. The only exception are bounded
quantifiers of the form "Q x : A" where A is one of two kinds of sets:
either a set interval, eg {0..n::nat}, or a set coming from a list, eg
"set xs". Formulas "ALL x. x < n --> ..." are not recognized as
executable. You have to rewrite them into the set interval form:

definition
m_cond :: "nat => (nat => nat) => bool" where
"m_cond n mf =
((ALL i : {0..n}. 0 < mf i) &
(ALL i : {0..n}. ALL j : {0..n}. i ~= j
--> gcd (mf i, mf j) = 1))"

Now

value "m_cond 1 (%x. 3)"

returns "false".

Note: you must import the theory "Executable_Set" for this to work!

Regards
Tobias

Duraid Madina wrote:

I was expecting a bool from the following, but instead got the error in the subject:

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
theory odd imports Primes begin

definition
m_cond :: "nat => (nat => nat) => bool" where
"m_cond n mf =
((ALL i. i <= n --> 0 < mf i) &
(ALL i j. i <= n & j <= n & i ~= j
--> gcd (mf i, mf j) = 1))"

value "m_cond 1 (%x. 3)"
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Am I doing something evil here?

Duraid

Email Gateway (Aug 18 2022 at 12:41):

From: Tobias Nipkow <nipkow@in.tum.de>
Tobias Nipkow wrote:
I forgot to add that this is inconsistent from a logical point of view:
it allows you to derive (via the ML level) that "some_elem {1,2} ~=
some_elem {2,1}". So beware of what you are doing when implementing SOME
by hand.

Tobias

Last updated: Nov 21 2024 at 12:39 UTC