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?

For the base case, you can use

```
by rewrite enum_fsetE enum_fset1.
```

Maybe `enum_fsetE`

can help with the full lemma as well.

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 `_ = _`

).

Or assume `t \notin s`

to begin with.

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?

It works, thank you. I tried `enum_fsetE`

but not `enum_fset1`

, and I still don't understand how it works.

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.

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.

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?

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]`

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.

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

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?

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

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

@Cyril Cohen there is an extra condition`t`

is not in `s`

even so, I do not see why `f t`

would come first

~~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]`

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

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.

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

what is it you are trying to prove?

Assume`f`

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`

.

I'm afraid I do not understand what `foo`

is supposed to be

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.

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

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`

.

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.

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

...

Emmm you mean given two finmap `f1`

and `f2`

, it is possible that `f1 = f2`

but `foo f1 <> foo f2`

?

no

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: Jul 25 2024 at 15:02 UTC