0

我很想了解 Coq 中的类型推断。在给定证明项/对象/程序的情况下，我想要在 Coq 中以一种具体的方式生成类型（定理）。所以给定一个证明项（可能有一个洞，可能没有洞，或者可能是一个证明子项）我可以确定地生成它的类型吗？我想知道 Coq 是否为此提供了这个功能，例如在伪 Coq 中：

program := (fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) eq_refl
  (fun (n' : nat) (IH : n' + 0 = n') =>
eq_ind_r (fun n0 : nat => S n0 = S n') eq_refl IH)
  n)
.

type := Coq.Proofterm_2_Type(program).

Print type.

Coq 中的正确功能是什么：给定一个证明术语，让我得到它的类型（基本上在 Coq/Gallina 中的类型推断）。

我在玩这个证明，它是证明对象：

Theorem add_easy_induct_1:
    forall n:nat,
      n + 0 = n.
  Proof.
    Show Proof.
    intros.
    Show Proof.
    induction n as [| n' IH].
    Show Proof.
    - simpl. reflexivity.
    Show Proof.
    - simpl. rewrite -> IH. reflexivity.
    Show Proof.
  Qed.

Print add_easy_induct_1.

一些输出示例：

?Goal
(fun n : nat => ?Goal)
(fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) ?Goal
  (fun (n' : nat) (IH : n' + 0 = n') => ?Goal0) n)
(fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) eq_refl
  (fun (n' : nat) (IH : n' + 0 = n') => ?Goal) n)
(fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) eq_refl
  (fun (n' : nat) (IH : n' + 0 = n') =>
eq_ind_r (fun n0 : nat => S n0 = S n') eq_refl IH)
  n)
add_easy_induct_1 = 
fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) eq_refl
  (fun (n' : nat) (IH : n' + 0 = n') =>
eq_ind_r (fun n0 : nat => S n0 = S n') eq_refl IH)
  n
     : forall n : nat, n + 0 = n

Arguments add_easy_induct_1 _%nat_scope

在等待 Coq、Opam 等安装到我的新计算机时，我使用了非常好的 jsCoq 。

4

2 回答 2

3

您可以使用Check来查看术语的类型：

Let example := (fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) eq_refl
  (fun (n' : nat) (IH : n' + 0 = n') =>
eq_ind_r (fun n0 : nat => S n0 = S n') eq_refl IH)
  n).

Check example.
(*
example
     : forall n : nat, n + 0 = n
*)
于 2021-12-17T16:39:14.080 回答
2 
Definition type_of {A} (_ : A) : Type := A.
于 2021-12-17T16:51:10.100 回答