Доказательство Идриса с RHS в качестве определения функции - PullRequest
Новая
       28

Доказательство Идриса с RHS в качестве определения функции

0 голосов
/ 02 октября 2019

Я пытаюсь разобраться в некоторых простых доказательствах, пытаясь доказать эквивалентность вычислительного метода вычисления треугольных чисел их замкнутой форме. Пока что все, чего мне удалось добиться, это: 

total 
tn_eval : (n : Nat) -> Nat
tn_eval Z = Z
tn_eval (S k)  = (S k) + tn_eval k

total 
tn_closed : (n: Nat) -> Nat
tn_closed Z = Z
tn_closed (S k) = div ((S k) * ((S k) - 1)) 2

total 
tn_closed_proof : (n : Nat) -> (tn_closed n) = (tn_eval n)
tn_closed_proof Z = ?strange_hole
tn_closed_proof (S k) = ?more_difficult_hole

Однако я застрял в том, каким должно быть возможное определение ?strange_hole. Проверка типа дает: 

Idris: Type of strange_hole
--------------------------------------
strange_hole : tn_closed 0 = 0

Что (как я понимаю) буквально является определением tn_closed Z, поэтому это должно быть доказано просто с помощью Refl, поскольку tn_closed 0 определенно эквивалентно0.

Однако это не правильно, так как, когда я пытаюсь это сделать, я получаю ошибку типа: 

When checking right hand side of tn_closed_proof with expected type
        tn_closed 0 = tn_eval 0

Type mismatch between
        0 = 0 (Type of Refl)
and
        tn_closed 0 = 0 (Expected type)

Specifically:
        Type mismatch between
                0
        and
                tn_closed 0

Наряду с предупреждением о совокупности: 

Arith.tn_closed is possibly not total due to: Prelude.Nat.Nat implementation of Prelude.Interfaces.Integral

Я чувствую, что последнее может быть причиной первого, но кроме этого я полностью застрял! Насколько я понял, tn_closed 0 и 0 были по определению эквивалентными, поэтому любое доказательство, требующее tn_closed 0 = 0, должно быть тривиальным или доказуемым с Refl, но может показаться, что я ошибаюсь...

1 Ответ

0 голосов
/ 02 октября 2019

Как только я задал вопрос, мне удалось его решить!

Насколько я понимаю, проблема заключалась в определении tn_closed, а именно: 

tn_closed (S k) = div ((S k) * ((S k) - 1)) 2

Это определение означало, что Идрис (по какой-то причине) не понимал этогоразделение было полным. Заменив это определение следующим: 

tn_closed (S k) = divNatNZ ((S k) * ((S k) - 1)) 2 SIsNotZ

Дали гораздо более доступное отверстие: 

Idris: Type of hole
--------------------------------------
hole : 0 = 0

Это довольно просто решить с помощью Refl!

...