Stream: Beginner Questions

Topic: fresh names

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"
``````

but when starting at 0

``````lemma "fresh {0::nat,1} = x"
``````

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 ∧...`?

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`.

Mathias Fleury (Jul 18 2021 at 18:01):

It is declared is `iff` rule

Mathias Fleury (Jul 18 2021 at 18:02):

So:

``````(simp add: fresh_def del: neq0_conv)
``````

Mathias Fleury (Jul 18 2021 at 18:05):

How do you handle infinite sets in `fresh`?

Mathias Fleury (Jul 18 2021 at 18:05):

like `UNIV:: 'a :: linorder set`

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.

Yes for supply

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?

Manuel Eberl (Jul 18 2021 at 18:07):

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

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…

Manuel Eberl (Jul 18 2021 at 18:08):

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

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

Mathias Fleury (Jul 18 2021 at 18:10):

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

Manuel Eberl (Jul 18 2021 at 18:10):

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

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.

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?

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 ;-)

Manuel Eberl (Jul 18 2021 at 18:12):

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

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.

Manuel Eberl (Jul 18 2021 at 18:12):

I was simply arguing for `Max` over `Least`.

Manuel Eberl (Jul 18 2021 at 18:13):

Fresh name generation is always a pain

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.

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 ?

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.

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.

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

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?

Mathias Fleury (Jul 18 2021 at 18:17):

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

Mathias Fleury (Jul 18 2021 at 18:18):

(such bijection exists because countable)

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.

Mathias Fleury (Jul 18 2021 at 18:20):

Not that I know of

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

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 …

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)

Mathias Fleury (Jul 18 2021 at 18:24):

But the Refinement Framework might be overkill for you

Robert Soeldner (Jul 18 2021 at 18:25):

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

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