时间戳

首页 > 解决方案 > 了解 Coq 中的复合类型 [软件基础]

coq - 了解 Coq 中的复合类型 [软件基础]

问题描述

软件基础、基础知识、复合类型

我正在尝试理解 Coq（第 2 天，请耐心等待，如果这很愚蠢，对不起），但我正在查看 Software Foundations 书中关于复合类型的部分，并试图理解这一点：

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

好的，所以这些是共归纳类型，我的问题是“主要”的定义。我看到 rgb 是一种枚举类型，颜色的一部分是，但主要是一个函数。

问题是，看起来这将是一个接受 rgb 并返回颜色的函数，但是该部分中的所有以下示例（单色，isred）都返回布尔值。

看起来我们在本书中一直使用的自反性属性（再次，像第 1 页，请耐心等待）看起来像你的策略，并证明了平等；到目前为止，我们所有的示例都已boolean = boolean格式化。

我们需要定义一个接受 rgb 并返回颜色的函数，并且我们可以使用反射性（因为这就是我们在第 1 页上所知道的）来解决，对吗？对于单元测试？

我在正确的轨道上吗？我想我只是对单色和 isred 的引入感到困惑，这又回到了使用布尔值，这似乎不是我们试图解决的问题，以获得一个有效的颜色示例。

标签： coq

解决方案

（第一的：

这些是互感类型

这些实际上是归纳类型，但这可能是一个错字。）

看起来这将是一个接受 rgb 并返回颜色的函数

是的，这正是primary：一个接受一个元素rgb并返回一个元素的函数color。这是一种特殊的函数，称为构造函数。构造函数与常规函数的不同之处在于，归纳类型的每个元素都是从该类型的一个构造函数中获得的。在第一章中，还有其他由模式匹配定义的函数，例如monochrome. 该函数返回一个布尔值，但我们也可以有其他函数返回color。例如：

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

自反性属性 [...] 采用您的策略，并证明相等

关于术语的注释：在这种情况下，reflexivity是一种策略，不以任何策略为论据。但是，您是对的，它用于证明等式。

我们需要定义一个接受 rgb 并返回颜色的函数，并且我们可以使用反射性（因为这就是我们在第 1 页上所知道的）来解决，对吗？对于单元测试？

你在说什么单元测试？本章提到了orb和binary类型的单元测试，但是没有color.

推荐阅读