coq

    3熱度

    1回答

    有人可以告訴我一個簡單的例子如何使用從Coq.Logic.EqdepFacts公理Streicher_K_公理? 也許用於顯示簡單的事實: Lemma single_proof : forall (A:Type)(x y:A) (u v:x = y), u = v. 我設法與Streicher_K_on_來證明這一點: Variable A:Type. Variable x:A. Axio

    2熱度

    1回答

    我想了解'上下文'表達式(與context模式相反)。在手動它被描述爲: 上下文IDENT [EXPR] IDENT必須表示由 匹配表達式的上下文圖案結合的上下文變量。這個表達式的計算結果用expr的值替換了ident的 值的空洞。 有人可以共享一個例子說明這種構造的用法嗎?我想它必須涉及match使用context模式,然後上述形式使用匹配的上下文。

    2熱度

    1回答

    我一直在嘗試共同誘導類型,並決定定義自然數和向量的共同誘導版本(與他們的大小類型列表)。我確定他們和無限多的像這樣: CoInductive conat : Set := | cozero : conat | cosuc : conat -> conat. CoInductive covec (A : Set) : conat -> Set := | conil : covec A co

    1熱度

    2回答

    我正在嘗試使用可以輕鬆生成的術語(在此特定示例中,從tauto)實例化存在量詞的策略。我第一次嘗試: Ltac mytac := match goal with | |- (exists (_ : ?X), _) => cut X; [ let t := fresh "t" in intro t ; exists t; firstorder

    0熱度

    1回答

    我必須證明: i < Datatypes.length (l0 ++ f :: nil) -> H 我有一個單獨的假說i < Datatypes.length l0和i = Datatypes.length l0。

    0熱度

    1回答

    總之,這可能嗎? 我試圖證明取消在一個組中工作。 我 a, b, x : G H: a <+> x = b <+> x ,我想證明 a = b 我的想法是讓一個假設 H2: a <+> x <+> i x = a <+> x <+> i x (i是反函數)。 我已經試過 pose proof eq_refl (a <+> x <+> i x) as H. 但這似乎並沒有工作。

    1熱度

    2回答

    我需要推理向量在Coq中的置換。標準庫僅包含列表的排列定義。正如我的第一次嘗試,我試圖模仿它的載體: Inductive VPermutation: forall n, vector A n -> vector A n -> Prop := | vperm_nil: VPermutation 0 [] [] | vperm_skip {n} x l l' : VPermutat

    0熱度

    1回答

    如何獲取Coq中所有父元素? 我在Coq的定義一組如下: Inductive Gen : Set := | BGen : nat -> nat -> Gen. 有許多實例,例如: Definition g1 = BGen 1 2. Definition g2 = BGen 2 3. 現在,我想獲得的3父母元件,即[1,2]。我寫一個函數: Fixpoint parents (c : n

    3熱度

    1回答

    我想通過Coq中的兩個參數定義一個嵌套的遞歸函數。 Require Import List. Import ListNotations. Fixpoint map_sequence2 {A B C : Set} (f : A -> B -> option C) (xs : list A) (ys : list B) : option (list C) := match xs, y

    0熱度

    2回答

    我使用的輔助證明COQ,我的第一個問題是關於Induction.v文件,爲什麼我們使用Require Export Basics,而不是Require Import basics?此外,當我們做Export basics.v,即使我改變了基本的名稱Mybasics.v爲什麼工作? 是什麼Require Export Basics.辦?它是導入還是導出? 我試圖編譯induction.v後執行lis