Обратитесь к внешним переменным в шаблонах Idris - PullRequest
Новая
       29

Обратитесь к внешним переменным в шаблонах Idris

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

Я собираюсь написать корректно проверенную функцию деления для натуральных чисел. Вот что у меня получилось: 

divMod : (n, d : Nat) -> {auto dGte1 : LTE 1 d} -> (q : (Nat, Nat) ** d * fst q + snd q = n)
divMod n Z impossible
divMod n d = divMod' ((0, n) ** rewrite multZeroRightZero d in Refl)
    where
    divMod' : (q : (Nat, Nat) ** d * fst q + snd q = n) -> (q' : (Nat, Nat) ** d * fst q' + snd q' = n)
    divMod' ((q, r) ** prf) with (cmp r d)
        divMod' ((q, r) ** prf) | with_pat = ?divMod_rhs

Идея состоит в том, чтобы создать пару (q, n) и вычесть d из n (увеличивая q каждый раз), пока она не станет меньше d. Финальная пара (q, n) будет содержать результат и остаток от деления. Проблема в том, что я не могу сделать правильное разделение регистра на with_pat, потому что это изменяет шаблоны слева, так что они зависят от d, к которому я, похоже, никак не могу обратиться.

Я знаю, что мог бы передать d в качестве другого аргумента divMod', что позволило бы мне сопоставить его с шаблоном. Однако это ужасная избыточность и, кроме того, она, вероятно, усложнит доказательство. Так есть ли лучший способ ссылаться на d в шаблонах divMod', не передавая его явно?

РЕДАКТИРОВАТЬ: Оказывается, это не сильно усложняет основное доказательство. Что усложняет, так это убеждение Идриса, что эта функция полная: 

divMod : (n, d : Nat) -> {auto dGte1 : LTE 1 d} -> (q : (Nat, Nat) ** d * fst q + snd q = n)
divMod n Z impossible
divMod n d = divMod' d ((0, n) ** rewrite multZeroRightZero d in Refl)
    where
    divMod' : (d' : Nat) -> (q : (Nat, Nat) ** d' * fst q + snd q = n) -> (q' : (Nat, Nat) ** d' * fst q' + snd q' = n)
    divMod' d ((q, r) ** prf) with (cmp r d)
        divMod' (r + (S x)) ((q, r) ** prf) | CmpLT x = ((q, r) ** prf)
        divMod' r ((q, r) ** prf)           | CmpEQ = ((S q, Z) **
                rewrite multRightSuccPlus r q in
                rewrite plusZeroRightNeutral (r + r * q) in
                rewrite plusCommutative r (r * q) in
                prf
            )
        divMod' d ((q, (d + (S x))) ** prf) | CmpGT x = divMod' (assert_smaller d d) ((S q, S x) **
                rewrite multRightSuccPlus d q in
                rewrite plusCommutative d (d * q) in
                rewrite sym $ plusAssociative (d * q) d (S x) in
                prf
            )

assert_smaller d d (однако false) здесь необходимо, чтобы убедить Идрис, что эта функция всегда завершается. Я полагаю, что это не было бы так, если бы d было очевидно постоянным на протяжении всей этой рекурсии ...

В любом случае, я все равно хотел бы отменить передачу d в divMod'. Возможно ли это?

...