Lean4での論理記号の取り扱いの勉強も後半です。今回は論理積と論理和の扱いを見ていきます。この辺はあまり難しい話は出てきません。
ゴールが論理積A ∧ Bの形の場合にはconstructorタクティクを使うとAとBが両方ともゴールとなり両方証明するとA ∧ Bの証明が終わります。
仮定にh:A ∧ Bがある場合には仮定としてAとBが成り立つのですからバラしてそれぞれを仮定としたいですよね。仮定にh1:Aとh2:Bを入れるにはrcases h with <h1,h2>とかhave <h1,h2>:=hなどとすれば良いです。
ゴールが論理和A∨ Bの形の場合にはAかBのどちらかを証明できれば良いです。証明したい方の命題をleftタクティク、rightタクティクで選ぶとゴールが選んだ方に変化します。この場合Aを証明したいのならleftタクティクを使えば良いです。ゴールがAになるのでAを証明すれば終わります。
仮定にh:A ∨ Bがある場合には現在のゴールを、Aが成り立つ場合とBが成り立つ場合の両方について証明する必要があります。rcases h with h1 | h2 とすると仮定がh1:Aだけを含む場合とh2:Bだけを含む場合に分かれます。どちらのゴールも元と同じで変化しません。
これらを使った簡単な例題を見て見ましょう。
example : A ∧ B → A ∨ B := by
intro h -- h: A ∧ B, ⊢ A ∨ B
have ⟨h1,_⟩ := h -- h1: A
left -- ⊢ A
assumption -- No goals
--の後ろはコメントです。そこにタクティクを実行した後の仮定とゴールの変化を追記して見ました。例えば最初のintro hで仮定にh: A ∧ Bが加わりゴールが ⊢ A ∨ Bに変化したことが分かります。次のhaveで仮定の論理積を分解してそれぞれを仮定に追加しています。ただし右側は使わない予定で _ としています。次にleftでゴールの左側を新たなゴールとして選択します。最後にassumptionタクティクを使ってゴールのAがすでに仮定の中にh1:Aとして入っていることを確認して証明が終了します。
