induction

10熱度

1回答

Agda中的大小類型是什麼？我試圖閱讀報紙約MiniAgda，但未能繼續因以下幾點：爲什麼是數據類型一般在它們的大小？據我所知，大小是誘導樹的深度。爲什麼數據類型在它們的大小上是協變的，即：i < = j - > T_i < = T_j？ >和#模式的含義是？

1熱度

2回答

Coq向量置換

我需要推理向量在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回答

感應證明與三個基本案例（伊莎貝爾）

我想能夠證明一個聲明在n（nat類型）上的歸納。它由一個條件組成，前提條件的前提條件是n> = 2。前提條件爲假的條件總是如此。所以我想證明n = 0，n = 1和n = 2的情況都與主要歸納步驟分開。是否有可能通過誘導基地情況下，像下面做一個證明： lemma "P (n::nat) --> Q" proof (induct n) case 0 show ?case

2熱度

1回答

有人可以爲我提供一個更好的證明和場景泡沫分類比較我已經證明

給出未分類元素的列表。初始條件是未排序的元素A =列表中，P = 1，N =總陣列尺寸 Bubble(A,p,N) if p>=N return for i=p to N-1 if A[i]>A[i+1] swap(A[i],A[i+1]) Bubble(A,p,N-1) 問題1：通過感應上N. 我的問題證明了該算法的正確性：我怎樣才能使用k Bubble上的+1（

1熱度

3回答

復發：T（n）= T（n/2）+ log N

我被困在一個復發問題上。 T（N）= T（N/2）+日誌N 我現在所擁有的是： T（N）= T（N/2）+日誌N T（N/2）= T（N/4）+日誌（N/2） ... T（N）= T（N/2^k）的總和+ [I = 0和k {log（N/2^i）}] 我被困在接下來要做的事情上。請給我一些建議。謝謝！

-1熱度

2回答

如何在haskell中設置歸納證明？

我需要證明 f (g xs) == g (f xs) whenver XS是INTS的有限列表。假設兩個F和G型[INT] - > [INT]

0熱度

2回答

在我的歸納步驟中找不到這個錯誤

幾天前，我正在解決一些應用程序的問題，我試着解決了這個問題。聲明這個「證明」有什麼問題？「定理」對於每個正整數n，如果x和y是max（x，y）= n的正整數，則x = y。基礎步驟：假設爲n = 1，如果最大值（X，Y）= 1，x和y爲正整數，我們有X = 1和y = 1。歸納步：令k爲一個正整數。假設只要max（x，y）= k且x和y是正整數，則x = y。現在讓max（x，y）= k

2熱度

1回答

爲什麼Lean強制遞歸類型參數在非遞歸類型參數後出現？

下面的定義是由精益拒絕： inductive natlist | nil : natlist | cons: natlist → ℕ → natlist 與錯誤消息「ARG＃ 'natlist.cons' 的2不是遞歸的，但它的遞歸參數之後發生」如預期的那樣，接受以下定義： inductive natlist | nil : natlist | cons: ℕ → natlist →

1熱度

1回答

列表中的歸納 - 證明更強的屬性（Haskell）

我會馬上說出這是一個任務，我不是在尋找答案 - 只是某個方向，因爲我一直在爲它現在有一段時間了。給出下面的尾遞歸總和函數： sumTR [ ] acc = acc sumTR (x:xs) acc = sumTR xs (x + acc) 我們通過感應來證明： sumTR xs (sumTR ys acc) = sumTR (ys ++ xs) acc 證明基本情況（中引起上XS和治療Y

1熱度

1回答

爲了證明功能

平等鑑於兩個功能： sumOne 0 = 0 -- I.a sumOne m | m > 0 = sumOne (m-1) + m -- II.a endSum m = helpSum 0 m -- I.b where helpSum x 0 = x -- II.b helpSum x m | m > 0 = helpSum (x