Почему перезапись не меняет тип выражения в этом случае? - PullRequest
Новая
       12

Почему перезапись не меняет тип выражения в этом случае?

0 голосов
/ 10 июня 2018

В (* 1) можно прочитать следующее

rewrite prf in expr

Если у нас есть prf : x = y, а требуемый тип для expr - это какое-то свойство x, синтаксис rewrite ... in будет искать x в требуемом типе expr и заменять его на y.

Теперь у меня есть следующий фрагмент кода (вы можете скопировать егов редактор и попробуйте ctrl-l) 

module Test

plusCommZ : y = plus y 0
plusCommZ {y = Z} = Refl
plusCommZ {y = (S k)} = cong $ plusCommZ {y = k}

plusCommS : S (plus y k) = plus y (S k)
plusCommS {y = Z} = Refl
plusCommS {y = (S j)} {k} = let ih = plusCommS {y=j} {k=k} in cong ih

plusComm : (x, y : Nat) -> plus x y = plus y x
plusComm Z y = plusCommZ
plusComm (S k) y =
  let
    ih = plusComm k y
    prfXeqY = sym ih
    expr = plusCommS {k=k} {y=y}
    -- res = rewrite prfXeqY in expr
  in ?hole

ниже показано, как отверстие выглядит как 

- + Test.hole [P]
 `--          k : Nat
              y : Nat
             ih : plus k y = plus y k
        prfXeqY : plus y k = plus k y
           expr : S (plus y k) = plus y (S k)
     -----------------------------------------
      Test.hole : S (plus k y) = plus y (S k)

Вопрос. Это выглядит как expr (от * 1) в прокомментированной строке равно S (plus y k) = plus y (S k).И prf равно plus y k = plus k y, где x равно plus y k, а y равно plus k y.И переписать следует искать x (а именно plus y k) в expr (а именно S (plus y k) = plus y (S k) и заменить x на y (а именно plus k y). И результат (res) долженбыть S (plus k y) = plus y (S k).

Но это не работает.

У меня есть следующий ответ от idris

переписывание с плюса yk на плюс ky не изменило тип letty

Я могу предположить, что перезапись предназначена только для изменения типа полученного выражения, поэтому она не работает в теле выражения let, а только в части «in». Это правильно?

(* 1) http://docs.idris -lang.org / ru / latest / proofs / patterns.html

PS. Пример из учебного пособия работает отлично. Япросто любопытно узнать, почему способ, которым я пытался использовать перезапись, не сработал.

Ответы [ 2 ]

0 голосов
/ 11 июня 2018

Хотя это явно не указано в документах, rewrite является синтаксически-сладким вызовом тактического скрипта Elab ( определено здесь ).

Почему ваш пример делаетне работает: «требуемый тип expr» не найден;только с res = rewrite prfXeqY in expr неясно, какой тип res должен иметь (даже объединитель может разрешить это с помощью let res = … in res.) Если вы укажете требуемый тип, он будет работать, как и ожидалось: 

res = the (S (plus k y) = plus y (S k)) (rewrite prfXeqY in expr)
0 голосов
/ 10 июня 2018

К сожалению, вы не указали точную строку, которая приводит к неправильному поведению вашего кода, почему-то вы, должно быть, сделали что-то странное, так как с вашими соображениями, изложенными выше, код работает хорошо: 

  let
    ih = plusComm k y -- plus k y = plus y k
    px = plusCommS {k=k} {y=y} -- S (plus y k) = plus y (S k)
    in rewrite ih in px
...