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変換します。Znat

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

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

標準のアキュムレータベースの変換であると思われる変換を実行し、と の両方に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''不変式は補題に対して完全に機能します。たぶん、帰納法を行う前に一般化するのを忘れたか、 と について書き直した事実を適用するのを忘れていたのではないaccでしょうか?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 に答える