不能证明关于非标准递归函数的琐碎定理。

Question

我在尝试证明一个我定义的函数时，即使是非常简单的外延，也遇到了很大的困难。这是我的定义。

Require Import List.
Require Export Omega.
Require Export FunInd.
Require Export Recdef.

Notation "A :: B" := (cons A B).
Notation "[]" := nil.
Notation "[[ A ]]" := (A :: nil).

Inductive tm :=
| E: nat -> tm
| L: list tm -> tm.

Definition T := list tm.

Fixpoint add_list (l: list nat) : nat :=
  match l with
  | [] => 0
  | n :: l' => n + (add_list l')
  end.

Fixpoint depth (t: tm) : nat :=
  match t with
  | E _ => 1
  | L l => 1 + (add_list (map depth l))
  end.

Definition sum_depth (l: T) := add_list (map depth l).

Function sum_total (l: T) {measure sum_depth l} : nat :=
  match l with
  | [] => 0
  | [[E n]] => n
  | [[L li]] => sum_total li
  | E n :: l' => n + (sum_total l')
  | L li :: l' => (sum_total li) + (sum_total l')
  end.
Proof.
  - auto.
  - intros; unfold sum_depth; subst. simpl; omega.
  - intros; subst; unfold sum_depth; simpl; omega.
  - intros; subst; unfold sum_depth; simpl; omega.
  Defined.

归纳类型是不能改变的。

我可以证明一些简单的命题，比如 Lemma test : forall n, sum_total [[E n]] = n. 使用 计算 伎俩，但另一个琐碎的乐章，如 Lemma test2 : forall l, sum_total [[L l]] = sum_total l. 挂起。

Answer 1

首先，似乎可以把 compute 战术 "挂在 "你提到的目标上（因为当使用 Function … Proof. … Defined. 定义方法，您的职能 sum_total 包含了一些证明项，而这些证明项并不是用来计算的--更多的是在一个任意的论点上。l；也许是一种策略，如 simpl 或 cbn 在这种情况下更合适）。)

独立于我的 批注我仔细看了一下你的形式化，好像是 Function 命令在你的情况下是不需要的，因为 sum_total 基本上是结构性的，所以你可以用单纯的 Fixpoint如果您正在寻找的归纳类型被稍微改写为一次性定义为一个相互定义的归纳类型，那么您就可以使用这个归纳类型(参见 归纳指令在Coq的Refman中的应用 其中给出了一个类似的、典型的 "树木森林 "的例子）。)

为了详细说明你的例子，你可能需要调整你的定义（如果你的用例可能的话），像这样。

Inductive tm :=
| E: nat -> tm
| L: T -> tm

with T :=
  Nil : T
| Cons : forall (e : tm) (l : T), T.

Notation "[[ A ]]" := (Cons A Nil).

Fixpoint sum_total (l: T) {struct l} : nat :=
  match l with
  | Nil => 0
  | [[E n]] => n
  | [[L li]] => sum_total li
  | Cons (E n) l' => n + (sum_total l')
  | Cons (L li) l' => (sum_total li) + (sum_total l')
  end.

(* and the lemma you were talking about is immediate *)
Lemma test2 : forall l, sum_total [[L l]] = sum_total l.
reflexivity.
Qed.

否则（如果你不能重新表述你的 tm 这样的归纳），另一种解决方案是使用另一种策略，而不是 Function 来定义你的 sum_total 函数，例如 Program Fixpoint或 Equations 插件（这比起 Function 当处理非结构化递归依赖型模式匹配时）。)

编辑。 由于OP提到归纳类型本身不能改变，所以有一个直接的解决方案，即使在使用单纯的 Function 机械：依靠定义自动生成的 "方程定理"。

更准确的说，如果你把你的脚本原封不动地拿出来，那么你就会 "免费 "得到下面的定理。

Search sum_total "equation".
(*
sum_total_equation:
  forall l : T,
  sum_total l =
  match l with
  | [] => 0
  | [[E n]] => n
  | E n :: (_ :: _) as l' => n + sum_total l'
  | [[L li]] => sum_total li
  | L li :: (_ :: _) as l' => sum_total li + sum_total l'
  end
*)

所以，你可以很容易地陈述和证明 你感兴趣的定理，通过这样做：

Lemma test2 : forall l, sum_total [[L l]] = sum_total l.
intros l.
rewrite sum_total_equation.
reflexivity.
Qed.