4

自然数の偶数性の帰納的および計算上の定義は次のとおりです。

Inductive ev : nat -> Prop :=
  | ev_0 : ev O
  | ev_SS : forall n:nat, ev n -> ev (S (S n)).

Definition even (n:nat) : Prop := 
  evenb n = true.

そして、一方が他方を暗示しているという証拠。

Theorem ev__even : forall n,
  ev n -> even n.
intros n E.
induction E as [ | n' E' ]. 
reflexivity. apply IHE'. Qed.

最初はこの証明についてあまり考えていませんでしたが、よく見ると厄介なことがわかりました。問題は、reflexivityステップの後にコンテキストが表示されることを期待していることです

1 subgoal
n' : nat
E : ev (S (S n'))
E' : ev n'
IHE' : ev n' -> even n'
====================================================================== (1/1)
even (S (S n'))

しかし、私が実際に得るのは代わりに

1 subgoal
n' : nat
E' : ev n'
IHE' : even n'
====================================================================== (1/1)
even (S (S n'))

定理はそのまま証明可能ですが、仮説が不思議なことに消えていくのを見るのは気がかりです。最初に期待したコンテキストを取得する方法を知りたいです。Web 検索から、これは Coq で構築された項に対する帰納法に関する一般的な問題であることを理解しています。SO に関する提案された解決策の 1 つはremember、仮説を保持するための戦術を使用することを提案しています。しかし、この証明でそれを試すと、

Theorem ev__even : forall n,
  ev n -> even n.
intros n E.
remember E.
induction E as [ | n' E' ].

ステップで次のエラー メッセージが表示されますinduction。

Error: Abstracting over the term "n" leads to a term
"fun n : nat => forall e : ev n, e = E -> even n" which is ill-typed.

私にはよくわかりません。問題は自由変数があることだと思いますが、その場合、も導入せずEに導入する方法がないため、行き詰まります。（それで一般化します）Engeneralize dependent nE

最初に予想されるコンテキストを取得する方法はありますか?

4

2 に答える 2

3

有用であるために、誘導タクティックは、誘導を行っているものに依存するすべての変数と、その型のインデックスに依存するものを一般化しようとします。あなたの場合、これnは、新しく生成された証明e : ev n、および等式を一般化することを意味しますe = E。Eただし、命題に対して自動的に生成される帰納法は証明の議論を無視するため、それ自体は一般化されません。残念ながら、これはその一般化が不適切な型付けになることを意味し、あなたの直感は正しいです:Eは で一般化されていないためn、その型は別の数値に言及し、等式e = Eの型付けが不適切になります。

于 2014-06-29T11:32:17.913 に答える
2

inductionここで戦術が何をしているのか理解できません。戦術が何をしているのか理解できないときはいつでも、自分で証明項を書こうとします。誘導原理を手動で呼び出すと、元の仮説を維持できます。

Theorem ev__even : forall n, ev n -> even n.
  intros n E.
  refine (ev_ind even _ _ n E).
  - reflexivity.
  - intros n' E' IH.
    apply IH.
Qed.

これは、誘導の 2 番目のケースでコンテキストがどのように見えるかです。

  n : nat
  E : ev n
  n' : nat
  E' : ev n'
  IH : even n'
  ============================
   even (S (S n'))

仮定

Fixpoint evenb (n:nat) : bool :=
  match n with
  | O        => true
  | S O      => false
  | S (S n') => evenb n'
  end.
于 2014-06-28T16:35:27.813 に答える