def Blaster.Optimize.diteToPropExpr? (iteType cond thn els : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given thn and els corresponding respectively to the then and else terms of a Blaster.dite' expression, perform the following normalization rules:

• When Type(t) = Prop ∧ t := fun h : c => e1 ∧ e := fun h : ¬ c => e2
  • return (h : c → e1) ∧ (h : ¬ c → e2)
• When Type(t) = Prop ∧ t := c → Prop ∧ e := ¬ c → Prop
  • return (h : c → t h) ∧ (h : ¬ c → e h)
• When `Type(t) ≠ Prop:
  • return none
• Otherwise
  • return ⊥

Equations

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

def Blaster.Optimize.diteToPropExpr?.toImpliesExpr (ite c : Lean.Expr) : TranslateEnvT Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.diteToPropExpr?.toImpliesExpr (Lean.Expr.lam n t b bi) c = pure (Lean.mkForall n bi t b)

def Blaster.Optimize.isITEBoolSwap? (c : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Return some (true = c') only when c := false = c'. This function also checks if true = c' is already in cache. Otherwise none.

Equations

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

def Blaster.Optimize.extractDependentITEExpr (e : Lean.Expr) : TranslateEnvT Lean.Expr

Given e, a Blaster.dite' then/else expression perform the following:

• When e := fun h : c => b:
  • return b
• When Type(e) := h : c → b:
  • return e
• Otherwise:
  • return ⊥

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.extractDependentITEExpr (Lean.Expr.lam n t b bi) = pure b

def Blaster.Optimize.isITESwap? (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given an Blaster.dite' expression:

• return some sif h : c' then e2 else e1 when c := ¬ c'
• return some sif h : true = c' then e2 else e1 when c := false = c' Otherwise none.

Equations

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

def Blaster.Optimize.diteFactorize? (a t e : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given a, 'tande` the condition, then and else expressions for a Blaster.dite' expression,

• When t := sif h2 : c1 then e1 else e2 ∧ e := sif h3 : c2 then e1 else e2 ∧ ¬ c1.hasLooseBVars ∧ ¬ c2.hasLooseBVars

  • return some $ sif h1 : (a ∧ c1) ∨ (¬ a ∧ c2) then e1 else e2

• When t := sif h2 : c then e1 else e2 ∧ e := sif h2 : c then e1 else e3

  • return some $ sif h2 : c then e1 else (sif h1 : a then e2 else e3)

• When t := sif h2 : c then e1 else e2 ∧ e := sif h2 : c then e3 else e2

  • return some $ sif h2 : c then (sif h1 : a then e1 else e3) else e2

• When t := sif h2 : c then e1 else e2 ∧ e := sif h2 : c then e2 else e1

  • return some $ sif h3 : a = c then e1 else e2

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.diteFactorize? a t e = pure none

def Blaster.Optimize.optimizeDITEChoice (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Apply the following simplification/normalization rules on Solve.dite' in the given order only when args.size ≥ 4:

• sif h : True then e1 else e2 ==> applyExtraArgs e1 -- TODO: consider proof reconstruction

• sif h : False then e1 else e2 ==> applyExtraArgs e2 -- TODO: consider proof reconstruction

• sif h : c then e1 else e2 ==> applyExtraArgs e1 (if c := _ ∈ hypothesisContext.hypothesisMap ∧ ¬ e1.hasLooseBVars)

• sif h : c then e1 else e2 ==> applyExtraArgs e2 (if ∃ e := _ ∈ hypothesisContext.hypothesisMap ∧ ¬ e2.hasLooseBVars ∧ e = ¬ c )

• sif h : c then e1 else e2 ==> applyExtraArgs e1[h/h'] (if c := h' ∈ hypothesisContext.hypothesisMap ∧ e1.hasLooseBVars)

• sif h : c then e1 else e2 ==> applyExtraArgs e2[h/h'] (if ∃ e := h' ∈ hypothesisContext.hypothesisMap ∧ e2.hasLooseBVars ∧ e = ¬ c)

• sif h : c then e1 else e2 ==> (h : c → e1) ∧ (h : ¬ c → e2) (if Type(e1) = Prop) -- TO BE REMOVED: when performing normalization at the implication level

• (sif h : c then e1 else e2) x₁ ... xₙ ==> (sif h : c' then e2 else e1) x₁ ... xₙ (if c = ¬ c')

• (sif h : c then e1 else e2) x₁ ... xₙ ==> (sif h : true = c' then e2 else e1) x₁ ... xₙ (if c := false = c')

with applyExtraArgs e := if args.size > 4 then let extra_args := args.extract 4 args.size mkAppN e extra_args else e Note that this function is called only when dite conditional has been optimized, i.e., then and else terms still have to be optimized (see DiteChoiceWaitForCond logic in optimizeStack).

Assume that f = Expr.const ``Blaster.dite'

Equations

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

@[inline]

def Blaster.Optimize.optimizeDITEChoice.applyExtraArgs (args : Array Lean.Expr) (e : Lean.Expr) : Lean.Expr

Equations

• Blaster.Optimize.optimizeDITEChoice.applyExtraArgs args e = if args.size > 4 then have extra_args := args.extract 4; Lean.mkAppN e extra_args else e

def Blaster.Optimize.optimizeDITEChoice.diteReduce? (cond t : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given cond and t the condition and then/else expression for a Blaster.dite' expression, perform the following:

• When t := fun h : c => e ∧ c := _ ∈ hypothesisContext.hypothesisMap ∧ ¬ e.hasLooseBVars
  • return some e
• When t := fun h : c => e ∧ c := h' ∈ hypothesisContext.hypothesisMap ∧ e.hasLooseBVars
  • return some e[h/h']
• When t := c → α ∧ c := h ∈ hypothesisContext.hypothesisMap
  • return some t h
• Otherwise
  • return none

Equations

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

def Blaster.Optimize.optimizeDITE (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT Lean.Expr

Apply simplification/normalization rules on Blaster.dite' in the given order. Note that dependent ite is written with notation if h : c then t else e, which is now replaced with Blaster.dite' c (fun h : c => t) (fun h : ¬ c => e) to ignore the decidable instance. In the following simplification rules Blaster.dite' is annotated as sif h : c then th else eh to facilitate comprehension.

The simplifcation/normalization rules applied are:

• sif h : c then e1 else e2 ==> e1 (if e1 =ₚₜᵣ e2)

• sif h1 : a then (sif h2 : c1 then e1 else e2) else (sif h3 : c2 then e1 else e2) ==> sif h1 : (a ∧ c1) ∨ (¬ a ∧ c2) then e1 else e2 (if ¬ c1.hasLooseBVars ∧ ¬ c2.hasLooseBVars) -- NOTE: rule is sound as h1, h2 and h3 can't be referenced in e1 and e2.

• sif h1 : a then (sif h2 : c then e1 else e2) else (sif h2 : c then e1 else e3) ==> sif h2 : c then e1 else (sif h1 : a then e2 else e3) -- NOTE: rule is sound as h1 can't be referenced in c and e1 but h1 and h2 can be referenced in e2 and e3.

• sif h1 : a then (sif h2 : c then e1 else e2) else (sif h2 : c then e3 else e2) ==> sif h2 : c then (sif h1 : a then e1 else e3) else e2 -- NOTE: rule is sound as h1 can't be referenced in c and e2 but h1 and h2 can be referenced in e1 and e3.

• sif h1 : a then (sif h2 : c then e1 else e2) else (if h2 : c then e2 else e1) ==> sif h3 : a = c then e1 else e2 -- NOTE: rule is sound as h1 and h2 can't be referenced in e1 and e2 and h1 can't be referenced in c.

Assume that f = Expr.const ``Blaster.dite' An error is triggered when args.size ≠ 4 (i.e., only fully applied dite' expected at this stage)

Equations

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