Stream: math-comp users

Topic: Induction on size of finite set

Guillaume Dubach (Oct 31 2020 at 09:13):

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!

Enrico Tassi (Nov 01 2020 at 11:57):

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

Christian Doczkal (Nov 02 2020 at 11:49):

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

Guillaume Dubach (Nov 04 2020 at 09:09):

Thanks!

Guillaume Dubach (Nov 05 2020 at 14:52):

@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?

Karl Palmskog (Nov 05 2020 at 14:55):

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

Karl Palmskog (Nov 05 2020 at 14:58):

here is one induction principle for {fset K}: https://github.com/math-comp/finmap/blob/master/finmap.v#L2490-L2491

Guillaume Dubach (Nov 05 2020 at 15:00):

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

Christian Doczkal (Nov 05 2020 at 15:18):

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.

Guillaume Dubach (Nov 12 2020 at 08:25):

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

Karl Palmskog (Nov 12 2020 at 08:26):

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

Karl Palmskog (Nov 12 2020 at 08:27):

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

Reynald Affeldt (Nov 12 2020 at 08:28):

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

Karl Palmskog (Nov 12 2020 at 08:32):

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

Open Scope fset_scope.

Guillaume Dubach (Nov 17 2020 at 09:03):

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

Karl Palmskog (Nov 17 2020 at 09:07):

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

Guillaume Dubach (Nov 17 2020 at 09:11):

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?

Karl Palmskog (Nov 17 2020 at 09:12):

why would f(x) be an element of A?

Guillaume Dubach (Nov 17 2020 at 09:12):

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?

Karl Palmskog (Nov 17 2020 at 09:19):

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

Karl Palmskog (Nov 17 2020 at 09:19):

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

Guillaume Dubach (Nov 17 2020 at 09:23):

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.

Christian Doczkal (Nov 17 2020 at 10:12):

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

Christian Doczkal (Nov 17 2020 at 10:16):

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

Guillaume Dubach (Nov 17 2020 at 10:29):

Thank you, this is extremely helpful!

Karl Palmskog (Nov 17 2020 at 10:32):

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.

Marie Kerjean (Nov 17 2020 at 10:40):

Couldn't an order relation be extended to any A : fset T once there is one on T ?

Christian Doczkal (Nov 17 2020 at 12:41):

@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: Oct 13 2024 at 01:02 UTC