CODEWITHSUNDEEP
mathsetcoq
Lance Pollard
Lance Pollard

Reputation: 79248

How to define non-empty set in Coq?

Trying to create my first Coq definitions after doing many tutorials. Wondering how to define something simple like an alphabet, if the definition is:

Σ is an alphabet iff it's a finite nonempty set of symbols.

Got this much:

Require Import Coq.Lists.ListSet.

Definition alphabet := set.

But how do you specify the "must be a finite, non-empty set" part?

Upvotes: 2

Views: 806

Answers (1)

Vinz
Vinz

Reputation: 6047

Since you choose your alphabet to be set, it is by definition finite, since set is defined as an instance of list, and inductive types are always finite.

The ListSet library you are using defines emptyset so your first option would be to state that

Definition not_empty (a: alphabet) : Prop := a <> empty_set.

Or you could rely on the fact that your set is list and pattern match on the expression:

Definition not_empty (a: alphabet) : bool := match a with
  | nil => false
  | _ => true
end.

(You can also define the latter in Prop instead of bool by using False and True.)

EDIT: Some clarification asked by Arthur (Simplification here, grab a real text-book about inductive types if you want a more precise explanation):

An inductive type can be inhabited by:

  • a finite number of elements (for example, bool),
  • an infinite number of elements (for example, nat)
  • no element at all (for example False).

However, any element of an inductive type is by construction finite. For example you can write any natural number by composing a finite number of time the constructor S but you have to use O at some point and ''stop'' the construction of your term. Same goes for lists: you can build an arbitrary long list, but its length will always be finite.

Upvotes: 1

Related Questions