問題タブ [coq-tactic]

私には目標があります

、しかし、「クワッド」の定義を覚えていないので、その定義の検索を開始したくありません。

quad をその定義にすばやく置き換えることができる戦術はありますか?

または、覚えて使用する必要があります

?

Coq 書き換えタクティクス モジュロ結合性と可換性をテストしていました ( aac_tactics)。次の例は整数 ( Z) に対して機能しますが、整数を有理数 ( ) に置き換えるとエラーが発生しますQ。

などで置き換えるRequire Import ZArith.とRequire Import QArith.、エラーが発生します。

エラー: 戦術の失敗: AC を法とする一致するオカレンスが見つかりません。

でaac_rewrite H.

との間に同様の不一致の問題がZあり、 /スコープが開いQているかどうかに関連していることが判明しました。ZQ

しかし、ここで aac の書き換えが機能しなかった理由がわかりません。Z不一致の原因は何ですか? また、とで同じように動作させるにはどうすればよいQですか?

等価とローカル定義の違いがよくわかりません。たとえば、set戦術に関するドキュメントを読む場合:

用語を ident として覚える

これは set ( ident := term ) in * として動作し 、ローカル定義の代わりに論理 (ライプニッツの) 等価性を使用します

それはそう、

1. set (ca := c + a) in *.たとえばca := c + a : Z、コンテキストで生成されますが、

2. remember (c + a ) as ca.コンテキストで生成さHeqca : ca = c + aれます。

ケース 2. の場合、生成された仮説を のようrewrite Heqca.に使用できますが、ケース 1. の場合、 を使用できませんrewrite ca。

ケース 1. の目的は何ですか? また、実際の使用に関してケース 2. とどのように違いますか?

また、2 つの違いが基本的なものである場合、ドキュメント (8.5p1) で のrememberバリアントとして説明されているのはなぜですか?set

Coq リファレンス マニュアル (8.5p1) から、私の印象はrevertの逆ですが、ある程度introはそうです。generalizeたとえば、revert以下generalize dependentは同じようです。

generalizeより強力なのはそれだけですかrevert？

また、ドキュメントは次のことを説明するのに少し循環的ですgeneralize:

この戦術は、あらゆる目標に適用されます。ある用語に関して結論を​​一般化します。

generalizeラムダ計算の抽象化演算子に似ていますか?

Coq リファレンス マニュアル (8.5p1) を読んでいます。

戦術のローカル適用

次の形式を使用して、さまざまな目標にさまざまな戦術を適用できます。

[ > expr1 | ::: | 式]

exprii = 0の場合、式は vi に評価されます。...; n そしてすべてが戦術でなければなりません。= 1 の場合、vi は i 番目のゴールに適用されます。...; n. フォーカスされたゴールの数が正確に n でない場合、失敗します。

idtacそこで、次のように、それぞれに2 つの些細な戦術を適用しようとする 2 つの目標を使用して、簡単なテストを行いました。

ただし、予想される戦術は 1 つだけであるというエラーが表示されました。

エラー: ゴール数が正しくありません (予想される 1 つの戦術)。

よくわかりません。誰かが私が間違ったことを説明できますか?正しい使用法は何ですか?

定義を展開して、Fixpoint定義の本体を取得しようとしていました。しかし、Coq は定義の本体を文字どおりには提供しません。(fix ...)代わりに、それは私が利用できない で始まる何かを私に与えています。

たとえば、Coq.Init.Wfから以下を証明する場合

状態は次のとおりです。

さて、Fix_FRHS では、LHS とまったく同じように定義されました。

私はそれを平等にしようとしましtrivialた:

それでも、(fix Fix_F ... )RHS のようなものが得られたので、これ以上先に進むことはできません。

質問は：

上記Fixpointを関数本体に展開する方法はありますか?

注: この例を証明するための回避策があることは知っています。

しかし、それが有効であれば、私はunfold-ing アプローチにもっと興味があります。

Coqで任意の帰納命題定義が与えられた場合、帰納命題で帰納戦術を呼び出すときに使用する合理的なdisj_conj_intro_patternを導出するための一般式はありますか?

一般に、帰納的定義のコンストラクターのいずれかの完全な intro_pattern には、複数の仮説および複数の帰納的仮説 (の名前) が必要な場合があります。この場合、パターンで提供される名前の順序には、すべてのパラメーターが含まれる場合があります。 1 つの仮説と対応する帰納的仮説、その後に仮説と帰納的仮説からなる 1 つまたは複数の追加のペアが続きます。たとえば、Software Foundations には次のものが含まれます。

この例では、MApp と MStarApp の intro_patterns にはそれぞれ、仮説と帰納的仮説の 2 つのペアがあります。おそらく、これら 2 つのコンストラクターにはそれぞれ次の形式の式が含まれているためです。

x -> y -> z

これについては、現在のリファレンス マニュアルには次のようにしか書かれていません。

disj_conj_intro_pattern としての帰納項

これは誘導項として動作しますが、disj_conj_intro_pattern の名前を使用して、コンテキストで導入された変数に名前を付けます。disj_conj_intro_pattern は通常、[ p11 … p1n1 | ] の形式でなければなりません。… | pm1 … pmnm ] ここで、m は項の型のコンストラクタの数です。i 番目のゴールのコンテキストで誘導によって導入された各変数は、リスト pi1 … pini から順番に名前を取得します。十分な名前がない場合、誘導は導入する残りの変数の名前を発明します。より一般的には、pij は任意の選言的/連言的導入パターンにすることができます (セクション 8.3.2 を参照)。たとえば、コンストラクターが 1 つの帰納型の場合、[ p1 … pn ] の代わりにパターン表記 (p1 , … , pn) を使用できます。

これは、所与の帰納的定義の完全な disj_conj_intro_pattern の正しい形式を決定する方法を指定していないようです。

1) 各コンストラクターの正式なパラメーターが最初に来て、対応する帰納的仮説とペアになったコンストラクターの仮説が続くという私の上記の経験的観察です。2) 仮説と帰納的仮説のペアの数は、コンストラクター内の仮説の数、問題の合計から得られますか? それともそれ以上のものがありますか？

リファレンスマニュアルの戦術の章と、第1章のガリーナ文法のパターンに関する非常に一般的な議論以外に、これに関する他の関連文書はありますか?