Объединение undef и списка равно undef - доказательство Haskell

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

undefined ++ xs = undefined

undefined haskell proof
person Jan kowalski    schedule 03.05.2015    source источник
comment
Я отредактировал тело вопроса, чтобы оно соответствовало вашему заголовку (поскольку я решил, что заголовок имеет больше смысла, чем тело). Не стесняйтесь повторно редактировать, если я неправильно догадался, что вы хотели спросить.   -  person Daniel Wagner    schedule 03.05.2015

Ответы (1)


arrow_upward
7
arrow_downward

Доказывать особо нечего. Существует просто правило (которое нельзя объяснить или разбить на что-то меньшее), что операторы case, которые пытаются сопоставить undefined с конструктором, приводят к undefined. Как только вы примете это правило, мы сможем наблюдать

undefined ++ ys
= { by definition of ++ }
case undefined of
    [] -> ys
    x:xs -> x : (xs ++ ys)
= { case that matches undefined against a constructor }
undefined
person Daniel Wagner    schedule 03.05.2015