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

Given a and b the operands for and, apply the simplification rules:

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

Equations

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

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

Apply the following simplification/normalization rules on and :

• false && e ==> false
• true && e ==> e
• e && not e ==> false
• e1 && e2 ==> e1 (if e1 =ₚₜᵣ e2)
• e1 && e2 ===> e2 (if true = e1 := _ ∈ hypothesisContext.hypothesisMap)
• e1 && e2 ===> e1 (if true = e2 := _ ∈ hypothesisContext.hypothesisMap)
• e1 && e2 ===> false (if ∃ e := _ ∈ hypothesisContext.hypothesisMap, e = false = e1)
• e1 && e2 ===> false (if ∃ e := _ ∈ hypothesisContext.hypothesisMap, e = false = e2)
• e1 && e2 ==> e2 && e1 (if e2 <ₒ e1) Assume that f = Expr.const ``and. An error is triggered when args.size ≠ 2 (i.e., only fully applied and expected at this stage)

TODO: reordering on list of && must be performed to regroup all decide e together and all boolean expression together. The reordering must be deterministic to produce the same sequence. TODO: consider additional simplification rules

Equations

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

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

Given a and b the operands for or, apply the simplification rules:

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

Equations

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

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

Apply the following simplification/normalization rules on or :

• false || e ==> e
• true || e ==> true
• e || not e ==> true
• e1 || e2 ==> e1 (if e1 =ₚₜᵣ e2)
• e1 || e2 ===> true (if true = e1 := _ ∈ hypothesisContext.hypothesisMap)
• e1 || e2 ===> true (if true = e2 := _ ∈ hypothesisContext.hypothesisMap)
• e1 || e2 ===> e2 (if ∃ e := _ ∈ hypothesisContext.hypothesisMap, e = false = e1)
• e1 || e2 ===> e1 (if ∃ e := _ ∈ hypothesisContext.hypothesisMap, e = false = e2)
• e1 || e2 ==> e2 || e1 (if e2 <ₒ e1) Assume that f = Expr.const ``or. An error is triggered when args.size ≠ 2 (i.e., only fully applied or expected at this stage)

TODO: reordering on list of || must be performed to regroup all decide e together and all boolean expression together. The reordering must be deterministic to produce the same sequence. TODO: consider additional simplification rules

Equations

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