Coq/Proof GeneralのAgdaのようなプログラミングですか？

Question

Agdaとは異なり、Coqは証明と機能を分離する傾向があります。 Coqが提供する戦術は、校正を書くのに最適ですが、Agdaモードの機能を再現する方法があるかどうかは疑問です。

具体的には、私がしたい：

• Agdaの?やHaskellの_の一部と同等に、私はそれを書いている間、機能の一部を省略し、（たぶん）コックは私伝える持つことができる場所タイプ私はあなたが機能して?ブロックを埋めるAgdaモード（具体化）、中
• がCcとクロムと同等のものを置く必要がある、と私はやっているとき、それは必要な引数
• のための新しい?ブロックを行います関数内にmatchがあり、Coqが自動的に書き込む（AgdaモードのC-c C-aのような）可能なブランチを展開してください。

これはCoqIdeまたはProof Generalで可能ですか？

Answer 1

コメントにejgallegoが示唆したように、（ほとんど）それを行うことができます。 company-coqツールがあり、これはProofGeneralの上で動作します。

map機能がcompany-coqとrefineの手法を使用してどのように実装できるかを説明しましょう。括弧内にカーソルを置き、CcとのCa RETリストRETを入力し、refine().に

Fixpoint map {A B} (f : A -> B) (xs : list A) : list B. 

タイプで開始 - それは手動で埋める穴を持つリストのmatch表現を挿入（のリストに記入しましょう名前とベースケース）。

Fixpoint map {A B} (f : A -> B) (xs : list A) : list B. 
    refine (match xs with 
      | nil => nil 
      | cons x x0 => cons _ _ 
      end). 

我々はtlへx0の名前を変更し、それを終えると、再帰的なケースexact (map A B f tl).提供するために：便利なキーボードショートカットに現在のゴールを抽出するのに役立ちますCcのカルシウムCxのもあり

Fixpoint map {A B} (f : A -> B) (xs : list A) : list B. 
    refine (match xs with 
      | nil => nil 
      | cons x tl => cons _ _ 
      end). 
    exact (f x). 
    exact (map A B f tl). 
Defined. 

を別の補助定/ヘルパー関数。

Answer 2

私はあなたに1つの変なトリックを教えさせてください。あなたの懸念に対する答えではないかもしれませんが、少なくとも概念的には助けになるかもしれません。

はあなたが戦術で追加を書いてみることができますが、この問題が発生した後者が

Inductive nat : Set := 
    | zero : nat 
    | suc : nat -> nat. 

によって与えられている、のが自然数の加算を実装してみましょう。

Theorem plus' : nat -> nat -> nat. 
Proof. 
    induction 1. 

plus' < 2 subgoals 

    ============================ 
    nat -> nat 

subgoal 2 is: 
nat -> nat 

あなたは何をしているのかわかりません。

このトリックは、自分が行っていることをより詳しく見ることです。私たちは、gratuitously依存型を導入することができます。クローン化nat。

Inductive PLUS (x y : nat) : Set := 
    | defPLUS : nat -> PLUS x y. 

アイデアはPLUS x yは「plus x yを計算する方法」の一種であるということです。そのような計算の結果を抽出できるように、投影が必要です。

Theorem usePLUS : forall x y, PLUS x y -> nat. 
Proof. 
    induction 1. 
    exact n. 
Defined. 

これで、私たちは証明することで準備が整いました。

Theorem mkPLUS : forall x y, PLUS x y. 
Proof. 

mkPLUS < 1 subgoal 

    ============================ 
    forall x y : nat, PLUS x y 

最終的な結論は、私たちの現在の左側と文脈を示しています。 AgdaでC-c C-cのアナログは...

induction x. 

mkPLUS < 2 subgoals 

    ============================ 
    forall y : nat, PLUS zero y 

subgoal 2 is: 
forall y : nat, PLUS (suc x) y 

であり、あなたはそれがケース分割を行っている見ることができます！ベースケースをノックアウトしましょう。

intros y. 
     exact (defPLUS zero y y). 

PLUSのコンストラクタを呼び出すことは、方程式を書くことに似ています。第3引数の前に=の符号があるとします。ステップの場合、再帰呼び出しを行う必要があります。

intros y. 
     eapply (fun h => (defPLUS (suc x) y (suc (usePLUS x y h)))). 

再帰呼び出しを行うために、我々はそれを計算する方法を、実際の説明である第三引数、オーバー我々は抽象ここxとy、私たちが望むの引数でusePLUSを呼び出しますが、。私たちには、そのサブゴールだけが残されています。誘導仮説は再帰呼び出しをカバーすることを確認し

 auto. 

mkPLUS < 1 subgoal 

    x : nat 
    IHx : forall y : nat, PLUS x y 
    y : nat 
    ============================ 
    PLUS x y 

そして今、かなりコックのguardednessチェックを使用するよりも、あなたが使用して... ...。 We're

私たちにはワーカーがいますが、ラッパーが必要です。

Theorem plus : nat -> nat -> nat. 
Proof. 
    intros x y. 
    exact (usePLUS x y (mkPLUS x y)). 
Defined. 

これで準備は整いました。あなた

Eval compute in (plus (suc (suc zero)) (suc (suc zero))). 

Coq <  = suc (suc (suc (suc zero))) 
    : nat 

はインタラクティブ構築ツールがあります。 ゲームは、タイプをより有益なものにすることで、あなたが解決している問題の適切な詳細を表示するためにゲームをプレイします。生成された証明スクリプト...

Theorem mkPLUS : forall x y, PLUS x y. 
Proof. 
    induction x. 
    intros y. 
     exact    (defPLUS zero y y). 
    intros y. 
     eapply (fun h => (defPLUS (suc x) y (suc (usePLUS x y h)))). 
     auto. 
Defined. 

...は構成するプログラムについては明示的です。追加が定義されていることがわかります。

あなたは、あなたが構築しているプログラムを示すインターフェイスと重要な問題-簡素化戦術を上の層、その後、プログラム構築のために、この設定を自動化した場合、あなたはあなたができる警句1