ssreflect

0熱度

1回答

我正在使用Coq（版本8.5-6），安裝w/Nix。我想安裝ssreflect，最好也是w/Nix。我發現的唯一信息是here。但是，這不是關於安裝ssreflect，只是嘗試它。儘管如此，我試圖嘗試一下，但最終得到了數百個警告（關於各種文件的內容.v和.ml4），並且不能等待該過程結束。一個相當典型的警告是這樣的：文件「./algebra/ssralg.v」，線路856字符0-39：警告：

3熱度

1回答

證明Martin-Lof的等式與Path Coction在Coq中的同構

我正在研究Coq並試圖證明Martin-Lof的等式與Path Induction的同構。我定義了兩個等式如下。 Module MartinLof. Axiom eq : forall A, A -> A -> Prop. Axiom refl : forall A, forall x : A, eq A x x. Axiom el : forall (A : Type) (C : fo

2熱度

2回答

在mathcomp的ssralg中從int_Ring類型中提取整數

針對該問題設置了一點：記號`_i被定義爲序列的第i個分量，但也被認爲是多項式的第i個係數。下面的代碼輸出Negz 2 : int_ZmodType： From mathcomp Require Import all_ssreflect. From mathcomp Require Import all_algebra. Open Scope ring_scope. Definition my

2熱度

1回答

在Coq/SSreflect中排序seq

我目前正在玩coq中的紅黑樹，並希望配備nat的訂單列表，以便使用MSetRBT模塊將它們存儲在紅黑樹上。出於這個原因，如圖所示我已經定義seq_lt： Fixpoint seq_lt (p q : seq nat) := match p, q with | _, [::] => false | [::], _ => true | h :: p', h' :: q'

2熱度

2回答

什麼時候在ssreflect/Coq中需要`：`（冒號）？

我試圖根據非ssreflect Coq來理解Coq/ssreflect證明中:（冒號）的確切含義。我讀到它與將事物移到目標（如概括??）和=>相反，它將事物移到假設。然而，我經常發現它令人困惑，因爲證據無論是否有:。下面是從一個教程的一個示例： Lemma tmirror_leaf2 t : tmirror (tmirror t) = Leaf -> t = Leaf. Proof. mov

4熱度

2回答

ssreflect是否假設被排除的中間？

我讀了ssreflect教程，which reads：下面，我們證明了...通過翻譯命題陳述到其布爾對應，這是很容易使用暴力力證明。這種證明技術被稱爲反射。 Ssreflect的設計允許和ssreflect的精神建議廣泛使用這種技術。這（反射）是否意味着ssreflect假定被排除的中間（forall A:Prop, A \/ ~A）？它看起來就是這樣，因爲所有的布爾值都滿足E.M.

1熱度

1回答

勒柯克 - 證明涉及bigops在Ssreflect

我試圖證明使用數學組件庫遵循嚴格的不等式： Lemma bigsum_aux (i: 'I_q) (j: 'I_q) (F G : 'I_q -> R): (forall i0, F i0 <= G i0) /\ (exists j0, F j0 < G j0) -> \sum_(i < q) F i < \sum_(i < q) G i. 起初，我試圖找到一些引理相當於b

2熱度

1回答

Coq的 - 在Ssreflect

證明約序列的元素條件I有一個目標，看起來像這樣： x \in [seq (f v j) | j <- enum 'I_m & P v j] -> 0 < x 在上文中，f是一個定義生成取決於v, j和P v j是一個不等式的溶液謂詞將j限制在滿足另一個不等式的指數上。我已經證明，Goal : P v j -> (f v j > 0)，但我怎麼能用這個證明它適用於序列中的任何x？我發現了幾個相

0熱度

1回答

自動化ssreflect的，勒柯克而與矛盾的假設處理有關NAT號

而在下面的引理使用ssreflect： From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype. Lemma nat_dec n m: (m <= n) -> (~~ (m <= n)) -> False. Proof. intros A notA. (* auto. *) red

1熱度

2回答

在Ssreflect中證明簡單的不等式

我在Coq中使用MathComp庫進行反射時遇到了一些非常簡單的問題。假設我要證明這個定理： From mathcomp Require Import ssreflect ssrbool ssrnat. Lemma example m n: n.+1 < m -> n < m. Proof. have predn_ltn_k k: (0 < k.-1) -> (0 < k).