Understanding compound types in Coq [Software Foundations]

Question

Software Foundations, Basics, Compound Types

I'm trying to understand Coq (day 2, so bear with me, sorry if this is stupid) but I'm looking at the section on compound types in Software Foundations book, and trying to understand this:

Inductive rgb : Type :=
  | red : rgb
  | green : rgb
  | blue : rgb.
    Inductive color : Type :=
  | black : color
  | white : color
  | primary : rgb → color.

Ok, so these are coinductive types, and my problem is with the definition of "primary". I see that rgb is an enumerated type, and parts of color are, but primary is a function.

The trouble is, it looks like this would be a function that takes rgb, and returns a color, however all of the following examples in that section (monochrome, isred) return booleans.

It also looks like the reflexivity property we've been using up to that point in the book (again, like page 1, bear with me) looks like it takes your tactic, and proves equality; so far all of our examples have been boolean = boolean in format.

We'd need a definition of a function that took rgb, and returned color, and we can use reflexivity (because that's all we know on page 1) to solve, right? For unit tests?

Am I on the right track? I guess I'm just confused by the introduction of monochrome and isred, which go back to using the booleans, which doesn't seem like what we're trying to solve for to get a valid example of color.

Arthur Azevedo De Amorim Arthur Azevedo De Amorim · Accepted Answer · 2018-08-14T21:16:28

(First:

these are coinductive types

These are actually inductive types, but this was perhaps a typo.)

it looks like this would be a function that takes rgb, and returns a color

Yes, this is precisely what primary is: a function that takes an element of rgb and returns an element of color. This is a special kind of function called a constructor. Constructors are different from regular functions in that every element of an inductive type is obtained from exactly one constructor of that type. In that first chapter, there are other functions defined by pattern-matching, such as monochrome. That function returns a boolean, but we could have other functions that return color as well. For instance:

Definition flip_color (c : color) : color :=
  match c with
  | white => black
  | black => white
  | primary _ => c
  end.

the reflexivity property [...] takes your tactic, and proves equality

A note on terminology: in this context, reflexivity is a tactic, and does not take any tactics as arguments. You are right, however, that it is used to prove equalities.

We'd need a definition of a function that took rgb, and returned color, and we can use reflexivity (because that's all we know on page 1) to solve, right? For unit tests?

What unit tests are you talking about? This chapter mentions unit tests for orb and the binary type, but there are no tests for color.

Understanding compound types in Coq [Software Foundations]

1 Answers