問題タブ [coq]

暗黙のパラメータに関して、Coq のある種の一貫性のない動作を見つけました。

Let定義は暗黙的でid1はないようですが、を置き換えてもエラーは発生しません。何か間違っているのでしょうか、それともバグですか?tLetDefinition

これは、問題の動作をキャプチャする、より大きな証明の簡略化されたスニペットです。

coq で置き換えるrewrite prop2と、不可解なエラーで失敗します。ただし、私の意見では、書き換えステップの後にrewrite propcoq は譲歩する必要があります。forall e : t, True誰でもこれで私を助けることができますか？

編集:私はおそらく、現在ここで問題をどのように回避しているかを言うべきです。順列の等価性を示すための原則を定義し、

次に、以下で私に問題を引き起こしている証明コンテキストで補題を適用し、イータ等価項が等しいことを示しています。したがって、用語がレコード内にネストされている場合、問題は eta-equivalence を示しているようです。でも私はレコードを扱うのが苦手なので、何かが欠けているかもしれません。

オリジナル：

レコード フィールドにネストされた eta に相当する用語の等価性を証明するのに問題があります。参考までに、eta-reduction は再帰性によって独立して証明できます。

私の現在の証明コンテキストでは、2 つのレコードがあり、それらの等価性を証明する必要があります。完全に破壊され展開されると、証明コンテキストと現在のサブゴールは次のようになります。

確立されなければならない平等は、

これらの等式は再帰性によって確立できるため、何が問題なのかわかりません。ただし、置換しようとすると適切なサブゴールが生成されますが、レコード内の用語は置換されないため、何かがλ x : U, perm0 xおかしいperm0と思われます。さらに、eqa_reduction を使用して書き直すと、抽象化に関するエラーが発生し、不適切な型の項やネストされた従属引数が発生します。

コンテキストを可能な限り単純化して、以下に貼り付けました。文体の問題と、私がまだ初心者であるという事実を除けば、現在の開発に問題は見られません。

最後に、Coq で私を助けてくれて辛抱強く待ってくれた皆さんに感謝します。

私はCoqを初めて使用し、破壊戦術について簡単な質問があります。count自然数のリスト内の特定の自然数の出現回数をカウントする関数があるとします。

次の定理を証明したいと思います。

n = 0の類似の定理を証明している場合、yを0またはSy'に単純に破棄できます。一般的なケースでは、私がやりたいのは（beq_nat ny）をtrueまたはfalseに破棄することですが、それを機能させることができないようです。Coq構文の一部が欠落しています。

何か案は？

証明のコンテキストで仮説を再帰的に反転するための戦術を定義するのに問題があります。たとえば、次のような仮説を含む証明コンテキストがあるとします。

仮説を繰り返し反転して、仮説を含む証明コンテキストを取得したい

もちろん、この証明コンテキストを取得するのは、反転戦術を繰り返し適用することで簡単です。ただし、仮説を反転すると、異なる仮説が異なるサブゴールに入れられることがあり、それぞれを反転するかどうかは、反転によって提供される情報の性質によって異なります。

明らかな問題は、証明コンテキストに対する無差別なパターンマッチングが非終了を引き起こすことです。たとえば、元の仮説を反転した後も保持したい場合、以下は機能しません。

これを行う簡単な方法はありますか？明らかな解決策は、すでに反転した仮説のスタックを保持することです。もう1つの解決策は、特定の深さまで仮説を反転することです。これにより、Ltacでの再帰呼び出しが削除されます。

コンテキスト: 私はSoftware Foundationsの演習に取り組んでいます。

最後の行の前に、私のサブゴールは次のとおりです。

そして、私はそれを次のように変換したいと思います:

ただし、ステップスルーしようとするとrewrite -> neg_move、次のエラーが発生します。

エラー: 変数 y のインスタンスが見つかりません。

これは本当に簡単だと思いますが、何が間違っているのでしょうか? evenb_n__oddb_Sn（私が完全に間違っている場合を除き、解決のために何も与えないでください）。

ラフで未熟な背景として、HoTTでは、帰納的に定義された型から一体を推測します

これにより、非常に一般的な構造が可能になります

これLemma transport は、HoTT の「置換」または「書き換え」戦術の中心になります。私が理解している限り、トリックは、あなたまたは私が抽象的に認識できる目標を想定することです.

必要な依存型 G が何であるかを把握するため、できるようになりますapply (transport G H)。これまでのところ、私が理解したのはそれだけです

十分に一般的ではありません。つまり、最初のidtacものはかなり頻繁に使用されます。

質問は

[ありますか | 正しいことは何ですか？

このタイプを減らすためのトリックはありますか？そこに冗長性xがあります。

モナドは型クラスです：(Set -> Set) -> Type

以下について質問があります Record。Definition

私はこの定義を持っています：

そのためのブール関数を書きます。

どこbeq_term : term -> term -> bool.

beq_ruleしたがって、実際に返す正確なタイプの定義は、beq_termここで必要なものではありません。タイプを返したい： rule -> rule -> bool.

そこで、ルールの定義を次のように変更しましたRecord。

と

私の質問は次のとおりです。

rule1) 最初に定義したusedDefinitionと別の usedの違いは何Recordですか?

2) ルールを定義したい場合Definition、エイリアスlhsとrhs好きなものをRecord定義できますか?