Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Equivalent inductive definitions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Equivalent inductive definitions


Chronological Thread 
  • From: Duckki Oe <duckki AT mit.edu>
  • To: Marcus Ramos <mvmramos AT gmail.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Equivalent inductive definitions
  • Date: Mon, 22 Jul 2013 16:20:24 -0400

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.






Archive powered by MHonArc 2.6.18.

Top of Page