Stream: Beginner Questions

Topic: fresh names


view this post on Zulip Robert Soeldner (Jul 18 2021 at 17:56):

I'm trying to generate fresh names (which can be executed). The idea is to keep track of the prev. used names and to pick the smallest element, see.

definition fresh :: "'a :: linorder set ⇒ 'a × 'a set" where
"fresh used = (let f = LEAST x. x ∉ used in (f, insert f used))"

The simple example works as expected

lemma "fresh {1::nat} = x"
  apply (simp add: fresh_def)

but when starting at 0

lemma "fresh {0::nat,1} = x"
  apply (simp add: fresh_def)

I do get the following goal:

proof (prove)
goal (1 subgoal):
 1. (let f = LEAST x. 0 < x ∧ x ≠ Suc 0 in (f, {f, 0, Suc 0})) = x

So, why is the first part of the goal given by 0 < x ∧... and not x ≠ 0 ∧...?

view this post on Zulip Mathias Fleury (Jul 18 2021 at 18:01):

lemma ‹n ≠ (0:: nat)›
  supply [[simp_trace]]
  apply simp
  oops

shows that the culprint is thm neq0_conv.

view this post on Zulip Mathias Fleury (Jul 18 2021 at 18:01):

It is declared is iff rule

view this post on Zulip Mathias Fleury (Jul 18 2021 at 18:02):

So:

(simp add: fresh_def del: neq0_conv)

view this post on Zulip Mathias Fleury (Jul 18 2021 at 18:05):

How do you handle infinite sets in fresh?

view this post on Zulip Mathias Fleury (Jul 18 2021 at 18:05):

like UNIV:: 'a :: linorder set

view this post on Zulip Robert Soeldner (Jul 18 2021 at 18:06):

This makes sense, is supply similar to using [[...]] ?
In my specific use-case, the set is always finite.

view this post on Zulip Mathias Fleury (Jul 18 2021 at 18:07):

Yes for supply

view this post on Zulip Mathias Fleury (Jul 18 2021 at 18:07):

For the finite case: sure, but won't that make it impossible to make the code executable?

view this post on Zulip Manuel Eberl (Jul 18 2021 at 18:07):

I'm surprised Least is executable at all. It can't be efficient.

view this post on Zulip Mathias Fleury (Jul 18 2021 at 18:08):

Well no by default but if the set is finite you can iterate over it to find the first missing value…

view this post on Zulip Manuel Eberl (Jul 18 2021 at 18:08):

I'd recommend using something like if X = {} then 0 else Suc (Max X) instead.

view this post on Zulip Mathias Fleury (Jul 18 2021 at 18:09):

… or directly remember the upper bound N on the indices and use {0..N} whenever you need the set

view this post on Zulip Mathias Fleury (Jul 18 2021 at 18:10):

But: both approaches create holes in the indices (if you also remove some indices)

view this post on Zulip Manuel Eberl (Jul 18 2021 at 18:10):

Yes, but you're going to have to supply custom code equations for this.

view this post on Zulip Manuel Eberl (Jul 18 2021 at 18:11):

Frankly, I'd just use the Max approach. Easier to reason about, and you get executability for free.

view this post on Zulip Robert Soeldner (Jul 18 2021 at 18:11):

this case is limited to nat, I was hoping to use strings as well... Or I could use of_char while parsing and to_char for printing?

view this post on Zulip Mathias Fleury (Jul 18 2021 at 18:12):

The side of me that proves things agrees with you Manuel… but the side that generates fast code strongly disagrees with you ;-)

view this post on Zulip Manuel Eberl (Jul 18 2021 at 18:12):

(Little-known fact, Sup also exists for nats and is executable. It's basically the same as Max, except that Max {} is undefined while Sup ({} :: nat set) = 0).

view this post on Zulip Manuel Eberl (Jul 18 2021 at 18:12):

Mathias Fleury said:

The side of me that proves things agrees with you Manuel… but the side that generates fast code strongly disagrees with you ;-)

Well sure, it's better to just remember the max index in the first place.

view this post on Zulip Manuel Eberl (Jul 18 2021 at 18:12):

I was simply arguing for Max over Least.

view this post on Zulip Manuel Eberl (Jul 18 2021 at 18:13):

Fresh name generation is always a pain

view this post on Zulip Manuel Eberl (Jul 18 2021 at 18:13):

For strings, the obvious approach is to just use some string encoding of numbers as all your variable names.

view this post on Zulip Robert Soeldner (Jul 18 2021 at 18:14):

Manuel Eberl said:

Fresh name generation is always a pain

This is good to know. What would be the keyword to check if I want to encode strings while parsing and later, back, while printing ?

view this post on Zulip Manuel Eberl (Jul 18 2021 at 18:14):

Otherwise, one can do a "name variant" approach, i.e. start with some "desired" name and then append stuff to it (e.g. ' or a, b, c, etc.) until you find one that isn't taken yet.

view this post on Zulip Manuel Eberl (Jul 18 2021 at 18:15):

Robert Soeldner said:

Manuel Eberl said:

Fresh name generation is always a pain

This is good to know. What would be the keyword to check if I want to encode strings while parsing and later, back, while printing ?

I don't understand what you mean.

view this post on Zulip Robert Soeldner (Jul 18 2021 at 18:16):

Manuel Eberl said:

Robert Soeldner said:

Manuel Eberl said:

Fresh name generation is always a pain

This is good to know. What would be the keyword to check if I want to encode strings while parsing and later, back, while printing ?

I don't understand what you mean.

Isnt there an option to instruct Isabelle to encode strings to nats while parsing? This would allow me to work with nat internally

view this post on Zulip Manuel Eberl (Jul 18 2021 at 18:17):

I don't really understand what it is you're trying to do here. Are you developing an Isabelle tool?

view this post on Zulip Mathias Fleury (Jul 18 2021 at 18:17):

why would there be a default option to encode strings as nat?

view this post on Zulip Mathias Fleury (Jul 18 2021 at 18:18):

(such bijection exists because countable)

view this post on Zulip Robert Soeldner (Jul 18 2021 at 18:18):

Mathias Fleury said:

why would there be a default option to encode strings as nat?

not a default, but user supplied.

view this post on Zulip Mathias Fleury (Jul 18 2021 at 18:20):

Not that I know of

view this post on Zulip Robert Soeldner (Jul 18 2021 at 18:20):

Manuel Eberl said:

I don't really understand what it is you're trying to do here. Are you developing an Isabelle tool?

I started developing a verification framework for the graph programming language GP2. Especially the logic given in https://arxiv.org/abs/2012.01662v1

view this post on Zulip Mathias Fleury (Jul 18 2021 at 18:21):

When I needed a mapping from string to nat, I used a hashmap and a fresh index …

view this post on Zulip Robert Soeldner (Jul 18 2021 at 18:22):

I'm still very new to Isabelle, your comments are highly appreciated.

view this post on Zulip Mathias Fleury (Jul 18 2021 at 18:24):

In short: I used the refinement framework to go from a string version to a nat version with the mapping because some operations required to the original string (sorting on the strings)

view this post on Zulip Mathias Fleury (Jul 18 2021 at 18:24):

But the Refinement Framework might be overkill for you

view this post on Zulip Robert Soeldner (Jul 18 2021 at 18:25):

Yea, I will initially take the Max approach and might ask again :-)

view this post on Zulip Manuel Eberl (Jul 18 2021 at 18:29):

You could presumably replace all the string variables with natural-number variables in a (possibly unverified) pre-processing step.


Last updated: Aug 13 2022 at 07:19 UTC