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

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

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

Equations

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

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

Apply the following simplification/normalization rules on And :

• False ∧ e ==> False
• True ∧ e ==> e
• e1 ∧ e2 ==> e1 (if e1 =ₚₜᵣ e2)
• e ∧ ¬ e ==> False
• true = e ∧ false = e ==> False
• e1 ∧ (e1 → e2) ==> e1 ∧ e2 (if ¬ e2.hasLooseBVars)
• e1 ∧ (e2 → e1) ==> e1
• (e1 → e2) ∧ (¬ e1 → e2) ==> e2
• e1 ∧ e2 ==> e2 (if e1 := _ ∈ hypothesisContext.hypothesisMap)
• e1 ∧ e2 ==> e1 (if e2 := _ ∈ hypothesisContext.hypothesisMap)
• e1 ∧ e2 ==> False (if ∃ e := _ ∈ hypothesisContext.hypothesisMap, e = ¬ e1)
• e1 ∧ e2 ==> False (if ∃ e := _ ∈ hypothesisContext.hypothesisMap, e = ¬ 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: consider additional simplification rules

Equations

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

def Blaster.Optimize.optimizeAnd.andImpliesReduce? (f a b : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

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

• When b := a → c ∧ ¬ c.hasLooseBVars
  • return some a ∧ c
• When b := c → a
  • return some a
• When a := c → d ∧ b := ¬ c → d
  • return some d
• Otherwise:
  • return none

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.optimizeAnd.andImpliesReduce? f a b = pure none

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

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

• When a := _ ∈ hypothesisContext.hypothesisMap,
  • return some True
• When b := _ ∈ hypothesisContext.hypothesisMap,
  • return some True
• When ∃ e := _ ∈ hypothesisContext.hypothesisMap, e = ¬ a
  • return some b
• 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.orImpliesReduce? (a b : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

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

• When b := a → c
  • return some True
• When b := c → a
  • return some b
• Otherwise:
  • return none

Equations

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

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

Apply the following simplification/normalization rules on Or :

• False ∨ e ==> e
• True ∨ e ==> True
• e1 ∨ e2 ==> e1 (if e1 =ₚₜᵣ e2)
• e ∨ ¬ e ==> True (classical)
• true = e ∨ false = e ==> True
• e1 ∨ (e1 → e2) ==> True
• e1 ∨ (e2 → e1) ==> (e2 → e1)
• e1 ∨ e2 ==> True (if e1 := _ ∈ hypothesisContext.hypothesisMap)
• e1 ∨ e2 ==> True (if e2 := _ ∈ hypothesisContext.hypothesisMap)
• e1 ∨ e2 ==> e2 (if ∃ e := _ ∈ hypothesisContext.hypothesisMap, e = ¬ e1)
• e1 ∨ e2 ==> e1 (if ∃ e := _ ∈ hypothesisContext.hypothesisMap, e = ¬ 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: consider additional simplification rules

Equations

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

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

Normalize p ↔ p to p → q ∧ p → q An error is triggered when args.size ≠ 2 (i.e., only fully applied ↔ expected at this stage)

Equations

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