3

依存型を持つプログラミング言語として coq を使用しようとしています。次の小さなプログラムを作成しました。

Inductive Good : list nat -> Set := 
  | GoodNonEmpty : forall h t, Good (h :: t).

Definition get_first(l : list nat)(good : Good l) : nat := 
  match l with
    | h :: t => h
    | nil => 
      match good with 
      end
  end.

空でないリストの型を定義し、空でないという証拠があれば、そのようなリストの最初の要素を取得する関数を作成します。先頭項目が 2 つの項目からなる場合はうまく処理できますが、空リストの不可能な場合は処理できません。coqでこれを行うにはどうすればよいですか?

4

1 に答える 1

6

あなたの試みよりも簡単な方法の1つは次のとおりです。

Definition get_first (l : list nat) (good : Good l) : nat :=
  match good with
  | GoodNonEmpty h _ => h
  end.

これがあなたがやりたかった方法でそれを行う方法です。「Good nil」がインラインで存在しないことを証明するのは非常に冗長であることに気付くでしょう。

Definition get_first (l : list nat) (good : Good l) : nat :=
  (
    match l as l' return (Good l' -> nat) with
    | nil =>
      fun (goodnil : Good nil) =>
        (
          match goodnil in (Good l'') return (nil = l'' -> nat) with
          | GoodNonEmpty h t =>
            fun H => False_rect _ (nil_cons H)
          end
        )
        (@eq_refl _ nil)
    | h :: _ => fun _ => h
    end
  ) good.

その一部を外部で定義して再利用できます。ただし、ベストプラクティスについては知りません。多分誰かが同じことをするためのより短い方法で来ることができます.

編集：

ちなみに、プルーフ モードでは、はるかに簡単な方法でほぼ同じ結果を得ることができます。

Definition get_first' (l : list nat) (good : Good l) : nat.
Proof.
  destruct l. inversion good. exact n.
Defined.

その後、次のことができます。

Print get_first'.

Coq がそれをどのように定義しているかを確認します。ただし、より複雑なことについては、解決策として提案された #coq IRC チャネルの gdsfhl に従う方がよい場合があります。

http://paste.in.ua/4782/

彼がこの戦術を使用して、refine書く用語の骨組みの一部を提供し、不足している証明を延期していることがわかります。

于 2012-09-22T18:48:35.163 に答える