5

できるだけ早く悪い入力を防ぐことに基づいたプログラミング スタイルを開発しようとしています。たとえば、自然数の先行関数の次のもっともらしい定義の代わりに:

Definition pred1 n :=
  match n with
    | O   => None
    | S n => Some n
  end.

以下のように書きたいと思います。

Theorem nope n (p : n = O) (q : n <> O) : False.
  contradict q.
  exact p.
Qed.

Definition pred2 n (q : n <> O) :=
  match n with
    | S n => n
    | O   =>
      let p := _ in
      match nope n p q with end
  end.

でも何と交換すればいいのかわからない_。私の直観は、ブランチassumption : n = Oに利用可能なものがいくつかあるに違いないことを示唆しています。| O =>Coqは本当にそのような仮定を導入していますか? もしそうなら、その名前は何ですか?

4

1 に答える 1

5

Coq はそのような仮説を自動的に導入しませんが、完全な形式のmatch構造を使用して明示的に導入できます。

Definition pred2 n (q : n <> O) :=
  match n as n' return n = n' -> nat with
    | S p => fun _ => p
    | O   => fun Heq => match q Heq with end
  end (eq_refl n).

説明:

  • return式全体の型を含む型注釈を導入しmatch ... endます。
  • asこの型注釈で使用できる変数名を導入し、各分岐の左側で置き換えられます。ここ、
    • 最初のブランチでは、右側に type がn = S p -> natあります。
    • 2 番目のブランチでは、右側に type がありn = O -> natます。したがって、q HeqタイプFalseがあり、一致する可能性があります。

詳細については、リファレンス マニュアルの拡張パターン マッチングの章を参照してください。

于 2012-12-29T21:24:20.257 に答える