coq

2热度

2回答

我正在尝试Coq，但我不完全确定我在做什么。方法是： Theorem new_theorem : forall x, P:Prop /\ Q:Prop 等同于： ∀x (P(x) and Q(x)) 编辑：我认为他们是。

2热度

1回答

我有以下定义在Coq中的电感类型。 Inductive natlist : Type := | nil : natlist | cons : nat -> natlist -> natlist. Notation "x :: l" := (cons x l) (at level 60, right associativity). Notation "[ ]" := nil. Notat

14热度

3回答

使用归纳时保存信息？

我正在使用Coq Proof Assistant来实现（小）编程语言的模型（扩展了Bruno De Fraine，Erik Ernst，MarioSüdholt的Featherweight Java的实现）。在使用induction策略时不断出现的一件事是如何保留包装在类型构造函数中的信息。我有一个子打字道具实现为 Inductive sub_type : typ -> typ -> Prop

7热度

2回答

Coq中的构造函数是什么？

我无法理解构造函数的原理以及它的工作原理。例如，在勒柯克，我们都被教导来定义自然数是这样的： Inductive nat : Type := | O : nat | S : nat -> nat. 而且已被告知，S是一个构造，但究竟是什么意思？如果我再做： Check (S (S (S (S O)))). 我得到的，它是4和nat类型。这是如何工作的，Coq如何知

3热度

2回答

使用Coq的证明谓词逻辑 - 初级语法

我试图证明在Coq的以下内容：目标（的forall X：X，P（X）/ \ Q（X）） - >（（X的forall ：X，P（x））/ \（全部x：X，Q（x）））。有人可以帮忙吗？我不知道是否分割，做一个假设等我的道歉，作为一个完整的小白

5热度

1回答

帮助与勒柯克证明了亚

我的定义归纳类型： Inductive InL (A:Type) (y:A) : list A -> Prop := | InHead : forall xs:list A, InL y (cons y xs) | InTail : forall (x:A) (xs:list A), InL y xs -> InL y (cons x xs). Inductive SubS

9热度

4回答

证明F（˚F布尔）=布尔

我在COQ如何，证明，接受一个布尔true|false并返回一个函数f一个bool true|false（如下所示）中，当在单个布尔施加两次true|false将始终返回相同值true|false： (f:bool -> bool) 例如功能f只能做4两件事，让调用函数b的输入：总是返回true 总是返回false 返回b（即，如果b为真反之亦然）返回返回true not b（即，如果b为