Как сделать теоремы, которые требуют взаимной рекурсии?

Question

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

Какие у меня есть варианты?

Для дальнейшей мотивации вопросаВот доказательство Агды, которое я хочу перевести на 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

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

Этот ответ фокусируется на конкретной проблеме.

---

Проблема очень близка к последнему упражнению Индукционные упражнения , за исключением того, что программа останавливается, когда инструкции Плюс дается слишком мало аргументов (что делает задачу немного сложнее).

Мы начнем с определений @ 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.

Итак, вот лемма Ларса:

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.

---

Также, здесь - документация rewrite <-? expr, в конце раздела rewrite:

Ориентацию -> или <- можно вставить перед каждым термином для перезаписи.

Во всех описанных выше формах перезаписи термину для переписывания может быть немедленно предшествен один из следующих модификаторов:

• ?: тактика rewrite ?term выполняет перезапись терма столько раз, сколько возможно (возможно, нулевое время). Эта форма никогда не подведет.

То есть rewrite <-? app_assoc, IHe1, IHe2. означает повторение (обратное) перезапись на app_assoc, а затем (прямое) перезапись на IHe1 и IHe2 по одному разу.