coq - 需要互递归的定理怎么做？

Question

我遇到了一个需要相互递归来解决的问题。我无法在 Coq 中做到这一点，但我怀疑在 Agda 中可能可以做到这一点，并证明了使用两个相互递归函数的情况就是如此。我不确定我到底应该做什么才能将该解决方案带回到 Coq 中，并且谷歌搜索这个问题并没有找到任何解决方案。

我有什么选择？

为了进一步激发这里的问题，我想将 Agda 证明转化为 Coq。它证明了树行走和扁平计算器之间的功能等同性。

证明要求 remove-from-stack 和 add-to-stack 以相互递归的方式相互调用。

open import Data.Product
open import Data.Nat
open import Data.List
open import Data.List.Properties
open import Function

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; subst)
open Eq.≡-Reasoning

data Sinstr : Set where
  SPush : ℕ → Sinstr
  SPlus : Sinstr

data Aexp : Set where
  ANum : (n : ℕ) → Aexp
  APlus : Aexp → Aexp → Aexp

s-execute : List Sinstr → List ℕ → List ℕ
s-execute [] stack = stack
s-execute (SPush x ∷ prog) stack = s-execute prog (x ∷ stack)
s-execute (SPlus ∷ prog) (x1 ∷ x2 ∷ stack) = s-execute prog (x2 + x1 ∷ stack)
s-execute _ stack = stack

aeval : Aexp → ℕ
aeval (ANum n) = n
aeval (APlus a a₁) = aeval a + aeval a₁

s-compile : Aexp → List Sinstr
s-compile (ANum n) = [ SPush n ]
s-compile (APlus a a₁) = s-compile a ++ s-compile a₁ ++ [ SPlus ]

++-assoc⁴ : ∀ {T : Set} (a b c d : List T) → (a ++ b ++ c) ++ d ≡ a ++ b ++ c ++ d
++-assoc⁴ a b c d =
  begin
    ((a ++ b ++ c) ++ d)
  ≡⟨ ++-assoc a (b ++ c) d ⟩
    (a ++ (b ++ c) ++ d)
  ≡⟨ cong (a ++_) (++-assoc b c d) ⟩
    (a ++ b ++ c ++ d)
  ∎

remove-from-stack : ∀ {e2 stack x} e1 →
  s-execute (s-compile e1 ++ e2) stack ≡ [ x ] →
  ∃[ a ] (s-execute e2 (a ∷ stack) ≡ [ x ] × s-execute (s-compile e1) [] ≡ [ a ])

add-to-stack : ∀ {e2 stack x} e1 →
  s-execute (s-compile e1) [] ≡ [ x ] →
  s-execute (s-compile e1 ++ e2) stack ≡ s-execute e2 (x ∷ stack)

remove-from-stack (ANum n) prf = n , (prf , refl)
remove-from-stack {rest} {stack} (APlus e1 e2) prf with subst (λ l → s-execute l stack ≡ _) (++-assoc⁴ (s-compile e1) (s-compile e2) [ _ ]  rest) prf
... | []∷stack with remove-from-stack e1 []∷stack
remove-from-stack {rest} {stack} (APlus e1 e2) _ | []∷stack | a , a∷stack , e1≡a with remove-from-stack e2 a∷stack
remove-from-stack {rest} {stack} (APlus e1 e2) _ | []∷stack | a , a∷stack , e1≡a | b , b∷a∷stack , e2≡b = a + b , b∷a∷stack , e1+e1≡a+b where
  e1+e1≡a+b : _
  e1+e1≡a+b =
    begin
      s-execute (s-compile e1 ++ s-compile e2 ++ SPlus ∷ []) []
    ≡⟨ add-to-stack e1 e1≡a ⟩
      s-execute (s-compile e2 ++ SPlus ∷ []) [ a ]
    ≡⟨ add-to-stack e2 e2≡b ⟩
      s-execute (SPlus ∷ []) (b ∷ [ a ])
    ≡⟨⟩
      (a + b ∷ [])
    ∎

add-to-stack (ANum n) refl = refl
add-to-stack (APlus e1 e2) []∷[] with remove-from-stack e1 []∷[]
add-to-stack (APlus e1 e2) []∷[] | a , a∷[] , e1≡a with remove-from-stack e2 a∷[]
add-to-stack {rest} {stack} (APlus e1 e2) []∷[] | a , a∷[] , e1≡a | b , refl , e2≡b =
  begin
    s-execute ((s-compile e1 ++ s-compile e2 ++ SPlus ∷ []) ++ rest) stack
  ≡⟨ cong (λ l → s-execute l stack) (++-assoc⁴ (s-compile e1) (s-compile e2) [ _ ]  rest) ⟩
    s-execute (s-compile e1 ++ s-compile e2 ++ SPlus ∷ [] ++ rest) stack
  ≡⟨ add-to-stack e1 e1≡a ⟩
    s-execute (s-compile e2 ++ SPlus ∷ [] ++ rest) (a ∷ stack)
  ≡⟨ add-to-stack e2 e2≡b ⟩
    s-execute rest (a + b ∷ stack)
  ∎

s-compile-correct : (e : Aexp) → s-execute (s-compile e) [] ≡ [ aeval e ]
s-compile-correct (ANum n) = refl
s-compile-correct (APlus l r) =
  begin
    (s-execute (s-compile l ++ s-compile r ++ SPlus ∷ []) [])
  ≡⟨ add-to-stack l (s-compile-correct l) ⟩
    (s-execute (s-compile r ++ SPlus ∷ []) (aeval l ∷ []))
  ≡⟨ add-to-stack r (s-compile-correct r) ⟩
    (s-execute (SPlus ∷ []) (aeval r ∷ aeval l ∷ []))
  ≡⟨⟩
    (aeval l + aeval r ∷ [])
  ∎

Answer 1

正如我所评论的，我不知道处理互递归定理的通用方法，但是(根据我的浅薄经验)我不需要一组互递归定理，除非它们涉及互递归数据类型或函数(在这种情况下，我建议 Equations plugin )。

这个答案侧重于具体问题。

---

这个问题与 Induction Exercises 的最后一个练习非常接近，除了当 Plus 指令给出的参数太少时程序会停止(这使得问题稍微困难一些)。

我们从 @larsr 的定义开始:

Require Import Coq.Lists.List.
Import ListNotations.

Inductive Sinstr : Set := SPush (_:nat) | SPlus.
Inductive Aexp : Set := ANum (_:nat) | APlus (_ _:Aexp).

Fixpoint sexec (p:list Sinstr) (s:list nat) : list nat :=
  match (p, s) with
  | ([], stack) => stack
  | ((SPush x)::prog, stack) => sexec prog (x::stack)
  | (Splus::prog, x1::x2::stack)  =>  sexec prog (x1+x2::stack)
  | (_, stack) => stack
  end.

Fixpoint aeval (a:Aexp) : nat :=
  match a with
  | ANum n => n
  | APlus a1 a2 => aeval a2 + aeval a1
  end.

Fixpoint compile (a:Aexp) : list Sinstr :=
  match a with
  | ANum n => [SPush n]
  | APlus a1 a2 => compile a1 ++ compile a2 ++ [SPlus] 
  end.

首先，我们直接尝试归纳证明:

Theorem compile_correct_try e : sexec (compile e) [] = [aeval e].
Proof.
  induction e; intros; auto. (* base case is easy *)
  simpl.

e1, e2 : Aexp
IHe1 : sexec (compile e1) [] = [aeval e1]
IHe2 : sexec (compile e2) [] = [aeval e2]
____________________________________________
sexec (compile e1 ++ compile e2 ++ [SPlus]) [] = [aeval e2 + aeval e1]

我们现在陷入困境。不过我们可以做出一些观察:

• 我们需要一个涉及两个程序串联的引理(显然)。
• 我们还需要一个适用于任何初始堆栈的引理(因为 compile e2 将在堆栈 [aeval e1] 上运行，而不是 [] )。

所以我们尝试写一个通用引理:

Lemma prg_concat :
  forall p1 p2 stack, sexec (p1 ++ p2) stack = sexec p2 (sexec p1 stack).

但这完全是错误的，因为 p2如果 p1 则不应运行被中止。那么我们应该确保p1不会中止。人们可能想要定义“运行到完成”属性，但我们有一个明显有效的特殊情况:compile e 。它非常适合我们的归纳情况，因为左侧操作数为 ++其形式为compile _ :

sexec (compile e1 ++ compile e2 ++ [SPlus]) stack
->
sexec (compile e2 ++ [SPlus]) (sexec (compile e1) stack)
->
sexec [SPlus] (sexec (compile e2) (sexec (compile e1) stack))

对应的语句是:

Lemma compile_concat :
  forall e p s, sexec (compile e ++ p) s = sexec p (sexec (compile e) s).

但这还不够，因为不能保证最终的SPlus将会成功。因此，我们将主要目标纳入sexec (compile e) = [aeval e]进入引理，即代替 sexec (compile e) s ，我们写 aeval e :: s 。现在我们可以保证，当我们到达最终的SPlus时，堆栈上至少有两个元素。 .

这是 larsr 的引理:

Lemma compile_ok (e:Aexp): 
  forall p s, sexec (compile e ++ p) s = sexec p (aeval e::s).
Proof.
  induction e.
  reflexivity.
  intros; simpl;
    rewrite <-? app_assoc, IHe1, IHe2; reflexivity.
Qed.

---

此外，here是 rewrite <-? expr 的文档，在 rewrite 部分的末尾:

Orientation -> or <- can be inserted before each term to rewrite.

In all forms of rewrite described above, a term to rewrite can be immediately prefixed by one of the following modifiers:

• ?: the tactic rewrite ?term performs the rewrite of term as many times as possible (perhaps zero time). This form never fails.

所以rewrite <-? app_assoc, IHe1, IHe2.表示通过 app_assoc 重复(反向)重写，然后(向前)重写为 IHe1和IHe2每个一次。