Proof automation based on the proof search on (modified) $\mathbf{LJpm}^*$

main reference: Grigori Mints, A Short Introduction to Intuitionistic Logic [Min00]

def LO.Meta.IntProver.Theorems.«term_⟶_» : Lean.TrailingParserDescr

Equations

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

theorem LO.Meta.IntProver.Theorems.to_twoSided {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} (h : Entailment.Tableaux.Valid 𝓢 [{ antecedent := Γ, succedent := Δ }]) : Entailment.TwoSided 𝓢 Γ Δ

theorem LO.Meta.IntProver.Theorems.to_provable {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {φ : F} (h : Entailment.Tableaux.Valid 𝓢 [{ antecedent := [], succedent := [φ] }]) : 𝓢 ⊢ φ

theorem LO.Meta.IntProver.Theorems.add_hyp {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {𝒯 : S} (s : 𝒯 ⪯ 𝓢) {Γ Δ : List F} {φ : F} (hφ : 𝒯 ⊢ φ) : Entailment.Tableaux.Valid 𝓢 [{ antecedent := φ :: Γ, succedent := Δ }] → Entailment.Tableaux.Valid 𝓢 [{ antecedent := Γ, succedent := Δ }]

theorem LO.Meta.IntProver.Theorems.right_closed {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} {φ : F} (h : φ ∈ Γ) : Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ, succedent := φ :: Δ } :: T)

theorem LO.Meta.IntProver.Theorems.left_closed {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} {φ : F} (h : φ ∈ Δ) : Entailment.Tableaux.Valid 𝓢 ({ antecedent := φ :: Γ, succedent := Δ } :: T)

theorem LO.Meta.IntProver.Theorems.remove {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : Entailment.Tableaux F} {Γ Δ : List F} : Entailment.Tableaux.Valid 𝓢 T → Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ, succedent := Δ } :: T)

theorem LO.Meta.IntProver.Theorems.rotate {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} : Entailment.Tableaux.Valid 𝓢 (T ++ [{ antecedent := Γ, succedent := Δ }]) → Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ, succedent := Δ } :: T)

theorem LO.Meta.IntProver.Theorems.remove_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} {φ : F} : Entailment.Tableaux.Valid 𝓢 (T ++ [{ antecedent := Γ, succedent := Δ }]) → Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ, succedent := φ :: Δ } :: T)

theorem LO.Meta.IntProver.Theorems.rotate_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} {φ : F} : Entailment.Tableaux.Valid 𝓢 (T ++ [{ antecedent := Γ, succedent := Δ ++ [φ] }]) → Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ, succedent := φ :: Δ } :: T)

theorem LO.Meta.IntProver.Theorems.verum_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} : Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ, succedent := ⊤ :: Δ } :: T)

theorem LO.Meta.IntProver.Theorems.falsum_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} : Entailment.Tableaux.Valid 𝓢 (T ++ [{ antecedent := Γ, succedent := Δ }]) → Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ, succedent := ⊥ :: Δ } :: T)

theorem LO.Meta.IntProver.Theorems.and_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} {φ ψ : F} : Entailment.Tableaux.Valid 𝓢 (T ++ [{ antecedent := Γ, succedent := Δ ++ [φ] }]) → Entailment.Tableaux.Valid 𝓢 (T ++ [{ antecedent := Γ, succedent := Δ ++ [ψ] }]) → Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ, succedent := φ ⋏ ψ :: Δ } :: T)

theorem LO.Meta.IntProver.Theorems.or_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} {φ ψ : F} : Entailment.Tableaux.Valid 𝓢 (T ++ [{ antecedent := Γ, succedent := Δ ++ [φ, ψ] }]) → Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ, succedent := φ ⋎ ψ :: Δ } :: T)

theorem LO.Meta.IntProver.Theorems.neg_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} {φ : F} : Entailment.Tableaux.Valid 𝓢 (T ++ [{ antecedent := Γ ++ [φ], succedent := [] }] ++ [{ antecedent := Γ, succedent := Δ }]) → Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ, succedent := ∼φ :: Δ } :: T)

theorem LO.Meta.IntProver.Theorems.imply_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} {φ ψ : F} : Entailment.Tableaux.Valid 𝓢 (T ++ [{ antecedent := Γ ++ [φ], succedent := [ψ] }] ++ [{ antecedent := Γ, succedent := Δ }]) → Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ, succedent := (φ 🡒 ψ) :: Δ } :: T)

theorem LO.Meta.IntProver.Theorems.iff_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} {φ ψ : F} : Entailment.Tableaux.Valid 𝓢 (T ++ [{ antecedent := Γ, succedent := Δ ++ [φ 🡒 ψ] }]) → Entailment.Tableaux.Valid 𝓢 (T ++ [{ antecedent := Γ, succedent := Δ ++ [ψ 🡒 φ] }]) → Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ, succedent := (φ 🡘 ψ) :: Δ } :: T)

theorem LO.Meta.IntProver.Theorems.remove_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} {φ : F} : Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ, succedent := Δ } :: T) → Entailment.Tableaux.Valid 𝓢 ({ antecedent := φ :: Γ, succedent := Δ } :: T)

theorem LO.Meta.IntProver.Theorems.rotate_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} {φ : F} : Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ ++ [φ], succedent := Δ } :: T) → Entailment.Tableaux.Valid 𝓢 ({ antecedent := φ :: Γ, succedent := Δ } :: T)

theorem LO.Meta.IntProver.Theorems.verum_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} : Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ, succedent := Δ } :: T) → Entailment.Tableaux.Valid 𝓢 ({ antecedent := ⊤ :: Γ, succedent := Δ } :: T)

theorem LO.Meta.IntProver.Theorems.falsum_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} : Entailment.Tableaux.Valid 𝓢 ({ antecedent := ⊥ :: Γ, succedent := Δ } :: T)

theorem LO.Meta.IntProver.Theorems.or_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} {φ ψ : F} : Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ ++ [φ], succedent := Δ } :: T) → Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ ++ [ψ], succedent := Δ } :: T) → Entailment.Tableaux.Valid 𝓢 ({ antecedent := φ ⋎ ψ :: Γ, succedent := Δ } :: T)

theorem LO.Meta.IntProver.Theorems.and_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} {φ ψ : F} : Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ ++ [φ, ψ], succedent := Δ } :: T) → Entailment.Tableaux.Valid 𝓢 ({ antecedent := φ ⋏ ψ :: Γ, succedent := Δ } :: T)

theorem LO.Meta.IntProver.Theorems.neg_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} {φ : F} : Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ ++ [∼φ], succedent := Δ ++ [φ] } :: T) → Entailment.Tableaux.Valid 𝓢 ({ antecedent := ∼φ :: Γ, succedent := Δ } :: T)

theorem LO.Meta.IntProver.Theorems.imply_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} {φ ψ : F} : Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ ++ [φ 🡒 ψ], succedent := Δ ++ [φ] } :: T) → Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ ++ [ψ], succedent := Δ } :: T) → Entailment.Tableaux.Valid 𝓢 ({ antecedent := (φ 🡒 ψ) :: Γ, succedent := Δ } :: T)

theorem LO.Meta.IntProver.Theorems.iff_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {T : List (Entailment.Tableaux.Sequent F)} {Γ Δ : List F} {φ ψ : F} : Entailment.Tableaux.Valid 𝓢 ({ antecedent := Γ ++ [φ 🡒 ψ, ψ 🡒 φ], succedent := Δ } :: T) → Entailment.Tableaux.Valid 𝓢 ({ antecedent := (φ 🡘 ψ) :: Γ, succedent := Δ } :: T)

structure LO.Meta.IntProver.Context : Type

• levelF : Lean.Level
• levelS : Lean.Level
• levelE : Lean.Level
• F : Q(Type udummy._uniq.39)
• instLC : Q(LogicalConnective unknown_1)
• instDE : Q(DecidableEq unknown_1)
• S : Q(Type udummy._uniq.45)
• E : Q(Entailment unknown_1 unknown_2)
• 𝓢 : Q(unknown_1)
• instInt : Q(Entailment.Int unknown_5)

@[reducible, inline]

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

The monad for int_prover contains.

Equations

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

def LO.Meta.IntProver.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.Int 𝓢], _ 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.instLC).app c.instDE).app c.S).app c.E).app c.𝓢).app c.instInt)

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

Equations

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

def LO.Meta.IntProver.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.IntProver.getGoalProvable (e : Q(Prop)) : Lean.MetaM ((c : Context) × have a := c.F; Q(«$a»))

@[reducible, inline]

abbrev LO.Meta.IntProver.Sequent : Type

Equations

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

@[reducible, inline]

abbrev LO.Meta.IntProver.Tableaux : Type

Equations

• LO.Meta.IntProver.Tableaux = LO.Entailment.Tableaux LO.Meta.Lit

def LO.Meta.IntProver.«term_⟶_» : Lean.TrailingParserDescr

Equations

• LO.Meta.IntProver.«term_⟶_» = Lean.ParserDescr.trailingNode `LO.Meta.IntProver.«term_⟶_» 0 45 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟶ ") (Lean.ParserDescr.cat `term 46))

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def LO.Meta.IntProver.mkTableauSequentQ {u_1 : Lean.Level} (F : Q(Type u_1)) (Γ Δ : Q(List «$F»)) : Q(Entailment.Tableaux.Sequent «$F»)

Equations

• LO.Meta.IntProver.mkTableauSequentQ F Γ Δ = q({ antecedent := «$Γ», succedent := «$Δ» })

def LO.Meta.IntProver.Tableaux.toExpr (T : Tableaux) : M Lean.Expr

Equations

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

def LO.Meta.IntProver.remove (T : Tableaux) (Γ Δ : Sequent) (e : Lean.Expr) : M Lean.Expr

Equations

• LO.Meta.IntProver.remove T Γ Δ e = do let T ← T.toExpr let Γ ← Γ.toExpr let Δ ← Δ.toExpr LO.Meta.IntProver.iapp `LO.Meta.IntProver.Theorems.remove #[T, Γ, Δ, e]

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

Equations

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

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

Equations

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

def LO.Meta.IntProver.removeRight (T : Tableaux) (Γ Δ : Sequent) (φ : Lit) (e : Lean.Expr) : M Lean.Expr

Equations

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

def LO.Meta.IntProver.removeLeft (T : Tableaux) (Γ Δ : Sequent) (φ : Lit) (e : Lean.Expr) : M Lean.Expr

Equations

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

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

Equations

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

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

Equations

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

def LO.Meta.IntProver.verumRight (T : Tableaux) (Γ Δ : Sequent) : M Lean.Expr

Equations

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

def LO.Meta.IntProver.falsumRight (T : Tableaux) (Γ Δ : Sequent) (e : Lean.Expr) : M Lean.Expr

Equations

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

def LO.Meta.IntProver.andRight (T : Tableaux) (Γ Δ : 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.IntProver.orRight (T : Tableaux) (Γ Δ : Sequent) (φ ψ : Lit) (e : Lean.Expr) : M Lean.Expr

Equations

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

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

Equations

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

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

Equations

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

def LO.Meta.IntProver.iffRight (T : Tableaux) (Γ Δ : 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.IntProver.rotate (T : Tableaux) (Γ Δ : Sequent) (e : Lean.Expr) : M Lean.Expr

Equations

• LO.Meta.IntProver.rotate T Γ Δ e = do let T ← T.toExpr let Γ ← Γ.toExpr let Δ ← Δ.toExpr LO.Meta.IntProver.iapp `LO.Meta.IntProver.Theorems.rotate #[T, Γ, Δ, e]

def LO.Meta.IntProver.verumLeft (T : Tableaux) (Γ Δ : Sequent) (e : Lean.Expr) : M Lean.Expr

Equations

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

def LO.Meta.IntProver.falsumLeft (T : Tableaux) (Γ Δ : Sequent) : M Lean.Expr

Equations

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

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

Equations

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

def LO.Meta.IntProver.orLeft (T : Tableaux) (Γ Δ : 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.IntProver.negLeft (T : Tableaux) (Γ Δ : Sequent) (φ : Lit) (e : Lean.Expr) : M Lean.Expr

Equations

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

def LO.Meta.IntProver.implyLeft (T : Tableaux) (Γ Δ : 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.IntProver.iffLeft (T : Tableaux) (Γ Δ : Sequent) (φ ψ : Lit) (e : Lean.Expr) : M Lean.Expr

Equations

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

def LO.Meta.IntProver.isWeakerSequent (Γ Δ : Sequent) (T : Tableaux) : M Bool

Equations

• One or more equations did not get rendered due to their size.
• LO.Meta.IntProver.isWeakerSequent Γ Δ [] = pure false

def LO.Meta.IntProver.prover (k : ℕ) (b : Bool) (T : Tableaux) : M Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• LO.Meta.IntProver.prover 0 b T = do let __do_lift ← T.toExpr Lean.throwError (Lean.toMessageData "Proof search failed: " ++ Lean.toMessageData __do_lift)
• LO.Meta.IntProver.prover k_2.succ false [] = Lean.throwError (Lean.toMessageData "Proof search failed: empty tableaux reached.")
• LO.Meta.IntProver.prover k_2.succ true [] = Lean.throwError (Lean.toMessageData "Proof search failed: empty tableaux reached.")

structure LO.Meta.IntProver.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.IntProver.synthProvable (e : Lean.Expr) : Lean.MetaM HypInfo

Equations

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

structure LO.Meta.IntProver.CompatibleHypInfo : Type

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

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

Equations

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

def LO.Meta.IntProver.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.IntProver.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.IntProver.addHyps prover Γ Δ [] = prover Γ Δ

def LO.Meta.IntProver.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.IntProver.toTwoSided (L R : List Lean.Expr) (e : Lean.Expr) : M Lean.Expr

Equations

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

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

Equations

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

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

Equations

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

def LO.Meta.IntProver.tacticInt_prover_2s__ : Lean.ParserDescr

Equations

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

def LO.Meta.IntProver.tacticInt_prover__ : Lean.ParserDescr

Equations

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