证明非尾递归函数和尾递归函数之间的等价性

Question

我有一个类似于 "optional map" 的递归函数*，具有以下签名：

omap (f : option Z -> list nat) (l : list Z) : option (list nat)

我定义了一个等价的（模列表反转）尾递归函数（下面的omap_tr），我想证明两者是等价的，至少在Some的情况下是这样。

我目前没有这样做，要么是因为我的归纳不变量不够强，要么是因为我没有正确应用双重归纳法。我想知道是否有这种转换的标准技术。

*功能已简化；例如 None 在这里似乎没有用，但在原始功能中是必需的。

代码

这是（简化的）非尾递归函数的代码，以及一个函数示例 f:

Fixpoint omap (f : option Z -> list nat) (l : list Z) : option (list nat) :=
  match l with
  | nil => Some nil
  | z :: zr =>
    let nr1 := f (Some z) in
    let nr2 := match omap f zr with
               | None => nil
               | Some nr' => nr'
               end in
    Some (nr1 ++ nr2)
  end.

Let f (oz : option Z) : list nat :=
  match oz with
  | None => nil
  | Some z => Z.to_nat z :: nil
  end.

例如，omap f 只是将 Z 整数转换为 nat 整数：

Compute omap f (1 :: 2 :: 3 :: 4 :: nil)%Z.

= Some (1%nat :: 2%nat :: 3%nat :: 4%nat :: nil)  : option (list nat)

我执行了我认为是标准的基于累加器的转换，将 acc 参数添加到 f 和 omap:

Fixpoint omap_tr (f_tr : option Z -> list nat -> list nat) (l : list Z)
                 (acc : list nat) : option (list nat) :=
  match l with
  | nil => Some acc
  | z :: zr => let nr1 := f_tr (Some z) acc in
               omap_tr f_tr zr nr1
  end.

Let f_tr rz acc :=
  match rz with
  | None => acc
  | Some z => Z.to_nat z :: acc
  end.

它似乎有效，尽管返回了一个反向列表。下面是一个使用非空累加器的例子：

Compute match omap_tr f_tr (3 :: 4 :: nil)%Z (rev (1 :: 2 :: nil))%nat with
          | Some r => Some (rev r)
          | None => None
        end.

= Some (1%nat :: 2%nat :: 3%nat :: 4%nat :: nil)  : option (list nat)

我的第一次尝试包括一个 nil 累加器：

Lemma omap_tr_failed:
  forall l res,
    omap_tr f_tr l nil = Some res ->
    omap f l = Some (rev res).

但是我没有做归纳。我想这一定是因为不变量不够强大，无法处理一般情况。

不过，在我看来，以下任何引理都应该是可证明的，但恐怕它们也不够强大，无法证明：

Lemma omap_tr':
  forall l acc res,
    omap_tr f_tr l acc = Some (res ++ acc) ->
    omap f l = Some (rev res).

Lemma omap_tr'':
  forall l acc res,
    omap_tr f_tr l acc = Some res ->
    exists res',
      omap f l = Some res' /\
      res = (rev res') ++ acc.

标准的双重归纳法应该允许直接证明这些引理，还是我需要更强的不变量？

Answer 1

是的，您的 omap_tr'' 不变量非常适合您的引理。也许您在进行归纳之前忘记了概括 acc 和 res，或者忘记应用一些关于 app 和 rev 的重写事实？

Lemma omap_tr'':
  forall l acc res,
    omap_tr f_tr l acc = Some res ->
    exists res',
      omap f l = Some res' /\
      res = (rev res') ++ acc.
Proof.
  induction l as [|x l IH]; intros acc res; simpl.
  - intros H. inversion H; subst acc; clear H.
    exists []; eauto.
  - intros H. apply IH in H.
    destruct H as (res' & H & ?). subst res.
    rewrite H.
    eexists; split; eauto.
    simpl. now rewrite <- app_assoc.
Qed.

Lemma omap_tr_correct :
  forall l res,
    omap_tr f_tr l [] = Some res ->
    omap f l = Some (rev res).
Proof.
  intros l res H. apply omap_tr'' in H.
  destruct H as (res' & ? & E).
  subst res.
  now rewrite app_nil_r, rev_involutive.
Qed.

证明非尾递归函数和尾递归函数之间的等价性

Proving equivalence between non-tail-recursive and tail-recursive functions

tail-recursion

coq

proof

equivalence

代码