shooting off your leg with class

[thedeemon]

Захотелось мне недавно реализовать циклический сдвиг непустого вектора (списка с длиной в типе) на Идрисе. Пишу:

rotLeft : Vect a (S n) -> Vect a (S n)
rotLeft v = tail v ++ [head v]

А компилятор мне отвечает, что он хоть и умный, но ленивый, и ему не очевидно, что n+1 это n+1, ну в смысле что результат применения функции сложения натурального числа n с константой 1 это следующее за n число.
"Can't unify Vect a (m + n) with Vect a (S n)
Specifically: Can't unify plus m with S"
Для случаев, когда код правильный, но компилятор не убежден в корректности типов, в Идрисе есть специальные доказательства и интерактивный режим их построения посредством тактик. Пишем так:

rotLeft v ?= tail v ++ [head v]

Знак вопроса перед равенством означает, что корректность типов будет доказана отдельной леммой. Запускаем REPL. Он такой код принимает, а по команде :m показывает, что есть одна незакрытая лемма:

Global metavariables:  [Main.rotLeft_lemma_1]

Спрашиваем ее тип:

> :t rotLeft_lemma_1
rotLeft_lemma_1 : (a : Type) -> (n : Nat) -> (Vect a (S n)) -> (Vect a (n + (S O))) 
-> Vect a (S n)

Тип ее говорит, что это функция, принимающая на вход аргументы исходной функции и ее результат в том виде, который смог вывести компилятор (Vect a (n + (S O)), где S O - это натуральная единица в унарной записи), а на выходе должна выдать значение того типа, что мы указали выходным типом исходной функции (Vect a (S n)). Перехожу в интерактивный режим доказательств: :p rotLeft_lemma_1, после чего как та мартышка с печатной машинкой пробую разные тактики (это был мой первый опыт, я тогда об этих тактиках почти ничего не знал). Вижу, что последовательность из двух тактик intros и trivial лемму закрывает:

> :p rotLeft_lemma_1
----------                 Goal:                  ----------
{ hole 0 }:
 (a : Type) ->
 (n : Nat) ->
 (Vect a (S n)) ->
 (Vect a (n + (S O))) -> Vect a (S n)
-Main.rotLeft_lemma_1> intros
----------              Other goals:              ----------
{ hole 3 }
{ hole 2 }
{ hole 1 }
{ hole 0 }
----------              Assumptions:              ----------
 a : Type
 n : Nat
 v : Vect a (S n)
 value : Vect a (n + (S O))
----------                 Goal:                  ----------
{ hole 4 }:
 Vect a (S n)
-Main.rotLeft_lemma_1> trivial
rotLeft_lemma_1: No more goals.
-Main.rotLeft_lemma_1> qed
Main.rotLeft_lemma_1 = proof {
  intros;
  trivial;
}

Команда qed там выводит запись доказательства, которую можно скопировать в исходник. Копирую, компилирую, все проходит успешно, ура! Пробую запустить и вижу, что работает-то код неправильно: rotLeft [1,2,3] выдает [1,2,3] вместо ожидаемого [2,3,1]. Вот так, используя зависимые типы и теорем-прувинг, можно неожиданно заставить корректный код работать некорректно. А дело тут вот в чем. Команда intros последовательно вводит все входные параметры в качестве предпосылок доказательства, записывает их в графу "дано". А команда trivial ищет среди уже доказанного терм, подходящий по форме к доказываемой цели. Поскольку на выходе мы хотим получить значение такого же типа, какое было на входе, прувер просто взял входное значение. Получилось, что лемма эта забивает на вычисленный телом функции результат и возвращает вместо него аргумент функции. Типы сошлись, все чудесно, но результат неверный.
Если же подойти к делу более осмысленно, то можно тактиками подсказать компилятору, что следует попытаться произвести вычисления (развернуть функцию сложения), затем ввести нужные парамерты в графу "дано", а потом применить лемму из стандартной библиотеки о коммутативности сложения. Тогда цель и вычисленное функцией значение окажутся с одинаковыми типами, и можно тактикой trivial взять нужное, на этот раз то самое. Вот так выглядит рабочее доказательство:

rotLeft_lemma_1 = proof {
  compute;  intro;  intro;  intro;  intro;
  rewrite plusCommutative n (S O);  trivial;
}

C ним уже код работает правильно. Так-то.

Comments

[nponeccop.livejournal.com]

> Вот так, используя зависимые типы и теорем-прувинг,
> можно неожиданно заставить корректный код работать некорректно.

Ужасы какие

[thinker8086.livejournal.com]

А почему 4 раза intro?

[thedeemon.livejournal.com]

intro вводит один параметр, а intros - сразу все. Если нужны не все, приходится писать столько, сколько нужно ввести.

[sassa-nf.livejournal.com]

а он знает, что [head v] : Vec a 1 ?

[thedeemon.livejournal.com]

Да, знает, не зря он пишет про n + (S O).

[migmit.livejournal.com]

Кошмар.

[gds.livejournal.com]

> rotLeft v ?= tail v ++ [head v]

в рот мне ноги, computational term выписан ведь правильно, зачем тактики его меняют?

[thedeemon.livejournal.com]

Они и не меняют, они просто берут другой по ошибке. :)

[gds.livejournal.com]

понятно, типы совпадают, но разве это позволяет идрису игнорировать уже имеющееся тело функции, которое без сомнений правильное?

[thedeemon.livejournal.com]

Ну вот да, получается, что сейчас позволяет. Автор сказал так:
There is a weakness in provisional definitions at the minute, in that there is no guarantee that the value you find in the proof is at all related to the value it is supposed to have, other than in its type. I think if provisional definitions generated an equality constraint it would be better.

[gds.livejournal.com]

фух, ну хоть так. Если автор это понимает -- уже хорошо.

[deni-ok.livejournal.com]

С другой стороны сам виноват - не указал в типе все нужные инварианты. Ну и получил по башке привет от proof irrelevance.

[dima-starosud.livejournal.com]

Я думаю лучше было бы коммутативность доказать, как дополнительную лемму, и ею воспользоваться.
А вообще после Coq, как только занялся Agda, понял что тактики (для меня) - это зло: вообще не понимаю, что происходит.

[thedeemon.livejournal.com]

Она уже доказана, и соответствующая лемма лежит в стандартной библиотеке, ей и воспользовался в итоге, см. конец поста.

[thedeemon.livejournal.com]

А как их правильно указать, чтобы в итоге получилась именно функция сдвига такого вектора, а не другого более сложного и точного типа? В общем, реквестирую кошерный вариант на агде.

[deni-ok.livejournal.com]

Для решения конкретно этой задачи в Агде есть Snoc такого вида

infixl 5 _∷ʳ_

_∷ʳ_ : ∀ {a n} {A : Set a} → Vec A n → A → Vec A (1 + n)
[]       ∷ʳ y = [ y ]
(x ∷ xs) ∷ʳ y = x ∷ (xs ∷ʳ y)

Ну и дальше всё выходит само собой, поскольку из определения плюса Агда "знает", что (1 + n) редуцируется к (suc n)

rotLeft : ∀ {n} {A : Set} →  Vec A (suc n) → Vec A (suc n)
rotLeft vs = tail vs ∷ʳ head vs 

[thedeemon.livejournal.com]

А, ну так-то и в идрисе можно, один в один.

snoc : Vect a n -> a -> Vect a (1+n)
snoc [] y = [y]
snoc (x::xs) y = x :: snoc xs y

rotLeft : Vect a (S n) -> Vect a (S n)
rotLeft v = tail v `snoc` head v

Оператор + определен матчингом по первому аргументу, поэтому 1+n редуцируется элементарно, а вот n+1 уже фиг.

Но такое решение не указывает в типе все инварианты.

[thedeemon.livejournal.com]

А без Snoc'a, аппендом как в посте, получится в агде?

[deni-ok.livejournal.com]

Ну можно ручками доказать коммутативность сложения

+-comm : (m n : ℕ) → m + n ≡ n + m
-- стандартное упражнение

Или воспользоваться тем, что ℕ - коммутативное полукольцо, получив массу свойств на халяву (в том числе и нужную коммутативность).

open import Algebra
import Data.Nat.Properties as Nat
private
  module CS = CommutativeSemiring Nat.commutativeSemiring

После чего принудительно приводим типы с помощью subst

open import Relation.Binary.PropositionalEquality

rotLeft : ∀ {n} {A : Set} →  Vec A (suc n) → Vec A (suc n)
rotLeft {n} {A} (v ∷ vs) = subst (Vec A) (sym (CS.+-comm 1 n)) (vs ++ v ∷ [])

[thedeemon.livejournal.com]

O, subst! Вот это мне и интересно было, спасибо!

[dmytrish.livejournal.com]

Не знаю, у меня вроде работает просто intros (возможно Идрис поумнел, он уже 0.9.19):

rotLeft_lemma_1 = proof
  intros
  rewrite plusCommutative n (S 0)
  trivial