Профилактическая автоматизация в Coq как разложить фактор

Question

Я следую за книгой Software Foundation, и я нахожусь в главе под названием «Imp».

Авторы выставляют небольшой язык является следующее:

Inductive aexp : Type := 
    | ANum : nat -> aexp 
    | APlus : aexp -> aexp -> aexp 
    | AMinus : aexp -> aexp -> aexp 
    | AMult : aexp -> aexp -> aexp. 

Вот функция, чтобы оценить эти выражения:

Fixpoint aeval (a : aexp) : nat := 
    match a with 
    | ANum n ⇒ n 
    | APlus a1 a2 ⇒ (aeval a1) + (aeval a2) 
    | AMinus a1 a2 ⇒ (aeval a1) - (aeval a2) 
    | AMult a1 a2 ⇒ (aeval a1) × (aeval a2) 
    end. 

Упражнение заключается в создании функции, оптимизировать оценку. Например:

APlus a (ANum 0) --> a 

Здесь есть моя оптимизируют функция:

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

И сейчас, я бы доказать, что функция оптимизации звука:

Theorem optimizer_a_sound : forall a, aeval (optimizer_a a) = aeval a. 

Это доказательство довольно сложно. Поэтому я попытался разложить доказательство, используя некоторые леммы.

Вот одна лемма:

Lemma optimizer_a_plus_sound : forall a b, aeval (optimizer_a (APlus a b)) = aeval (APlus (optimizer_a a) (optimizer_a b)). 

У меня есть доказательство, но скучный. Я индукция на, а затем, для каждого случая, я б и уничтожить уничтожение ехра обрабатывать случай, когда б 0.

мне нужно сделать, потому что

n+0 = n 

не уменьшает автоматически, нам нужна теорема, которая равна плюс_0_r.

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

Вот мое доказательство этой леммы:

http://pastebin.com/pB76JFGv

Я думаю, что я должен использовать «Подсказка Перепишите plus_0_r», но я не знаю, как.

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

Answer 1

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

destruct X; try congruence; auto. 

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

Lemma opt1: forall a b, a = ANum 0 -> optimizer_a (APlus a b) = optimizer_a b. 
    intros. 
    destruct a; try congruence; auto; 
    destruct n; try congruence; auto. 
Qed. 

Lemma opt2: forall a b, b = ANum 0 -> optimizer_a (APlus a b) = optimizer_a a. 
    intros; 
    destruct a; try congruence; auto; 
    destruct b; try congruence; auto; 
    destruct n; try congruence; auto; 
    destruct n0; try congruence; auto. 
Qed. 

Lemma opt3: 
    forall a b, 
    a <> ANum 0 -> b <> ANum 0 -> 
    optimizer_a (APlus a b) = APlus (optimizer_a a) (optimizer_a b). 
Proof. 
    intros. 
    destruct a; try congruence; auto; 
    destruct b; try congruence; auto; 
    destruct n; try congruence; auto; 
    destruct n0; try congruence; auto. 
Qed. 

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

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

В любом случае, теперь, когда мы имеем эти леммы, мы можем рассматривать различные случаи (Is a = ANum 0 или нет? Is b?) И просто переписать. Чтобы рассмотреть случаи, нам нужна еще одна лемма, которая гласит, что a либо ANum 0, либо нет.

Lemma ANum0_dec: forall a, {a = ANum 0} + { a <> ANum 0}. 
    destruct a; try destruct n; try (right; discriminate); left; auto. 
Qed. 

Мы можем уничтожить ANum0_dec a и получить либо a = ANum 0 в контексте, или a <> ANum 0 в контексте.

Require Import Arith. (* for "auto with arith" to handle n = n + 0 *) 

Lemma optimizer_a_plus_sound : 
    forall a b, 
    aeval (optimizer_a (APlus a b)) = aeval (APlus (optimizer_a a) (optimizer_a b)). 
Proof. 
    intros a b. 
    destruct (ANum0_dec a); destruct (ANum0_dec b). 
    - rewrite opt1; subst; auto. 
    - rewrite opt1; subst; auto. 
    - rewrite opt2; subst; simpl; auto with arith. 
    - rewrite opt3; subst; auto. 
Qed. 

Answer 2

Если вы используете технику выше, вы можете определить свою тактику, поэтому вам не нужно набирать столько же. А поскольку доказательства очень короткие, вы можете обойтись без лемм. (Я назвал тактический dca для destruct-congruence-auto.)

Более короткое доказательство не является читаемым, но по существу: рассмотрим случаи переменных.

Lemma ANum0_dec: forall a, {a = ANum 0} + { a <> ANum 0}. 
    destruct a; try destruct n; try (right; discriminate); left; auto. 
Qed. 

Require Import Arith. 

Ltac dca v := destruct v; try congruence; auto. 

Lemma optimizer_a_plus_sound : 
    forall a b, 
    aeval (optimizer_a (APlus a b)) = aeval (APlus (optimizer_a a) (optimizer_a b)). 
Proof. 
    intros a b; 
    destruct (ANum0_dec a), (ANum0_dec b). 
    - dca a; dca n. 
    - dca a; dca n0. 
    - dca b; dca n0; dca a; simpl; auto with arith; dca n0. 
    - dca a; dca b; dca n1; dca n2. 
Qed. 

Затем используйте его

Theorem optimizer_a_sound : forall a, aeval (optimizer_a a) = aeval a. 

    induction a. 
    * auto. 
    * rewrite optimizer_a_plus_sound; simpl; auto. 
    *  (* ... and so on for Minus and Mult *) 

Вы могли бы также сделать полное доказательство в этой компактной форме.