coq

1熱度

1回答

我無法證明使用coq的策略的簡單邏輯max a b <= a+b。我應該如何解決它？以下是我到現在爲止的代碼。 s_le_n已被證明，但爲簡單起見，此處未提及。 Theorem s_le_n: forall (a b: nat), a <= b -> S a <= S b. Proof. Admitted. Theorem max_sum: forall (a b: nat), max a

-1熱度

2回答

勒柯克：如何證明如果語句涉及字符串？

我有一個string b和string a上比較，如果有平等的string c，否則有string x。我知道的假設fun x <= fun c。我如何證明以下陳述？ fun是一些函數，它發生在string並返回nat。 fun (if a == b then c else x) <= S (fun c) 的邏輯似乎是顯而易見的，但我無法將拆分COQ的if語句。任何幫助，將不勝感激。謝謝！

1熱度

1回答

在綁定器下泛化表達式

我需要在綁定器下泛化表達式。例如，我有我的目標，兩個表達式： (fun a b => g a b c) 和 (fun a b => f (g a b c)) 我想概括g _ _ c部分：一種方法做的是第一重寫它們分爲： (fun a b => (fun x y => g x y c) a b) 第二入： (fun a b => f ( (fun x y => g

0熱度

1回答

減少配以鑑於假設</p> <pre><code>H0 : n <> 0 </code></pre> <p>在COQ

自然數條件如何減少術語 ... if match n with | 0 => false | S m' => n =? m' end then ... 在目標？

2熱度

1回答

從可計算函數移動到歸納關係

我想了解如何從運算可計算函數的定理轉移到使用歸納定義關係來表示計算的定理。考慮下面這個簡單的開發。讓我們先從關係及其屬性的標準定義： Definition relation (X : Type) := X -> X -> Prop. Definition reflexive {X : Type} (R : relation X) := forall a, R a a. Defin

0熱度

1回答

有沒有一種很好的方法來阻止自動發生在目標中的beta減少？

假設您想證明(fun (x : unit) => false) <> (fun (x : unit) => true)。證明這一點的明顯方法是將intro一些H : (fun _ : unit => false) = (fun _ : unit => true)和使用H進行重寫以證明false = (fun x => false) tt = (fun x => true) tt = true)。但

0熱度

1回答

錯誤：非法應用（非功能性構造）

我正在嘗試使用HoTT書籍中的類型構造函數/消除器來闡述各種deMorgans法則的一些證明。我已經跳過了相關的東西挑選https://mdnahas.github.io/doc/Reading_HoTT_in_Coq.pdf並將其全部轉儲到.v文本文件中。我需要消除/介紹產品，聯產品和建立否定的方法規則。到目前爲止，我有， Definition idmap {A:Type} (x:A) : A

0熱度

2回答

錯誤：在當前環境中找不到參考fst

我正在編寫一個小程序，以便我可以使用HoTT書（等）中的類型導入/消除規則來對deMorgans定律進行一些證明。我的模型/示例代碼都在這裏，https://mdnahas.github.io/doc/Reading_HoTT_in_Coq.pdf。到目前爲止，我有， Definition idmap {A:Type} (x:A) : A := x. Inductive prod (A B:T

2熱度

2回答

有關函數值的嵌套歸納的定點證明

我試圖在Coq中證明歸納原理。由於數據結構的定義，必須通過兩個嵌套式導入來顯示該原理。外部感應通過Fixpoint構造完成，內部感應通過原理list_ind完成。發生的問題是現在內部歸納的歸納論證是一個函數的結果，即dfs t。 Inductive SearchTree (A : Type) : Type := | empty : SearchTree A | leaf :

0熱度

1回答

FORALL平等勒柯克

我試圖證明以下等式： Lemma Foo (A : Type) (n : nat) (gen : forall p : nat, p < S n -> A) (ic0 : 0 < S n) (ic1 : 0 mod S n < S n): gen (n - n) ic1 = gen 0 ic0. 的n-n值爲0 Nat.sub_diag和0 mod S n也爲0的Nat.mod_0