Expr helpers for the inclusion tactic

This file defines helpers for matching or building certain expressions that are used in the core of the inclusion tactic.

def Inclusion.toSetMem? (e : Lean.Expr) : Option (Lean.Expr × Lean.Expr × Lean.Expr)

If e is an Expr of the form x ∈ s using a ToSet instance, return some (x, s, toSetInst).

Equations

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

def Inclusion.mkToSetMem (xType setType x s toSetInst : Lean.Expr) : Lean.MetaM Lean.Expr

Given expressions x : xType, s : setType, and toSetInst : ToSet setType xType, create the expression x ∈ s.

Equations

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

def Inclusion.IExpr.mkMem (iExpr : IExpr) (set : Lean.Expr) : Lean.MetaM Lean.Expr

Given iExpr : IExpr and set : iExpr.iType.setType, create the expression iExpr.expr ∈ set.

Equations

• iExpr.mkMem set = Inclusion.mkToSetMem iExpr.iType.elemType iExpr.iType.setType iExpr.expr set iExpr.iType.toSetInst

def Inclusion.IVar.mkCoverMap (iVar : IVar) (outputType : IType) (source cover coarsen inclusion : Lean.Expr) : Lean.MetaM Lean.Expr

Given

· source : iVar.type.setType, · outputType : IType, · cover : Cover iVar.type.setType iVar.type.elemType, · coarsen : Coarsen outputType.setType outputType.elemType, and · inclusion : iVar.type.setType → outputType.setType,

create the expression cover.coverMap source inclusion : outputType.setType.

Equations

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

def Inclusion.IVar.mkCoverMapProof (iVar : IVar) (output : IExpr) (source : ExprInclusionBody) (cover coarsen inclusion proof : Lean.Expr) : Lean.MetaM Lean.Expr

Given

· a source inclusion body for iVar, · output : IExpr, · cover : Cover iVar.type.setType iVar.type.elemType, · coarsen : Coarsen output.iType.setType output.iType.elemType, · inclusion : iVar.type.setType → output.iType.setType, and · proof : ∀ s, iVar.expr ∈ s → output.expr ∈ inclusion s,

create a proof of output.expr ∈ cover.coverMap source.inclusionBody inclusion.

Equations

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

def Inclusion.IType.synthCoarsen (iType : IType) : Lean.MetaM Lean.Expr

Given iType : IType, synthesize an expression of type Coarsen iType.setType iType.elemType.

Equations

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

def Inclusion.IType.mkRefine (iType : IType) (refiner left right : Lean.Expr) : Lean.MetaM Lean.Expr

Given iType : IType, refiner : Refine iType.setType iType.elemType, and expressions left right : iType.setType, create the expression refiner.refine left right.

Equations

• iType.mkRefine refiner left right = Lean.Meta.mkAppOptM `Inclusion.Refine.refine #[some iType.setType, some iType.elemType, some iType.toSetInst, some refiner, some left, some right]

def Inclusion.IType.synthRefine (iType : IType) : Lean.MetaM Lean.Expr

Given iType : IType, synthesize an expression of type Refine iType.setType iType.elemType.

Equations

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

def Inclusion.IType.mkUniv (iType : IType) (univ : Lean.Expr) : Lean.MetaM Lean.Expr

Given iType : IType and univ : Univ iType.setType iType.elemType, create the expression univ.univ : iType.setType.

Equations

• iType.mkUniv univ = Lean.Meta.mkAppOptM `Inclusion.Univ.univ #[some iType.setType, some iType.elemType, some iType.toSetInst, some univ]

def Inclusion.IExpr.mkMemUniv (iExpr : IExpr) (univ : Lean.Expr) : Lean.MetaM Lean.Expr

Given iExpr : IExpr and univ : Univ iExpr.iType.setType iExpr.iType.elemType, create a proof of iExpr.expr ∈ univ.univ.

Equations

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

def Inclusion.IType.synthUniv (iType : IType) : Lean.MetaM Lean.Expr

Given iType : IType, synthesize an expression of type Univ iType.setType iType.elemType.

Equations

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

def Inclusion.mkIntervalBoolRefl (b : Lean.Expr) : Lean.Expr

Given an expression b : IntervalBool, create the expression proving b = b.

Equations

• Inclusion.mkIntervalBoolRefl b = Lean.mkApp2 (Lean.mkConst `Eq.refl [Lean.Level.zero.succ]) (Lean.mkConst `Inclusion.IntervalBool) b

def Inclusion.ExprInclusion.mkGoalProof (inc : ExprInclusion) (goal inclusionProof : Lean.Expr) : Lean.Expr

Given an ExprInclusion inc for goal, and a proof inclusionProof : inc.inclusion = IntervalBool.true create a proof of goal.

Equations

• inc.mkGoalProof goal inclusionProof = Lean.mkAppN (Lean.mkConst `Inclusion.true_of_mem_intervalBool_eq_true) #[goal, inc.inclusion, inc.proof, inclusionProof]