問題タブ [agda]

次の例を知っている人はいますか？

1. 証明アシスタント ( Coqなど) における正規表現(後方参照で拡張される可能性があります)に関する証明の開発。
2. 正規表現に関する従属型言語 ( Agdaなど) のプログラム。

は、私が解決してサポートしようとしている公理です。(コア ライブラリの) cong を使用してみましたが、cong コンストラクターに問題があります。

cong の場合、等値と型の refl を指定する必要があることはわかっていますが、どの型を指定すればよいかわかりません。アイデア？

これは大学での小さな課題のためなので、実際の回答を書くよりも、私が見逃していたことを誰かに示してもらいたいのですが、ある程度のサポートをお願いします.

Haskell で書いたプログラムに基づいて、いくつかの表示セマンティクスを Agda にエンコードしようとしています。

Agda では、直訳すると次のようになります。

しかし、FunVal に関連するエラーが発生します。

Value は、Value の定義のコンストラクター FunVal の型の矢印の左側にあるため、厳密には正ではありません。

これは何を意味するのでしょうか？これを Agda でエンコードできますか? 私はそれについて間違った方法で進んでいますか？

ありがとう。

私は Agda で単純な補題を証明しようとしていますが、これは正しいと思います。

ベクトルに 2 つ以上の要素がある場合、head次の要素を取得することは、すぐにinit取得することと同じです。head

以下のように定式化しました。

それは私に与えます。

応答として。

(init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs))コンポーネントの読み方がよくわかりません。私の質問は次のとおりだと思います。それは可能ですか、その用語はどのように、そして何を意味しますか。

どうもありがとう。

Agdaメーリングリストで、ConorMcBrideは次のように質問しました。

推定のような操作を手に入れる方法はありますか

何も与えられていない場合、これは実際には（ミルナーの意味で）Just and Goes Wrongをチェックしませんか？

Agdaは多分a==Just1 aを証明するかもしれません、そして合計型の中間コンストラクターは排除されるかもしれません。

unsafeCoerce＃またはunpackClosure＃を使用したアプローチを考えることができますが、他の誰かが考えていますか？

ただし、このsegfaults（単一のコンストラクタータイプは、クロージャーのオーバーヘッドの一部を回避できます）。コアは大丈夫​​に見えます：

私はアグダに不慣れです。AnaBoveとPeterDybjerによる「DependentTypesatWork」という論文を読んでいます。有限集合の説明（私のコピーの15ページ）がわかりません。

このペーパーでは、Finタイプを定義しています。

明らかな何かが欠けているに違いありません。この定義がどのように機能するのかわかりません。誰かがの定義Finを日常の英語に簡単に翻訳できますか？論文のこの部分を理解するために必要なのはそれだけかもしれません。

私の質問を読むために時間を割いてくれてありがとう。それは有り難いです。

構造帰納法を使用して定義された関数を Agda の終了チェッカーで受け入れることができません。

この問題を示す最も単純な例として、次の例を作成しました。次の の定義sizeは拒否されますが、厳密に小さいコンポーネントで常に再帰します。

この問題の一般的な解決策はありますか? Recursorデータ型に対してを作成する必要がありますか? はいの場合、どうすればよいですか？Recursor（ forを定義する方法の例があれば、List Aそれで十分なヒントが得られると思いますか？）

[0, ..., n-1]mod-nカウンターを、間隔を2つの部分に分割したものとして表現しようとしています。

これを使用すると、2つの重要な操作を定義するのは簡単です（簡潔にするためにいくつかの証明は省略されています）。

+1問題は、それ-1が逆であることを証明しようとするときに発生します。subst導入されたこれらのエリミネーターが必要な状況に遭遇し続けます。

しかし、これは（ある程度）論点先取であることが判明しました：それはタイプチェッカーによって受け入れられません、なぜならsubst B x=x' y : B x'そしてy : B x...