1

簡単に測定できる引数のない再帰関数を定義する必要があります。使用される引数のリストを保持して、各引数が最大 1 回使用され、入力スペースが有限であることを確認します。

メジャーを使用する(inpspacesize - (length l))とほとんどの場合機能しますが、1 つのケースで行き詰まります。の前のレイヤーが正しく構築されているという情報が欠落しているようですl。つまり、重複はなく、すべてのエントリは実際には入力スペースからのものです。

今、私は必要なことを行うリストの代替品を探しています。

編集これを次のように減らしました。

私はnat与えられたよりも小さい sを持ってmaxおり、関数がすべての数値に対して最大 1 回呼び出されるようにする必要があります。私は次のことを思いつきました：

(* the condition imposed *)
Inductive limited_unique_list (max : nat) : list nat -> Prop :=
  | LUNil  : limited_unique_list max nil
  | LUCons : forall x xs, limited_unique_list max xs
             -> x <= max
             -> ~ (In x xs)
             -> limited_unique_list max (x :: xs).

(* same as function *)
Fixpoint is_lulist (max : nat) (xs0 : list nat) : bool :=
  match xs0 with
  | nil     => true
  | (x::xs) => if (existsb (beq_nat x) xs) || negb (leb x max)
                 then false
                 else is_lulist max xs
  end.

(* really equivalent *)
Theorem is_lulist_iff_limited_unique_list : forall (max:nat) (xs0 : list nat),
    true = is_lulist max xs0 <-> limited_unique_list max xs0.
Proof. ... Qed.

(* used in the recursive function's step *)
Definition lucons {max : nat} (x : nat) (xs : list nat) : option (list nat) :=
  if is_lulist max (x::xs)
    then Some (x :: xs)
    else None.

(* equivalent to constructor *)
Theorem lucons_iff_LUCons : forall max x xs, limited_unique_list max xs ->
    (@lucons max x xs = Some (x :: xs) <-> limited_unique_list max (x::xs)).
Proof. ... Qed.

(* unfolding one step *)
Theorem lucons_step : forall max x xs v, @lucons max x xs = v ->
  (v = Some (x :: xs) /\ x <= max /\ ~ (In x xs)) \/ (v = None).
Proof. ... Qed.

(* upper limit *)
Theorem lucons_toobig : forall max x xs, max < x
    -> ~ limited_unique_list max (x::xs).
Proof. ... Qed.

(* for induction: increasing max is ok *)
Theorem limited_unique_list_increasemax : forall max xs,
  limited_unique_list max xs -> limited_unique_list (S max) xs.
Proof. ... Qed.

要素を完全なリストに挿入できないことを帰納的に証明しようとすると、スタックし続けます (IH が使用できなくなるか、必要な情報を見つけることができません)。この挿入不可能性は終了を示すために重要だと思うので、私はまだ有効な解決策を見つけていません。

これを別の方法で証明する方法、または上記を再構築する方法についての提案はありますか?

4

1 に答える 1

1

詳細がなければ、多くを語ることはできません (詳しく説明してください!) が、:

  • プログラムコマンドを使用していますか? 重要な手段で関数を定義するのに非常に役立ちます。
  • 一意性については、セットを試してみるとうまくいきませんか? 私はあなたが言っていることと非常によく似た関数を書いたことを覚えています: 私は引数にアイテムのセットを含む関数を持っていました. このアイテムのセットは単調に増加し、アイテムの有限スペースに制限されていたため、終了引数が与えられました。
于 2011-07-05T08:14:09.637 に答える