时间戳

首页 > 解决方案 > 无法证明非标准递归函数的微不足道的引理

coq - 无法证明非标准递归函数的微不足道的引理

问题描述

我很难证明关于我定义的函数的非常简单的引理。这是我的定义：

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.挂起。

标签： coqcoq-tactic

解决方案

首先，策略“挂”在您提到的目标上似乎是可以的compute（因为在使用Function … Proof. … Defined.定义方法时，您的函数sum_total包含一些不打算计算的证明术语 - 尤其是在任意参数上l；也许是一种策略例如simpl或cbn更适合这种情况）。

独立于我对 list notations 的评论，我仔细研究了您的形式化，Function在您的情况下似乎不需要该命令，因为sum_total本质上是结构性的，因此您可以使用 mere Fixpoint，前提是您正在查看的归纳类型稍微改写一次性定义为相互定义的归纳类型（请参阅Coq 的 refman 中 Inductive 命令的相应文档，其中给出了“树/森林”的类似典型示例）。

为了详细说明您的示例，您可能需要像这样调整您的定义（如果可能适用于您的用例）：

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.

推荐阅读