Logic.AutoProver.Prover

source

def LO.Gentzen.rEmLeft {F : Type u_1} [LO.LogicalConnective F] [LO.Gentzen F] {Γ : List F} {Δ : List F} {p : F} (h : p ∈ Δ) :

p :: Γ ⊢² Δ

Equations

LO.Gentzen.rEmLeft h = LO.Gentzen.closed p ⋯ h

Instances For

source

def LO.Gentzen.rEmRight {F : Type u_1} [LO.LogicalConnective F] [LO.Gentzen F] {Γ : List F} {Δ : List F} {p : F} (h : p ∈ Γ) :

Γ ⊢² p :: Δ

Equations

LO.Gentzen.rEmRight h = LO.Gentzen.closed p h ⋯

Instances For

source

def LO.Gentzen.rNegLeft {F : Type u_1} [LO.LogicalConnective F] [LO.Gentzen F] {Γ : List F} {Δ : List F} {p : F} (dp : Γ ⊢² Δ ++ [p]) :

~p :: Γ ⊢² Δ

Equations

LO.Gentzen.rNegLeft dp = LO.Gentzen.negLeft (LO.Gentzen.wk dp ⋯ ⋯)

Instances For

source

def LO.Gentzen.rNegRight {F : Type u_1} [LO.LogicalConnective F] [LO.Gentzen F] {Γ : List F} {Δ : List F} {p : F} (dp : Γ ++ [p] ⊢² Δ) :

Γ ⊢² ~p :: Δ

Equations

LO.Gentzen.rNegRight dp = LO.Gentzen.negRight (LO.Gentzen.wk dp ⋯ ⋯)

Instances For

source

def LO.Gentzen.rOrLeft {F : Type u_1} [LO.LogicalConnective F] [LO.Gentzen F] {Γ : List F} {Δ : List F} {p : F} {q : F} (dp : Γ ++ [p] ⊢² Δ) (dq : Γ ++ [q] ⊢² Δ) :

p ⋎ q :: Γ ⊢² Δ

Equations

LO.Gentzen.rOrLeft dp dq = LO.Gentzen.orLeft (LO.Gentzen.wk dp ⋯ ⋯) (LO.Gentzen.wk dq ⋯ ⋯)

Instances For

source

def LO.Gentzen.rOrRight {F : Type u_1} [LO.LogicalConnective F] [LO.Gentzen F] {Γ : List F} {Δ : List F} {p : F} {q : F} (d : Γ ⊢² Δ ++ [p, q]) :

Γ ⊢² p ⋎ q :: Δ

Equations

LO.Gentzen.rOrRight d = LO.Gentzen.orRight (LO.Gentzen.wk d ⋯ ⋯)

Instances For

source

def LO.Gentzen.rAndLeft {F : Type u_1} [LO.LogicalConnective F] [LO.Gentzen F] {Γ : List F} {Δ : List F} {p : F} {q : F} (d : Γ ++ [p, q] ⊢² Δ) :

p ⋏ q :: Γ ⊢² Δ

Equations

LO.Gentzen.rAndLeft d = LO.Gentzen.andLeft (LO.Gentzen.wk d ⋯ ⋯)

Instances For

source

def LO.Gentzen.rAndRight {F : Type u_1} [LO.LogicalConnective F] [LO.Gentzen F] {Γ : List F} {Δ : List F} {p : F} {q : F} (dp : Γ ⊢² Δ ++ [p]) (dq : Γ ⊢² Δ ++ [q]) :

Γ ⊢² p ⋏ q :: Δ

Equations

LO.Gentzen.rAndRight dp dq = LO.Gentzen.andRight (LO.Gentzen.wk dp ⋯ ⋯) (LO.Gentzen.wk dq ⋯ ⋯)

Instances For

source

def LO.Gentzen.rImplyLeft {F : Type u_1} [LO.LogicalConnective F] [LO.Gentzen F] {Γ : List F} {Δ : List F} {p : F} {q : F} (dp : Γ ⊢² Δ ++ [p]) (dq : Γ ++ [q] ⊢² Δ) :

(p ⟶ q) :: Γ ⊢² Δ

Equations

LO.Gentzen.rImplyLeft dp dq = LO.Gentzen.implyLeft (LO.Gentzen.wk dp ⋯ ⋯) (LO.Gentzen.wk dq ⋯ ⋯)

Instances For

source

def LO.Gentzen.rImplyRight {F : Type u_1} [LO.LogicalConnective F] [LO.Gentzen F] {Γ : List F} {Δ : List F} {p : F} {q : F} (d : Γ ++ [p] ⊢² Δ ++ [q]) :

Γ ⊢² (p ⟶ q) :: Δ

Equations

LO.Gentzen.rImplyRight d = LO.Gentzen.implyRight (LO.Gentzen.wk d ⋯ ⋯)

Instances For

source

@[reducible, inline]

abbrev LO.AutoProver.DerivationQ {u : Lean.Level} {F : Q(Type u)} (instLS : Q(LO.LogicalConnective «$F»)) (instGz : Q(LO.Gentzen «$F»)) (L : List (LO.Litform.Meta.Lit F)) (R : List (LO.Litform.Meta.Lit F)) :

Type

Equations

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

Instances For

source

def LO.AutoProver.DerivationQ.DEq {u_1 : Lean.Level} {F : Q(Type u_1)} :

LO.Litform.Meta.Lit F → LO.Litform.Meta.Lit F → Lean.MetaM Bool

Instances For

source

def LO.AutoProver.DerivationQ.DMem {u_1 : Lean.Level} {F : Q(Type u_1)} (p : LO.Litform.Meta.Lit F) (Δ : List (LO.Litform.Meta.Lit F)) :

Lean.MetaM Bool

Equations

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

Instances For

source

def LO.AutoProver.DerivationQ.rotateLeft {u : Lean.Level} {F : Q(Type u)} {instLS : Q(LO.LogicalConnective «$F»)} {instGz : Q(LO.Gentzen «$F»)} (L : List (LO.Litform.Meta.Lit F)) (R : List (LO.Litform.Meta.Lit F)) {p : LO.Litform.Meta.Lit F} (d : LO.AutoProver.DerivationQ instLS instGz (L ++ [p]) R) :

LO.AutoProver.DerivationQ instLS instGz (p :: L) R

Equations

LO.AutoProver.DerivationQ.rotateLeft L R d = let x := d; q(LO.Gentzen.rotateLeft «$d»)

Instances For

source

def LO.AutoProver.DerivationQ.rotateRight {u : Lean.Level} {F : Q(Type u)} {instLS : Q(LO.LogicalConnective «$F»)} {instGz : Q(LO.Gentzen «$F»)} (L : List (LO.Litform.Meta.Lit F)) (R : List (LO.Litform.Meta.Lit F)) {p : LO.Litform.Meta.Lit F} (d : LO.AutoProver.DerivationQ instLS instGz L (R ++ [p])) :

LO.AutoProver.DerivationQ instLS instGz L (p :: R)

Equations

LO.AutoProver.DerivationQ.rotateRight L R d = let x := d; q(LO.Gentzen.rotateRight «$d»)

Instances For

source

def LO.AutoProver.DerivationQ.verum {u : Lean.Level} {F : Q(Type u)} {instLS : Q(LO.LogicalConnective «$F»)} {instGz : Q(LO.Gentzen «$F»)} (L : List (LO.Litform.Meta.Lit F)) (R : List (LO.Litform.Meta.Lit F)) :

LO.AutoProver.DerivationQ instLS instGz L (⊤ :: R)

Equations

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

Instances For

source

def LO.AutoProver.DerivationQ.falsum {u : Lean.Level} {F : Q(Type u)} {instLS : Q(LO.LogicalConnective «$F»)} {instGz : Q(LO.Gentzen «$F»)} (L : List (LO.Litform.Meta.Lit F)) (R : List (LO.Litform.Meta.Lit F)) :

LO.AutoProver.DerivationQ instLS instGz (⊥ :: L) R

Equations

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

Instances For

source

def LO.AutoProver.DerivationQ.rEmLeftOfEq {u : Lean.Level} {F : Q(Type u)} {instLS : Q(LO.LogicalConnective «$F»)} {instGz : Q(LO.Gentzen «$F»)} (L : List (LO.Litform.Meta.Lit F)) (R : List (LO.Litform.Meta.Lit F)) {p : LO.Litform.Meta.Lit F} :

Lean.MetaM (LO.AutoProver.DerivationQ instLS instGz (p :: L) R)

Equations

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

Instances For

source

def LO.AutoProver.DerivationQ.rEmRightOfEq {u : Lean.Level} {F : Q(Type u)} {instLS : Q(LO.LogicalConnective «$F»)} {instGz : Q(LO.Gentzen «$F»)} (L : List (LO.Litform.Meta.Lit F)) (R : List (LO.Litform.Meta.Lit F)) {p : LO.Litform.Meta.Lit F} :

Lean.MetaM (LO.AutoProver.DerivationQ instLS instGz L (p :: R))

Equations

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

Instances For

source

def LO.AutoProver.DerivationQ.rNegLeft {u : Lean.Level} {F : Q(Type u)} {instLS : Q(LO.LogicalConnective «$F»)} {instGz : Q(LO.Gentzen «$F»)} (L : List (LO.Litform.Meta.Lit F)) (R : List (LO.Litform.Meta.Lit F)) {p : LO.Litform.Meta.Lit F} (d : LO.AutoProver.DerivationQ instLS instGz L (R ++ [p])) :

LO.AutoProver.DerivationQ instLS instGz (~p :: L) R

Equations

LO.AutoProver.DerivationQ.rNegLeft L R d = let d := d; q(LO.Gentzen.rNegLeft «$d»)

Instances For

source

def LO.AutoProver.DerivationQ.rNegRight {u : Lean.Level} {F : Q(Type u)} {instLS : Q(LO.LogicalConnective «$F»)} {instGz : Q(LO.Gentzen «$F»)} (L : List (LO.Litform.Meta.Lit F)) (R : List (LO.Litform.Meta.Lit F)) {p : LO.Litform.Meta.Lit F} (d : LO.AutoProver.DerivationQ instLS instGz (L ++ [p]) R) :

LO.AutoProver.DerivationQ instLS instGz L (~p :: R)

Equations

LO.AutoProver.DerivationQ.rNegRight L R d = let d := d; q(LO.Gentzen.rNegRight «$d»)

Instances For

source

def LO.AutoProver.DerivationQ.rAndLeft {u : Lean.Level} {F : Q(Type u)} {instLS : Q(LO.LogicalConnective «$F»)} {instGz : Q(LO.Gentzen «$F»)} (L : List (LO.Litform.Meta.Lit F)) (R : List (LO.Litform.Meta.Lit F)) {p : LO.Litform.Meta.Lit F} {q : LO.Litform.Meta.Lit F} (d : LO.AutoProver.DerivationQ instLS instGz (L ++ [p, q]) R) :

LO.AutoProver.DerivationQ instLS instGz (p ⋏ q :: L) R

Equations

LO.AutoProver.DerivationQ.rAndLeft L R d = let d := d; q(LO.Gentzen.rAndLeft «$d»)

Instances For

source

def LO.AutoProver.DerivationQ.rAndRight {u : Lean.Level} {F : Q(Type u)} {instLS : Q(LO.LogicalConnective «$F»)} {instGz : Q(LO.Gentzen «$F»)} (L : List (LO.Litform.Meta.Lit F)) (R : List (LO.Litform.Meta.Lit F)) {p : LO.Litform.Meta.Lit F} {q : LO.Litform.Meta.Lit F} (dp : LO.AutoProver.DerivationQ instLS instGz L (R ++ [p])) (dq : LO.AutoProver.DerivationQ instLS instGz L (R ++ [q])) :

LO.AutoProver.DerivationQ instLS instGz L (p ⋏ q :: R)

Equations

LO.AutoProver.DerivationQ.rAndRight L R dp dq = let dp := dp; let dq := dq; q(LO.Gentzen.rAndRight «$dp» «$dq»)

Instances For

source

def LO.AutoProver.DerivationQ.rOrLeft {u : Lean.Level} {F : Q(Type u)} {instLS : Q(LO.LogicalConnective «$F»)} {instGz : Q(LO.Gentzen «$F»)} (L : List (LO.Litform.Meta.Lit F)) (R : List (LO.Litform.Meta.Lit F)) {p : LO.Litform.Meta.Lit F} {q : LO.Litform.Meta.Lit F} (dp : LO.AutoProver.DerivationQ instLS instGz (L ++ [p]) R) (dq : LO.AutoProver.DerivationQ instLS instGz (L ++ [q]) R) :

LO.AutoProver.DerivationQ instLS instGz (p ⋎ q :: L) R

Equations

LO.AutoProver.DerivationQ.rOrLeft L R dp dq = let dp := dp; let dq := dq; q(LO.Gentzen.rOrLeft «$dp» «$dq»)

Instances For

source

def LO.AutoProver.DerivationQ.rOrRight {u : Lean.Level} {F : Q(Type u)} {instLS : Q(LO.LogicalConnective «$F»)} {instGz : Q(LO.Gentzen «$F»)} (L : List (LO.Litform.Meta.Lit F)) (R : List (LO.Litform.Meta.Lit F)) {p : LO.Litform.Meta.Lit F} {q : LO.Litform.Meta.Lit F} (d : LO.AutoProver.DerivationQ instLS instGz L (R ++ [p, q])) :

LO.AutoProver.DerivationQ instLS instGz L (p ⋎ q :: R)

Equations

LO.AutoProver.DerivationQ.rOrRight L R d = let d := d; q(LO.Gentzen.rOrRight «$d»)

Instances For

source

def LO.AutoProver.DerivationQ.rImplyLeft {u : Lean.Level} {F : Q(Type u)} {instLS : Q(LO.LogicalConnective «$F»)} {instGz : Q(LO.Gentzen «$F»)} (L : List (LO.Litform.Meta.Lit F)) (R : List (LO.Litform.Meta.Lit F)) {p : LO.Litform.Meta.Lit F} {q : LO.Litform.Meta.Lit F} (dp : LO.AutoProver.DerivationQ instLS instGz L (R ++ [p])) (dq : LO.AutoProver.DerivationQ instLS instGz (L ++ [q]) R) :

LO.AutoProver.DerivationQ instLS instGz ((p ⟶ q) :: L) R

Equations

LO.AutoProver.DerivationQ.rImplyLeft L R dp dq = let dp := dp; let dq := dq; q(LO.Gentzen.rImplyLeft «$dp» «$dq»)

Instances For

source

def LO.AutoProver.DerivationQ.rImplyRight {u : Lean.Level} {F : Q(Type u)} {instLS : Q(LO.LogicalConnective «$F»)} {instGz : Q(LO.Gentzen «$F»)} (L : List (LO.Litform.Meta.Lit F)) (R : List (LO.Litform.Meta.Lit F)) {p : LO.Litform.Meta.Lit F} {q : LO.Litform.Meta.Lit F} (d : LO.AutoProver.DerivationQ instLS instGz (L ++ [p]) (R ++ [q])) :

LO.AutoProver.DerivationQ instLS instGz L ((p ⟶ q) :: R)

Equations

LO.AutoProver.DerivationQ.rImplyRight L R d = let d := d; q(LO.Gentzen.rImplyRight «$d»)

Instances For

source

def LO.AutoProver.DerivationQ.deriveAux {u : Lean.Level} {F : Q(Type u)} (instLS : Q(LO.LogicalConnective «$F»)) (instGz : Q(LO.Gentzen «$F»)) :

ℕ → Bool → (L R : List (LO.Litform.Meta.Lit F)) → Lean.MetaM (LO.AutoProver.DerivationQ instLS instGz L R)

Equations

One or more equations did not get rendered due to their size.
LO.AutoProver.DerivationQ.deriveAux instLS instGz s.succ true [] x = LO.AutoProver.DerivationQ.deriveAux instLS instGz s false [] x
LO.AutoProver.DerivationQ.deriveAux instLS instGz s.succ false x [] = LO.AutoProver.DerivationQ.deriveAux instLS instGz s true x []

Instances For

source

def LO.AutoProver.DerivationQ.derive {u : Lean.Level} {F : Q(Type u)} (instLS : Q(LO.LogicalConnective «$F»)) (instGz : Q(LO.Gentzen «$F»)) (s : ℕ) (L : List (LO.Litform.Meta.Lit F)) (R : List (LO.Litform.Meta.Lit F)) :

Lean.MetaM (LO.AutoProver.DerivationQ instLS instGz L R)

Equations

LO.AutoProver.DerivationQ.derive instLS instGz s L R = LO.AutoProver.DerivationQ.deriveAux instLS instGz s true L R

Instances For

source

def LO.AutoProver.isExprProvable? (ty : Q(Prop)) :

Lean.MetaM ((u : Lean.Level) × (v : Lean.Level) × (_ : Lean.Level) × (F : Q(Type u)) × (S : Q(Type v)) × Q(«$S») × Q(«$F»))

Equations

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

Instances For

source

def LO.AutoProver.prove! {u : Lean.Level} {v : Lean.Level} {w : Lean.Level} {F : Q(Type u)} {S : Q(Type v)} (instLS : Q(LO.LogicalConnective «$F»)) (instSys : Q(LO.System «$F» «$S»)) (instGz : Q(LO.Gentzen «$F»)) (instLTS : Q(LO.LawfulTwoSided «$S»)) (s : ℕ) (𝓢 : Q(«$S»)) (p : Q(«$F»)) :

Lean.MetaM Q(«$𝓢» ⊢! «$p»)

Equations

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

Instances For

source

def LO.AutoProver.termSeq :

Lean.ParserDescr

Equations

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

Instances For

source

def LO.AutoProver.proofOfProvable? {u : Lean.Level} {v : Lean.Level} {w : Lean.Level} {F : Q(Type u)} {S : Q(Type v)} (instSys : Q(LO.System «$F» «$S»)) (T : Q(«$S»)) (e : Lean.Expr) :

Lean.MetaM ((p : Q(«$F»)) × Q(«$T» ⊢! «$p»))

Equations

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

Instances For

source

def LO.AutoProver.proverL₀ {u : Lean.Level} {v : Lean.Level} {w : Lean.Level} {F : Q(Type u)} {S : Q(Type v)} (instLS : Q(LO.LogicalConnective «$F»)) (instSys : Q(LO.System «$F» «$S»)) (T : Q(«$S»)) (seq : Option (Lean.TSyntax `LO.AutoProver.termSeq)) :

Lean.Elab.TermElabM ((L₀ : List (LO.Litform.Meta.Lit F)) × let a := (LO.Litform.Meta.denotation F instLS).toExprₗ L₀; let toQList_1 := Qq.toQList (List.map Denotation.toExpr' L₀); Q(∀ q ∈ «$toQList_1», «$T» ⊢! q))

Equations

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

Instances For

source

def LO.AutoProver.proveL₀! {u : Lean.Level} {v : Lean.Level} {w : Lean.Level} {F : Q(Type u)} {S : Q(Type v)} (instLS : Q(LO.LogicalConnective «$F»)) (instSys : Q(LO.System «$F» «$S»)) (instGz : Q(LO.Gentzen «$F»)) (instLTS : Q(LO.LawfulTwoSided «$S»)) (s : ℕ) (T : Q(«$S»)) (p : Q(«$F»)) (L₀ : List (LO.Litform.Meta.Lit F)) (H₀ : let a := (LO.Litform.Meta.denotation F instLS).toExprₗ L₀; let toQList_1 := Qq.toQList (List.map Denotation.toExpr' L₀); Q(∀ q ∈ «$toQList_1», «$T» ⊢! q)) :

Lean.MetaM Q(«$T» ⊢! «$p»)

Equations

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

Instances For

source

def LO.AutoProver.tacticTautology_ :

Lean.ParserDescr

Equations

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

Instances For

source

def LO.AutoProver.tacticProver__ :

Lean.ParserDescr

Equations

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

Instances For