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

如何使用 Coq 在一阶逻辑中构造项？

How can I construct terms in first-order logic using Coq?

coq

first-order-logic