partial def Blaster.Optimize.structEq? (op1 op2 : Lean.Expr) : TranslateEnvT (Option Bool)

Return some true if op1 and op2 are constructors that are structurally equivalent modulo variable name/function equivalence Return some false if op1 and op2 are constructors that are NOT structurally equivalent. Return none otherwise. Assume that memoization is performed on expressions.

partial def Blaster.Optimize.structEq?.visit (op1 op2 : Lean.Expr) : TranslateEnvT (Option Bool)

def Blaster.Optimize.structEq?.updateLattice : Option Bool → Option Bool → Option Bool

update the lattice for application arguments such that:

• some true corresponds to the bottom element
• some false corresponds to the top element (the identity element)
• some none the middle element The join rules applied on update are the following:
• some true, some false ==> some false
• none, some false ==> some false
• some false, some false ==> some false
• some true, none ==> none
• none, none ==> none
• some true, some true ==> some true

Equations

• Blaster.Optimize.structEq?.updateLattice (some false) x✝ = some false
• Blaster.Optimize.structEq?.updateLattice x✝ (some false) = some false
• Blaster.Optimize.structEq?.updateLattice none x✝ = none
• Blaster.Optimize.structEq?.updateLattice x✝ none = none
• Blaster.Optimize.structEq?.updateLattice (some true) (some true) = some true

def Blaster.Optimize.structEq?.isTop : Option Bool → Bool

Equations

• Blaster.Optimize.structEq?.isTop (some false) = true
• Blaster.Optimize.structEq?.isTop x✝ = false

def Blaster.Optimize.zeroEqNegReduce? (op1 op2 eqType : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

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

def Blaster.Optimize.natZeroEqMulReduce? (op1 op2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

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

def Blaster.Optimize.intZeroEqMulReduce? (op1 op2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

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

def Blaster.Optimize.natAddEqReduce? (op1 op2 : Lean.Expr) : TranslateEnvT (Option (Lean.Expr × Lean.Expr))

Equations

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

def Blaster.Optimize.intAddEqReduce? (op1 op2 : Lean.Expr) : TranslateEnvT (Option (Lean.Expr × Lean.Expr))

Equations

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

def Blaster.Optimize.natMulEqReduce? (op1 op2 : Lean.Expr) : TranslateEnvT (Option (Lean.Expr × Lean.Expr))

Equations

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

def Blaster.Optimize.intMulEqReduce? (op1 op2 : Lean.Expr) : TranslateEnvT (Option (Lean.Expr × Lean.Expr))

Equations

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

def Blaster.Optimize.intEqReduce? (op1 op2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given op1 and op2 corresponding to the operands for Eq:

• return some False when op1 := N + e ∧ op2 := e ∧ N ≠ 0 ∧ Type(N) = Int
• return some False when op1 := a + b ∧ op2 := a ∧ Type(a) = Int ∧ nonZeroIntInHyps b
• return some False when op1 := b + a ∧ op2 := a ∧ Type(a) = Int ∧ nonZeroIntInHyps b Otherwise none.

Equations

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

def Blaster.Optimize.natEqReduce? (op1 op2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given op1 and op2 corresponding to the operands for Eq:

• return some False when op1 := N + e ∧ op2 := e ∧ N ≠ 0 ∧ Type(N) = Nat
• return some False when op1 := a + b ∧ op2 := a ∧ Type(a) = Nat ∧ nonZeroNatInHyps b
• return some False when op1 := b + a ∧ op2 := a ∧ Type(a) = Nat ∧ nonZeroNatInHyps b Otherwise none.

Equations

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

def Blaster.Optimize.addNatEqReduce? (op1 op2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given op1 and op2 corresponding to the operands for Eq:

• return some False when op1 := N1 ∧ op2 := N2 + a ∧ N1 < N2 ∧ Type(a) = Nat:
• return some N1 "-" N2 = a when op1 := N1 ∧ op2 := N2 + a ∧ N1 ≥ N2 ∧ Type(a) = Nat:
• return some N1 "-" min(N1, N2) + a = N2 "-" min(N1, N2) + b when op1 := N1 + a ∧ op2 := N2 + b ∧ Type(a) = Nat: Otherwise none.

Equations

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

def Blaster.Optimize.addIntEqReduce? (op1 op2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given op1 and op2 corresponding to the operands for Eq:

• return some N1 "-" N2 = a when op1 := N1 ∧ op2 := N2 + a ∧ Type(a) = Int:
• return some N1 "-" min(N1, N2) + a = N2 "-" min(N1, N2) + b when op1 := N1 + a ∧ op2 := N2 + b ∧ Type(a) = Int: Otherwise none.

Equations

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

def Blaster.Optimize.arithEq? (op1 op2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Apply the following simplification/normalization rules on Eq :

• N + e = e | e = N + e ==> False (if Type(e) ∈ [Nat, Int])
• a + b = a | a = a + b | b + a = a | a = b + a ==> False (if Type(a) ∈ [Nat, Int] ∧ nonZeroInHyps b)
• N2 = N1 + a ==> False (if Type(a) = Nat) ∧ N2 < N1)
• N2 = N1 + a ==> N2 "-" N1 = a (if Type(a) = Nat) if N2 ≥ N1) (restart)
• N2 = N1 + a ===> N2 "-" N1 = a (if Type(a) = Int) (restart)
• N1 + a = N2 + b ==> N1 "-" min(N1, N2) + a = N2 "-" min(N1, N2) + b (if Type(a) ∈ [Nat, Int]) with: nonZeroInHyps x := nonZeroNatInHyps x If Type(x) = Nat := nonZeroIntInHyps x Otherwise

Equations

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

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

Apply the following simplification/normalization rules on Eq :

• False = e ==> ¬ e
• True = e ==> e
• e = ¬ e ==> False
• e = not e ==> False
• e1 = e2 ==> True (if e1 =ₚₜᵣ e2)
• e1 = e2 ==> False (if structEq? e1 e2 = some false) (NOTE: some true case already handled by =ₚₜᵣ)
• true = not e ==> false = e
• false = not e ==> true = e
• ¬ e1 = ¬ e2 ==> e1 = e2 (require classical)
• not e1 = not e2 ==> e1 = e2
• 0 = (-e) ==> 0 = e (if Type(e) = Int)
• -e1 = -e2 ==> e1 = e2 (if Type(e1) = Int)
• 0 = x * y ==> False (if Type(x) ∈ [Nat, Int] ∧ nonZeroInHyps x ∧ nonZeroInHyps y)
• e1 = e2 ==> r (if some r ← arithEq? e1 e2)
• x + y = x + z | y + x = x + z | x + y = z + x | y + x = z + x ==> y = z (if Type(x) ∈ [Nat, Int]]
• x * y = x * z | y * x = x * z | x * y = z * x | y * x = z * x ==> y = z (if Type(x) ∈ [Nat, Int] ∧ nonZeroInHyps x]
• e1 = e2 ==> e2 = e1 (if e2 <ₒ e1) with: nonZeroInHyps x := nonZeroNatInHyps x If Type(x) = Nat := nonZeroIntInHyps x Otherwise Assume that f = Expr.const ``Eq. Do nothing if operator is partially applied (i.e., args.size < 3)

TODO: consider additional simplification rules TODO: seperate rewriting that require classical reasoning from others. TODO: add an option to activate/deactivate classical simplification (same for optimizeProp).

Equations

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

def Blaster.Optimize.optimizeEq.intNegEqReduce? (op1 op2 : Lean.Expr) : TranslateEnvT (Option (Lean.Expr × Lean.Expr))

Equations

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

def Blaster.Optimize.optimizeEq.notNegEqSimp? (op1 op2 : Lean.Expr) : TranslateEnvT (Option (Lean.Expr × Lean.Expr))

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.optimizeEq.notNegEqSimp? (Lean.Expr.const `Bool.true us) op2 = do Blaster.Optimize.setRestart let __do_lift ← Blaster.Optimize.mkBoolFalse pure (some (__do_lift, e))
• Blaster.Optimize.optimizeEq.notNegEqSimp? (Lean.Expr.const `Bool.false us) op2 = do Blaster.Optimize.setRestart let __do_lift ← Blaster.Optimize.mkBoolTrue pure (some (__do_lift, e))
• Blaster.Optimize.optimizeEq.notNegEqSimp? op1✝ op2 = do Blaster.Optimize.setRestart pure (some (e1, e2))

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

Apply the following simplification/normalization rules on BEq.beq :

• false == e ==> not e
• true == e ==> e
• e == not e ==> false
• e1 == e2 ==> true (if e1 =ₚₜᵣ e2)
• e1 = e2 ==> false (if structEq? e1 e2 = some false) (NOTE: some true case already handled by =ₚₜᵣ)
• not e1 == not e2 ==> e1 == e2
• e1 == e2 ==> e2 == e1 (if e2 <ₒ e1)

Assume that f = Expr.const ``BEq.beq. This function simply returns the function application when:

• `BEq.beq is partially applied (i.e., args.size < 4)
• isOpaqueRelational f.constName args is not satisfied.

NOTE: The above simplification rules are applied only on BEq.beq satisfiying isOpaqueRelational predicate. In fact, we can't assume that BEq.beq will properly be defined for user-defined types or parametric inductive types.

NOTE: BEq.beq is expected to be unfolded if isOpaqueRelational predicate is not satisfied. However, class constraint [BEq α] for which there is no defined instance the unfolding will not be performed (see getUnfoldFunDef?).

TODO: consider additional simplification rules

Equations

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

def Blaster.Optimize.optimizeBEq.boolNotEqReduce? (f : Lean.Expr) (args : Array Lean.Expr) (op1 op2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given op1 and op2 corresponding to the operands for BEq.beq, return some e1 == e2 when op1 := not e1 ∧ op2 := not e2. Otherwise none.

Equations

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

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

Equations

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

def Blaster.Optimize.optimizeDecideEq.isBeqCompatibleType? (e : Lean.Expr) : TranslateEnvT (Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr))

Equations

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

def Blaster.Optimize.optimizeDecideEq.mkBeqToEq (f beq_sort beq_op1 beq_op2 c : Lean.Expr) : TranslateEnvT Lean.Expr

Equations

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

def Blaster.Optimize.optimizeDecideEq.beqToEq? (f op1 op2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

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

def Blaster.Optimize.optimizeDecideEq.boolEqtoEq? (f op1 op2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

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

def Blaster.Optimize.optimizeDecideEq.decideBoolEqSimp? (op1 op2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.optimizeDecideEq.decideBoolEqSimp? (Lean.Expr.const `Bool.true us) op2 = pure (some e)
• Blaster.Optimize.optimizeDecideEq.decideBoolEqSimp? op1✝ op2 = pure none

def Blaster.Optimize.optimizeDecideEq.decideEqDecide? (f op1 op2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

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

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

Apply simplification and normalization rules on Eq and BEq.beq :

Equations

• Blaster.Optimize.optimizeEquality? (Lean.Expr.const `Eq us) args = do let a ← Blaster.Optimize.optimizeDecideEq (Lean.Expr.const `Eq us) args pure (some a)
• Blaster.Optimize.optimizeEquality? (Lean.Expr.const `BEq.beq us) args = do let a ← Blaster.Optimize.optimizeBEq (Lean.Expr.const `BEq.beq us) args pure (some a)
• Blaster.Optimize.optimizeEquality? (Lean.Expr.const n us) args = pure none
• Blaster.Optimize.optimizeEquality? f args = pure none