Показ (руководитель. 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, поскольку лемма не зависит от содержимого вектора.

Answer 2

Хорошо. Я получил это путем обмана, и я надеюсь, что у кого-то есть лучшее решение. Я выбросил всю дополнительную информацию, которую вы получаете от init, определяемой в терминах initLast, и создал собственную наивную версию.

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

Теперь лемма тривиальна.

Любые другие предложения?