CD
если реверс выдаст пустой ответ, то любая использующая функция сломается на любом тесте
Size: a a a
2020 August 24
CD
если реверс это id аналогично
p
Реверс списков каждый доказать может, а ты мне перемножение матриц докажи
Ну там будет лемма вида
foo: (a: Vect n (Vect m elem)) -> (b: Vect m (Vect n elem)) -> (x: Nat) -> (y: Nat) -> LessThan n y -> LessThan m x -> { res: multiply a b } -> res[x][y] = ... --Забыл как там матрицы перемножаютсяEG
Ну там будет лемма вида
foo: (a: Vect n (Vect m elem)) -> (b: Vect m (Vect n elem)) -> (x: Nat) -> (y: Nat) -> LessThan n y -> LessThan m x -> { res: multiply a b } -> res[x][y] = ... --Забыл как там матрицы перемножаютсяТо есть тупо перепечатка исходного кода?
EG
А почему ты не учитываешь вероятность, что ты тупо допустишь ту же самую ошибку в доказательстве?
CD
То есть тупо перепечатка исходного кода?
Да, мы же доказываем соответствие определению
EG
И у тебя будет доказательство с ошибкой успешно доказывать, что ты перемножаешь матрицы с ошибкой.
CD
Если исходный код был определение, то это его точная копия
p
То есть тупо перепечатка исходного кода?
Где? Тут гораздо больше информации чем в исходном коде.
EG
Пока не вижу
EG
Пока вижу функцию для умножения матриц
p
А почему ты не учитываешь вероятность, что ты тупо допустишь ту же самую ошибку в доказательстве?
s/доказательстве/тесте/
CD
Где? Тут гораздо больше информации чем в исходном коде.
Ты хочешь доказать соответствие функции-определения чему-то
EG
s/доказательстве/тесте/
Потому что ты тестируешь не функцию, а поведение крупным планом.
p
Пока вижу функцию для умножения матриц
Как минимум здесь есть информация о размерах матрицы
CD
s/доказательстве/тесте/
Тест будет не такой
CD
Тест будет для случайного x верно (AB)x = A(Bx)
EG
Как минимум здесь есть информация о размерах матрицы
В самой функции эта информация тоже есть, очевидно, мы ж на идрисе пишем
EG
Так что она сама по себе принимает и возвращает векторы
EG
Вот векторы это, кстати, хороший пример, где типы скорее помогают, чем мешают