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

Apply the following simplification/normalization rules on Int.neg :

• • (N) ==> "-" N
• • (- n) ==> n Assume that f = Expr.const ``Int.neg. An error is triggered if args.size ≠ 1 (i.e., only fully applied Int.neg 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.optimizeIntAdd (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT Lean.Expr

Apply the following simplification/normalization rules on Int.add :

• 0 + n ==> n
• N1 + N2 ==> N1 "+" N2
• N1 + (N2 + n) ==> (N1 "+" N2) + n
• N1 + -(N2 + n) ==> (N1 "-" N2) + -n
• n1 + (-n2) ==> 0 if (if n1 =ₚₜᵣ n2)
• n1 + n2 ==> n2 + n1 (if n2 <ₒ n1) Assume that f = Expr.const ``Int.add. An error is triggered when args.size ≠ 2 (i.e., only fully applied Int.add expected at this stage)

Equations

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

@[inline]

def Blaster.Optimize.optimizeIntAdd.cstAddProp? (f : Lean.Expr) (mv1 : Option Int) (op2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.optimizeIntAdd.cstAddProp? f none op2 = pure none

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

Apply the following simplification/normalization rules on Int.mul :

• 0 * n ==> 0
• 1 * n ==> n
• -1 * n ==> -n
• N1 * N2 ==> N1 "*" N2
• N1 * (N2 * n) ==> (N1 "*" N2) * n
• n1 * n2 ==> n2 * n1 (if n2 <ₒ n1) Assume that f = Expr.const ``Int.mul. An error is triggered when args.size ≠ 2 (i.e., only fully applied Int.mul expected at this stage)

Equations

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

@[inline]

def Blaster.Optimize.optimizeIntMul.cstMulProp? (f : Lean.Expr) (mv1 : Option Int) (op2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

• Blaster.Optimize.optimizeIntMul.cstMulProp? f (some n1) op2 = do let __do_lift ← Blaster.Optimize.evalBinIntOp Int.mul n1 n2 pure (some (Lean.mkApp2 f __do_lift e2))
• Blaster.Optimize.optimizeIntMul.cstMulProp? f mv1✝ op2 = pure none

@[inline]

def Blaster.Optimize.intDivSelfReduce? (e1 e2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given e1 and e2 corresponding to the operands for Int.ediv, Int.tdiv and Int.fdiv, return some 1 only when the following conditions are satisfied:

• e1 =ₚₜᵣ e2 ∧
• 0 < e1 := _ ∈ hypothesisContext.hypothesisMap ∨ e1 < 0 := _ ∈ hypothesisContext.hypothesisMap ∨ ¬ (0 = e1) := _ ∈ hypothesisContext.hypothesisMap Otherwise, return none.

Equations

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

@[inline]

def Blaster.Optimize.mulIntDivReduceExpr? (e1 e2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given e1 and e2 corresponding to the operands for Int.ediv, Int.tdiv and Int.fdiv, return some n only when one of the following conditions is satisfied:

• e1 := m * n ∧ e2 = m ∧ ( 0 < m := _ ∈ hypothesisContext.hypothesisMap ∨ m < 0 := _ ∈ hypothesisContext.hypothesisMap ∨ ¬ (0 = m) := _ ∈ hypothesisContext.hypothesisMap ); or
• e1 := n * m ∧ e2 = m ∧ ( 0 < m := _ ∈ hypothesisContext.hypothesisMap ∨ m < 0 := _ ∈ hypothesisContext.hypothesisMap ∨ ¬ (0 = m) := _ ∈ hypothesisContext.hypothesisMap ); Otherwise, return none.

Equations

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

@[inline]

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

Given op1 and op2 corresponding to the operands for Int.ediv, Int.tdiv and Int.fdiv, try to apply the following simplification rules:

• n / 0 ==> 0
• n / 1 ==> n
• 0 / n ==> 0
• N1 / N2 ==> N1 "/" N2
• n / n ==> 1 (if 0 < n := _ ∈ hypothesisContext.hypothesisMap ∨ ¬ (0 = n) := _ ∈ hypothesisContext.hypothesisMap ∨ n < 0 := _ ∈ hypothesisContext.hypothesisMap )
• (m * n) / m | (n * m) / m ==> n (if 0 < m := _ ∈ hypothesisContext.hypothesisMap ∨ ¬ (0 = m) := _ ∈ hypothesisContext.hypothesisMap ∨ m < 0 := _ ∈ hypothesisContext.hypothesisMap)

Equations

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

@[inline]

def Blaster.Optimize.cstCommonDivProp? (op1 op2 : Lean.Expr) (f_div : Int → Int → Int) : TranslateEnvT (Option (Lean.Expr × Lean.Expr))

Equations

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

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

Apply the following simplification/normalization rules on Int.ediv:

• n / 0 ==> 0
• n / 1 ==> n
• 0 / n ==> 0
• N1 / N2 ==> N1 "/ₑ" N2
• n / n ==> 1 (if 0 < n := _ ∈ hypothesisContext.hypothesisMap ∨ ¬ (0 = n) := _ ∈ hypothesisContext.hypothesisMap ∨ n < 0 := _ ∈ hypothesisContext.hypothesisMap )
• (m * n) / m | (n * m) / m ==> n (if 0 < m := _ ∈ hypothesisContext.hypothesisMap ∨ ¬ (0 = m) := _ ∈ hypothesisContext.hypothesisMap ∨ m < 0 := _ ∈ hypothesisContext.hypothesisMap)
• (N1 * n) / N2 ===> ((N1 "/" Int.gcd N1 N2) * n) / (N2 "/ₑ" Int.gcd N1 N2) (if N2 ≠ 0 ∧ Int.gcd N1 N2 ≠ 1) Assume that f = Expr.const ``Int.ediv. An error is triggered when args.size ≠ 2 (i.e., only fully applied Int.ediv expected at this stage)

Equations

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

@[inline]

def Blaster.Optimize.intModToZeroExpr? (e1 e2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given e1 and e2 corresponding to the operands for Int.emod, Int.fmod and Int.tmod, return some 0 only when one of the following conditions is satisfied:

• e1 =ₚₜᵣ e2; or
• e1 := m * n ∧ e2 = m; or
• e1 := n * m ∧ e2 = m; Otherwise, return none.

Equations

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

@[inline]

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

Given op1 and op2 corresponding to the operands for Int.emod, Int.fmod and Int.tmod, try to apply the following simplification rules:

• n % 0 ==> n
• n % 1 ==> 0
• 0 % n ==> 0
• N1 % N2 ==> N1 "%" N2
• (N1 * n) % N2 ==> 0 (if N1 % N2 = 0)
• n1 % n2 ==> 0 (if n1 =ₚₜᵣ n2)
• (m * n) % m | (n * m) % m ==> 0

Equations

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

@[inline]

def Blaster.Optimize.optimizeIntModCommon.cstModProp? (op1 : Lean.Expr) (mv2 : Option Int) : TranslateEnvT (Option Lean.Expr)

Equations

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

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

Apply the following simplification/normalization rules on Int.emod :

• n % 0 ==> n
• n % 1 ==> 0
• 0 % n ==> 0
• N1 % N2 ==> N1 "%" N2
• (N1 * n) % N2 ==> 0 (if N1 % N2 = 0)
• n1 % n2 ==> 0 (if n1 =ₚₜᵣ n2)
• (m * n) % m | (n * m) % m ==> 0 Assume that f = Expr.const ``Int.emod. An error is triggered when args.size ≠ 2 (i.e., only fully applied Int.emod expected at this stage)

Equations

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

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

Apply the following simplification/normalization rules on Int.tdiv:

• n / 0 ==> 0
• n / 1 ==> n
• 0 / n ==> 0
• N1 / N2 ==> N1 "/" N2
• n / n ==> 1 (if 0 < n := _ ∈ hypothesisContext.hypothesisMap ∨ ¬ (0 = n) := _ ∈ hypothesisContext.hypothesisMap ∨ n < 0 := _ ∈ hypothesisContext.hypothesisMap )
• (m * n) / m | (n * m) / m ==> n (if 0 < m := _ ∈ hypothesisContext.hypothesisMap ∨ ¬ (0 = m) := _ ∈ hypothesisContext.hypothesisMap ∨ m < 0 := _ ∈ hypothesisContext.hypothesisMap)
• (n / N1) / N2 ==> n / (N1 "*" N2) (only valid for Int.tdiv)
• (N1 * n) / N2 ===> ((N1 "/" Int.gcd N1 N2) * n) / (N2 "/" Int.gcd N1 N2) (if N2 ≠ 0 ∧ Int.gcd N1 N2 ≠ 1) Assume that f = Expr.const ``Int.tdiv. An error is triggered when args.size ≠ 2 (i.e., only fully applied Int.tdiv expected at this stage)

Equations

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

@[inline]

def Blaster.Optimize.optimizeIntTDiv.cstTDivProp? (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.optimizeIntTMod (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT Lean.Expr

Apply the following simplification/normalization rules on Int.tmod :

• n % 0 ==> n
• n % 1 ==> 0
• 0 % n ==> 0
• N1 % N2 ==> N1 "%" N2
• (N1 * n) % N2 ==> 0 (if N1 % N2 = 0)
• n1 % n2 ==> 0 (if n1 =ₚₜᵣ n2)
• (m * n) % m | (n * m) % m ==> 0 Assume that f = Expr.const ``Int.tmod. An error is triggered when args.size ≠ 2 (i.e., only fully applied Int.tmod expected at this stage)

Equations

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

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

Apply the following simplification/normalization rules on Int.fdiv:

• n / 0 ==> 0
• n / 1 ==> n
• 0 / n ==> 0
• N1 / N2 ==> N1 "/" N2
• n / n ==> 1 (if 0 < n := _ ∈ hypothesisContext.hypothesisMap ∨ ¬ (0 = n) := _ ∈ hypothesisContext.hypothesisMap ∨ n < 0 := _ ∈ hypothesisContext.hypothesisMap )
• (m * n) / m | (n * m) / m ==> n (if 0 < m := _ ∈ hypothesisContext.hypothesisMap ∨ ¬ (0 = m) := _ ∈ hypothesisContext.hypothesisMap ∨ m < 0 := _ ∈ hypothesisContext.hypothesisMap)
• (N1 * n) / N2 ===> ((N1 "/" Int.gcd N1 N2) * n) / (N2 "/" Int.gcd N1 N2) (if N2 ≠ 0 ∧ Int.gcd N1 N2 ≠ 1) Assume that f = Expr.const ``Int.fdiv. An error is triggered when args.size ≠ 2 (i.e., only fully applied Int.fdiv expected at this stage)

Equations

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

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

Apply the following simplification/normalization rules on Int.fmod :

• n % 0 ==> n
• n % 1 ==> 0
• 0 % n ==> 0
• N1 % N2 ==> N1 "%" N2
• (N1 * n) % N2 ==> 0 (if N1 % N2 = 0)
• n1 % n2 ==> 0 (if n1 =ₚₜᵣ n2)
• (m * n) % m | (n * m) % m ==> 0 Assume that f = Expr.const ``Int.fmod. An error is triggered when args.size ≠ 2 (i.e., only fully applied Int.fmod expected at this stage)

Equations

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

@[inline]

def Blaster.Optimize.intNegOfNat? (n : Lean.Expr) : Option Lean.Expr

Return some e if n := Int.neg (Int.ofNat e). Otherwise return none.

Equations

• Blaster.Optimize.intNegOfNat? n = match Blaster.Optimize.intNeg? n with | some e => e.app1? `Int.ofNat | none => none

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

Apply the following simplification rules on Int.toNat :

• Int.toNat N1 ===> "Int.toNat" N1
• Int.toNat (Int.ofNat e) ===> e
• Int.toNat (Int.neg (Int.ofNat e)) ===> 0 Assume that f = Expr.const ``Int.toNat. An error is triggered if args.size ≠ 1.

Equations

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

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

Normalize Int.negSucc n to Int.neg (Int.ofNat (1 + n)) only when n is not a constant value. An error is triggered if args.size ≠ 1. Assume that f = Expr.const ``Int.negSucc. NOTE: This rule is still required here to avoid normalizationg Int.negSucc when n is a constant value.

Equations

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

@[inline]

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

Apply simplification/normalization rules on Int operators.

Equations

• Blaster.Optimize.optimizeInt? (Lean.Expr.const `Int.add us) args = do let a ← Blaster.Optimize.optimizeIntAdd (Lean.Expr.const `Int.add us) args pure (some a)
• Blaster.Optimize.optimizeInt? (Lean.Expr.const `Int.mul us) args = do let a ← Blaster.Optimize.optimizeIntMul (Lean.Expr.const `Int.mul us) args pure (some a)
• Blaster.Optimize.optimizeInt? (Lean.Expr.const `Int.neg us) args = do let a ← Blaster.Optimize.optimizeIntNeg (Lean.Expr.const `Int.neg us) args pure (some a)
• Blaster.Optimize.optimizeInt? (Lean.Expr.const `Int.negSucc us) args = do let a ← Blaster.Optimize.optimizeIntNegSucc (Lean.Expr.const `Int.negSucc us) args pure (some a)
• Blaster.Optimize.optimizeInt? (Lean.Expr.const `Int.toNat us) args = do let a ← Blaster.Optimize.optimizeIntToNat (Lean.Expr.const `Int.toNat us) args pure (some a)
• Blaster.Optimize.optimizeInt? (Lean.Expr.const `Int.ediv us) args = do let a ← Blaster.Optimize.optimizeIntEDiv (Lean.Expr.const `Int.ediv us) args pure (some a)
• Blaster.Optimize.optimizeInt? (Lean.Expr.const `Int.emod us) args = do let a ← Blaster.Optimize.optimizeIntEMod (Lean.Expr.const `Int.emod us) args pure (some a)
• Blaster.Optimize.optimizeInt? (Lean.Expr.const `Int.tdiv us) args = do let a ← Blaster.Optimize.optimizeIntTDiv (Lean.Expr.const `Int.tdiv us) args pure (some a)
• Blaster.Optimize.optimizeInt? (Lean.Expr.const `Int.tmod us) args = do let a ← Blaster.Optimize.optimizeIntTMod (Lean.Expr.const `Int.tmod us) args pure (some a)
• Blaster.Optimize.optimizeInt? (Lean.Expr.const `Int.fdiv us) args = do let a ← Blaster.Optimize.optimizeIntFDiv (Lean.Expr.const `Int.fdiv us) args pure (some a)
• Blaster.Optimize.optimizeInt? (Lean.Expr.const `Int.fmod us) args = do let a ← Blaster.Optimize.optimizeIntFMod (Lean.Expr.const `Int.fmod us) args pure (some a)
• Blaster.Optimize.optimizeInt? (Lean.Expr.const n us) args = pure none
• Blaster.Optimize.optimizeInt? f args = pure none