Идрис: восстановить равенство после сопоставления с образцом

Я разбиваю список на голову и хвост, но позже мне нужно доказательство того, что они возвращают мне исходный список при объединении:

test: Bool -> String
test b = let lst = the (List Nat) ?getListFromOtherFunction in
        case lst of
          Nil => ""
          x :: xs =>
            let eq = the ((x::xs) = lst) ?howToDoIt in ""

Я использую Идрис 1.3.1.


dependent-type idris
person simpadjo    schedule 24.12.2018    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Вы можете сделать это с зависимым сопоставлением шаблонов:

test: List Nat -> String
test lst with (lst) proof prf
  | Nil = ""
  | (x :: xs) = ?something

Здесь prf будет держать ваше равенство.

Однако я думаю, что лучше просто сопоставить lst в LHS, тогда ваши доказательства будут автоматически упрощаться там, где это необходимо.

person Alexander Gryzlov    schedule 24.12.2018
comment
спасибо! Я должен выучить зависимые p-m. Но похоже, что with можно использовать только для аргументов функций верхнего уровня. Я немного изменил свой вопрос. Возможно ли это сейчас? - person simpadjo; 25.12.2018
comment
Да, это несколько неудачное ограничение. Его можно обойти, создав вспомогательную функцию для оставшейся части вашего доказательства и используя в нем with на верхнем уровне. - person Alexander Gryzlov; 22.02.2019