CODEWITHSUNDEEP
coq
Tony
Tony

Reputation: 373

Define basic inductive types in coq

Very basic question about coq. How do I define the following two inductive types?

Type 1 containing: o fo, ffo, fffo... k, sk, ssk, sssk... Note that the f here could alternatively be characterized as the natural number index for o.

Type 2 containing the same but now we can also have terms like fsffsk and sfsfso.

Upvotes: 1

Views: 272

Answers (2)

Lucien David
Lucien David

Reputation: 320

Do you actually need to base type2's definition on type1 ? Because actually just a simple definition : 

Inductive type2 : Type :=
| o : type2
| k : type2
| f : type2 -> type2
| s : type2 -> type2
.

And then define examples like :

Definition typeExample : type2 := f (s (f (s (s (f (s (k))))))).

Upvotes: 2

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23582

If I understand your first type correctly, you can represent it by combining simpler types defined in the Coq standard library:

Definition t1 : Type := nat + nat.

The + operator on types is the disjoint union of two types. The idea is that the element inl n, which is injected on the left of the union, represents the string fff...o, with n occurrences of f, whereas the element inr n, which is injected on the right of the union, represents the string sss...k, with n occurrences of s.

I do not understand the patterns on the second type. Did you really mean to write fsffsk instead of fsfsfsk?

Upvotes: 1

Related Questions