Core implementation of the inclusion tactic

This file defines the TacticM core of the inclusion tactic.

Implimentation Notes

The approach to the implimentation of the kernel == true and native == true options mirrors the approach used by the decide tactic (and reuses the code where possible).

structure Inclusion.InclusionConfig : Type

Configuration for the inclusion tactic.

• kernel : Bool

  If kernel == true then skip the compiled check.

• native : Bool

  If native == true then use compiled computation in the proof (warning: this adds the Lean compiler to the trusted codebase).

• paramSettings : Lean.NameMap Lean.Expr

  A map from inclusion parameter names to their user-supplied values.

• families : Array Lean.Name

  The names of the enabled inclusion extension families.

def Inclusion.compileInclusionCheck (inclusionExpr : Lean.Expr) : Lean.MetaM IntervalBool

Compile and evaluate the closed IntervalBool expression inclusionExpr.

Equations

• Inclusion.compileInclusionCheck inclusionExpr = Inclusion.compileInclusionCheck.unsafe_impl_2 inclusionExpr

def Inclusion.mkInclusionTrueProof (inclusionExpr : Lean.Expr) : Lean.MetaM Lean.Expr

Check that inclusionExpr equals IntervalBool.true using a compiled computation, and then pass the proof term to the kernel (where it will be verified again by reflection).

Equations

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

def Inclusion.mkKernelInclusionTrueProof (inclusionExpr : Lean.Expr) : Lean.MetaM Lean.Expr

Prove that inclusionExpr equals IntervalBool.true using kernel reduction (without any prior compiled check).

Equations

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

def Inclusion.mkNativeInclusionTrueProof (inclusionExpr : Lean.Expr) : Lean.MetaM Lean.Expr

Use native evaluation to prove that inclusionExpr equals IntervalBool.true.

Equations

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

def Inclusion.inclusionCore (goal : Lean.Expr) (config : InclusionConfig) : Lean.MetaM Lean.Expr

Prove goal, by constructing an exprInclusion for it and verifying that exprInclusion.inclusion evaluates to IntervalBool.true.

Equations

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