sorry
証明の細部を埋める前にコンパイルが通るようにしたいとき、証明で埋めるべき箇所に sorry
と書くとコンパイルが通るようになります。ただし、sorry
を使用しているという旨の警告が出ます。
-- Fermat の最終定理
def FermatLastTheorem :=
∀ x y z n : Nat, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n
/- warning: declaration uses 'sorry' -/
theorem flt : FermatLastTheorem :=
sorry
補足: sorry 使用の痕跡は隠すことができる
基本的に、sorry
タクティクを使用すれば sorryAx
という公理が使用されて、#print axioms
コマンドの出力に現れるようになります。
/- info: 'flt' depends on axioms: [sorryAx] -/
#print axioms flt
しかし、[csimp]
属性を経由することで sorryAx
を隠し、Lean.ofReduceBool
の背後に隠してしまうことができます。
def one := 1
def two := 2
@[csimp] theorem one_eq_two : one = two := by
sorry
theorem false_theorem : 1 = 2 := by
rw [show 1 = one from rfl]
native_decide
/- info: 'false_theorem' depends on axioms: [Lean.ofReduceBool] -/
#print axioms false_theorem