Stream: math-comp users

Topic: Induction on size of finite set


view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Guillaume Dubach (Nov 04 2020 at 09:09):

Thanks!

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Guillaume Dubach (Nov 05 2020 at 15:00):

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

view this post on Zulip 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.

view this post on Zulip 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?...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reynald Affeldt (Nov 12 2020 at 08:28):

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

view this post on Zulip 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.

view this post on Zulip 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?...

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Nov 17 2020 at 09:12):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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].

view this post on Zulip 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 <.

view this post on Zulip Guillaume Dubach (Nov 17 2020 at 10:29):

Thank you, this is extremely helpful!

view this post on Zulip 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.

view this post on Zulip 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 ?

view this post on Zulip 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: Feb 08 2023 at 04:04 UTC