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_listor 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: Apr 20 2024 at 04:19 UTC