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爲