在Agda中顯示（head。init）= head

我試圖在Agda中證明一個簡單的引理，我認爲這是真的。在Agda中顯示（head。init）= head

如果一個矢量具有兩個以上的元件，利用其head以下服用init相同立即服用其head。

我已經如下配製它：

lem-headInit : ∀{l} (xs : Vec ℕ (suc (suc l))) 
        -> head (init xs) ≡ head xs 
lem-headInit (x ∷ xs) = ?

這給了我;

.l : ℕ 
x : ℕ 
xs : Vec ℕ (suc .l) 
------------------------------ 
Goal: head (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)) ≡ x

作爲響應。我不完全瞭解如何閱讀(init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs))組件。我想我的問題是;是否有可能，該術語的含義和含義如何？

非常感謝。

來源

2010-08-10 Jason Reich

我不完全瞭解如何閱讀(init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs))組件。假設我的問題是，我 ;可能，是什麼意思，以及是什麼意思。

這告訴你值init (x ∷ xs)取決於|右邊的所有值。當你在Agda的函數中證明某些東西時，你的證明必須具有原始定義的結構。

在這種情況下，您必須對initLast的結果進行處理，因爲initLast的定義會在生成任何結果之前執行此操作。

init : ∀ {a n} {A : Set a} → Vec A (1 + n) → Vec A n 
init xs   with initLast xs 
       -- ⇧ The first thing this definition does is case on this value 
init .(ys ∷ʳ y) | (ys , y , refl) = ys

所以這裏是我們如何編寫引理。

module inithead where 

open import Data.Nat 
open import Data.Product 
open import Data.Vec 
open import Relation.Binary.PropositionalEquality 

lem-headInit : {A : Set} {n : ℕ} (xs : Vec A (2 + n)) 
      → head (init xs) ≡ head xs 

lem-headInit (x ∷ xs) with initLast xs 
lem-headInit (x ∷ .(ys ∷ʳ y)) | ys , y , refl = refl

我把你的推廣引理的自由去Vec A因爲引理不依賴於向量的內容。

來源

2010-11-07 22:26:29 glguy

好的。我通過作弊得到了這個，我希望有人有更好的解決方案。我扔掉了從init獲得的所有額外信息，這些信息被定義爲initLast並創建了我自己的天真版本。

initLazy : ∀{A l} → Vec A (suc l) → Vec A l 
initLazy (x ∷ []) = [] 
initLazy (x ∷ (y ∷ ys)) = x ∷ (initLazy (y ∷ ys))

現在引理是微不足道的。

任何其他優惠？

來源

2010-08-11 16:20:42

在Agda中顯示（head。init）= head

回答

相關問題