def Blaster.Optimize.isOneNat (e : Lean.Expr) : Bool

Return true when e corresponds to the one nat literal.

Equations

• Blaster.Optimize.isOneNat e = match Blaster.Optimize.isNatValue? e with | some 1 => true | x => false

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

Given op1 and op2 corresponding to the operands for LT.lt:

• return some False when op1 := N + e ∧ op2 := e ∧ N > 0 ∧ Type(N) = Int
• return some True when op1 := N + e ∧ op2 := e ∧ N < 0 ∧ Type(N) = Int
• return some False when op1 := a + b ∧ op2 := a ∧ Type(N) = Int ∧ geqZeroIntInHyps b
• return some False when op1 := b + a ∧ op2 := a ∧ Type(N) = Int ∧ geqZeroIntInHyps b
• return some True when op1 := a + b ∧ op2 := a ∧ Type(N) = Int ∧ ltZeroIntInHyps b
• return some True when op1 := b + a ∧ op2 := a ∧ Type(N) = Int ∧ ltZeroIntInHyps b Otherwise none.

Equations

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

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

Given op1 and op2 corresponding to the operands for LT.lt:

• return some True when op1 := e ∧ op2 := N + e ∧ N > 0 ∧ Type(N) = Int
• return some False when op1 := e ∧ op2 := N + e ∧ N < 0 ∧ Type(N) = Int
• return some False when op1 := a ∧ op2 := a + b ∧ Type(a) = Int ∧ leqZeroIntInHyps b
• return some False when op1 := a ∧ op2 := b + a ∧ Type(a) = Int ∧ leqZeroIntInHyps b
• return some True when op1 := a ∧ op2 := a + b ∧ Type(a) = Int ∧ gtZeroIntInHyps b
• return some True when op1 := a ∧ op2 := b + a ∧ Type(a) = Int ∧ gtZeroIntInHyps b Otherwise none.

Equations

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

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

Given op1 and op2 corresponding to the operands for LT.lt:

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

Equations

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

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

Given op1 and op2 corresponding to the operands for LT.lt:

• return some True when op1 := e ∧ op2 := N + e ∧ N > 0 ∧ Type(N) = Nat
• return some False when op1 := a ∧ op2 := a + b ∧ Type(a) = Nat ∧ eqZeroNatInHyps b
• return some False when op1 := a ∧ op2 := b + a ∧ Type(a) = Nat ∧ eqZeroNatInHyps b
• return some True when op1 := a ∧ op2 := a + b ∧ Type(a) = Nat ∧ gtZeroNatInHyps b
• return some True when op1 := a ∧ op2 := b + a ∧ Type(a) = Nat ∧ gtZeroNatInHyps b Otherwise none.

Equations

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

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

Given op1 and op2 corresponding to the operands for LT.lt:

• return some (N1 "<" N2) when op1 := N1 ∧ op2 := N2 ∧ Type(op1) = Nat
• return some (N1 "<" N2) when op1 := N1 ∧ op2 := N2 ∧ Type(op1) = Int
• return some (S1 "<" S2) when op1 := S1 ∧ op2 := S2 ∧ Type(op1) = String NOTE: This function need to be updated each time we are opacifying other Lean inductive types. Otheriwse none.

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.cstLTProp? (Lean.Expr.lit (Lean.Literal.natVal n1)) (Lean.Expr.lit (Lean.Literal.natVal n2)) = do let a ← Blaster.Optimize.mkPropLit (n1.blt n2) pure (some a)
• Blaster.Optimize.cstLTProp? (Lean.Expr.lit (Lean.Literal.strVal s1)) (Lean.Expr.lit (Lean.Literal.strVal s2)) = do let a ← Blaster.Optimize.mkPropLit (decide (s1 < s2)) pure (some a)

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

Given op1 and op2 corresponding to the operands for LT.lt:

• return some ¬ (b < op1) when op2 := 1 + b ∧ Type(op1) = Int Otherwise none.

Equations

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

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

Given op1 and op2 corresponding to the operands for LT.lt:

• return some b < 0 when op1 := 0 ∧ op2 := -b ∧ Type(op1) = IntOtherwisenone`.

Equations

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

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

Given op1 and op2 corresponding to the operands for LT.lt:

• return some ¬ (b < op1) when op2 := 1 + b ∧ Type(a) = Nat Otherwise none.

Equations

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

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

Given op1 and op2 corresponding to the operands for LT.lt such that, op1 := N1 + a, op2 := N2 and Type(a) = Nat`:

• return some False when N2 ≤ N1
• return some a < N2 "-" N1 when N2 > N1 Otherwise none.

Equations

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

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

Given op1 and op2 corresponding to the operands for LT.lt such that, op1 := N1, op2 := N2 + a and Type(a) = Nat`:

• return some True when N1 < N2
• return some N1 "-" N2 < a when N1 ≥ N2 Otherwise none.

Equations

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

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

Given op1 and op2 corresponding to the operands for LT.lt such that, op1 := N1 + a, op2 := N2 and Type(a) = Int`:

• return some a < N2 "-" N1 Otherwise none.

Equations

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

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

Given op1 and op2 corresponding to the operands for LT.lt such that, op1 := N1, op2 := N2 + a and Type(a) = Int`:

• return some N1 "-" N2 < a Otherwise none.

Equations

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

def Blaster.Optimize.predCstLTInHyp (op1 op2 : Lean.Expr) : TranslateEnvT Bool

Given op1 and op2 corresponding to the operands for LT.lt, return true only when the following conditions are satisfied

• op1 := N ∧
• ¬ (N - 1 < op2) _ ∈ hypothesisContext.hypothesisMap ∧
• Type(op2) ∈ [Nat, Int]

Equations

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

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

Apply the following simplification/normalization rules on LT.lt :

• e1 < e2 ==> False (if e1 =ₚₜᵣ e2)
• e < 0 ==> False (if Type(e) = Nat)
• 0 < -e ==> e < 0 (if Type(e) = Int)
• N1 < N2 ==> N1 "<" N2
• N < e ==> False (if ¬ (N - 1 < e) := _ ∈ hypothesisContext.hypothesisMap ∧ Type(e) ∈ [Nat, Int])
• e < 1 ==> 0 = e (if Type(e) = Nat)
• a + b < a | b + a < a ==> False (if Type(a) = Nat)
• N + e < e ==> False (if N > 0 ∧ Type(e) = Int)
• N + e < e ==> True (if N < 0 ∧ Type(e) = Int)
• a + b < a | b + a < a ==> False (if Type(a) = Int ∧ geqZeroIntInHyps b)
• a + b < a | b + a < a ==> True (if Type(a) = Int ∧ ltZeroIntInHyps b)
• e < N + e ==> True (if N > 0 ∧ Type(N) ∈ [Nat, Int])
• e < N + e ==> False (if N < 0 ∧ Type(N) = Int)
• a < a + b | a < b + a ==> False (if Type(a) = Nat ∧ eqZeroNatInHyps b)
• a < a + b | a < b + a ==> True (if Type(a) = Nat ∧ gtZeroNatInHyps b)
• a < a + b | a < b + a ==> False (if Type(a) = Int ∧ leqZeroIntInHyps b)
• a < a + b | a < b + a ==> True (if Type(a) = Int ∧ gtZeroIntInHyps b)
• N1 + a < N2 ==> False (if Type(a) = Nat ∧ N2 ≤ N1)
• N1 + a < N2 ==> a < N2 "-" N1 (if Type(a) = Nat ∧ N2 > N1)
• N1 + a < N2 ==> a < N2 "-" N1 (if Type(a) = Int)
• N1 < N2 + a ==> True (if Type(a) = Nat ∧ N1 < N2)
• N1 < N2 + a ==> N1 "-" N2 < a (if Type(a) = Nat ∧ N1 ≥ N2)
• N1 < N2 + a ==> N1 "-" N2 < a (if Type(a) = Int)
• N1 + a < N2 + b ==> N1 "-" min(N1, N2) + a < N2 "-" min(N1, N2) + b (if Type(a) ∈ [Nat, Int])
• a < 1 + b ==> ¬ (b < a) (if Type(a) ∈ [Nat, Int]) The simplifications are only applied when isOpaqueRelational predicate is satisfied Assume that f = Expr.const ``LT.lt. Do nothing if operator is partially applied (i.e., args.size < 4)

Equations

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

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

Given op1 and op2 corresponding to the operands for LT.lt such that, op1 := N1 + a, op2 := N2 + b and Type(a) = Nat`:

• return some N1 "-" min(N1, N2) + a < N2 "-" min(N1, N2) + b Otherwise none

Equations

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

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

Given op1 and op2 corresponding to the operands for LT.lt such that, op1 := N1 + a, op2 := N2 + b and Type(a) = Int`:

• return some N1 "-" min(N1, N2) + a < N2 "-" min(N1, N2) + b Otherwise none

Equations

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

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

Apply the following snormalization rule on LE.le :

• e1 ≤ e2 ==> ¬ (e2 < e1)

This normalization rule is applied only when isOpaqueRelational predicate is satisfied Assume that f = Expr.const ``LE.le.

Equations

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

def Blaster.Optimize.optimizeLE.mkNotLtExpr (t op1 op2 : Lean.Expr) : TranslateEnvT Lean.Expr

Equations

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

def Blaster.Optimize.optimizeLE.findLtInstance (t : Lean.Expr) : TranslateEnvT Lean.Expr

Equations

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

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

Apply simplification and normalization rules on LE.le and LT.lt :

Equations

• Blaster.Optimize.optimizeRelational? (Lean.Expr.const `LE.le us) args = do let a ← Blaster.Optimize.optimizeLE (Lean.Expr.const `LE.le us) args pure (some a)
• Blaster.Optimize.optimizeRelational? (Lean.Expr.const `LT.lt us) args = do let a ← Blaster.Optimize.optimizeLT (Lean.Expr.const `LT.lt us) args pure (some a)
• Blaster.Optimize.optimizeRelational? (Lean.Expr.const n us) args = pure none
• Blaster.Optimize.optimizeRelational? f args = pure none