Как выполнить вычисление в 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))

to 

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))

to

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 в доказательстве.


coq coq-tactic
person tinlyx    schedule 25.11.2015    source источник

Ответы (3)


arrow_upward
3
arrow_downward

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

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) или нет (в этом случае вторая ветвь будут приняты)?

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

person gallais    schedule 25.11.2015
comment
+1 Спасибо, что указали на мою ошибку в случае 0. Я обновил вопрос, чтобы он касался не 0 случаев. Я думаю, что мой первоначальный план должен работать для каждого из них, верно? Если да, то как мне сделать сокращение на один шаг, пожалуйста. - person tinlyx; 26.11.2015

arrow_upward
1
arrow_downward

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

  • сформулируйте лемму о переписывании именно того, что вы хотите, докажите ее и затем используйте. Это лучшее решение, когда вам нужно выполнить очень сложную переписывание, но оно не так хорошо масштабируется, поскольку вам нужно написать лемму для каждой из ваших ситуаций. Например, здесь вы можете заявить (и тривиально доказать, используя simpl):

      forall a1 a2, optimize_0plus (APlus a1 a2) = APlus (optimize_0plus a1) (optimize_0plus a2).

  • Если я правильно помню, simpl и другие не подпадают под переплет. Вы можете использовать тактику pattern для извлечения той части, которую хотите упростить, чтобы simpl или unfold работали только с некоторым подтермоном вашего выражения. Вам следует прочитать документацию, поскольку здесь слишком много объяснений. .

  • РЕДАКТИРОВАТЬ: Я забыл поговорить о тактике replace, которая действует как решение rewrite, но попросит вас сразу же доказать лемму в качестве подцели.

person Vinz    schedule 25.11.2015
comment
change будет работать даже лучше, чем replace, поскольку не требует доказательства - person Anton Trunov; 03.01.2018
comment
Правда, change отсутствует в моем опросе. Однако не забывайте, что change может выйти из строя, если преобразование неочевидно для Coq, поэтому необходимо учитывать оба варианта. - person Vinz; 04.01.2018

arrow_upward
1
arrow_downward

Я согласен, что не всегда легко заставить 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>. Однако я не считаю это хорошим стилем и не предлагаю его использовать.

person eponier    schedule 25.11.2015