proof_wanted
proof_wanted
はその名の通り、証明を公募するためのコマンドです。
sorry
とよく似た機能を持つコマンドです。構文的には theorem
に似ていますが、証明を書く必要がありません。証明を書かないで済むのは sorry
と同様ですが、proof_wanted
で証明された定理は後で参照することができないという違いがあります。
import Batteries.Util.ProofWanted
variable (n : Nat)
-- proof_wanted で証明を省略できる
proof_wanted result : n + 0 = n
-- sorry で同様のことができる
theorem another_result : n + 0 = n := by sorry
-- sorry で証明した定理は参照できるが
#check another_result
-- proof_wanted で宣言した定理は参照できない
#check_failure result