問題タブ [coq-tactic]

rewriteltac で呼び出して 1 つのオカレンスのみを書き換えるにはどうすればよいですか? coqのドキュメントに何か言及されていると思いますrewrite atが、実際に実際に使用できておらず、例もありません。

これは私がやろうとしていることの例です:

私は Coq と一緒に、私が定義した 2 つの型の間の関係を調べています。1 つ目は の有限部分集合のようなものでnat、要素は 3 つだけです。

2 つ目は、要素が命題を満たすシグマ型{x: nat | x < 3}です。その定義は次のとおりです。

この 2 つの型が同型であることを証明したいと思います。関係する 2 つの関数を次のように定義しました。

l_0_3、l_1_3、およびl_2_3は単なる公理です。

同型の最初の部分を定義することに成功しました

しかし、反対側を定義することはできません。これまでに行ったことは次のとおりです。

残りの定義についてはまったくわかりません。xonと onのパターンマッチも試みました(N3_to_lt3 (lt3_to_N3 x))が、何を返すかわかりません。

助けてくれてありがとう。

項に空の置換を適用すると、指定された項と等しいことを証明しようとしています。コードは次のとおりです。

この関数のいくつかのプロパティを証明しようとしています。

私は再帰の後に立ち往生しています。私はタームでリストビルドの誘導をしたかったのですが、そうするとループに陥ってしまいます。私はどんな助けにも感謝します。