Структурные индукции в haskell. Списки и сумма

Question

Привет, я совершенно новичок в haskell и просто получил структурную индукцию и задавался вопросом, может ли кто-нибудь объяснить, какие шаги я должен предпринять, было бы очень полезно.

Вопрос: - вычисляет сумму всех чисел в списке

sum :: [Integer] -> Integer 
sum []  = 0 
sum (x:xs) = x + sum xs 

- присоединяет два списка

(++) :: [Integer] -> [Integer] -> [Integer] 
[]  ++ ys = ys 
(x:xs) ++ ys = x : (xs ++ ys) 

Докажи (с помощью структурной индукции), что имеет место равенство, для всех списков целых чисел xs и ys:

sum (xs ++ ys) = sum xs + sum ys 

Не забывайте называть IH. на стадии индукции. Также убедитесь, что вы четко указываете причины, по которым вы делаете шаги в своих доказательствах.

Мои шаги: Чтобы доказать:

sum (xs ++ ys) = sum xs + sum ys 

Доказательство: по структурной индукции

Пусть P() < --- действительно не знаю, что типа там, так что если кто-то может взять его там я бы очень оценил это!

Answer 1

++ определяется по индукции по первому аргументу xs, поэтому это обычно является хорошим признаком того, что нам необходимо продолжить индукцию по xs.

Таким образом, мы фиксируем ys один раз для всех, и определить P(xs) следующим

P(xs) = (sum (xs ++ ys) == sum xs + sum ys) 

Теперь вы должны доказать, что P(xs) справедливо для всех xs. Примените принцип индукции в списках, и вы должны быть в порядке.