idrisにマップID = IDを証明しますか？

Question

私はちょうどidrisと定理を証明して遊んでいます。私はインターネット上の基本的な事実の証拠の例のほとんどを追うことができるので、私は自分自身で何かを試してみたかったのです。だから、私は、マップの次の基本的な性質のための証拠用語を書きたい：

map : (a -> b) -> List a -> List b 
prf : map id = id 

直感的に、私は証拠がどのように動作するかを想像することができます：任意のリストlを取り、地図のidリットルの可能性を分析します。 lが空のときは明らかです。 が空でない場合は、関数アプリケーションが等価を保持するという概念に基づいています。

prf' : (l : List a) -> map id l = id l 

それは、すべての文のようなものだ： だから、私はこのような何かを行うことができます。関係する関数の平等を証明するにはどうしたらいいですか？

Answer 1

できません。 Idrisのタイプ理論（CoqやAgdaなど）は、一般的な拡張性をサポートしていません。 2つの関数fとgが同じ動作をすると、Not (f = g)を証明することはできませんが、fとgがアルファとη等価に等しいと定義されている場合にのみ、f = gを証明することができます。残念なことに、高次関数を考えると、状況は悪化するだけです。そのようなことについてCoqの標準ライブラリには定理がありますが、私はそれを今見つけたり覚えているようには見えません。