?

Log in

No account? Create an account

Previous Entry | Next Entry

shooting off your leg with class

Захотелось мне недавно реализовать циклический сдвиг непустого вектора (списка с длиной в типе) на Идрисе. Пишу:
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 ним уже код работает правильно. Так-то.

Tags:

Comments

( 21 comments — Leave a comment )
nponeccop
Feb. 11th, 2013 05:04 am (UTC)
> Вот так, используя зависимые типы и теорем-прувинг,
> можно неожиданно заставить корректный код работать некорректно.

Ужасы какие
thinker8086
Feb. 11th, 2013 05:51 am (UTC)
А почему 4 раза intro?
thedeemon
Feb. 11th, 2013 06:03 am (UTC)
intro вводит один параметр, а intros - сразу все. Если нужны не все, приходится писать столько, сколько нужно ввести.
dmytrish
Oct. 15th, 2015 07:37 pm (UTC)
Не знаю, у меня вроде работает просто intros (возможно Идрис поумнел, он уже 0.9.19):

rotLeft_lemma_1 = proof
  intros
  rewrite plusCommutative n (S 0)
  trivial
sassa_nf
Feb. 11th, 2013 07:03 am (UTC)
а он знает, что [head v] : Vec a 1 ?
thedeemon
Feb. 11th, 2013 07:37 am (UTC)
Да, знает, не зря он пишет про n + (S O).
migmit
Feb. 11th, 2013 08:31 am (UTC)
Кошмар.
gds
Feb. 11th, 2013 08:52 am (UTC)
> rotLeft v ?= tail v ++ [head v]

в рот мне ноги, computational term выписан ведь правильно, зачем тактики его меняют?
thedeemon
Feb. 11th, 2013 09:46 am (UTC)
Они и не меняют, они просто берут другой по ошибке. :)
gds
Feb. 11th, 2013 12:51 pm (UTC)
понятно, типы совпадают, но разве это позволяет идрису игнорировать уже имеющееся тело функции, которое без сомнений правильное?
thedeemon
Feb. 11th, 2013 01:19 pm (UTC)
Ну вот да, получается, что сейчас позволяет. Автор сказал так:
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
Feb. 11th, 2013 01:22 pm (UTC)
фух, ну хоть так. Если автор это понимает -- уже хорошо.
deni_ok
Feb. 11th, 2013 02:47 pm (UTC)
С другой стороны сам виноват - не указал в типе все нужные инварианты. Ну и получил по башке привет от proof irrelevance.
thedeemon
Feb. 11th, 2013 11:29 pm (UTC)
А как их правильно указать, чтобы в итоге получилась именно функция сдвига такого вектора, а не другого более сложного и точного типа? В общем, реквестирую кошерный вариант на агде.
deni_ok
Feb. 12th, 2013 05:12 am (UTC)
Для решения конкретно этой задачи в Агде есть 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
Feb. 12th, 2013 06:08 am (UTC)
А, ну так-то и в идрисе можно, один в один.
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
Feb. 12th, 2013 06:10 am (UTC)
А без Snoc'a, аппендом как в посте, получится в агде?
deni_ok
Feb. 12th, 2013 07:34 am (UTC)
Ну можно ручками доказать коммутативность сложения
+-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
Feb. 12th, 2013 07:57 am (UTC)
O, subst! Вот это мне и интересно было, спасибо!
dima_starosud
Feb. 11th, 2013 04:07 pm (UTC)
Я думаю лучше было бы коммутативность доказать, как дополнительную лемму, и ею воспользоваться.
А вообще после Coq, как только занялся Agda, понял что тактики (для меня) - это зло: вообще не понимаю, что происходит.
thedeemon
Feb. 11th, 2013 11:26 pm (UTC)
Она уже доказана, и соответствующая лемма лежит в стандартной библиотеке, ей и воспользовался в итоге, см. конец поста.
( 21 comments — Leave a comment )