Proof automation based on the proof search on $\mathbf{LK}$

theorem LO.Meta.ClProver.Theorems.to_provable {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (φ : F) (h : Entailment.TwoSided 𝓢 [] [φ]) : 𝓢 ⊢ φ

theorem LO.Meta.ClProver.Theorems.rotate_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ : F) (hφ : Entailment.TwoSided 𝓢 Γ (Δ ++ [φ])) : Entailment.TwoSided 𝓢 Γ (φ :: Δ)

theorem LO.Meta.ClProver.Theorems.rotate_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ : F) (hφ : Entailment.TwoSided 𝓢 (Γ ++ [φ]) Δ) : Entailment.TwoSided 𝓢 (φ :: Γ) Δ

theorem LO.Meta.ClProver.Theorems.add_hyp {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (𝒯 : S) (s : 𝒯 ⪯ 𝓢) (Γ Δ : List F) (φ : F) (hφ : 𝒯 ⊢ φ) (h : Entailment.TwoSided 𝓢 (φ :: Γ) Δ) : Entailment.TwoSided 𝓢 Γ Δ

theorem LO.Meta.ClProver.Theorems.right_closed {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ : F) (h : φ ∈ Γ) : Entailment.TwoSided 𝓢 Γ (φ :: Δ)

theorem LO.Meta.ClProver.Theorems.left_closed {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ : F) (h : φ ∈ Δ) : Entailment.TwoSided 𝓢 (φ :: Γ) Δ

theorem LO.Meta.ClProver.Theorems.verum_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) : Entailment.TwoSided 𝓢 Γ (⊤ :: Δ)

theorem LO.Meta.ClProver.Theorems.falsum_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) : Entailment.TwoSided 𝓢 (⊥ :: Γ) Δ

theorem LO.Meta.ClProver.Theorems.falsum_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (h : Entailment.TwoSided 𝓢 Γ Δ) : Entailment.TwoSided 𝓢 Γ (⊥ :: Δ)

theorem LO.Meta.ClProver.Theorems.verum_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (h : Entailment.TwoSided 𝓢 Γ Δ) : Entailment.TwoSided 𝓢 (⊤ :: Γ) Δ

theorem LO.Meta.ClProver.Theorems.and_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ ψ : F) (hφ : Entailment.TwoSided 𝓢 Γ (Δ ++ [φ])) (hψ : Entailment.TwoSided 𝓢 Γ (Δ ++ [ψ])) : Entailment.TwoSided 𝓢 Γ (φ ⋏ ψ :: Δ)

theorem LO.Meta.ClProver.Theorems.or_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ ψ : F) (hφ : Entailment.TwoSided 𝓢 (Γ ++ [φ]) Δ) (hψ : Entailment.TwoSided 𝓢 (Γ ++ [ψ]) Δ) : Entailment.TwoSided 𝓢 (φ ⋎ ψ :: Γ) Δ

theorem LO.Meta.ClProver.Theorems.or_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ ψ : F) (h : Entailment.TwoSided 𝓢 Γ (Δ ++ [φ, ψ])) : Entailment.TwoSided 𝓢 Γ (φ ⋎ ψ :: Δ)

theorem LO.Meta.ClProver.Theorems.and_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ ψ : F) (h : Entailment.TwoSided 𝓢 (Γ ++ [φ, ψ]) Δ) : Entailment.TwoSided 𝓢 (φ ⋏ ψ :: Γ) Δ

theorem LO.Meta.ClProver.Theorems.neg_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ : F) (h : Entailment.TwoSided 𝓢 (Γ ++ [φ]) Δ) : Entailment.TwoSided 𝓢 Γ (∼φ :: Δ)

theorem LO.Meta.ClProver.Theorems.neg_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ : F) (h : Entailment.TwoSided 𝓢 Γ (Δ ++ [φ])) : Entailment.TwoSided 𝓢 (∼φ :: Γ) Δ

theorem LO.Meta.ClProver.Theorems.imply_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ ψ : F) (h : Entailment.TwoSided 𝓢 (Γ ++ [φ]) (Δ ++ [ψ])) : Entailment.TwoSided 𝓢 Γ ((φ 🡒 ψ) :: Δ)

theorem LO.Meta.ClProver.Theorems.imply_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ ψ : F) (hφ : Entailment.TwoSided 𝓢 Γ (Δ ++ [φ])) (hψ : Entailment.TwoSided 𝓢 (Γ ++ [ψ]) Δ) : Entailment.TwoSided 𝓢 ((φ 🡒 ψ) :: Γ) Δ

theorem LO.Meta.ClProver.Theorems.iff_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ ψ : F) (hr : Entailment.TwoSided 𝓢 (Γ ++ [φ]) (Δ ++ [ψ])) (hl : Entailment.TwoSided 𝓢 (Γ ++ [ψ]) (Δ ++ [φ])) : Entailment.TwoSided 𝓢 Γ ((φ 🡘 ψ) :: Δ)

theorem LO.Meta.ClProver.Theorems.iff_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ ψ : F) (hr : Entailment.TwoSided 𝓢 Γ (Δ ++ [φ, ψ])) (hl : Entailment.TwoSided 𝓢 (Γ ++ [φ, ψ]) Δ) : Entailment.TwoSided 𝓢 ((φ 🡘 ψ) :: Γ) Δ

def LO.Meta.ClProver.cl_prover : Lean.ParserDescr

Equations

• LO.Meta.ClProver.cl_prover = Lean.ParserDescr.node `LO.Meta.ClProver.cl_prover 1024 (Lean.ParserDescr.nonReservedSymbol "cl_prover" false)

structure LO.Meta.ClProver.Context : Type

• levelF : Lean.Level
• levelS : Lean.Level
• levelE : Lean.Level
• F : Q(Type udummy._uniq.39)
• LC : Q(LogicalConnective unknown_1)
• DC : Q(DecidableEq unknown_1)
• S : Q(Type udummy._uniq.45)
• E : Q(Entailment unknown_1 unknown_2)
• 𝓢 : Q(unknown_1)
• CL : Q(Entailment.Cl unknown_5)

@[reducible, inline]

abbrev LO.Meta.ClProver.M (α : Type) : Type

The monad for cl_prover contains.

Equations

• LO.Meta.ClProver.M = ReaderT LO.Meta.ClProver.Context Mathlib.Tactic.AtomM

def LO.Meta.ClProver.Context.app (c : Context) (n : Lean.Name) : Array Lean.Expr → Lean.Expr

Apply the function n : ∀ {F} [LogicalConnective F] [DecidableEq F] {S} [Entailment S F] {𝓢} [Entailment.Cl 𝓢], _ to the implicit parameters in the context, and the given list of arguments.

Equations

• c.app n = Lean.mkAppN ((((((((Lean.Expr.const n [c.levelF, c.levelS, c.levelE]).app c.F).app c.LC).app c.DC).app c.S).app c.E).app c.𝓢).app c.CL)

def LO.Meta.ClProver.iapp (n : Lean.Name) (xs : Array Lean.Expr) : M Lean.Expr

Equations

• LO.Meta.ClProver.iapp n xs = do let c ← read pure (c.app n xs)

def LO.Meta.ClProver.getGoalTwoSided (e : Q(Prop)) : Lean.MetaM ((c : Context) × List (have a := c.F; Q(«$a»)) × List (have a := c.F; Q(«$a»)))

def LO.Meta.ClProver.getGoalProvable (e : Q(Prop)) : Lean.MetaM ((c : Context) × have a := c.F; Q(«$a»))

@[reducible, inline]

abbrev LO.Meta.ClProver.Sequent : Type

Equations

• LO.Meta.ClProver.Sequent = List LO.Meta.Lit

def LO.Meta.ClProver.litToExpr (φ : Lit) : M Lean.Expr

Equations

• LO.Meta.ClProver.litToExpr φ = do let c ← read pure (LO.Meta.Litform.toExpr c.LC φ)

def LO.Meta.ClProver.exprToLit (e : Lean.Expr) : M Lit

Equations

• LO.Meta.ClProver.exprToLit e = do let c ← read liftM (LO.Meta.Litform.denote c.LC e)

def LO.Meta.ClProver.Sequent.toExprList (Γ : Sequent) : M (List Lean.Expr)

Equations

• Γ.toExprList = do let c ← read pure (List.map (LO.Meta.Litform.toExpr c.LC) Γ)

def LO.Meta.ClProver.exprListToLitList (l : List Lean.Expr) : M (List Lit)

Equations

• LO.Meta.ClProver.exprListToLitList l = do let c ← read liftM (List.mapM (LO.Meta.Litform.denote c.LC) l)

def LO.Meta.ClProver.Sequent.toExpr (Γ : Sequent) : M Lean.Expr

Equations

• Γ.toExpr = do let c ← read pure (Qq.toQList (List.map (LO.Meta.Litform.toExpr c.LC) Γ))

def LO.Meta.ClProver.tryRightClose (φ : Lit) (Γ Δ : Sequent) : M (Option Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.

def LO.Meta.ClProver.tryLeftClose (φ : Lit) (Γ Δ : Sequent) : M (Option Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.

def LO.Meta.ClProver.rotateRight (Γ Δ : Sequent) (φ : Lit) (e : Lean.Expr) : M Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def LO.Meta.ClProver.rotateLeft (Γ Δ : Sequent) (φ : Lit) (e : Lean.Expr) : M Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def LO.Meta.ClProver.verumRight (Γ Δ : Sequent) : M Lean.Expr

Equations

• LO.Meta.ClProver.verumRight Γ Δ = do let eΓ ← Γ.toExpr let eΔ ← Δ.toExpr LO.Meta.ClProver.iapp `LO.Meta.ClProver.Theorems.verum_right #[eΓ, eΔ]

def LO.Meta.ClProver.falsumRight (Γ Δ : Sequent) (e : Lean.Expr) : M Lean.Expr

Equations

• LO.Meta.ClProver.falsumRight Γ Δ e = do let eΓ ← Γ.toExpr let eΔ ← Δ.toExpr LO.Meta.ClProver.iapp `LO.Meta.ClProver.Theorems.falsum_right #[eΓ, eΔ, e]

def LO.Meta.ClProver.andRight (Γ Δ : Sequent) (φ ψ : Lit) (e₁ e₂ : Lean.Expr) : M Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def LO.Meta.ClProver.orRight (Γ Δ : Sequent) (φ ψ : Lit) (e : Lean.Expr) : M Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def LO.Meta.ClProver.negRight (Γ Δ : Sequent) (φ : Lit) (e : Lean.Expr) : M Lean.Expr

Equations

• LO.Meta.ClProver.negRight Γ Δ φ e = do let eΓ ← Γ.toExpr let eΔ ← Δ.toExpr let eφ ← LO.Meta.ClProver.litToExpr φ LO.Meta.ClProver.iapp `LO.Meta.ClProver.Theorems.neg_right #[eΓ, eΔ, eφ, e]

def LO.Meta.ClProver.implyRight (Γ Δ : Sequent) (φ ψ : Lit) (e : Lean.Expr) : M Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def LO.Meta.ClProver.iffRight (Γ Δ : Sequent) (φ ψ : Lit) (e₁ e₂ : Lean.Expr) : M Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def LO.Meta.ClProver.verumLeft (Γ Δ : Sequent) (e : Lean.Expr) : M Lean.Expr

Equations

• LO.Meta.ClProver.verumLeft Γ Δ e = do let eΓ ← Γ.toExpr let eΔ ← Δ.toExpr LO.Meta.ClProver.iapp `LO.Meta.ClProver.Theorems.verum_left #[eΓ, eΔ, e]

def LO.Meta.ClProver.falsumLeft (Γ Δ : Sequent) : M Lean.Expr

Equations

• LO.Meta.ClProver.falsumLeft Γ Δ = do let eΓ ← Γ.toExpr let eΔ ← Δ.toExpr LO.Meta.ClProver.iapp `LO.Meta.ClProver.Theorems.falsum_left #[eΓ, eΔ]

def LO.Meta.ClProver.andLeft (Γ Δ : Sequent) (φ ψ : Lit) (e : Lean.Expr) : M Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def LO.Meta.ClProver.orLeft (Γ Δ : Sequent) (φ ψ : Lit) (e₁ e₂ : Lean.Expr) : M Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def LO.Meta.ClProver.negLeft (Γ Δ : Sequent) (φ : Lit) (e : Lean.Expr) : M Lean.Expr

Equations

• LO.Meta.ClProver.negLeft Γ Δ φ e = do let eΓ ← Γ.toExpr let eΔ ← Δ.toExpr let eφ ← LO.Meta.ClProver.litToExpr φ LO.Meta.ClProver.iapp `LO.Meta.ClProver.Theorems.neg_left #[eΓ, eΔ, eφ, e]

def LO.Meta.ClProver.implyLeft (Γ Δ : Sequent) (φ ψ : Lit) (e₁ e₂ : Lean.Expr) : M Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def LO.Meta.ClProver.iffLeft (Γ Δ : Sequent) (φ ψ : Lit) (e₁ e₂ : Lean.Expr) : M Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def LO.Meta.ClProver.toProvable (φ e : Lean.Expr) : M Lean.Expr

Equations

• LO.Meta.ClProver.toProvable φ e = LO.Meta.ClProver.iapp `LO.Meta.ClProver.Theorems.to_provable #[φ, e]

def LO.Meta.ClProver.prover (k : ℕ) (b : Bool) (Γ Δ : Sequent) : M Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• LO.Meta.ClProver.prover k_2.succ false Γ [] = LO.Meta.ClProver.prover k_2 true Γ []
• LO.Meta.ClProver.prover k_2.succ true [] Δ = LO.Meta.ClProver.prover k_2 false [] Δ

structure LO.Meta.ClProver.HypInfo : Type

• levelF : Lean.Level
• levelS : Lean.Level
• levelE : Lean.Level
• F : Q(Type udummy._uniq.28)
• S : Q(Type udummy._uniq.29)
• E : Q(Entailment unknown_1 unknown_2)
• 𝓢 : Q(unknown_1)
• φ : Q(unknown_1)
• proof : Q(unknown_4 ⊢ unknown_5)

def LO.Meta.ClProver.synthProvable (e : Lean.Expr) : Lean.MetaM HypInfo

Equations

• One or more equations did not get rendered due to their size.

structure LO.Meta.ClProver.CompatibleHypInfo : Type

• 𝓢 : Lean.Expr
• WT : Lean.Expr
• φ : Lit
• proof : Lean.Expr

def LO.Meta.ClProver.HypInfo.toCompatible (h : HypInfo) : M CompatibleHypInfo

Equations

• One or more equations did not get rendered due to their size.

def LO.Meta.ClProver.addHyp (𝓣 wt : Lean.Expr) (Γ Δ : Sequent) (φ : Lit) (E e : Lean.Expr) : M Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def LO.Meta.ClProver.addHyps (prover : Sequent → Sequent → M Lean.Expr) (Γ Δ : Sequent) : List HypInfo → M Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• LO.Meta.ClProver.addHyps prover Γ Δ [] = prover Γ Δ

def LO.Meta.ClProver.main (n : ℕ) (hyps : Array HypInfo) (L R : List Lean.Expr) : M Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def LO.Meta.ClProver.termSeq : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def LO.Meta.ClProver.tacticCl_prover_2s__ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def LO.Meta.ClProver.tacticCl_prover__ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.