ssreflect

    0熱度

    1回答

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

    3熱度

    1回答

    我正在研究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回答

    針對該問題設置了一點:記號`_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中的紅黑樹,並希望配備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來理解Coq/ssreflect證明中:(冒號)的確切含義。 我讀到它與將事物移到目標(如概括??)和=>相反,它將事物移到假設。然而,我經常發現它令人困惑,因爲證據無論是否有:。下面是從一個教程的一個示例: Lemma tmirror_leaf2 t : tmirror (tmirror t) = Leaf -> t = Leaf. Proof. mov

    4熱度

    2回答

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

    1熱度

    1回答

    我試圖證明使用數學組件庫遵循嚴格的不等式: 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回答

    證明約序列的元素條件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: 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回答

    我在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).