coq - 如何使用 Coq 构建一阶逻辑项？

Question

我正在尝试在 Coq 中定义一阶逻辑，并从术语开始。 假设c1和c2是两个常量符号，变量分别是nat和f1和f2是两个函数符号，其参数分别为1和2，我写了下面的代码。

Definition var := nat.

Inductive const : Type :=
| c1
| c2.

Inductive term : Type :=
| Con : const -> term
| Var : var -> term
| F1 : term -> term
| F2 : term -> term -> term.

然后，我得到了想要的感应。

Check term_ind.
(* ==> term_ind
     : forall P : term -> Prop,
       (forall c : const, P (Con c)) ->
       (forall v : var, P (Var v)) ->
       (forall t : term, P t -> P (F1 t)) ->
       (forall t : term, P t -> forall t0 : term, P t0 -> P (F2 t t0)) ->
       forall t : term, P t *)

然后我想将函数与term的定义分开，所以我重写了上面的内容。

(*Idea A*)
Inductive funct {X : Type} : Type :=
| f1 : X -> funct
| f2 : X -> X -> funct.

Inductive term : Type :=
| Con : const -> term
| Var : var -> term
| Fun : @funct term -> term.

Check term_ind.
(* ==> term_ind
     : forall P : term -> Prop,
       (forall c : const, P (Con c)) ->
       (forall v : var, P (Var v)) ->
       (forall f1 : funct, P (Fun f1)) -> 
       forall t : term, P t *)
Check funct_ind term.
(* ==> funct_ind term
     : forall P : funct -> Prop,
       (forall x : term, P (f1 x)) ->
       (forall x x0 : term, P (f2 x x0)) -> 
       forall f1 : funct, P f1 *)

(*Idea B*)
Inductive term : Type :=
| Con : const -> term
| Var : var -> term
| Fun : funct -> term
with funct : Type :=
| f1 : term -> funct
| f2 : term -> term -> funct.

Check term_ind.
(* ==> term_ind
     : forall P : term -> Prop,
       (forall c : const, P (Con c)) ->
       (forall v : var, P (Var v)) ->
       (forall f1 : funct, P (Fun f1)) ->
       forall t : term, P t *)
Check funct_ind.
(* ==> funct_ind
     : forall P : funct -> Prop,
       (forall t : term, P (f1 t)) ->
       (forall t t0 : term, P (f2 t t0)) ->
       forall f1 : funct, P f1 *)

但是，这两种方法似乎都无法产生所需的归纳，因为它们没有归纳假设。

如何在不丢失正确归纳的情况下构造具有与 term 定义分离的函数的 term？

谢谢。

Answer 1

这是 Coq 的一个常见问题:为互归纳类型和具有复杂递归发生的类型生成的归纳原理太弱。幸运的是，这可以通过手动定义归纳原理来解决。在你的例子中，最简单的方法是使用互归纳定义，因为 Coq 可以帮助我们证明这个原理。

首先，让 Coq 不要生成它的弱默认归纳原理:

Unset Elimination Schemes.
Inductive term : Type :=
| Con : const -> term
| Var : var -> term
| Fun : funct -> term
with funct : Type :=
| f1 : term -> funct
| f2 : term -> term -> funct.
Set Elimination Schemes.

(这并不是绝对必要的，但它有助于保持全局命名空间清洁。)

现在，让我们使用Scheme命令来生成这些类型的互感原理:

Scheme term_ind' := Induction for term Sort Prop
with funct_ind' := Induction for funct Sort Prop.

(*
term_ind'
 : forall (P : term -> Prop) (P0 : funct -> Prop),
   (forall c : const, P (Con c)) ->
   (forall v : var, P (Var v)) ->
   (forall f1 : funct, P0 f1 -> P (Fun f1)) ->
   (forall t : term, P t -> P0 (f1 t)) ->
   (forall t : term, P t -> forall t0 : term, P t0 -> P0 (f2 t t0)) ->
   forall t : term, P t
*)

这个原理已经足够强大，足以让我们证明term的属性，但是使用起来有点尴尬，因为它要求我们指定一个我们想要证明的关于的属性>funct 类型(P0 谓词)。我们可以稍微简化一下，以避免提及这个辅助谓词:我们需要知道的是函数调用中的术语满足我们想要证明的谓词。

Definition lift_pred (P : term -> Prop) (f : funct) : Prop :=
  match f with
  | f1 t => P t
  | f2 t1 t2 => P t1 /\ P t2
  end.

Lemma term_ind (P : term -> Prop) :
  (forall c, P (Con c)) ->
  (forall v, P (Var v)) ->
  (forall f, lift_pred P f -> P (Fun f)) ->
  forall t, P t.
Proof.
intros HCon HVar HFun.
apply (term_ind' P (lift_pred P)); trivial.
now intros t1 IH1 t2 IH2; split.
Qed.

如果您愿意，您还可以重写它，使其看起来更像原始的归纳原理:

Reset term_ind.
Lemma term_ind (P : term -> Prop) :
  (forall c, P (Con c)) ->
  (forall v, P (Var v)) ->
  (forall t, P t -> P (Fun (f1 t))) ->
  (forall t1, P t1 -> forall t2, P t2 -> P (Fun (f2 t1 t2))) ->
  forall t, P t.
Proof.
intros HCon HVar HFun_f1 HFun_f2.
apply (term_ind' P (lift_pred P)); trivial.
- now intros [t|t1 t2]; simpl; intuition.
- now simpl; intuition.
Qed.

编辑

要获得其他方法的归纳原理，您必须手动编写证明项:

Definition var := nat.

Inductive const : Type :=
| c1
| c2.

Inductive funct (X : Type) : Type :=
| f1 : X -> funct X
| f2 : X -> X -> funct X.
Arguments f1 {X} _.
Arguments f2 {X} _ _.

Unset Elimination Schemes.
Inductive term : Type :=
| Con : const -> term
| Var : var -> term
| Fun : funct term -> term.
Set Elimination Schemes.

Definition term_ind (P : term -> Type)
  (HCon : forall c, P (Con c))
  (HVar : forall v, P (Var v))
  (HF1  : forall t, P t -> P (Fun (f1 t)))
  (HF2  : forall t1, P t1 -> forall t2, P t2 -> P (Fun (f2 t1 t2))) :
  forall t, P t :=
  fix loop (t : term) : P t :=
    match t with
    | Con c => HCon c
    | Var v => HVar v
    | Fun (f1 t) => HF1 t (loop t)
    | Fun (f2 t1 t2) => HF2 t1 (loop t1) t2 (loop t2)
    end.