Доказательства функций, зависящих от порядка их альтернатив

Question

Имея достаточно опыта в Haskell, я только недавно начал использовать Idris для доказательства теоремы. Это минимальный пример, который иллюстрирует проблему, с которой я столкнулся при попытке доказать довольно простые утверждения.

Рассмотрим мы имеем общую функцию test:

total test : Integer -> Integer 
test 1 = 1 
test n = n 

Конечно, мы видим, что функция может быть упрощена test n = n, но давайте это доказать. Я просто собираюсь на все случаи:

total lemma_test : (n : Integer) -> test n = n 
lemma_test 1 = Refl 
lemma_test n = Refl 

Но это не проверять тип:

Type mismatch between 
     n = n (Type of Refl) and 
     test n = n (Expected type) 

Specifically: 
     Type mismatch between 
       n 
     and 
       test n 

Таким образом, проблема, кажется, что Идрис не может сделать вывод для второго случая lemma_test что n не равно 1 и что также должен применяться второй случай test.

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

total lemma_test : (n : Integer) -> test n = n 
lemma_test 1 = Refl 
lemma_test 2 = Refl 
lemma_test 3 = Refl 
... 

Есть ли способ доказать, что такие заявления для функций, которые не определены над конечным набором конструкторов данных, но вместо этого зависят от того, что сопоставление шаблонов работает сверху донизу, например test в этом примере?

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

Answer 1

Как и другие, Integer является примитивным, а не индуктивно определенным типом Idris, поэтому мы не можем выполнять исчерпывающий сопоставление шаблонов. Более конкретно, проблема заключается в том, что в Идрисе (и на самом деле в современной Agda тоже!) Мы не можем действительно доказывать, что касается совпадений шаблонов по умолчанию, поскольку они не содержат информации обо всех предыдущих шаблонах которые не совпадали. В нашем случае не дает нам доказательств того, что n не равно 1.

Обычным решения является использование разрешимого равенства (Boolean равенства может быть тоже хорошо), а осень-через:

import Prelude 

%default total 

test : Integer -> Integer 
test n with (decEq n 1) 
    test n | Yes p = 1 
    test n | No p = n 

lemma_test : (n : Integer) -> (test n) = n 
lemma_test n with (decEq n 1) 
lemma_test _ | (Yes Refl) = Refl 
lemma_test n | (No contra) = Refl 

Здесь No результата несет явные свидетельства о неудачной игре.

Answer 2

Я не уверен, как определяется Integer, или как сделать индукцию на нем и т. Д., Так что это не полный ответ на ваш вопрос; но, может быть, версия Nat будет информативной для вас? (Также, возможно, вы на самом деле имели в виде Nat, так как в вашем втором примере вы только перечислить положительное Naturals?)

Если изменить test использовать Nat S:

total test : Nat -> Nat 
test (S Z) = 1 
test n = n 

, то вы можете сделать исчерпывающий шаблон в lemma_test:

total lemma_test : (n : Nat) -> test n = n 
lemma_test (S Z) = Refl 
lemma_test Z = Refl 
lemma_test (S (S k)) = Refl 

Answer 3

Integer не определен в Идриса, а сдвинуто GMP bigints. Это действительно непрозрачно для Идриса, и, по-видимому, это не то, что вы можете рассуждать о случаях во время компиляции таким образом. С чем-то вроде Nat, который определяется индуктивно, вы можете говорить о доказательствах в виде базового футляра и рекурсивного случая.

Этот тип ошибки около n не был test n сообщает вам, что Идрис не может уменьшить выражение test n. Я не уверен, что так оно и должно вести себя - очевидно, это полная функция, и она должна уменьшить общие функции afaik. Может быть, это связано с непрозрачностью Integer Идрису?

Вы можете проверить редукцию в repl, введя свободную переменную как параметр labmda. Например.\n => test n просто отголоски назад \n => test n : Integer -> Integer (при этом ничего не изменилось), однако, если вы удалите футляр test 1 = 1 из своего определения и повторите попытку, он откликнется обратно \n => n : Integer -> Integer - он уменьшен test n до n. И тогда ваше доказательство будет работать как есть.