Stream: math-comp users

Topic: A question on fset


view this post on Zulip Xiaokun Luan (Apr 19 2021 at 08:38):

I am trying to prove [seq f x | x <- t |` s] = f t :: [seq f x | x <- s] by induction on size of s, which is a fset.
But even when s is fset0, I can't prove [seq f x | x <- [fset t]] = [:: f t].
I thought that the coercion enum_fset from finSet to seq should lead the left-hand side term to something like [seq f x | x <- [:: t]], but it doesn't. So what is the correct way to prove this?

view this post on Zulip Ana de Almeida Borges (Apr 19 2021 at 12:45):

For the base case, you can use

  by rewrite enum_fsetE enum_fset1.

Maybe enum_fsetE can help with the full lemma as well.

view this post on Zulip Ana de Almeida Borges (Apr 19 2021 at 12:50):

But alas, now that I look at it again, are you sure it's true? If t \in s, then t |` s = s. So I think you need undup on the right-hand-side, and probably something to deal with the order of the resulting list. Or prove that both lists have the same elements and the same size instead of proving equality (ie, prove _ =i undup _ instead of _ = _).

view this post on Zulip Ana de Almeida Borges (Apr 19 2021 at 12:53):

Or assume t \notin s to begin with.

view this post on Zulip Laurent Théry (Apr 19 2021 at 12:55):

Are you sure this is really what you want to do?
Is it not something like : [fset f x | x in t |`s] = f t |` [fset f x | x in s]? Why you want to manipulate list?

view this post on Zulip Xiaokun Luan (Apr 19 2021 at 14:31):

It works, thank you. I tried enum_fsetE but not enum_fset1, and I still don't understand how it works.

view this post on Zulip Xiaokun Luan (Apr 19 2021 at 14:38):

Laurent Théry said:

Are you sure this is really what you want to do?
Is it not something like : [fset f x | x in t |`s] = f t |` [fset f x | x in s]? Why you want to manipulate list?

Sorry I didn't mention the precondition t \notin s. The reason that I want to manipulate list is that I wrote a function that maps the domain of a fmap to a list of objects, and then I applied foldr to this list to get its maximum, so the order doesn't matter, but still thanks for the advice all the same.

view this post on Zulip Ana de Almeida Borges (Apr 19 2021 at 14:48):

then I applied foldr to this list to get its maximum

Maybe \max could be useful here. You can get the maximum of a set without going through seq (well, maybe that's how it's implemented under the hood, but this should be immaterial). See https://math-comp.github.io/htmldoc/mathcomp.ssreflect.bigop.html

So if you have your set s and a function f : s -> nat, you can do \max_(x <- s) f x. There are already some lemmas about bigmax, which should be useful.

view this post on Zulip Xiaokun Luan (Apr 19 2021 at 15:04):

Ana de Almeida Borges said:

Maybe \max could be useful here. You can get the maximum of a set without going through seq (well, maybe that's how it's implemented under the hood, but this should be immaterial). See https://math-comp.github.io/htmldoc/mathcomp.ssreflect.bigop.html

I took a quick look at the document, it seems that \max is defined on the %N scope, but the object in the list I need to deal with is actually also list, and the relation is defined by a boolean comparison function. Is there another way to deal with this? Or maybe \max can also be defined by passing a comparison function?

view this post on Zulip Ana de Almeida Borges (Apr 19 2021 at 15:06):

You can use \big[op/idx], where op is the operation you wish to iterate and idx is the base case. So for example, \max = \big[maxn/0]

view this post on Zulip Xiaokun Luan (Apr 19 2021 at 15:12):

That's very good news for me, maybe it can save lots of proofs. But for now, I'm in hurry and this project is almost finished, so maybe I will try to rewrite the definition and proofs later.

view this post on Zulip Ana de Almeida Borges (Apr 19 2021 at 15:14):

Yeah, using already-existing unknown-to-you libraries does have a learning curve.

view this post on Zulip Xiaokun Luan (Apr 19 2021 at 15:19):

I'm currently stuck at the induction case, don't know what to do after rewriting enum_fsetE. Frankly, I don't know much about the mechanism, and I often feel like a reinforcement learning agent, trying different combinations of tactics to get the goal proved... So do you have any advice on the proof of induction case?

view this post on Zulip Cyril Cohen (Apr 19 2021 at 15:36):

Xiaokun Luan said:

I am trying to prove [seq f x | x <- t |` s] = f t :: [seq f x | x <- s]

I see no reason why this would be true: sets are equivalent to lists quotiented by duplication and permutation, the sequence obtained from a finite set is one canonical representative but has no guarantee of stability by set operation (here union with a singleton).

view this post on Zulip Cyril Cohen (Apr 19 2021 at 15:37):

the best you can hope to prove is [seq f x | x <- t |` s] =i f t :: [seq f x | x <- s]

view this post on Zulip Laurent Théry (Apr 19 2021 at 15:37):

@Cyril Cohen there is an extra conditiont is not in s

view this post on Zulip Cyril Cohen (Apr 19 2021 at 15:38):

even so, I do not see why f t would come first

view this post on Zulip Cyril Cohen (Apr 19 2021 at 15:38):

and the best would then be perm_eq [seq f x | x <- t |` s] (f t :: [seq f x | x <- s])

EDIT: not even because even if t \notin s, f t might be in [fset f x | x in s]

view this post on Zulip Laurent Théry (Apr 19 2021 at 15:40):

it will not but i think the problem is in fact to find the maximum in a set of set of nat

view this post on Zulip Xiaokun Luan (Apr 19 2021 at 15:50):

I see... I thought the definition of union is [fset[fsetU_key] x in enum_fset A ++ enum_fset B] so that when mapping the union to list, f t would come first.

view this post on Zulip Cyril Cohen (Apr 19 2021 at 15:51):

Xiaokun Luan said:

I see... I thought the definition of union is [fset[fsetU_key] x in enum_fset A ++ enum_fset B] so that when mapping the union to list, f t would come first.

[fset x in stuff] is the canonical surjection in the type of fsets, the particular ordering of elements disappears then

view this post on Zulip Cyril Cohen (Apr 19 2021 at 15:52):

what is it you are trying to prove?

view this post on Zulip Xiaokun Luan (Apr 19 2021 at 15:56):

Assumef is a finmap from K to V, and foo is a function that maps the domain of the finmap to a list of lists, I want to prove that there exists two lists s1 and s2 such that foo f = s1 ++ s2 /\ foo f.[k <- v] = s1 ++ x :: s2, where x is a list that can be computed from k.

view this post on Zulip Cyril Cohen (Apr 19 2021 at 15:59):

I'm afraid I do not understand what foo is supposed to be

view this post on Zulip Xiaokun Luan (Apr 19 2021 at 16:05):

The finmap f maps a block's hash value(block is a struct) to the block itself, and every block has a field prev_block that points to its previous block. Assume that there is another function g that takes a finmap and a block's hash value as input, and returns the longest chain starting from the given block. What foo does is applying the function g to each hash value in its domain to return a list of chain.

view this post on Zulip Cyril Cohen (Apr 19 2021 at 16:10):

Then I do not see why it would satisfy foo f = s1 ++ s2 nor foo f.[k <- v] = s1 ++ x :: s2 , but I do not see the link with your previous question...

view this post on Zulip Xiaokun Luan (Apr 19 2021 at 16:14):

I'm sorry I didn't explain myself clearly.
The thing that I want to prove is that, if the finmap f is already a tree, every block's previous block is also in this tree(except for the root node), and if there is a new block v added to the tree, then what foo returns on f.[k <- v] differs from the output foo f only at one element, which is the chain starting from v.

view this post on Zulip Xiaokun Luan (Apr 19 2021 at 16:16):

At first, I thought that s1 = [::] would be sufficient, so what I want to prove in the first place is foo f = s2 /\ foo f.[k <- v] = x :: s2, which I think is also wrong.

view this post on Zulip Cyril Cohen (Apr 19 2021 at 16:17):

maybe a list of list is not even the right output for foo...

view this post on Zulip Xiaokun Luan (Apr 19 2021 at 16:19):

Emmm you mean given two finmap f1 and f2, it is possible that f1 = f2 but foo f1 <> foo f2?

view this post on Zulip Cyril Cohen (Apr 19 2021 at 16:21):

no

view this post on Zulip Xiaokun Luan (Apr 19 2021 at 16:33):

The definition of foo is [seq compute_blockchain bt b | b <- [seq get_block bt k | k <- domf bt]] where compute_blockchain is the function g that computes the chain and get_block bt k returns the block whose hash is k
Anyway thanks a lot for your patience


Last updated: Feb 08 2023 at 04:04 UTC