عرض (رأس. init) = رأس في أجدا

Question

أحاول إثبات ليمما بسيطة في أجدا ، والتي أعتقد أنها صحيحة.

إذا كان لدى المتجه أكثر من عنصرين ، فأخذها 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)) مكون. أفترض أسئلتي ؛ هل هو ممكن وكيف وماذا يعني هذا المصطلح.

شكرا جزيلا.

Answer 1

أنا لا أفهم تمامًا كيفية قراءة (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 لأن Lemma لا يعتمد على محتويات المتجه.

Answer 2

موافق. لقد حصلت على هذا من خلال الغش وآمل أن يكون لدى شخص ما حل أفضل. ألقيت كل المعلومات الإضافية التي تحصل عليها init يتم تعريفها من حيث initLast وخلق نسختي الساذجة.

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

الآن lemma تافهة.

أي عروض أخرى؟