The Coq mailing list

[Duckki Oe <duckki AT mit.edu>]

Hello, Marcus. 

Of course, you can define an isomorphism between the two structures, and 
switch back and forth as you wanted. But, before that, your definitions are 
roughly equivalent to (tree string) and (list string). I don't clearly see 
why you need these new definitions.  Coq library has more abstract definition 
of Sets like Ensemble and also ListSet, which is a set backed by a list (just 
like your second definition). I like Ensemble because the equivalence 
relation is more natural than the List-based set. I hope their definitions 
could give you an inspiration.

Back to the original question, I like the second definition because it has a 
simpler structure (linear). Let's assume that we defined the string_set as 
(list string). When you want to case-split on the union of sets, you may use 
this kind of lemma. (note: the "++" operator is used as the union operator 
and "In" as the set-membership operator.)

Lemma ss_app_split : forall x y (a : string), In a (x ++ y) -> In a x \/ In a 
y.
  induction x; simpl; auto; destruct 1; subst; auto.
  edestruct in_app_or; eauto 3.
Qed.



-- Duckki



On Sunday, July 21, 2013 at 5:56 PM, Marcus Ramos wrote:

> Hi,
> 
> As a novice user of Coq, I have difficulties deciding what is the best
> definition for an inductive type. For example, I have this definition of a
> string set:
> 
> Inductive string_set: Set :=
> | ss_empty: string_set
> | ss_str: string->string_set
> | ss_build: string_set->string_set->string_set.
> 
> which is appropriate for some purposes (a few fixpoints that I am writing).
> However, for other purposes, I find it almost impossibile to advance with 
> this
> definition. In this case, the following definition suits better for my
> objectives (another set of fixpoints):
> 
> Inductive string_set: Set :=
> | ss_empty: string_set
> | ss_str: string->string_set
> | ss_build: string->string_set->string_set.
> 
> (the difference is in the type of ss_build constructor).
> 
> My question is: how can I be able to take advantage of both ways of defining
> this inductive type, and thus be able to define all my fixpoints properly? 
> Can
> I combine them somehow? Or convert from one to the other? Or...?
> 
> Thanks in advance,
> Marcus.