I would like to prove a property for any finite set, morally, by induction on its cardinal. Is finType the appropriate structure to do this? If yes, what would the correct syntax look like? If no, what else should I import? Thank you very much in advance!

Have a look at https://math-comp.github.io/htmldoc/mathcomp.ssreflect.finset.html and `card`

and maybe also bigop

@Guillaume Dubach . The pattern on how do to induction on an arbitrary metric such as `#|A|`

, where `A`

can be either a finite type or a finite set), is explained in `ssrnat`

. See the comment above this lemma: https://math-comp.github.io/htmldoc/mathcomp.ssreflect.ssrnat.html#ubnP.

Thanks!

@Enrico Tassi @Christian Doczkal So, actually the problem is that I need to do this induction, not on subsets of a fintype, but rather on finite subsets of an infinite type (namely triples in nat * nat * nat). It seems that these notations do not apply to that case... Any suggestion?

@Guillaume Dubach maybe you are looking for finitely supported sets then? They are in mathcomp-finmap: https://github.com/math-comp/finmap/blob/master/finmap.v (type `{fset K}`

, where `K`

is a `choiceType`

)

here is one induction principle for `{fset K}`

: https://github.com/math-comp/finmap/blob/master/finmap.v#L2490-L2491

@Karl Palmskog Yes! This looks like exactly what I need. Thank you very much.

I would say it depends on how much you need. If large parts of your development use finite sets over countable types (e.g., `nat`

) then finmap is certainly the way to go. If you only need this for a few inductions, then maybe using the size of (duplicate free) lists may do the trick and require less dependencies and a lower investment.

@Karl Palmskog I imported finmap all right, but when I try to define a finite subset with the notations explained in finmap.v I get the error message: "Unknown interpretation for notation "[ fset _ : _ | _ ]". Can you guess what is the matter?...

@Guillaume Dubach hmm, not off the top of my head, but @Cyril Cohen is likely to be able to tell

if it helps, here is some example code using finmap and its notations: https://github.com/runtimeverification/algorand-verification/blob/master/theories/algorand_model.v#L459

What if you write ([fset _ : _ | _])%fset ?

right, the problem could be that the desired scope is not opened, e.g., in the file linked we have:

```
Open Scope fset_scope.
```

@Karl Palmskog @Reynald Affeldt Yes, it works, thanks ! At least the definition of the set is recognized now and I can make a few things work. But I have another related issue: if I have a variable A : {fset nat} and a function f: A->A in my context, I cannot write for instance propositions like "x < f(x)". I get the error message: The term "x" has type "fset_sub_type A" while it is expected to have type "nat"... So, what is the correct syntax here? If A is a subset of nat then in particular it should be ok to consider its elements as natural integers?...

@Guillaume Dubach not sure I can make sense of this. If you want to make a claim over elements of `A : {fset nat}`

, you have to say `x \in A`

and `y \in A`

, and then `x < y`

will make sense.

If f is defined as a function from A to A, then Coq infers the type of x when I write f(x), isn't it so?

why would `f(x)`

be an element of `A`

?

Because in the context f appears with the type A->A. But perhaps this is not the good notation for functions defined on finite subsets?

my default view for set libraries in Coq is that you can't simply assume that an element `t`

of a set type `T`

is such that `t : T`

set libraries typically just give you a way to query membership, get a hold of all elements, etc.

For instance I can write the following and it works:

Variable (A:{fset nat}).

Definition fixedpt (f:A->A) (x: A) := (f x = x)%nat.

So that should mean Coq is ok with me saying that f x and x are the same as natural integers ? But if I replace = by < it doesn't work anymore.

Well, `A : {fset nat}`

seen as a type is the type of dependent pairs of `n:nat`

and proofs of `n \in A`

. This implements both the finType interface and is a subtype of nat. So you can write:

```
Definition foo (f:A->A) (x: A) := (val (f x) < val x).
```

Here `val`

is the generic first projection for subtypes. In the other direction, you have the `[` _]`

notation as in

```
Definition intoA (n : nat) (p : n \in A) : A := [` p].
```

Also, you should not confuse the following:

```
Definition fixedpt (f:A->A) (x: A) := (f x = x)%nat.
Definition fixedpt (f:A->A) (x: A) := (f x = x :> nat).
```

The first merely opens the (already open) nat_scope for (f x = x), which changes nothing far as the typing of `f x = x`

is concerned. The latter tries to type the equality at type `nat`

and produces the same error as you get when replacing `=`

with `<`

.

Thank you, this is extremely helpful!

I think it should be noted that Coq itself doesn't do subtyping in general. MathComp subtypes are just one (tried and tested) way to do it on top of existing mechanisms/libraries.

Couldn't an order relation be extended to any `A : fset T`

once there is one on `T`

?

@Marie Kerjean The infrastructure for this is clearly there, see

```
Order.SubOrder.sub_OrderType:
forall {disp : unit} {T : orderType disp} [P : predPredType T],
subType (T:=T) P -> orderType disp
```

However, I don't know enough on the interplay between `leq`

/`ltn`

as defined in `ssrnat`

and the generic infrastructure in `order`

for setting this up. In any event, inserting `val`

in the right places might help to distinguish the types at which the comparison is done.

Last updated: Jul 15 2024 at 19:01 UTC