coq中的遞歸函數定義，限制可能的輸入集合

Question

我需要定義一個不容易測量的參數的遞歸函數。我保存一個使用過的參數列表，以確保每個參數最多使用一次，並且輸入空間是有限的。

使用度量(inpspacesize - (length l))主要工作，但我陷入了一種情況。看來我錯過了前面幾層l已經正確構建的信息，即沒有重複，並且所有條目都來自輸入空間。

現在我正在尋找一個能夠滿足我需要的列表替換。

編輯我已經減少了這個到現在以下幾點：

我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命令？用非常重的措施定義函數當然非常有用。
• 爲了唯一性，它不會工作，如果你嘗試設置？我記得寫一個函數，聽起來很像你所說的：我有一個函數，其中一個參數包含一組項目。這組項目單調增長，僅限於項目的有限空間，給出了終止論證。