【Lean4】aesop

aesop

論理的な証明を自動探索する

example (P Q : Prop)
    (hP : P)
    (hQ : Q) :
    P ∧ Q := by
  aesop

example (P Q : Prop)
    (hP : P)
    (hQ : Q) :
    P ∧ Q := by
  aesop

Lean4の関連記事

• 【Lean4】namespace
• 【Lean4】section
• 【Lean4】variable
• 【Lean4】abbrev
• 【Lean4】constructor
• 【Lean4】#check
• 【Lean4】def
• 【Lean4】exact
• 【Lean4】rfl
• 【Lean4】intro
• 【Lean4】apply
• 【Lean4】unfold
• 【Lean4】rw
• 【Lean4】simp
• 【Lean4】simpa
• 【Lean4】constructor
• 【Lean4】left,right
• 【Lean4】cases
• 【Lean4】rcases
• 【Lean4】refine
• 【Lean4】use
• 【Lean4】have
• 【Lean4】show
• 【Lean4】change
• 【Lean4】subst
• 【Lean4】by_cases
• 【Lean4】induction
• 【Lean4】ext
• 【Lean4】funext
• 【Lean4】congrArg
• 【Lean4】norm_num
• 【Lean4】ring
• 【Lean4】linarith
• 【Lean4】aesop
• 【Lean4】structure
• 【Lean4】where
• 【Lean4】@[simp]
• 【Lean4】 #eval
• 【Lean4】let
• 【Lean4】if（条件分岐）
• 【Lean4】match（パターンマッチ）
• 【Lean4】リスト
• 【Lean4】Option
• 【Lean4】inductive