Supporting results for pointwise provable equality.

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

structure PointwiseComposition.FFL.Meta.ClProver.Context : Type

The cl prover construction in FFL.Meta.ClProver.

• levelF : Lean.Level

  The level F construction in FFL.Meta.ClProver.Context.

• levelS : Lean.Level

  The level S construction in FFL.Meta.ClProver.Context.

• levelE : Lean.Level

  The level E construction in FFL.Meta.ClProver.Context.

• F : Q(Type udummy._uniq.33)

  The F construction in FFL.Meta.ClProver.Context.

• LC : Q(LogicalConnective unknown_1)

  The LC construction in FFL.Meta.ClProver.Context.

• LN : Q(LogicalNeutral unknown_1)

  The LN construction in FFL.Meta.ClProver.Context.

• S : Q(Type udummy._uniq.40)

  The S construction in FFL.Meta.ClProver.Context.

• E : Q(Entailment unknown_1 unknown_2)

  The E construction in FFL.Meta.ClProver.Context.

• 𝓢 : Q(unknown_1)

  The 𝓢 construction in FFL.Meta.ClProver.Context.

• CL : Q(Entailment.Cl unknown_6)

  The CL construction in FFL.Meta.ClProver.Context.

@[reducible, inline]

abbrev PointwiseComposition.FFL.Meta.ClProver.M (α : Type) : Type

The monad for cl_prover contains.

Equations

• PointwiseComposition.FFL.Meta.ClProver.M = ReaderT PointwiseComposition.FFL.Meta.ClProver.Context Mathlib.Tactic.AtomM

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

Apply the function n : ∀ {F} [LogicalConnective F] [LogicalNeutral 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.mkAppN (Lean.Expr.const n [c.levelF, c.levelS, c.levelE]) #[c.F, c.LC, c.LN, c.S, c.E, c.𝓢, c.CL])

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

The iapp construction in FFL.Meta.ClProver.

Equations

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

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

The get Goal Two Sided construction in FFL.Meta.ClProver.

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

The get Goal Provable construction in FFL.Meta.ClProver.

@[reducible, inline]

abbrev PointwiseComposition.FFL.Meta.ClProver.Sequent : Type

The Sequent construction in FFL.Meta.ClProver.

Equations

• PointwiseComposition.FFL.Meta.ClProver.Sequent = List PointwiseComposition.FFL.Meta.Lit

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

The lit To Expr construction in FFL.Meta.ClProver.

Equations

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

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

The expr To Lit construction in FFL.Meta.ClProver.

Equations

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

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

The to Expr List construction in FFL.Meta.ClProver.Sequent.

Equations

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

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

The expr List To Lit List construction in FFL.Meta.ClProver.

Equations

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

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

The to Expr construction in FFL.Meta.ClProver.Sequent.

Equations

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

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

The try Right Close construction in FFL.Meta.ClProver.

Equations

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

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

The try Left Close construction in FFL.Meta.ClProver.

Equations

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

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

The rotate Right construction in FFL.Meta.ClProver.

Equations

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

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

The rotate Left construction in FFL.Meta.ClProver.

Equations

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

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

The verum Right construction in FFL.Meta.ClProver.

Equations

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

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

The falsum Right construction in FFL.Meta.ClProver.

Equations

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

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

The and Right construction in FFL.Meta.ClProver.

Equations

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

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

The or Right construction in FFL.Meta.ClProver.

Equations

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

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

The neg Right construction in FFL.Meta.ClProver.

Equations

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

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

The imply Right construction in FFL.Meta.ClProver.

Equations

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

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

The iff Right construction in FFL.Meta.ClProver.

Equations

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

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

The verum Left construction in FFL.Meta.ClProver.

Equations

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

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

The falsum Left construction in FFL.Meta.ClProver.

Equations

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

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

The and Left construction in FFL.Meta.ClProver.

Equations

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

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

The or Left construction in FFL.Meta.ClProver.

Equations

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

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

The neg Left construction in FFL.Meta.ClProver.

Equations

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

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

The imply Left construction in FFL.Meta.ClProver.

Equations

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

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

The iff Left construction in FFL.Meta.ClProver.

Equations

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

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

The to Provable construction in FFL.Meta.ClProver.

Equations

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

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

The prover construction in FFL.Meta.ClProver.

Equations

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

structure PointwiseComposition.FFL.Meta.ClProver.HypInfo : Type

Data and laws for Hyp Info in FFL.Meta.ClProver.

• levelF : Lean.Level

  The level F construction in FFL.Meta.ClProver.HypInfo.

• levelS : Lean.Level

  The level S construction in FFL.Meta.ClProver.HypInfo.

• levelE : Lean.Level

  The level E construction in FFL.Meta.ClProver.HypInfo.

• F : Q(Type udummy._uniq.28)

  The F construction in FFL.Meta.ClProver.HypInfo.

• S : Q(Type udummy._uniq.29)

  The S construction in FFL.Meta.ClProver.HypInfo.

• E : Q(Entailment unknown_1 unknown_2)

  The E construction in FFL.Meta.ClProver.HypInfo.

• 𝓢 : Q(unknown_1)

  The 𝓢 construction in FFL.Meta.ClProver.HypInfo.

• φ : Q(unknown_1)

  The φ construction in FFL.Meta.ClProver.HypInfo.

• proof : Q(unknown_4 ⊢ unknown_5)

  The proof construction in FFL.Meta.ClProver.HypInfo.

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

The synth Provable construction in FFL.Meta.ClProver.

Equations

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

structure PointwiseComposition.FFL.Meta.ClProver.CompatibleHypInfo : Type

Data and laws for Compatible Hyp Info in FFL.Meta.ClProver.

• 𝓢 : Lean.Expr

  The 𝓢 construction in FFL.Meta.ClProver.CompatibleHypInfo.

• WT : Lean.Expr

  The WT construction in FFL.Meta.ClProver.CompatibleHypInfo.

• φ : Lit

  The φ construction in FFL.Meta.ClProver.CompatibleHypInfo.

• proof : Lean.Expr

  The proof construction in FFL.Meta.ClProver.CompatibleHypInfo.

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

The to Compatible construction in FFL.Meta.ClProver.HypInfo.

Equations

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

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

The add Hyp construction in FFL.Meta.ClProver.

Equations

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

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

The add Hyps construction in FFL.Meta.ClProver.

Equations

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

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

The main construction in FFL.Meta.ClProver.

Equations

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

def PointwiseComposition.FFL.Meta.ClProver.termSeq : Lean.ParserDescr

The term Seq construction in FFL.Meta.ClProver.

Equations

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

def PointwiseComposition.FFL.Meta.ClProver.tacticCl_prover_2s__ : Lean.ParserDescr

Prove a two-sided classical sequent, optionally supplying a search depth and hypotheses.

Equations

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

def PointwiseComposition.FFL.Meta.ClProver.tacticCl_prover__ : Lean.ParserDescr

Prove a classical entailment, optionally supplying a search depth and hypotheses.

Equations

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