我很想了解 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 。