- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
考虑到以下假设:
Variable A : finType.
Variable B : finType.
Variable C : finType.
记录定义为:
Record example := Example {
example_A : A;
example_B : B;
example_C : C;
}.
直观上,示例似乎也必须是 finType
。
查看其他代码库,我看到人们使用以下形式的构造派生出仅具有一个非证明术语的记录的 finType
Definition <record>_subType := Eval hnf in [subtype for <record-accessor>].
Definition <record>_finMixin := Eval hnf in [finMixin of <record> by <:].
但在本例中,记录有多个字段。
是否有一种自动方法可以为记录派生 fintype,如果没有,如何为记录派生 fintype?
最佳答案
数学组件中的许多接口(interface)实现可以通过显示您的类型是实现该接口(interface)的其他类型的缩回来派生。在您的示例中,我们只需将记录转换为元组。
From mathcomp Require Import
ssreflect ssrfun ssrbool ssrnat eqtype seq choice fintype.
Variables A B C : finType.
Record example := Example {
example_A : A;
example_B : B;
example_C : C
}.
Definition prod_of_example e :=
let: Example a b c := e in (a, b, c).
Definition example_of_prod p :=
let: (a, b, c) := p in Example a b c.
Lemma prod_of_exampleK : cancel prod_of_example example_of_prod.
Proof. by case. Qed.
Definition example_eqMixin :=
CanEqMixin prod_of_exampleK.
Canonical example_eqType :=
Eval hnf in EqType example example_eqMixin.
Definition example_choiceMixin :=
CanChoiceMixin prod_of_exampleK.
Canonical example_choiceType :=
Eval hnf in ChoiceType example example_choiceMixin.
Definition example_countMixin :=
CanCountMixin prod_of_exampleK.
Canonical example_countType :=
Eval hnf in CountType example example_countMixin.
Definition example_finMixin :=
CanFinMixin prod_of_exampleK.
Canonical example_finType :=
Eval hnf in FinType example example_finMixin.
在此代码段的末尾,example
被声明为 finType
。 (请注意,eqType
、choiceType
等的所有其他声明也是必要的,因为 finType
是它们的子类。)
关于coq - 在 coq 中导出记录的规范结构 (ssreflect),我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/51516954/
我正在阅读 ssreflect 教程,which reads : Below, we prove the ... by translating the propositional statement
我正在尝试制作 ssreflect OrdType来自涉及字符串的自定义类型。我假设 ssreflect 中有一些内置的字符串订单类型,但我无法在任何地方找到它。我在 Coq 的标准库中看到一个,但我
我正在尝试处理 ssreflect 中的规范结构。我从 here 中提取了 2 段代码. 我将为 bool 和选项类型带来作品。 Section BoolFinType. Lemma bool_e
我是 Coq 新手,因此为了提高我对证明检查的理解,我尝试使用 Ssreflect 库。 我已经在终端上运行的 Mac OS v 10.10.3 ( Yosemite ) 上安装了 Ssreflect
例如,coq 在其标准库中有一个 Classical 包,其中包含经典逻辑中的引理,例如与 forall 和 exists 相关的引理 (https://coq.inria.fr/library/Co
我在 Coq 的 SSReflect 扩展中发现了两个约定,它们看起来特别有用,但我还没有在较新的依赖类型语言(Lean、Agda、Idris)中看到它们被广泛采用。 首先,在可能的情况下,谓词被表示
我有下一个定义(代码可以编译): From mathcomp Require Import all_ssreflect. Set Implicit Arguments. Set Asymmetric
我有下一个定义(代码可以编译): From mathcomp Require Import all_ssreflect. Set Implicit Arguments. Set Asymmetric
考虑到以下假设: Variable A : finType. Variable B : finType. Variable C : finType. 记录定义为: Record example :=
在我看来,使用 ssreflect,当我们进行依赖模式匹配时,隐式构造函数字段会变成显式字段,并且设置各种隐式选项不会影响此行为。 以下代码适用于 Coq 8.6: Require Import Co
我试图以非 ssreflect Coq 的方式理解 Coq/ssreflect 证明中 : (冒号)的确切含义。 我读到它与将事情转移到目标有关(例如概括??),并且与 => 相反,后者将事情转移到假
Coq 有一些方便的策略来自动证明算术引理,例如 lia : From Coq Require Import ssreflect ssrfun ssrbool. From mathcomp Requi
我有以下反射(reflect)谓词: Require Import mathcomp.ssreflect.all_ssreflect. Inductive reflect (P : Prop) (b
我已经在 Linux (Ubuntu 17.04) 中成功安装了 Coq 8.6 和 CoqIDE。但是,我不知道如何继续将 SSReflect 和 MathComp 添加到此安装中。我检查过的所有引
我有一个结构,由有限类型上的序列和该序列的 uniq 证明组成。这应该描述一个显然是有限的类型,但我不知道如何证明这一点。 我以为我可以使用 UniqFinMixin,但是它需要 - 如果我理解正确的
在 Vanilla Coq 中,我会写 Require Import Coq.Arith.Arith. Goal nat -> nat -> False. intros n m. destru
我是一名优秀的程序员,十分优秀!