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

Question

Учитывая следующие функции:

let rec foo l1 l2 = 
    match (l1,l2) with 
     ([],ys) -> ys 
     | (x::xs,ys) -> foo xs (x::ys)) 

Доказать следующее свойство:

• foo (foo xs ys) zs = foo ys (xs@zs)

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

Базовый вариант:

• foo (foo [] ys) zs = foo ys ([]@zs)
• foo ys zs = foo ys zs

Индуктивный Корпус:

• foo (foo (x::xs) ys) zs = foo ys ((x::xs)@zs)

Answer 1

Очерк рода доказательства вы просите о следующем. Я включил базовый футляр. Индуктивный корпус остается для вас. Убедитесь, что вы используете предположение, упомянутое в схеме, где-то в индуктивном случае, чтобы завершить его. Я использую = для «равенства» и => для оценки. Я не знаю, какие отношения доступны в вашем контексте, что вы можете предположить об оценке и равенстве, или вам разрешено использовать леммы о @ или иметь абстрактное определение. Таким образом, вам, вероятно, придется это изменить.

Доказательство по индукции по строению xs.

Корпус: xs = []:

foo (foo xs ys) zs 
    = foo (foo [] ys) zs   (* structure of xs *) 
    => foo (match ([], ys) with ([], ys) -> ys | (* ... *) 
           (* def. of foo, substitution *) 
    => foo (ys) zs     (* eval. of match *) 
    = foo ys zs     (* drop parentheses *) 
    = foo ys ([] @ zs)   (* abstract def. of @ *) 
    = foo ys (xs @ zs)   (* structure of xs *) 

Корпус: xs = x::xs':

Вот, предположим, что для всех ys, zs, foo (foo xs' ys) zs = foo ys (xs' @ zs). (Это так называемая индуктивная гипотеза.)

foo (foo xs ys) zs 
    = foo (foo (x::xs') ys) zs (* structure of xs *) 
    = foo (match (x::xs', ys) with (* ... *) | (x::xs', ys) -> (* ... *) 
           (* def. of foo, substitution *) 
    => foo (foo xs' (x::ys)) zs (* eval. of match *) 

    (* for you *) 

    = foo ys ((x::xs') @ zs)  (* by some argument from you *) 
    = foo ys (xs @ zs)   (* structure of xs *) 

---

Как вы можете видеть, доказательство начинается с выбора значения, чтобы сделать структурную индукцию по (вы уже выбрали xs в вашем вопросе). Затем доказательство разбивается на случаи по всем возможным способам, которые могут быть построены xs. Поскольку xs, по-видимому, является списком (вот почему важна информация о типе), есть только два вида вещей: он может быть [], или он может быть x::xs' для некоторого значения x и список xs'. Это приводит к основному случаю и индуктивному случаю, соответственно. В обоих случаях нам нужно доказать одно и то же оригинальное свойство, но мы знаем дополнительную информацию о том, что выглядит xs (т. Е. «Структура» xs).

Для каждого случая вы используете структуру, чтобы выяснить, какое заявление вы хотите получить (приблизительно правильно в исходном вопросе).Затем вы выполните , попробуйте, чтобы просто перейти от выражения в левой части инструкции к выражению с правой стороны, используя правила оценки, идентификационные данные и любые доступные вам леммы. В индуктивном случае у вас есть дополнительный факт, который вы можете использовать около xs' («индуктивная гипотеза»). Этот «прямой» подход не будет работать во всех (возможно, большинстве) случаях на уровне исследований, но он отлично подходит для этого упражнения.

Фактические утверждения, доказанные в случаях

1. Если xs = [], foo (foo xs ys) zs = foo ys (xs @ zs); и
2. Если xs = x::xs' и foo (foo xs' ys) zs = foo ys (xs' @ zs), то foo (foo xs ys) zs = foo ys (xs @ zs).

ys и zs неявно определяются количественно.