BeiZero

В этой статье я постараюсь подробно расписать решение задачи про то, что суффикс списка не может быть больше, чем сам список.

Рекомендую перед чтением статьи сначала попытаться решить задачу самостоятельно.

#agda #codewars

Импорты и определение модуля:

{-# OPTIONS  #-}
module Codewars.LessNoMore where

open import Relation.Nullary
open import Data.List

Определение суффикса: – Любой список l является суффиксом для самого себя – Если есть l', который является суффиксом l, то для любого x список l' является суффиксом списка x ∷ l

В коде:

data Suf {X : Set} : List X → List X → Set where
  sinit : ∀ l → Suf l l
  scons : ∀ x l l' → Suf l l' → Suf (x ∷ l) l'

Примеры:

-- список [1,5,2]
ex0 = 1 ∷ 5 ∷ 2 ∷ []

-- суффикс [1,5,2] списка [1,5,2]
ex1 = sinit ex0 

-- суффикс [1,5,2] списка [4,1,5,2]
ex2 = scons 4 ex0 ex0 (sinit ex0)

В задаче нужно доказать, что

less-is-not-more : ∀ {X} a (l : List X) → ¬ Suf l (a ∷ l)

Решение:

Будем действовать по индукции и рассмотрим сначала случай с пустым списком и этот случай является тривиальным, т.к. не подходит ни конструктор sinit для Suf, ни scons. Можем записать это используя абсурдный паттерн(absurd pattern).

less-is-not-more _ [] ()

остается второй случай, когда список не пустой, тогда для суффикса подходит только конструктор scons, распишем подробнее этот случай:

less-is-not-more a (x ∷ l) (scons .x .l (.a ∷ .x ∷ .l) suf) = ?

теперь нужно показать, что невозможно построить терм типа Suf (x ∷ l) (a ∷ x ∷ l). По предположению индукции мы знаем, что невозможно создать терм типа Suf l (x ∷ l), но нам “мешает” a. Чтобы избавиться от a докажем лемму про то, что если убрать из суффикса один элемент, то он останется суффиксом.

lemma : ∀ {X} a (l₁ l₂ : List X) → Suf l₁ (a ∷ l₂) → Suf l₁ l₂ 
-- если суффикс был построен с помощью sinit
lemma a (.a ∷ l) .l (sinit (.a ∷ .l)) = scons a l l (sinit l)
-- если суффикс был построен с помощью scons
lemma a (x ∷ l₁) l₂ (scons .x .l₁ (.a ∷ .l₂) suf) = scons x l₁ l₂ (lemma a l₁ l₂ suf)

Теперь можем завершить доказательство, целиком оно будет выглядеть так:

less-is-not-more : ∀ {X} a (l : List X) → ¬ Suf l (a ∷ l)
less-is-not-more _ [] ()
less-is-not-more a (x ∷ l) (scons .x .l (.a ∷ .x ∷ .l) suf) = less-is-not-more x l (lemma a l (x ∷ l) suf)