Documentation

Blaster.Optimize.Lemmas.LemmasInt

Lemmas validating the normalization and simplifications on Int #

source
theorem Blaster.int_not_lt_of_lt {a b : Int} (h : a < b) :
¬b < a
source
theorem Blaster.int_not_lt_right_of_eq {a b : Int} (h : a = b) :
¬b < a
source
theorem Blaster.int_not_lt_left_of_eq {a b : Int} (h : a = b) :
¬a < b
source
theorem Blaster.int_not_eq_of_lt_left {a b : Int} (h : a < b) :
¬a = b
source
theorem Blaster.int_not_eq_of_lt_right {a b : Int} (h : b < a) :
¬a = b
source
theorem Blaster.int_not_zero_eq_of_lt_zero {a : Int} (h : a < 0) :
¬0 = a
source
theorem Blaster.int_not_zero_eq_of_zero_lt {a : Int} (h : 0 < a) :
¬0 = a
source
theorem Blaster.zero_lt_neg_of_lt_zero {a : Int} (h : a < 0) :
0 < -a
source
theorem Blaster.lt_zero_of_zero_lt_neg {a : Int} (h : 0 < -a) :
a < 0
source
theorem Blaster.sub_min_int_of_eq (N1 N2 a b : Int) (h : N1 + a = N2 + b) :
N1 - min N1 N2 + a = N2 - min N1 N2 + b
source
def Blaster.mkInt_not_lt_of_lt :
Optimize.TranslateEnvT Lean.Expr

Return Blaster.int_not_lt_of_lt const expression and cache result.

Equations
Instances For
    source
    def Blaster.mkInt_not_lt_right_of_eq :
    Optimize.TranslateEnvT Lean.Expr

    Return Blaster.int_not_lt_right_of_eq const expression and cache result.

    Equations
    Instances For
      source
      def Blaster.mkInt_not_lt_left_of_eq :
      Optimize.TranslateEnvT Lean.Expr

      Return Blaster.int_not_lt_left_of_eq const expression and cache result.

      Equations
      Instances For
        source
        def Blaster.mkInt_not_eq_of_lt_left :
        Optimize.TranslateEnvT Lean.Expr

        Return Blaster.int_not_eq_of_lt_left const expression and cache result.

        Equations
        Instances For
          source
          def Blaster.mkInt_not_eq_of_lt_right :
          Optimize.TranslateEnvT Lean.Expr

          Return Blaster.int_not_eq_of_lt_right const expression and cache result.

          Equations
          Instances For
            source
            def Blaster.mkInt_not_zero_eq_of_lt_zero :
            Optimize.TranslateEnvT Lean.Expr

            Return Blaster.int_not_zero_eq_of_lt_zero const expression and cache result.

            Equations
            Instances For
              source
              def Blaster.mkInt_not_zero_eq_of_zero_lt :
              Optimize.TranslateEnvT Lean.Expr

              Return Blaster.int_not_zero_eq_of_zero_lt const expression and cache result.

              Equations
              Instances For
                source
                def Blaster.mkInt_zero_lt_neg_of_lt_zero :
                Optimize.TranslateEnvT Lean.Expr

                Return Blaster.zero_lt_neg_of_lt_zero const expression and cache result.

                Equations
                Instances For
                  source
                  def Blaster.mkInt_lt_zero_of_zero_lt_neg :
                  Optimize.TranslateEnvT Lean.Expr

                  Return Blaster.lt_zero_of_zero_lt_neg const expression and cache result.

                  Equations
                  Instances For
                    source
                    def Blaster.mkInt_sub_min_int_of_eq :
                    Optimize.TranslateEnvT Lean.Expr

                    Return Blaster.sub_min_int_of_eq const expression and cache result.

                    Equations
                    Instances For