証明図から証明項に引き写すのは手作業。支援系とかいいながら、ソフトウェアは何も支援してくれない。
/-! example_1.lean -/
namespace Imp
def elim_right {A B: Prop} (f:A → B) (a:A) : B :=
f a
def elim_left {A B: Prop} (a:A) (f:A → B) : B :=
f a
end Imp
variable (A B C D: Prop)
def example_1 (p1: A) (p2: A→B) (p3: B→C) : C∧(A∨D) :=
/-(1)-/ have a: A := p1
/-(2)-/ have a_imp_b := p2
/-(3)-/ have b: B := Imp.elim_left a a_imp_b
/-(4)-/ have c_imp_b := p3
/-(5)-/ have c: C := Imp.elim_right c_imp_b b
/-(6) = (1) -/ -- 重複記述はできない
/-(7)-/ have a_or_d: A∨D := Or.intro_left D a
/-(8)-/ show C∧(A∨D) from And.intro c a_or_d
#check example_1
def example_1' (p1: A) (p2: A→B) (p3: B→C) : C∧(A∨D) :=
/-(1)-/ have b: B := p2 p1
/-(2)-/ have c: C := p3 b
/-(3)-/ have a_or_d: A∨D := Or.intro_left D p1
/-(4)-/ show C∧(A∨D) from And.intro c a_or_d
#check example_1'
