3

Omegaを使ってCoqで証明しようとしています。私はそれに多くの時間を費やしましたが、何も思い浮かびませんでした。私は Coq を初めて使用するので、この種の言語には慣れておらず、あまり経験がありません。しかし、私はそれに取り組んでいます。

これが私が証明しなければならないコードです：

Require Import Arith Omega.

Fixpoint div2 (n : nat) :=
 match n with
   S (S p) => S (div2 p)
 | _ => 0
 end.

Fixpoint mod2 (n : nat) :=
 match n with
   S (S p) => mod2 p
 | x => x
 end.

この証明を行うには、最初にこの補題を帰納法で証明すると役立つと思いました。

Lemma div2_eq : forall n, 2 * div2 n + mod2 n = n.

次に、これは、 omega と div2_eq を使用して:

Lemma div2_le : forall n, div2 n <= n.

しかし、私はそれ以上進むことができませんでした。

誰も何をすべきか知っていますか？

4

1 に答える 1

4

div2関数から誘導原理を簡単に導き出すことができますmod2。

Functional Scheme div2_ind := Induction for div2 Sort Prop.
Functional Scheme mod2_ind := Induction for mod2 Sort Prop.

div2_indmod2_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.

機能的帰納法に慣れる必要がありますが、さらに重要なことは、十分に根拠のある帰納法に精通する必要があります。

于 2012-12-15T21:38:30.277 に答える