Как я могу описать это свойство делимости в Идрисе? - PullRequest
Новая
       8

Как я могу описать это свойство делимости в Идрисе?

0 голосов
/ 14 октября 2018

Я хочу доказать, что если b (целое число) делит a (целое число), то b также делит a * c (где c - целое число).Во-первых, мне нужно переформулировать проблему в понятную для компьютера проблему, здесь была попытка: 

-- If a is divisible by b, then there exists an integer such that a = b * n
divisibleBy : (a, b : Integer) ->
              (n : Integer **
              (a = b * n))

-- If b | a then b | ac.
alsoDividesMultiples : (a, b, c : Integer) ->
                       (divisibleBy a b) ->
                       (divisibleBy (a * c) b)

Однако я получаю TypeUnification failure.Я не совсем уверен, что не так. 

  |
7 | alsoDividesMultiples : (a, b, c : Integer) ->
  |                      ^
When checking type of Numbris.Divisibility.alsoDividesMultiples:
Type mismatch between
        (n : Integer ** a = b * n) (Type of divisibleBy a b)
and
        Type (Expected type)

Specifically:
        Type mismatch between
                (n : Integer ** a = prim__mulBigInt b n)
        and
                TypeUnification failure


In context:
        a : Integer
        b : Integer
        c : Integer
        {a_509} : Integer
        {b_510} : Integer

1 Ответ

0 голосов
/ 14 октября 2018

В Идрисе предложения представлены типами, а доказательства предложений представлены элементами этих типов.Основная проблема здесь в том, что вы определили divisibleBy как функцию, которая возвращает элемент (то есть доказательство), а не тип (предложение).Таким образом, как вы определили здесь, divisbleBy фактически подразумевает доказательство того, что все целые числа делятся на все другие целые числа, что явно не соответствует действительности!Я думаю, что вы на самом деле ищете что-то вроде этого. 

DivisibleBy : Integer -> Integer -> Type
DivisibleBy a b = (n : Integer ** a = b * n)

alsoDividesMultiples : (a, b, c : Integer) ->
                       DivisibleBy a b ->
                       DivisibleBy (a * c) b
...