問題タブ [lean]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
131 問題
0
投票する
1
に答える
486
参照
theorem-proving - リーンで帰納法によって証明を単純化する方法は?
リーンの帰納法による証明を簡単にしたいと思います。
リーンで 3 つのコンストラクターを持つ誘導型を定義し、この型のバイナリ関係を定義しました。Lean では公理を rel のコンストラクタとして使用できないため、公理を含めました。
目標は、次の定理を証明することでした。
x、y、z の帰納法によって証明しました。「z」は、上記の pw_o_2 の定義に由来します。しかし、証明は非常に長い (~136 行)。より短い証明を持つ別の方法はありますか？
0
投票する
1
に答える
146
参照
0
投票する
1
に答える
78
参照
agda - Agda はどのようにして `Vec.foldl` への暗黙の引数を推測していますか?
上記の関数をリーンに翻訳すると、その本当の形が実際には...
fAgda が暗黙の引数を正しく推論できることは本当に印象的です。それはどのようにやっているのですか？