Coq中的术语"10"到底是什么？

Question

关于Coq(使用Init库)的一个非常基本的问题:术语10是类型nat,并且类型nat是归纳定义的:

Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

Q1.但"10"是"捷径" S(S(...S(0)...))吗？

Q2.是否有以下引理的最短(正式)证明？(不使用欧米茄)

Lemma gg : 3 <= 10.
apply le_S.
apply le_S.
apply le_S.
apply le_S.
apply le_S.
apply le_S.
apply le_S.
apply le_n.
Qed.

换句话说,n <= m(只有Peano公理)证明需要指数长度吗？

Answer 1

Q1:是的.

Q2:你可以使用反射证明技术来消除这些琐碎的大样本.本章介绍了您希望如何以及为什么要这样做:

http://adam.chlipala.net/cpdt/html/Reflection.html

Answer 2

A1.对.

A2.据我所知,le(<=)的定义,你必须使用le_S并le_n构建它的证明.

Inductive le (n : nat) : nat -> Prop :=
    le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m

...除非你定义一个引理使你的工作更轻松.

你可以这样做:

Lemma gg : 3 <= 10.
Proof.
  do 7 (apply le_S).
  apply le_n.
Qed.

... 要么

Lemma gg' : 3 <= 10.
Proof. repeat constructor. Qed.

......或者反过来说:

Lemma le_s : forall n m, n <= m -> S n <= S m.
Proof.
  intros. induction H. constructor.
  constructor. apply IHle.
Qed.

Lemma gg'' : 3 <= 10.
Proof.
  pose proof (le_n 0).
  do 3 (apply le_s in H).
  do 7 (apply le_S in H).
  apply H.
Qed.

Answer 3

下面是Ptival答案的一个例子.

Require Import Coq.Arith.Arith.

Check @eq_refl.
Check leb_complete.

Goal 3 <= 10. Proof. apply leb_complete. apply eq_refl. Qed.

Goal 30 <= 100. Proof. apply leb_complete. apply eq_refl. Qed.

Goal 300 <= 1000. Proof. apply leb_complete. apply eq_refl. Qed.

想一想,是不是omega也是反思的一种证明形式？或者它是否在OCaml中编程？