def Blaster.Optimize.mkImpliesExpr (a b : Lean.Expr) : TranslateEnvT Lean.Expr

mkImpliesExpr a b return expression a → b without applying any normalization.

Equations

• Blaster.Optimize.mkImpliesExpr a b = do let __do_lift ← Lean.Elab.Term.mkFreshBinderName pure (Lean.mkForall __do_lift Lean.BinderInfo.default a b)

def Blaster.Optimize.isCstImplies? (h a b : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given h : a → b, apply the simplification rules:

• When a := True ∧ Type(b) = Prop:
  • When ¬ fVarInExpr h.fvarId! b:
    • return some b
  • When fVarInExpr h.fvarId! b:
    • return some b[h/True.intro]
• When a := False ∧ Type(b) = Prop:
  • return some True
• Otherwise
  • return none

TODO: We need to find a way to replace h in body with the proper h in hypothesis.

Equations

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

def Blaster.Optimize.isNotDef? (a b : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given a → b, apply the following normalization rule:

• When b := False ∧ Type(a) = Prop
  • return some ¬ a
• Otherwise
  • return none

Equations

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

def Blaster.Optimize.impliesToNeg? (a b : Lean.Expr) (h : HypothesisMap) : TranslateEnvT (Option Lean.Expr)

Given a → b, apply the simplification rules:

• When ∃ e := _ ∈ h, e = ¬ b
  • return some ¬ a
• When ∃ e := _ ∈ hypothesisContext.hypothesisMap, e = ¬ b
  • return some ¬ a
• Otherwise:
  • return none

Equations

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

def Blaster.Optimize.impliesToTrue? (a b : Lean.Expr) (h : HypothesisMap) : TranslateEnvT (Option Lean.Expr)

Given a → b, apply the simplification rules:

• When ∃ e := _ ∈ h, e = b
  • return some True
• When ∃ e := _ ∈ hypothesisContext.hypothesisMap, e = b
  • return some True
• When ∃ e := _ ∈ hypothesisContext.hypothesisMap, e = ¬ a
  • return some True
• Otherwise:
  • return none

Equations

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

def Blaster.Optimize.impliesInHyp (h b : Lean.Expr) : TranslateEnvT Bool

Given h : a → b returns true only when the following condition is satisfied:

• ∃ h : a → b := _ ∈ hypothesisContext.hypothesisMap,

Equations

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

def Blaster.Optimize.hypReduction? (h a b : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given h : a → b, apply the simplification rules:

• When a := p ∈ hypothesisContext.hypothesisMap ∧ Type(b) = Prop
  • When ¬ fVarInExpr h.fvarId! b
    • return some b
  • When fVarInExpr h.fvarId! b
    • return `some b[h/p]
• Otherwise:
  • return none

Equations

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

def Blaster.Optimize.optimizeForall (n t : Lean.Expr) (h : HypothesisMap) (b : Lean.Expr) : TranslateEnvT Lean.Expr

Apply the following simplification/normalized rules on forallE. Note that implication a → b is internally represented as forallE _ a b bi. The simplification/normalization rules applied are: - ∀ (n : t), True | e → True ==> True - False → e ==> True (if Type(e) = Prop) - h : True → e ==> e (if Type(e) = Prop ∧ ¬ fVarInExpr h.fvarId! e) - h : True → e ==> e[h/True.intro] (if Type(e) = Prop ∧ fVarInExpr h.fvarId! e) TODO: replace True.intro with proper proof - e → False ==> ¬ e - e1 → e2 ==> True (if e1 =ₚₜᵣ e2 ∧ Type(e1) = Prop) - e1 → e2 ==> True (if ∃ e1 → e2 := _ ∈ hypothesisContext.hypothesisMap) - e1 → e2 ==> ¬ e1 (if ∃ e := _ ∈ h, e = ¬ e2) - e1 → e2 ==> ¬ e1 (if ∃ e := _ ∈ hypothesisContext.hypothesisMap, e = ¬ e2) - e1 → e2 ==> True (if e2 := _ ∈ h) - e1 → e2 ==> True (if e2 := _ ∈ hypothesisContext.hypothesisMap) - e1 → e2 ==> True (if ∃ e := _ ∈ hypothesisContext.hypothesisMap, e = ¬ e1 ∧ Type(e2) = Prop) - h : e1 → e2 ==> e2 (if e1 := _ ∈ hypothesisContext.hypothesisMap ∧ ¬ fVarInExpr h.fvarId! e2 ∧ Type(e2) = Prop) - h : e1 → e2 ==> e2[h/h'] (if e1 := h' ∈ hypothesisContext.hypothesisMap ∧ fVarInExpr h.fvarId! e2 ∧ Type(e2) = Prop ) - ∀ (n : t), e ===> e (if isSortOrInhabited t ∧ Type(e) = Prop ∧ ¬ fVarInExpr n.fvarId! e) Assume that n is a free variable expression. An error is triggered if this is not the case. Assume that h corresponds to the hypothesis map updated with hypotheses in t.

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.optimizeForall n t h (Lean.Expr.const `True us) = pure (Lean.Expr.const `True us)