Предположим, у меня есть следующий исходный код idris:
module Source
import Data.Vect
--in order to avoid compiler confusion between Prelude.List.(++), Prelude.String.(++) and Data.Vect.(++)
infixl 0 +++
(+++) : Vect n a -> Vect m a -> Vect (n+m) a
v +++ w = v ++ w
--NB: further down in the question I'll assume this definition isn't needed because the compiler
-- will have enough context to disambiguate between these and figure out that Data.Vect.(++)
-- is the "correct" one to use.
lemma : reverse (n :: ns) +++ (n :: ns) = reverse ns +++ (n :: n :: ns)
lemma {ns = []} = Refl
lemma {ns = n' :: ns} = ?lemma_rhs
Как показано, базовый вариант для lemma тривиально Refl. Но я не могу найти способ доказать индуктивный случай: ответ "просто" выплевывает следующее
*source> :t lemma_rhs
phTy : Type
n1 : phTy
len : Nat
ns : Vect len phTy
n : phTy
-----------------------------------------
lemma_rhs : Data.Vect.reverse, go phTy
(S (S len))
(n :: n1 :: ns)
[n1, n]
ns ++
n :: n1 :: ns =
Data.Vect.reverse, go phTy (S len) (n1 :: ns) [n1] ns ++
n :: n :: n1 :: ns
Я понимаю, что phTy означает "фантомный тип", неявный тип из векторов, которые я рассматриваю. Я также понимаю, что go - это имя функции, определенной в предложении where для определения библиотечной функции reverse.
Вопрос
Как я могу продолжить доказательство? Оправдана ли моя индуктивная стратегия? Есть ли лучший?
Context
Это появилось в одном из моих игрушечных проектов, где я пытаюсь определить произвольные тензоры; в частности, это, по-видимому, необходимо для определения «полного сокращения индекса». Я немного подробнее остановлюсь на этом:
Я определяю тензоры таким образом, что примерно эквивалентно
data Tensor : (rank : Nat) -> (shape : Vector rank Nat) -> Type where
Scalar : a -> Tensor Z [] a
Vector : Vect n (Tensor rank shape a) -> Tensor (S rank) (n :: shape) a
, приукрашивающему остальную часть исходного кода (поскольку это не имеет отношения и это довольно долго и неинтересно на данный момент), я смог определить следующие функции
contractIndex : Num a =>
Tensor (r1 + (2 + r2)) (s1 ++ (n :: n :: s2)) a ->
Tensor (r1 + r2) (s1 ++ s2) a
tensorProduct : Num a =>
Tensor r1 s1 a ->
Tensor r2 s2 a ->
Tensor (r1 + r2) (s1 ++ s2) a
contractProduct : Num a =>
Tensor (S r1) s1 a ->
Tensor (S r2) ((last s1) :: s2) a ->
Tensor (r1 + r2) ((take r1 s1) ++ s2) a
, и я работаю над этой другой
fullIndexContraction : Num a =>
Tensor r (reverse ns) a ->
Tensor r ns a ->
Tensor 0 [] a
fullIndexContraction {r = Z} {ns = []} t s = t * s
fullIndexContraction {r = S r} {ns = n :: ns} t s = ?rhs
, которая должна " итерируйте contractProduct как можно больше (то есть r раз) "; эквивалентно, можно было бы определить его как tensorProduct, составленный из максимально возможного числа contractIndex (опять же, эта сумма должна быть r).
Я включаю все это, потому что, возможно, это проще просто решить эту проблему, не доказав lemma выше: если бы это было так, я также был бы полностью удовлетворен. Я просто подумал, что с «более короткой» версией, приведенной выше, легче разобраться, так как я уверен, что сам смогу найти недостающие фрагменты.
Версия idris, которую я использую: 1.3.2-git:PRE (это то, что говорит repl при вызове из командной строки).
Edit : ответ xa sh охватывает почти все, и я смог написать следующее functions
nreverse_id : (k : Nat) -> nreverse k = k
contractAllIndices : Num a =>
Tensor (nreverse k + k) (reverse ns ++ ns) a ->
Tensor Z [] a
contractAllProduct : Num a =>
Tensor (nreverse k) (reverse ns) a ->
Tensor k ns a ->
Tensor Z []
Я также написал «причудливую» версию reverse, назовем ее fancy_reverse, которая автоматически переписывает nreverse k = k в своем результате. Поэтому я попытался написать функцию, которая не имеет nreverse в своей подписи, что-то вроде
fancy_reverse : Vect n a -> Vect n a
fancy_reverse {n} xs =
rewrite sym $ nreverse_id n in
reverse xs
contract : Num a =>
{auto eql : fancy_reverse ns1 = ns2} ->
Tensor k ns1 a ->
Tensor k ns2 a ->
Tensor Z [] a
contract {eql} {k} {ns1} {ns2} t s =
flip contractAllProduct s $
rewrite sym $ nreverse_id k in
?rhs
сейчас, предполагаемый тип для rhs равен Tensor (nreverse k) (reverse ns2), и я имею в виду переписать Правило для k = nreverse k, но я не могу понять, как переписать неявное eql доказательство для проверки этого типа: я делаю что-то не так?