Stream: math-comp users

Topic: A question on fset

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?

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.

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 _ = _).

Ana de Almeida Borges (Apr 19 2021 at 12:53):

Or assume t \notin s to begin with.

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?

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.

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.

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.

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?

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]

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.

Ana de Almeida Borges (Apr 19 2021 at 15:14):

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

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?

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

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]

Laurent Théry (Apr 19 2021 at 15:37):

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

Cyril Cohen (Apr 19 2021 at 15:38):

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

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]

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

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.

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

Cyril Cohen (Apr 19 2021 at 15:52):

what is it you are trying to prove?

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.

Cyril Cohen (Apr 19 2021 at 15:59):

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

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.

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

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.

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.

Cyril Cohen (Apr 19 2021 at 16:17):

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

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?

Cyril Cohen (Apr 19 2021 at 16:21):

no

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