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

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

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

Equations

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

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

Equations

• Blaster.Optimize.optimizeNatAdd.cstAddProp? f (some n1) op2 = do let __do_lift ← Blaster.Optimize.evalBinNatOp Nat.add n1 n2 pure (some (Lean.mkApp2 f __do_lift e2))
• Blaster.Optimize.optimizeNatAdd.cstAddProp? f mv1✝ op2 = pure none

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

Apply the following simplification/normalization rules on Nat.sub :

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

Equations

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

def Blaster.Optimize.optimizeNatSub.cstSubPropRight? (f : Lean.Expr) (mv1 : Option Nat) (op2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.optimizeNatSub.cstSubPropRight? f mv1✝ op2 = pure none

def Blaster.Optimize.optimizeNatSub.cstSubPropLeft? (f op1 : Lean.Expr) (mv2 : Option Nat) : TranslateEnvT (Option Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.optimizeNatSub.cstSubPropLeft? f op1 mv2 = pure none

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

Apply the following simplification/normalization rules on Nat.pow :

• n ^ 0 ==> 1
• N1 ^ N2 ==> N1 "^" N2 Assume that f = Expr.const ``Nat.pow. An error is triggered when args.size ≠ 2 (i.e., only fully applied Nat.pow expected at this stage)

Equations

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

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

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

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

Equations

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

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

Equations

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

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

Given e1 and e2 corresponding to the operands for Nat.mul, return some e1^(m + 1) only when e2 := e1 ^ m

Equations

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

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

Given e1 and e2 corresponding to the operands for Nat.div (i.e., e1 / e2), return some n only when one of the following conditions is satisfied:

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

Equations

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

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

Given e1 and e2 corresponding to the operands for Nat.div (i.e., e1 / e2), return some 1 only when the following conditions are satisfied:

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

Equations

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

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

Apply the following simplification/normalization rules on Nat.div :

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

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

Equations

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

def Blaster.Optimize.optimizeNatDiv.cstDivProp? (f op1 : Lean.Expr) (mv2 : Option Nat) : TranslateEnvT (Option Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.optimizeNatDiv.cstDivProp? f op1 mv2 = pure none

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

Given e1 and e2 corresponding to the operands for Nat.mod (i.e., e1 % e2), 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.

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

Apply the following simplification/normalization rules on Nat.mod :

• 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 ``Nat.mod. An error is triggered when args.size ≠ 2 (i.e., only fully applied Nat.mod expected at this stage)

Equations

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

def Blaster.Optimize.optimizeNatMod.cstModProp? (op1 : Lean.Expr) (mv2 : Option Nat) : TranslateEnvT (Option Lean.Expr)

Equations

• Blaster.Optimize.optimizeNatMod.cstModProp? op1 (some n2) = if (n1.mod n2 == 0) = true then some <$> Blaster.Optimize.mkNatLitExpr 0 else pure none
• Blaster.Optimize.optimizeNatMod.cstModProp? op1 mv2✝ = pure none

def Blaster.Optimize.optimizeNatBeq (f : Lean.Expr) (b_args : Array Lean.Expr) : TranslateEnvT Lean.Expr

Normalize Nat.beq x y to x == y only when option normalizeFunCall is set to true. Assume that f = Expr.const ``Nat.beq NOTE: This normalization rule is still required here mainly to properly handle the case where another rec function is equivalent to Nat.beq

Equations

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

def Blaster.Optimize.optimizeNatble (f : Lean.Expr) (b_args : Array Lean.Expr) : TranslateEnvT Lean.Expr

Normalize Nat.ble x y to decide' (x ≤ y) only when option normalizeFunCall is set to true. Assume that f = Expr.const ``Nat.ble NOTE: This normalization rule is still required here mainly to properly handle the case where another rec function is equivalent to Nat.beq

Equations

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

@[inline]

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

Apply simplification/normalization rules on Nat operators.

Equations

• Blaster.Optimize.optimizeNat? (Lean.Expr.const `Nat.add us) args = do let a ← Blaster.Optimize.optimizeNatAdd (Lean.Expr.const `Nat.add us) args pure (some a)
• Blaster.Optimize.optimizeNat? (Lean.Expr.const `Nat.sub us) args = do let a ← Blaster.Optimize.optimizeNatSub (Lean.Expr.const `Nat.sub us) args pure (some a)
• Blaster.Optimize.optimizeNat? (Lean.Expr.const `Nat.mul us) args = do let a ← Blaster.Optimize.optimizeNatMul (Lean.Expr.const `Nat.mul us) args pure (some a)
• Blaster.Optimize.optimizeNat? (Lean.Expr.const `Nat.div us) args = do let a ← Blaster.Optimize.optimizeNatDiv (Lean.Expr.const `Nat.div us) args pure (some a)
• Blaster.Optimize.optimizeNat? (Lean.Expr.const `Nat.mod us) args = do let a ← Blaster.Optimize.optimizeNatMod (Lean.Expr.const `Nat.mod us) args pure (some a)
• Blaster.Optimize.optimizeNat? (Lean.Expr.const `Nat.beq us) args = do let a ← Blaster.Optimize.optimizeNatBeq (Lean.Expr.const `Nat.beq us) args pure (some a)
• Blaster.Optimize.optimizeNat? (Lean.Expr.const `Nat.ble us) args = do let a ← Blaster.Optimize.optimizeNatble (Lean.Expr.const `Nat.ble us) args pure (some a)
• Blaster.Optimize.optimizeNat? (Lean.Expr.const `Nat.pow us) args = do let a ← Blaster.Optimize.optimizeNatPow (Lean.Expr.const `Nat.pow us) args pure (some a)
• Blaster.Optimize.optimizeNat? (Lean.Expr.const n us) args = pure none
• Blaster.Optimize.optimizeNat? f args = pure none