## Stream: Beginner Questions

### Topic: finite_induct over sets

#### Max Nowak (Mar 10 2021 at 14:30):

I'm trying to lead an inductive proof over a finite set, and I found the `Finite_Set.finite_induct` lemma which seems to be what I want (though I may in future need to induct over the elements in a specified linear order, but not yet). But I can't figure out how to start the proof, other than just `proof (rule finite_induct)`, but it feels like there should be a more idiomatic way of using it?

#### Mathias Fleury (Mar 10 2021 at 14:38):

I assume that you just forgot to add the `finite S` fact to the context:

``````  using `finite S`
proof (induct rule: finite_induct)
``````

#### Max Nowak (Mar 10 2021 at 14:39):

Oh, yeap, that was it. Thanks!

#### Max Nowak (Mar 10 2021 at 14:44):

Is there a way to fold over elements in a finite set (with `Finite_Set.fold` or something similar) in a specified linear order? (And then that'll constrain the `finite_induct` proof as well I assume..)

#### Max Nowak (Mar 10 2021 at 14:45):

Though I guess at that point I might as well just use a list, but it'd be unhandy with the rest of my definitions & lemmas..

#### Mathias Fleury (Mar 10 2021 at 14:53):

why would you want to do that?

#### Max Nowak (Mar 10 2021 at 14:54):

Yeah good question, guess that's a bad idea then.

#### Mathias Fleury (Mar 10 2021 at 14:55):

A set is by definitions unordered. If you need an order, then you don't have a set anymore…

#### Mathias Fleury (Mar 10 2021 at 14:55):

IIRC, there is a `sorted_list_of_list`or something like that to convert a set to an ordered list

#### Max Nowak (Mar 10 2021 at 18:15):

Yeah there is `List.sorted_list_of_set :: 'a set => 'a list`, but it takes no linear order as an argument, so I don't know how to call that..

#### Mathias Fleury (Mar 10 2021 at 18:35):

`'a` is assumed to have a linear order

#### Max Nowak (Mar 10 2021 at 18:40):

Ah, hm, guess I'll finally have to dive into locales then

#### Mathias Fleury (Mar 10 2021 at 18:58):

but why do you need an order? For non-determinism, I would use an inductive predicate

#### Manuel Eberl (Mar 11 2021 at 11:02):

You can also always just "obtain" a list using the theorem `finite_list`. If you need this top-level for whatever reason (i.e. outside an Isar proof), you can use `SOME` in combination with that theorem (`SOME xs. set xs = A`). None of this is executable, of course (while `sorted_list_of_set`) ist.

#### Manuel Eberl (Mar 11 2021 at 11:02):

I would, however, generally avoid working with lists instead of finite sets unless you have a good reason for doing so.

#### Max Nowak (Mar 11 2021 at 14:21):

I am working with an existing framework which gives me a set of elected alternatives E, and for each alternative I want to do something. And the order in which I draw those candidates may affect the outcome, but I am not sure.

#### Mathias Fleury (Mar 11 2021 at 14:23):

If you are not sure and don't care, use an inductive predicate to express a nondetirministic fold…

#### Max Nowak (Mar 11 2021 at 14:25):

Oh sorry I had somehow missed your message yesterday.

#### Manuel Eberl (Mar 11 2021 at 14:28):

`Library/Multiset_Permutations` also has `permutations_of_set` which gives you all the lists that are a permutation of a given finite set `A`

#### Max Nowak (Mar 11 2021 at 15:02):

How would I use an inductive predicate to express some fold then? Right now I'm trying to define a `function` which computes my result (pattern matching on `{}` and `insert x xs`), but to be honest I have no clue what I'm doing.

#### Max Nowak (Mar 11 2021 at 15:03):

`finite` is already an inductive predicate, so maybe that could be reused.

#### Max Nowak (Mar 11 2021 at 15:04):

``````function draw :: "'a set ⇒ 'a list" where
"draw {} = []" |
"finite (insert x xs) ⟹ draw (insert x xs) = x # draw xs"
``````

This is just a minimal example, something roughly like this is what I had in mind. (yes I know it's probably terribly wrong, please don't laugh :P)

#### Mathias Fleury (Mar 11 2021 at 16:06):

that is the whole point of the discussion: this is not possible.

#### Mathias Fleury (Mar 11 2021 at 16:06):

You cannot do that.

#### Mathias Fleury (Mar 11 2021 at 16:06):

The definition is not well defined

#### Mathias Fleury (Mar 11 2021 at 16:11):

What you can define is a fold-like predicate:

``````inductive fold_set :: ‹_ ⇒ 'b ⇒ 'a set ⇒ bool›
for f :: ‹'b ⇒ 'a ⇒ 'b›
where
"fold_set f dflt {}" |
"fold_set f a S ⟹ fold_set f (f a b) (insert b S)"
``````

#### Mathias Fleury (Mar 11 2021 at 16:17):

`dflt` must be a meaningfull constant in you case or another parameter

#### Jakub Kądziołka (Mar 11 2021 at 16:38):

This is available as `Finite_Set.fold_graph`

#### Mathias Fleury (Mar 11 2021 at 17:08):

ah, I did not know about that predicate. Thanks

#### Jakub Kądziołka (Mar 11 2021 at 17:13):

If your operation is commutative, i.e. the result doesn't depend on the order used (and you can prove it), then there's `Finite_Set.fold` which uses `THE` on `fold_graph`

#### Max Nowak (Apr 27 2021 at 11:05):

I gave up on this last time, but the issue has come up again, and I'm at my wit's end to be honest. I have a set `A`, and a subset `S` of A. And I have a linear order `linord` on A. How do I get `S` transformed into a list according to the linear order? I know there is `List.sorted_list_of_set`, but it uses Locales and I have no time to dig into that for something this (seemingly) simple, sorry..

#### Lukas Stevens (Apr 27 2021 at 11:07):

Is the linear order on the type or or just the set `S`?

#### Max Nowak (Apr 27 2021 at 11:07):

Just on `A` (and S is a subset).

#### Mathias Fleury (Apr 27 2021 at 11:08):

can you use `SOME xs. set xs = A`?

#### Lukas Stevens (Apr 27 2021 at 11:08):

If it is on the set, then you are out of luck currently without resorting to `Types-To-Sets`. I have already relativised the `folding` locale to sets but the changes will be in the next release at the earliest.

#### Manuel Eberl (Apr 27 2021 at 11:09):

I have something like that in the AFP: https://www.isa-afp.org/browser_info/current/AFP/Comparison_Sort_Lower_Bound/Linorder_Relations.html

#### Manuel Eberl (Apr 27 2021 at 11:09):

`sorted_wrt_list_of_set`

#### Manuel Eberl (Apr 27 2021 at 11:09):

It uses its own notation of "linear order", but that should be easy to adapt.

#### Max Nowak (Apr 27 2021 at 11:14):

Looks like `linorder_on` is equivalent to `linear_order_on`

#### Max Nowak (Apr 27 2021 at 11:16):

Looks like what I need then! I never used AFP before, is there a canonical way of importing theories from AFP? It also seems to depend on List_Index which is AFP-only as well by the looks of it

#### Manuel Eberl (Apr 27 2021 at 11:18):

The easiest way is to download the AFP, include it as a component (that's explained on the website) and then you can import it by writing `Comparison_Sort_Lower_Bound.Linorder_Relations`.

#### Manuel Eberl (Apr 27 2021 at 11:19):

You can also try just copying out whatever parts of the theory you need (no need to cite me or anything).

Last updated: Aug 10 2022 at 19:17 UTC