您可以轻松地从函数中得出归纳原则,div2
如下mod2
所示:
Functional Scheme div2_ind := Induction for div2 Sort Prop.
Functional Scheme mod2_ind := Induction for mod2 Sort Prop.
div2_ind
并mod2_ind
有或多或少的类型:
forall P1,
P1 0 0 ->
P1 1 0 ->
(forall n1, P1 n1 (div2 n1) -> P1 (S (S n1)) (S (div2 n1))) ->
forall n1, P1 n1 (div2 n1)
forall P1,
P1 0 0 ->
P1 1 1 ->
(forall n1, P1 n1 (mod2 n1) -> P1 (S (S n1)) (mod2 n1)) ->
forall n1, P1 n1 (mod2 n1)
要应用这些定理,您可以方便地编写functional induction (div2 n)
或functional induction (mod2 n)
通常编写的地方induction n
。
但更强的归纳原理与这些功能相关:
Lemma nat_ind_alt : forall P1 : nat -> Prop,
P1 0 ->
P1 1 ->
(forall n1, P1 n1 -> P1 (S (S n1))) ->
forall n1, P1 n1.
Proof.
intros P1 H1 H2 H3. induction n1 as [[| [| n1]] H4] using lt_wf_ind.
info_auto.
info_auto.
info_auto.
Qed.
事实上,任何函数的域都是一个有用的归纳原理的线索。例如,与功能域相关的归纳原理plus : nat -> nat -> nat
就是mult : nat -> nat -> nat
结构归纳。这让我想知道为什么Functional Scheme
不只是产生这些更一般的原则。
在任何情况下,您的定理证明将变为:
Lemma div2_eq : forall n, 2 * div2 n + mod2 n = n.
Proof.
induction n as [| | n1 H1] using nat_ind_alt.
simpl in *. omega.
simpl in *. omega.
simpl in *. omega.
Qed.
Lemma div2_le : forall n, div2 n <= n.
Proof.
induction n as [| | n1 H1] using nat_ind_alt.
simpl. omega.
simpl. omega.
simpl. omega.
Qed.
您应该熟悉功能归纳,但更重要的是,您应该真正熟悉有根据的归纳。