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

没有更多细节很难说(请详细说明！(，但是：

• 您正在使用程序命令吗？这对于用非平凡的度量定义函数当然非常有帮助
• 为了独特性，如果你尝试套装，它不会起作用吗？我记得我写过一个函数，这个函数听起来很像你说的：我有一个函数的自变量包含一组项。这组项是单调增长的，并且被限制在有限的项空间内，给出了终止参数