Как проанализировать две, казалось бы, эквивалентные программы с разным поведением в coq?

Я работаю над доказательством корректности компилятора в основах языка программирования и часами чесал в затылке, прежде чем сдаться и применить это решение, которое я нашел в сети (https://github.com/haklabbeograd/software-Foundation-coq-shops/blob/master/Imp.v ). Я попытался адаптировать свою функцию (первый s_execute), но она все равно не сработает, чтобы доказать приведенную ниже лемму (работает только последняя реализация). Кроме того, я могу заставить онлайн-решение работать только тогда, когда я запускаю его в его файле, а не в моем (все определения одинаковы, за исключением instr vs sinstr, а переменные определены немного по-другому). Почему это так (в частности, почему ошибка объединения возникает только в первом решении)? Кроме того, в книге сказано:

Помните, что в спецификации не указано, что делать при обнаружении инструкции [SPlus], [SMinus] или [SMult], если стек содержит менее tw элементов. (Чтобы упростить доказательство правильности, возможно, вам будет полезно вернуться и изменить свою реализацию!)

Какое определение автор намеревается изменить, чтобы сделать это правильным?

Fixpoint s_execute (st : state) (stack : list nat)
                   (prog : list instr)
  : list nat :=
  match prog with
  | [] => stack
  | x :: xs => match x, stack with
                 | (SPush n), ys => s_execute st (n :: ys) xs
                 | (SLoad x), ys => s_execute st ((st x) :: ys) xs
                 | SPlus, y1 :: y2 :: ys => s_execute st ((y1 + y2) :: ys) xs
                 | SMinus, y1 :: y2 :: ys => s_execute st ((y2 - y1) :: ys) xs
                 | SMult, y1 :: y2 :: ys => s_execute st ((y2 * y1) :: ys) xs
                                                      | _, _ => stack
               end
  end.

Fixpoint s_execute (st : state) (stack : list nat)
                   (prog : list instr)
                 : list nat :=
let newstack :=
  match prog with
    | [] => stack
    | (SPush n)::_ => n::stack
    | (SLoad id)::_ => (st id)::stack
    | SPlus::_  => match stack with
                        | n::(m::rest) => (m+n)::rest
                        | _ => stack
                      end
    | SMinus::_  => match stack with
                         | n::m::rest => (m-n)::rest
                         | _ => stack
                       end
    | SMult::_  => match stack with
                        | n::m::rest => (m*n)::rest
                        | _ => stack
                      end
  end in
  match prog with
    | [] => stack
    | instr::rest => s_execute st newstack rest
  end.

Приведенная ниже лемма работает только со второй реализацией, хотя обе соответствуют приведенным примерам s_execute (1 | 2).

Lemma s_execute_app : forall st p1 p2 stack,
  s_execute st stack (p1 ++ p2) = s_execute st (s_execute st stack p1) p2.
  intros st p1.
  induction p1.
  intros; reflexivity.
  intros.
  apply IHp1.
Qed.

compiler-construction theorem-proving coq
person Community    schedule 23.12.2019    source источник
comment
Я потратил пару часов на доказательство леммы. Часть, в которой я застрял, не смогла создать индуктивную гипотезу, обобщенную как в p2, так и в стеке. Обратите внимание, что в авторском доказательстве s_execute_app первая строка - это intros st p1, а не intros. обобщить зависимый p2.   -  person Cookie Monster    schedule 27.03.2020

Ответы (1)


arrow_upward
0
arrow_downward

Эти два определения s_execute не эквивалентны: при обнаружении недопустимой инструкции первое останавливается немедленно (_, _ => stack), а второе пропускает его, но все равно оценивает остальную часть программы (s_execute ... rest).

Из-за этой разницы первая версия не удовлетворяет s_execute_app лемме. Однако эта лемма не является частью упражнения, это всего лишь добавление автора найденного вами решения, которое может облегчить окончательное доказательство, но не является строго обязательным.

Это основная причина, по которой доказательство не проходит: оно не проходит.

Однако доказательство застревает немного раньше, чем могло бы, из-за различий в синтаксисе: первое определение делает больше matches, прежде чем подвергнуть рекурсивный вызов s_execute, тогда как второе определение делает только один match в начале и скрывает остальное в местном определении newstack.

  let newstack := ... in
  match prog with                                   (* One match... *)
    | [] => stack
    | instr::rest => s_execute st newstack rest     (* ... and the recursive call is revealed *)
  end.

Если вы посмотрите, где вы застряли в доказательстве с вашей версией s_execute, цель - большая куча match, которая не похожа на гипотезу индукции, и поэтому последняя apply не проходит. Обычно, когда в цели есть match, это destruct все, что соответствует. Два случая легко обрабатываются с помощью apply IHp1, поэтому мы можем связать эти тактики, как это, чтобы оставить три арифметических операции, где гипотеза индукции все еще не применима.

destruct a eqn:Ea; try apply IHp1.

Опять больше matches в воротах.

destruct stack.

и вот мы подошли к неразрешимой цели:

--------------------------------------
[ ] = s_execute st [ ] p2

Попытайтесь понять, почему это неверно, а затем, шаг за шагом возвращаясь, вы сможете восстановить контрпример к первоначальному утверждению.

Какое определение автор намеревается изменить, чтобы сделать это правильным?

Оба определения выглядят правильными (я не проверял ваше), но второе определение, скорее всего, приводит к некоторым более кратким доказательствам по причинам, которые я объяснил выше.

person Li-yao Xia    schedule 23.12.2019
comment
Спасибо, @ Ли-яо Ся. Есть ли еще одна «более естественная» лемма, которую вы бы предложили использовать для доказательства корректности компилятора? - person ; 23.12.2019
comment
Не уверен, что для этого вам понадобится специальная лемма. Борьба с теоремой, чтобы получить представление о правильном способе обобщения ее для индукции, является стандартным способом решения этой проблемы. - person Li-yao Xia; 23.12.2019