Ssreflect Users Discussion List

[Georges Gonthier <>]

Hi Aleks,

 

   The rationale for the design is that any type that’s an eqType should also be a choiceType:

 - if comparison is defined effectively, then the type must be a concrete datatype, therefore countable, hence have a choiceType

 - if comparison is simply assumed (via strong excluded middle), then choice can be assumed as well

Note that “all eqTypes are countable in an axiom-free development” is a meta-fact, not an actual theorem.

I’ve yet to write the boilerplate to make it easier to supply the evidence for it on a case-by-case basis (e.g., encoding tree shapes in nat), though

choice.v should provide most of the basic technology (such as the countType structure on seq nat).

 

  Georges

 

---

From: Aleks Nanevski [mailto:]
Sent: 18 June 2009 07:05
To:
Subject: finite types

 

Hi everyone,

 

I was wondering what is the easiest way to define a finite type out of a sequence of elements of type T : eqType.

 

The stuff given in SeqFinType section of fintype.v is a bit too demanding, as it is asking me to first prove that T : choiceType.

 

In the previous version of ssreflect, there was a way to do this in one line (via lemma which used to be called seq_enum), but that seems to have disappeared in the new version of the libraries.

 

Thanks,

Aleks