Как выполнить вычисление ровно один раз в Coq?

Question

Как выполнить вычисление ровно один раз в Coq?

У меня есть нижеприведенное доказательство с еще тремя подцелями. Доказательство - о правильности оптимизации plus 0 (optimize_0plus) на простом арифметическом языке, продемонстрированном здесь. aexp является "арифметическим выражением" и aeval это "арифметическая оценка".

3 subgoal
a1 : aexp
a2 : aexp
IHa1 : aeval (optimize_0plus a1) = aeval a1
IHa2 : aeval (optimize_0plus a2) = aeval a2
______________________________________(1/3)
aeval (optimize_0plus (APlus a1 a2)) = aeval (APlus a1 a2)

, где optimize_0plus является:

Fixpoint optimize_0plus (a:aexp) : aexp :=
  match a with
  | ANum n =>
      ANum n
  | APlus (ANum 0) e2 =>
      optimize_0plus e2
  | APlus e1 e2 =>
      APlus (optimize_0plus e1) (optimize_0plus e2)
  | AMinus e1 e2 =>
      AMinus (optimize_0plus e1) (optimize_0plus e2)
  | AMult e1 e2 =>
      AMult (optimize_0plus e1) (optimize_0plus e2)
  end.

Мой план войны - подать заявку optimize_0plus в LHS текущей подцели и получить:

aeval (APlus (optimize_0plus a1) (optimize_0plus a2)) = aeval (APlus a1 a2)

(Но я не могу понять, как это сделать в Coq).

Затем через некоторые simplполучить:

(aeval (optimize_0plus a1)) + (aeval (optimize_0plus a2)) = (aeval a1) + (aeval a2)

и применить гипотезы индукции IHa1 а также IHa2 чтобы завершить доказательство.

Мой вопрос:

Как я могу сказать Coq применить определение optimize_0plus ровно один раз, а не больше и не меньше?

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

Заметки:

1. Это связано с моим ранним вопросом здесь, но ответы там об использовании simpl XXX не похоже на работу здесь. Это, кажется, более сложный случай.

2. Оригинальный сайт предлагает доказательство того, что работает. Но доказательство там кажется более сложным, чем необходимо, поскольку оно начинает делать анализ случая на условиях a1 и т.п.

  Case "APlus". destruct a1.
    SCase "a1 = ANum n". destruct n.
      SSCase "n = 0". simpl. apply IHa2.
      SSCase "n ≠ 0". simpl. rewrite IHa2. reflexivity.
    SCase "a1 = APlus a1_1 a1_2".
      simpl. simpl in IHa1. rewrite IHa1.
      rewrite IHa2. reflexivity.
    SCase "a1 = AMinus a1_1 a1_2".
      simpl. simpl in IHa1. rewrite IHa1.
      rewrite IHa2. reflexivity.
    SCase "a1 = AMult a1_1 a1_2".
      simpl. simpl in IHa1. rewrite IHa1.
      rewrite IHa2. reflexivity.

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

-- ОБНОВИТЬ --

Благодаря @gallais мой первоначальный план неверен, так как можно изменить

aeval (optimize_0plus (APlus a1 a2))

в

aeval (APlus (optimize_0plus a1) (optimize_0plus a2))

только для случаев, когда a1 не является ANum 0, 0 дело должно рассматриваться отдельно destruct a1. как и на сайте курса, указанном в Примечании 2.

Тем не менее, у меня все еще остается тот же вопрос для других случаев, перечисленных ниже, и я думаю, что мой первоначальный план должен работать:

5 subgoal
SCase := "a1 = APlus a1_1 a1_2" : String.string
Case := "APlus" : String.string
a1_1 : aexp
a1_2 : aexp
a2 : aexp
IHa1 : aeval (optimize_0plus (APlus a1_1 a1_2)) = aeval (APlus a1_1 a1_2)
IHa2 : aeval (optimize_0plus a2) = aeval a2
______________________________________(1/5)
aeval (optimize_0plus (APlus (APlus a1_1 a1_2) a2)) =
aeval (APlus (APlus a1_1 a1_2) a2)
...

______________________________________(5/5)
aeval (optimize_0plus (AMult a1 a2)) = aeval (AMult a1 a2)

Кажется, что для каждого из этих 5 случаев одно приложение (beta сокращение optimize_0plus должны позволить нам изменить, например, (для AMinus)

aeval (optimize_0plus (AMinus a1 a2))

в

aeval (AMinus (optimize_0plus a1) (optimize_0plus a2))

, право?

Если так, как я могу сделать это сокращение за один шаг?

Примечание: я пытался

Eval cbv beta in (aeval (optimize_0plus (AMinus a1 a2))).

И я даже не мог получить aeval (AMinus (optimize_0plus a1) (optimize_0plus a2)) как я хотел бы использовать Eval в доказательство.

2

coq coq-tactic

Источник

user683218 25 ноя '15 в 04:14

3 ответа

Другие вопросы по тегам coq coq-tactic

user727667 25 ноя '15 в 12:50 2015-11-25 12:50 · Answer 1 · 2015-11-25 12:50

Проблема в том, что уравнение, на которое вы рассчитываете полагаться, просто неверно. Не может быть так, чтобы:

optimize_0plus (APlus a1 a2) = APlus (optimize_0plus a1) (optimize_0plus a2)

учитывая определение optimize_0plus Вы дали: если a1 является ANum 0 затем optimize_0plus (APlus a1 a2) уменьшится до optimize_0plus a2 один, а не APlusтермин.

Однако основная теорема, которую вы пытаетесь доказать, действительно верна и может быть доказана путем проверки a1: это ANum 0 (в этом случае первая ветка будет запущена вызовом simpl) или это не так (в каком случае будет взята вторая ветка)?

Как правило, каждый раз, когда вы хотите доказать теорему о функции, определенной с помощью сопоставления с образцом / рекурсивных вызовов, вам необходимо пройти одну и ту же серию гипотез анализа случая / индукции. Это то, что обычно называют функциональной индукцией или индукцией на графе вызовов функции.

user5153939 25 ноя '15 в 13:47 2015-11-25 13:47 · Answer 2 · 2015-11-25 13:47

Я согласен, что не всегда легко заставить Coq выполнять столько вычислений, сколько мы хотим. Но здесь, вопреки тому, что вы говорите, первое переписывание - это не просто шаг вычисления. В самом деле, optimize_0plus разрушает свои аргументы один раз, но когда находит что-то в форме APlus _ _, он должен уничтожить первый новый аргумент, поэтому здесь нужно уничтожить a1 вычислить.

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

Lemma optimize_0plus_aux : forall a1 a2,
  aeval (optimize_0plus (APlus a1 a2)) =
  aeval (APlus (optimize_0plus a1) (optimize_0plus a2)).
Proof.
Admitted.

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

Я знаю, что вы не хотите использовать rewrite каждый раз, но, по моему мнению, наличие леммы об уравнении - лучший способ применить фиксированную точку один раз. Обратите внимание, что вы можете вообще создать эту лемму автоматически Functional Scheme, Вот,
```
Functional Scheme optimize_0plus_ind := Induction for optimize_0plus Sort Prop.
```
В редких случаях есть функция, которую вы никогда не захотите развернуть во время доказательства. В таких случаях вы можете временно сделать определение непрозрачным с помощью Opaque <function>, В конце доказательства сделайте его снова прозрачным с помощью Transparent <function>, Тем не менее, я не думаю, что это хороший стиль и не предлагаю использовать его.

user341499 25 ноя '15 в 08:26 2015-11-25 08:26 · Answer 3 · 2015-11-25 08:26

Я вижу два решения здесь:

сформулируйте переписывающую лемму именно с тем, что вы хотите, докажите это и затем используйте это. Это лучшее решение, когда вам нужно выполнить очень сложное переписывание, но оно не так хорошо масштабируется, поскольку вам нужно написать лемму для каждой из ваших ситуаций. Например, здесь вы можете заявить (и тривиально доказать, используя simpl):
```
forall a1 a2, optimize_0plus (APlus a1 a2) = APlus (optimize_0plus a1) (optimize_0plus a2).
```
Если я правильно помню, simpl и другие не идут под переплетом. Вы можете использовать pattern тактика "извлечь" часть, которую вы хотите упростить, так что simpl или же unfold выступать только на каком-то подслове вашего выражения. Вы должны прочитать документацию, так как здесь немного долго объяснять.
РЕДАКТИРОВАТЬ: я забыл поговорить о replace тактика, которая действует как rewrite решение, но попросит вас доказать лемму сразу, как подзадачу.