Идрис не расширит `мульт` в доказательство закона экспоненты - PullRequest
Новая
       73

Идрис не расширит `мульт` в доказательство закона экспоненты

0 голосов
/ 08 сентября 2018

Я пытаюсь написать доказательство того, что 2^n * 2^m = 2^(n+m) в Идрисе. Прямо сейчас у меня есть это: 

expLaw : (power 2 n) * (power 2 m) = power 2 (n + m)
expLaw {n=Z} {m} = plusZeroRightNeutral (power 2 m)
expLaw {n=S n'} {m=m'} = 
  trans (multAssociative 2 (power 2 n') (power 2 m')) $ 
  cong {f=mult 2} $ expLaw {n=n'} {m=m'}

Это дает мне ошибку: 

When checking an application of function trans:
        Type mismatch between
                mult 2 (power 2 n' * power 2 m') = mult 2 (power 2 (n' + m')) (Type of cong powExp)
        and
                mult (mult 2 (power 2 n')) (power 2 m') = plus (power 2 (plus n' m')) (plus (power 2 (plus n' m')) 0) (Expected type)

        Specifically:
                Type mismatch between
                        mult 2 (power 2 (n' + m'))
                and
                        plus (power 2 (plus n' m')) (plus (power 2 (plus n' m')) 0)

Насколько я могу судить, это, по сути, говорит о том, что он видит 2 * 2^(n+m) там, где он хочет 2^(n+m) + (2^(n+m) + 0). Однако, по определению мульт, первое должно тривиально сводиться ко второму. В частности, следующие без проблем компилируются: 

foo : 2 * a = a + (a + 0)
foo = Refl

Для меня это означает, что расширение работает так, как я ожидал. Но по какой-то причине в моей реализации expLaw компилятор застрял. Мне интересно, может ли это быть как-то связано с использованием mult и plus против * и +, но я не уверен. Как я могу это исправить?

В качестве альтернативы, если у кого-то есть лучший способ реализовать expLaw, я буду рад это услышать.

1 Ответ

0 голосов
/ 08 сентября 2018

Это помогает добавлять доказательства шаг за шагом с let … in … блоками, так что вы можете легко проверить типы. Ошибка происходит при trans, поэтому с учетом 

expLaw : (power 2 n) * (power 2 m) = power 2 (n + m)
expLaw {n=Z} {m} = plusZeroRightNeutral (power 2 m)
expLaw {n=S n'} {m=m'} =
  let prf1 = cong {f=mult 2} $ expLaw {n=n'} {m=m'} in
  let prf2 = multAssociative 2 (power 2 n') (power 2 m') in
  ?hole

> :t hole
  m' : Nat
  n' : Nat
  prf1 : plus (mult (power 2 n') (power 2 m'))
              (plus (mult (power 2 n') (power 2 m')) 0) =
         plus (power 2 (plus n' m')) (plus (power 2 (plus n' m')) 0)
  prf2 : plus (mult (power 2 n') (power 2 m'))
              (plus (mult (power 2 n') (power 2 m')) 0) =
         mult (plus (power 2 n') (plus (power 2 n') 0)) (power 2 m')
--------------------------------------
hole : mult (plus (power 2 n') (plus (power 2 n') 0)) (power 2 m') =
       plus (power 2 (plus n' m')) (plus (power 2 (plus n' m')) 0)

Вы можете видеть, что порядок равенств prf2 : a = b, prf1 : a = c не совпадает с trans : (a = b) -> (b = c) -> a = c. Но с простым sym : (a = b) -> b = a это работает. Так что у тебя это почти получилось. : -) 

 …
 let prf3 = trans (sym prf2) prf1 in
 prf3
...