Застрял на доказательстве Coq с индукцией списка

ProgramBox

Застрял на доказательстве Coq с индукцией списка

Post author:admin
Запись опубликована:7 февраля, 2023
Post category:Вопросы по программированию

#coq

Вопрос:

Я обнаружил, что застрял на доказательстве Coq.

Предварительные определения:

 Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import Coq.omega.Omega.
Require Import Coq.Lists.List.
Require Export Coq.Strings.String.
Import ListNotations.


Definition total_map (A:Type) := string -> A.
Definition state := total_map nat.

Inductive sinstr : Type :=
| SPush : nat -> sinstr
| SLoad : string -> sinstr
| SPlus : sinstr
| SMinus : sinstr
| SMult : sinstr.



Definition s_execute_instr (st : state) (stack : list nat)
         (instr : sinstr)
  : option (list nat) :=
  match instr with
  | SPush n => Some (n :: stack)
  | SLoad x => Some (st x :: stack)
  | SPlus => match stack with
            | x :: y :: stack' => Some (x y :: stack')
            | _ => None
            end
  | SMinus => match stack with
             | x :: y :: stack' => Some (y-x :: stack')
             | _ => None
             end
  | SMult => match stack with
            | x :: y :: stack' => Some (x*y::stack')
            | _ => None
            end
  end.

Fixpoint s_execute (st : state) (stack : list nat)
                   (prog : list sinstr)
  : option (list nat) :=
  match prog with
  | [] => Some (stack)
  | instr::prog' => match (s_execute_instr st stack instr) with
                  | Some stack' => s_execute st stack' prog'
                  | None => None
                  end
  end.

И моя попытка доказательства теоремы:

 Theorem s_execute_relational : forall (l1 l2: list sinstr) (sk sk': list nat) (st : state),
  s_execute st sk l1 = Some sk' ->
  s_execute st sk (l1    l2) = s_execute st sk' l2.
Proof.
  intros l1 l2 sk sk' st H.
  induction l1 as [|l1' l1].
  - inversion H. reflexivity.
  -

Текущее состояние:

   l1' : sinstr
  l1, l2 : list sinstr
  sk, sk' : list nat
  st : state
  H : s_execute st sk (l1' :: l1) = Some sk'
  IHl1 : s_execute st sk l1 = Some sk' -> s_execute st sk (l1    l2) = s_execute st sk' l2
  ============================
  s_execute st sk ((l1' :: l1)    l2) = s_execute st sk' l2

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

Я тоже пробовал индукцию l2 , но, похоже, это тоже ни к чему не привело;

 Theorem s_execute_relational : forall (l1 l2: list sinstr) (sk sk': list nat) (st : state),
  s_execute st sk l1 = Some sk' ->
  s_execute st sk (l1    l2) = s_execute st sk' l2.
Proof.
  intros l1 l2 sk sk' st H.
  induction l2 as [|l2' l2].
  - simpl. rewrite <- H. replace (l1    []) with l1.
      reflexivity.
      symmetry. apply app_nil_r.
  -

   l1 : list sinstr
  l2' : sinstr
  l2 : list sinstr
  sk, sk' : list nat
  st : state
  H : s_execute st sk l1 = Some sk'
  IHl2 : s_execute st sk (l1    l2) = s_execute st sk' l2
  ============================
  s_execute st sk (l1    l2' :: l2) =
  s_execute st sk' (l2' :: l2)

Странно задавать вопросы такого типа на SO, потому что это не … действительно многоразовый вопрос / заголовок плох, но не уверен, как улучшить этот фронт.

Ответ №1:

вы не должны вводить все переменные, как вы делаете в первой строке. Сначала вы должны взглянуть на свои рекурсивные функции и задать себе два вопроса:

Каковы рекурсивные функции и их «структурно рекурсивные аргументы» здесь. Возможно, вы заметили, что когда Coq принимает рекурсивное определение, оно сообщает вам, в отношении какого аргумента оно структурно рекурсивно.
Что происходит с аргументами, которые не являются структурно рекурсивными в функции: меняются ли они между рекурсивным вызовом или нет?

Ответ на вопрос 1:

В вашем случае у нас есть две основные рекурсивные функции List.app и s_execute . Рекурсивный аргумент to s_execute находится l1 в левой части импликации. Рекурсивный аргумент to s_execute находится l1 l2 в левой части окончательного равенства, а рекурсивный аргумент to s_execute находится только l2 в правой части. Поскольку l1 l2 находится в позиции рекурсивного аргумента, теперь мы можем взглянуть на рекурсивный аргумент app , просмотрев его код, и мы видим, что аргумент, который структурно уменьшается при рекурсивном вызове, снова l1 . Это дает сильное ощущение, что индукция должна выполняться l1 .

Ответ на вопрос 2:
s_execute принимает три аргумента. Состояние не меняется во время выполнения, но стек меняется. Таким образом, вы можете исправить st все доказательство, но аргумент стека не должен быть исправлен. Аналогичное наблюдение появляется для app : второй аргумент не изменяется во время рекурсивных вызовов.

Практически, вы можете начать свое доказательство с

 intros l1 l2.
induction l1 ....

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

Просто для удовольствия вы можете попробовать ввести больше аргументов, но вы должны освободить гибкие аргументы, используя revert тактику. Вот так:

 intros l1 l2 sk sk' st; revert sk.
induction l1 as ....

Здесь нужно только sk освободить (или отменить, или отменить).

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

Позже редактировать

Вот как я начал ваше доказательство:

 Theorem s_execute_relational : forall (l1 l2: list sinstr) (sk sk': list nat) (st : state),
  s_execute st sk l1 = Some sk' ->
  s_execute st sk (l1    l2) = s_execute st sk' l2.
Proof.
intros l1 l2 sk sk' st; revert sk.
induction l1 as [ | n l1 Ih].  
  simpl; intros sk [= skk']; rewrite skk'; easy.

Теперь мы находимся на этапе индукции. Стек по-прежнему повсеместно определяется количественно в заключении цели. Таким образом, гипотеза индукции и цель на самом деле говорят о двух потенциально разных стеках. Следующий шаг — исправить произвольный стек для обоснования вывода.

 intros sk.

Затем мы вычисляем,

 simpl.

Мы рассуждаем о символическом выполнении кода, и мы не знаем, как (s_execute_instr st sk n) это произойдет, поэтому нам нужно охватить оба случая, это то, что destruct делает шаг.

 destruct (s_execute_instr st sk n) as [sk1 | ].

В первом случае (для выполнения (s_execute_instr st sk n) ) появляется новое состояние sk1 , в котором будет выполняться выполнение, и мы знаем, что
выполнение l1 из этого состояния приводит именно к Some sk' . Давайте дадим имя complete_l1 этому новому состоянию. Теперь случается, что доказательство может быть завершено путем создания экземпляра гипотезы индукции в этом новом состоянии.

   intros complete_l1.
  now rewrite (Ih sk1).

Остается другой случай, созданный destruct шагом, но этот случай содержит самосогласованное предположение о форме None = Some sk' . easy Тактика знает, как избавиться от этого (на самом деле easy полагается на discriminate , который реализует то, что я хотел бы назвать свойством неразберихи типов данных).

 easy.
Qed.

Пожалуйста, скажите мне, чего не хватало в вашей попытке? Это был destruct шаг?

1. Я все еще не уверен, как sk мне помогает free. Должен ли я представить их отдельно в разделе индуктивной гипотезы? Что мне делать в части индуктивной гипотезы? Я все еще чувствую себя потерянным.

2. Ваш комментарий неясен: что вы называете «разделом индуктивной гипотезы». Когда вы делаете доказательство по индукции, у вас есть две цели. В каждом из них вы должны сделать intros sk , потому что цель, которую вы получаете после шага индукции, является универсальной количественной оценкой. Итак, как и в вашей попытке, у вас будет a sk в вашем контексте, но разница в том, что на этапе индукции гипотеза индукции будет универсально определена количественно, а не только для sk .

3. Правильно, я имел в виду индуктивный шаг (в отличие от базового варианта). Я хотел спросить, что делать на индуктивном этапе, теперь, когда у меня есть универсальная количественная sk оценка. Я до сих пор не знаю, куда идти после этого.

4. Я бы предпочел привести вам пример более простого доказательства, но я не могу найти, как продолжить этот разговор в чате, поскольку комментарии довольно громоздки для этого.

5. Я бы предпочел привести вам пример более простого доказательства, но я не могу найти, как продолжить этот разговор в чате, поскольку комментарии довольно громоздки для этого.

Ответ №2:

В конце концов, я понял это.

 Theorem s_execute_relational : forall (l1 l2: list sinstr) (sk sk': list nat) (st : state),
  s_execute st sk l1 = Some sk' ->
  s_execute st sk (l1    l2) = s_execute st sk' l2.
Proof.
  intros l1.
  induction l1 as [| l1' l1].
  - intros l2 sk sk' st H. simpl.
    inversion H. reflexivity.
  - intros l2 sk sk' st H.
    assert (forall (x:sinstr) (xs ys: list sinstr), (x::xs)   ys = x::(xs  ys)) as app_comm_cons.
    {
      auto.
    }
    rewrite app_comm_cons.
    unfold s_execute in *. destruct (s_execute_instr st sk l1').
      eapply IHl1. apply H.
      inversion H.
Qed.