我需要定义一个没有容易测量的参数的递归函数。我保留了一个已使用参数的列表,以确保每个参数最多使用一次,并且输入空间是有限的。
使用措施(inpspacesize - (length l))
最有效,但我陷入了一种情况。看来我错过了前几层l
已正确构建的信息,即没有重复,所有条目都来自输入空间。
现在我正在寻找一个可以满足我需要的列表替换。
编辑我现在将其简化为以下内容:
我的nat
s 小于给定的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 无法使用或我找不到我需要的信息)时,我一直卡住。由于我认为这种不可插入性对于显示终止至关重要,因此我仍然没有找到可行的解决方案。
关于如何以不同方式证明这一点或重组上述内容的任何建议?