Lean #03 - 2025/09/21

https://lambda-kansai.connpass.com/event/369415/

第3章 Lean における論理

命題 proposition

Lean では Prop 型

述語 predicate

True False は Prop 型

kakkun61.icon Bool じゃないんだ

true, false はBoolですねebi_chan.icon

kakkun61.icon ほ～

仮定 hypothesis

含意 implication

apply タクティク

intro タクティク

code:lean

¬ P ≡ P → False

contradiction タクティク

exfalso タクティク

Metaprogramming in Lean

constructor タクティク

これ ↓

code:LeanBook/Logic/PropLogic.lean

example (P Q : Prop) (h1 : P → Q) (h2 : Q → P) : P ↔ Q := by

constructor

· exact h1

· exact h2

は、こう ↓ でもいい

code:lean

example (P Q : Prop) (h1 : P → Q) (h2 : Q → P) : P ↔ Q := by

constructor

apply h1

apply h2

<;> タクティク結合子

rw タクティク

left right タクティク

cases タクティク

inl は left injection らしい

ebi_chan.iconマジか。全然違うこと言っちゃった

nagarath.icon圏論の用語（として僕は知っているのですが）でどの「和」にも使います。

code:Init/Prelude.lean

/--

Or a b, or a ∨ b, is the disjunction of propositions. There are two

constructors for Or, called Or.inl : a → a ∨ b and Or.inr : b → a ∨ b,

and you can use match or cases to destruct an Or assumption into the

two cases.

inductive Or (a b : Prop) : Prop where

/-- Or.inl is "left injection" into an Or. If h : a then Or.inl h : a ∨ b. -/

| inl (h : a) : Or a b

/-- Or.inr is "right injection" into an Or. If h : b then Or.inr h : a ∨ b. -/

| inr (h : b) : Or a b

suffices タクティク

「サファイセズ」：（英）充分である

コード 3.34 と 3.35 について補足

guard_hyp や guard_target は他の言語での assertion (表明) に近い。

このコードがなくても Lean プログラムとしては機能する。

次回 Lean #04