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

Question

我有一个递归函数*，它类似于"可选映射"，具有以下签名：

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)

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

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.