可能な入力の集合に対する制限付きのcoqにおける再帰関数定義

Question

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

小節を使用すると、ほとんどが動作しますが、私は1つのケースで立ち往生します。 lの以前のレイヤーが正しく構築されているという情報が失われているようです。 e。重複はなく、すべてのエントリは実際に入力スペースからのものです。

今、私が必要とするリストを探しています。

編集私は今、次のようにこれを削減しました：

私はnatが与えられたmaxより小さいよ持っており、機能が多くて一回数のためと呼ばれていることを確認する必要があります。私は、次のを作ってみた：

(* 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が使用できなく出てくるか、私は情報を見つけることができませんいずれか立ち往生保ちます私は欲しい）。この非挿入性は終了を示すために重要だと私は考えていますが、私はまだ解決策を見つけていません。

これを別の方法で証明する方法や、上記の再構成方法に関する提案はありますか？

Answer 1

（手の込んだしてください！）詳細はせずに多くを言うのは難しい、しかし：

• あなたはProgramコマンドを使用していますか？これは確かに重要ではない関数で関数を定義するのに非常に役立ちます。
• あなたはセットを試しても一意ではないでしょうか？私は、あなたが言っていることと非常によく似た機能を書いていることを覚えています。引数に一連の項目が含まれている関数がありました。この一連の項目は単調に増えていて、有限の項目空間に限定され、終了引数が与えられました。