عرض (رأس. init) = رأس في أجدا
-
27-09-2019 - |
سؤال
أحاول إثبات ليمما بسيطة في أجدا ، والتي أعتقد أنها صحيحة.
إذا كان لدى المتجه أكثر من عنصرين ، فأخذها
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))
مكون. أفترض أسئلتي ؛ هل هو ممكن وكيف وماذا يعني هذا المصطلح.
شكرا جزيلا.
المحلول
أنا لا أفهم تمامًا كيفية قراءة
(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 لا يعتمد على محتويات المتجه.
نصائح أخرى
موافق. لقد حصلت على هذا من خلال الغش وآمل أن يكون لدى شخص ما حل أفضل. ألقيت كل المعلومات الإضافية التي تحصل عليها init
يتم تعريفها من حيث initLast
وخلق نسختي الساذجة.
initLazy : ∀{A l} → Vec A (suc l) → Vec A l
initLazy (x ∷ []) = []
initLazy (x ∷ (y ∷ ys)) = x ∷ (initLazy (y ∷ ys))
الآن lemma تافهة.
أي عروض أخرى؟