2

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

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)

我执行了我认为是标准的基于累加器的转换，同时为and添加了一个acc参数：fomap

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.

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

4

1 回答 1

3

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

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.
于 2015-04-16T20:47:38.500 回答