@[reducible, inline]

abbrev Blaster.Optimize.UpdatedHypContext : Type

Equations

• Blaster.Optimize.UpdatedHypContext = (Bool × Blaster.Optimize.HypothesisContext)

@[inline]

def Blaster.Optimize.gtZeroNatInHyps (e : Lean.Expr) : TranslateEnvT Bool

Return true only when the following condition is satisfied:

• 0 < e := _ ∈ hypothesisContext.hypothesisMap

Equations

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

@[inline]

def Blaster.Optimize.eqZeroNatInHyps (e : Lean.Expr) : TranslateEnvT Bool

Return true only when the following condition is satisfied:

• 0 = e := _ ∈ hypothesisContext.hypothesisMap

Equations

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

def Blaster.Optimize.nonZeroNatInHyps (e : Lean.Expr) : TranslateEnvT Bool

Return true only when one of the following conditions is satisfied:

• 0 < e := _ ∈ hypothesisContext.hypothesisMap; or
• ¬ (0 = e) := _ ∈ hypothesisContext.hypothesisMap

Equations

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

@[inline]

def Blaster.Optimize.ltZeroIntInHyps (e : Lean.Expr) : TranslateEnvT Bool

Return true only when the following condition is satisfied:

• e < 0 := _ ∈ hypothesisContext.hypothesisMap

Equations

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

@[inline]

def Blaster.Optimize.gtZeroIntInHyps (e : Lean.Expr) : TranslateEnvT Bool

Return true only when the following condition is satisfied:

• 0 < e := _ ∈ hypothesisContext.hypothesisMap

Equations

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

def Blaster.Optimize.nonZeroIntInHyps (e : Lean.Expr) : TranslateEnvT Bool

Return true only when one of the following conditions is satisfied:

• 0 < e := _ ∈ hypothesisContext.hypothesisMap; or
• e < 0 := _ ∈ hypothesisContext.hypothesisMap; or
• ¬ (0 = e) := _ ∈ hypothesisContext.hypothesisMap

Equations

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

def Blaster.Optimize.geqZeroIntInHyps (e : Lean.Expr) : TranslateEnvT Bool

Return true only when one of the following conditions is satisfied:

• 0 < e := _ ∈ hypothesisContext.hypothesisMap; or
• 0 = e := _ ∈ hypothesisContext.hypothesisMap; or
• ¬ (e < 0) := _ ∈ hypothesisContext.hypothesisMap

Equations

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

def Blaster.Optimize.leqZeroIntInHyps (e : Lean.Expr) : TranslateEnvT Bool

Return true only when one of the following conditions is satisfied:

• e < 0 := _ ∈ hypothesisContext.hypothesisMap; or
• 0 = e := _ ∈ hypothesisContext.hypothesisMap; or
• ¬ (0 < e) := _ ∈ hypothesisContext.hypothesisMap

Equations

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

@[inline]

def Blaster.Optimize.addHypotheses (e h : Lean.Expr) (isNotPropBody : Bool := false) : TranslateEnvT UpdatedHypContext

Perform the following actions: Let hyps := (← get).optEnv.options.hypothesisContext Let hMap := hyps.hypothesisMap

• When Type(e) = Prop:

  • let hMap' := hMap ∪ [ e := h | ¬ ∃ e := h' ∈ hMap ] ∪ [ e₁ := Blaster.and_left e₁ e₂ h | e := e₁ ∧ e₂, ¬ ∃ e₁ := h' ∈ hMap ] ∪ [ e₂ := Blaster.and_right e₁ e₂ h | e := e₁ ∧ e₂, ¬ ∃ e₂ := h' ∈ hMap ]

  • return (hMap' ≠ hMap, {hypothesisMap := hMap', equalityMap := default}) Otherwise:

• return (false, hyps) Note: flag isNotPropBody is set only when a forall body is not of type Prop.

Equations

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

@[inline]

def Blaster.Optimize.addHypotheses.updateHypMap (h : Bool × HypothesisMap) (e fv : Lean.Expr) : Bool × HypothesisMap

Equations

• Blaster.Optimize.addHypotheses.updateHypMap h e fv = match Std.HashMap.get? h.snd e with | none => (true, Std.HashMap.insert h.snd e fv) | x => h

@[inline]

def Blaster.Optimize.addHypotheses.updateHypContext (h : UpdatedHypContext) (e fv : Lean.Expr) : UpdatedHypContext

Equations

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

partial def Blaster.Optimize.addHypotheses.visit (es : List (Lean.Expr × Lean.Expr)) (h : UpdatedHypContext) : TranslateEnvT UpdatedHypContext

@[inline]

def Blaster.Optimize.inHypMap (e : Lean.Expr) (h : HypothesisMap) : TranslateEnvT (Option Lean.Expr)

Given e and hypothesis map h perform the following:

• When e := p ∈ h:

  • return some p

• When `e := ¬ (a = b) ∧ Type(a) = Int ∧ a < b := p ∈ h

  • return some Blaster.int_not_eq_of_lt_left a b p

• When `e := ¬ (a = b) ∧ Type(a) = Int ∧ b < a := p ∈ h

  • return some Blaster.int_not_eq_of_lt_right a b p

• When `e := ¬ (0 = a) ∧ Type(a) = Int ∧ a < 0 := p ∈ h

  • return some Blaster.int_not_zero_eq_of_lt_zero a p

• When `e := ¬ (0 = a) ∧ Type(a) = Int ∧ 0 < a := p ∈ h

  • return some Blaster.int_not_zero_eq_of_zero_lt a p

• When `e := ¬ (a = b) ∧ Type(a) = Nat ∧ a < b := p ∈ h

  • return some Blaster.nat_not_eq_of_lt_left a b p

• When `e := ¬ (a = b) ∧ Type(a) = Nat ∧ b < a := p ∈ h

  • return some Blaster.nat_not_eq_of_lt_right a b p

• When `e := ¬ (0 = a) ∧ Type(a) = Nat ∧ 0 < a := p ∈ h

  • return some Blaster.nat_not_zero_eq_of_zero_lt a p

• When `e := ¬ (a < b) ∧ Type(a) = Int ∧ a = b := p ∈ h

  • return some Blaster.int_not_lt_left_of_eq a b p

• When `e := ¬ (a < b) ∧ Type(a) = Int ∧ b = a := p ∈ h

  • return some Blaster.int_not_lt_right_of_eq b a p

• When `e := ¬ (a < b) ∧ Type(a) = Int ∧ b < a := p ∈ h

  • return some Blaster.int_not_lt_of_lt b a p

• When `e := ¬ (a < b) ∧ Type(a) = Nat ∧ a = b := p ∈ h

  • return some Blaster.nat_not_lt_left_of_eq a b p

• When `e := ¬ (a < b) ∧ Type(a) = Nat ∧ b = a := p ∈ h

  • return some Blaster.nat_not_lt_right_of_eq b a p

• When `e := ¬ (a < b) ∧ Type(a) = Nat ∧ b < a := p ∈ h

  • return some Blaster.nat_not_lt_of_lt b a p

• When `e := 0 < a ∧ Type(a) = Nat ∧ ¬ 0 = a := p ∈ h

  • return some Blaster.nat_zero_lt_of_not_zero_eq a p

• Otherwise:

  • return none

Note that:

• a ≤ b is normalized to ¬ (b < a) when Type(a) ∈ [Int, Nat]
• 0 = -a is normalized to 0 = a when Type(a) = Int`

Equations

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

@[inline]

def Blaster.Optimize.inHypMap.zeroNatLtInHyp? (h : HypothesisMap) (e : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Perform the following:

• When `e := 0 < a ∧ Type(a) = Nat ∧ ¬ 0 = a := p ∈ h
  • return some Blaster.nat_zero_lt_of_not_zero_eq a p
• Otherwise:
  • return none

Equations

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

@[inline]

def Blaster.Optimize.inHypMap.notEqInHyp? (h : HypothesisMap) (e : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Perform the following:

• When `e := ¬ (a = b) ∧ Type(a) = Int ∧ a < b := p ∈ h

  • return some Blaster.int_not_eq_of_lt_left a b p

• When `e := ¬ (a = b) ∧ Type(a) = Int ∧ b < a := p ∈ h

  • return some Blaster.int_not_eq_of_lt_right a b p

• When `e := ¬ (0 = a) ∧ Type(a) = Int ∧ a < 0 := p ∈ h

  • return some Blaster.int_not_zero_eq_of_lt_zero a p

• When `e := ¬ (0 = a) ∧ Type(a) = Int ∧ 0 < a := p ∈ h

  • return some Blaster.int_not_zero_eq_of_zero_lt a p

• When `e := ¬ (a = b) ∧ Type(a) = Nat ∧ a < b := p ∈ h

  • return some Blaster.nat_not_eq_of_lt_left a b p

• When `e := ¬ (a = b) ∧ Type(a) = Nat ∧ b < a := p ∈ h

  • return some Blaster.nat_not_eq_of_lt_right a b p

• When `e := ¬ (0 = a) ∧ Type(a) = Nat ∧ 0 < a := p ∈ h

  • return some Blaster.nat_not_zero_eq_of_zero_lt a p

• Otherwise:

  • return none

Equations

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

def Blaster.Optimize.inHypMap.notLtInHyp? (h : HypothesisMap) (e : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Perform the following:

• When `e := ¬ (a < b) ∧ Type(a) = Int ∧ a = b := p ∈ h

  • return some Blaster.int_not_lt_left_of_eq a b p

• When `e := ¬ (a < b) ∧ Type(a) = Int ∧ b = a := p ∈ h

  • return some Blaster.int_not_lt_right_of_eq b a p

• When `e := ¬ (a < b) ∧ Type(a) = Int ∧ b < a := p ∈ h

  • return some Blaster.int_not_lt_of_lt b a p

• When `e := ¬ (a < b) ∧ Type(a) = Nat ∧ a = b := p ∈ h

  • return some Blaster.nat_not_lt_left_of_eq a b p

• When `e := ¬ (a < b) ∧ Type(a) = Nat ∧ b = a := p ∈ h

  • return some Blaster.nat_not_lt_right_of_eq b a p

• When `e := ¬ (a < b) ∧ Type(a) = Nat ∧ b < a := p ∈ h

  • return some Blaster.nat_not_lt_of_lt b a p

• Otherwise:

  • return none

Equations

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

@[inline]

def Blaster.Optimize.notInHypMap (e : Lean.Expr) (h : HypothesisMap) : TranslateEnvT (Option Lean.Expr)

Given e and hypothesis map h perform the following:

• When some p := inHypMap (← optimizeNot (¬ e)) h
  • return some p

Equations

• Blaster.Optimize.notInHypMap e h = do let __do_lift ← Blaster.Optimize.mkPropNotOp let not_e ← Blaster.Optimize.optimizeNot __do_lift #[e] false Blaster.Optimize.inHypMap not_e h