Leanの推論規則

Lean

\require{color} \newcommand{\hyp}{\mbox{-}}% \newcommand{\To}{\Rightarrow}% \newcommand{\F}[1]{ \langle\![{#1}]\!\rangle }% \newcommand{\As}{\;::\;}%
連言

  • and.left : ?M_1 ∧ ?M_2 → ?M_1 （A∧B ⇒ A）
  • and.right : ?M_1 ∧ ?M_2 → ?M_2 （A∧B ⇒ B)
  • and.intro : ?M_1 → ?M_2 → ?M_1 ∧ ?M_2 （A B ⇒ A∧B）

含意

  • 空白〈right-eval〉 : ((?M_1 → ?M_2) → ?M1) → ?M_2 (（A → B) A ⇒ B）
  • assume 変数 : 型, 式 ≡ λ 変数 : 型, 式
assume h : A ∧ ¬ B,
and.intro (and.right h) (and.left h)

{}^\cap(copy;(\F{and.right} \otimes \F{and.left}) ; \F{and.intro})\\ \xymatrix { {} &{\# 1 \;\lambda\, h} \ar[d]^{A\land \lnot B} &{} \\ {} &*{\bullet} \ar[dl] \ar[dr] &{} \\ {\bar{\urcorner} } \ar[d]_-{\lnot B} &{} &{\bar{\ulcorner} } \ar[d]^-{A} \\ {}\ar[dr]_-{\lnot B} &{} &{}\ar[dl]^-{A} \\ {} &*{\blacktriangledown} \ar[d]^-{\lnot B \land A} &{} \\ {\#1} &*+[o][F]{\to} \ar[l] \ar[d]^-{A\land \lnot B \,\to\, \lnot B \land A} &{} \\ {} & & }

選言

  • or.inl : ?M_1 → ?M_1 ∨ ?M_2 （A ⇒ A∨B）
  • or.inr : ?M_2 → ?M_1 ∨ ?M_2 （B ⇒ A∨B）
  • or.elim : ?M_1 ∨ ?M_2 → (?M_1 → ?M_3) → (?M_2 → ?M_3) → ?M_3 （A∨B A→C B→C ⇒ C）
section
  variable h : A ∨ B
  variables (ha : A → C) (hb : B → C)
  example : C :=
  or.elim h
    (assume h1 : A,
      show C, from ha h1)
    (assume h1 : B,
      show C, from hb h1)
end

否定（矛盾）

  • true, false : Prop
  • false.elim : false → ?M_1 （⊥ → A）
  • trivial : true
  • by_contradiction : (¬?M_1 → false) → ?M_1 （¬¬A → A）