The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Saturday, September 24, 2011 10:29:58 AM Vladimir Voevodsky wrote:
> It is arguable whether overusing induction and Prop is of any benefit for
> the type-theoretic formalization of mathematics. In my experience one can
> formalize everything with very few uses of [ Inductive ] and no use of
> Prop at all.
> 
> For example the use of inductive definition for "less or equal" on [ nat ]
> is unnecessary. One can define boolean less or equal [ leb ] as a
> fix-point and then define type-valued less or equal as [ Identity ( leb n
> m ) true ] . The proofs of all the properties are rather straightforward.
> 
> Vladimir.

What about a case like "the subgroup generated by a subset"?  Using an 
Inductive definition gives something which is fairly straightforward:

Inductive GeneratedSubgroup {G} `{!Group G} (S:Ensemble G) : Ensemble G :=
| GS_incl_S : forall g:G, In S g -> In (GeneratedSubgroup S) g
| GS_group_op_closed : forall g h:G, In (GeneratedSubgroup S) g -> In 
(GeneratedSubgroup S) h -> In (GeneratedSubgroup S) (g*h)
| GS_inv_closed : forall g:G, In (GeneratedSubgroup S) g -> In 
(GeneratedSubgroup S) (inv g)
| GS_contains_unit : In (GeneratedSubgroup S) group_unit.

You could replace the first with "Included S (GeneratedSubgroup S)".  And 
maybe 
(I'm not clear on this) you could even replace the last three with just "| 
GS_subgroup : Subgroup (GeneratedSubgroup S)", where Subgroup is a Class or 
Structure encapsulating the three conditions.  Even if not, if you give names 
like ClosedUnderBinaryOp and ClosedUnderUnaryOp, you could still make it more 
readable.

This is clearer, to my mind, than a definition from above as "the 
intersection 
of all subgroups containing S", or a definition from below as "there exists a 
list of elements of G such that x is the product of the list, and each entry 
in the list is either in S or the inverse of something in S".  Of course, the 
second characterization could be something useful to prove afterwards, based 
on the inductive definition.
-- 
Daniel