如何使用 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.