Stream: Beginner Questions

Topic: finite_induct over sets


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Max Nowak (Mar 10 2021 at 14:39):

Oh, yeap, that was it. Thanks!

view this post on Zulip 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..)

view this post on Zulip 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..

view this post on Zulip Mathias Fleury (Mar 10 2021 at 14:53):

why would you want to do that?

view this post on Zulip Max Nowak (Mar 10 2021 at 14:54):

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

view this post on Zulip 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…

view this post on Zulip 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

view this post on Zulip 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..

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

'a is assumed to have a linear order

view this post on Zulip Max Nowak (Mar 10 2021 at 18:40):

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

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

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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…

view this post on Zulip Max Nowak (Mar 11 2021 at 14:25):

Oh sorry I had somehow missed your message yesterday.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Max Nowak (Mar 11 2021 at 15:03):

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

view this post on Zulip 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)

view this post on Zulip Mathias Fleury (Mar 11 2021 at 16:06):

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

view this post on Zulip Mathias Fleury (Mar 11 2021 at 16:06):

You cannot do that.

view this post on Zulip Mathias Fleury (Mar 11 2021 at 16:06):

The definition is not well defined

view this post on Zulip 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)"

view this post on Zulip Mathias Fleury (Mar 11 2021 at 16:17):

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

view this post on Zulip Jakub Kądziołka (Mar 11 2021 at 16:38):

This is available as Finite_Set.fold_graph

view this post on Zulip Mathias Fleury (Mar 11 2021 at 17:08):

ah, I did not know about that predicate. Thanks

view this post on Zulip 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

view this post on Zulip 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..

view this post on Zulip Lukas Stevens (Apr 27 2021 at 11:07):

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

view this post on Zulip Max Nowak (Apr 27 2021 at 11:07):

Just on A (and S is a subset).

view this post on Zulip Mathias Fleury (Apr 27 2021 at 11:08):

can you use SOME xs. set xs = A?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Manuel Eberl (Apr 27 2021 at 11:09):

sorted_wrt_list_of_set

view this post on Zulip Manuel Eberl (Apr 27 2021 at 11:09):

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

view this post on Zulip Max Nowak (Apr 27 2021 at 11:14):

Looks like linorder_on is equivalent to linear_order_on

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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: Sep 25 2021 at 08:21 UTC