Documentation

Blaster.Optimize.Lemmas.LemmasNat

Lemmas validating the normalization and simplifications rules on Nat #

Lemma to validate the following simplification rules - N1 - (N2 + n) ===> (N1 "-" N2) - n. - (n - N1) - N2 ==> n - (N1 "+" N2).

source
theorem Blaster.nat_sub_add_eq_sub_sub (x y z : Nat) :
x - (y + z) = x - y - z

Lemma to validate simplification rule (N1 - n) - N2 ==> (N1 "-" N2) - n.

source
theorem Blaster.nat_sub_assoc (x y z : Nat) :
x - y - z = x - z - y

Lemma to validate simplification rule (N1 + n) - N2 ==> (N1 "-" N2) + n (if N1 ≥ N2).

source
theorem Blaster.nat_add_sub_assoc (x y z : Nat) :
x ≥ z → x + y - z = x - z + y
source
theorem Blaster.nat_not_lt_of_lt {a b : Nat} (h : a < b) :
¬b < a
source
theorem Blaster.nat_not_lt_right_of_eq {a b : Nat} (h : a = b) :
¬b < a
source
theorem Blaster.nat_not_lt_left_of_eq {a b : Nat} (h : a = b) :
¬a < b
source
theorem Blaster.nat_not_eq_of_lt_left {a b : Nat} (h : a < b) :
¬a = b
source
theorem Blaster.nat_not_eq_of_lt_right {a b : Nat} (h : b < a) :
¬a = b
source
theorem Blaster.nat_not_zero_eq_of_zero_lt {a : Nat} (h : 0 < a) :
¬0 = a
source
theorem Blaster.nat_zero_lt_of_not_zero_eq {a : Nat} (h : ¬0 = a) :
0 < a
source
theorem Blaster.sub_min_nat_of_eq (N1 N2 a b : Nat) (h : N1 + a = N2 + b) :
N1 - N1.min N2 + a = N2 - N1.min N2 + b
source
def Blaster.mkNat_not_lt_of_lt :
Optimize.TranslateEnvT Lean.Expr

Return Blaster.nat_not_lt_of_lt const expression and cache result.

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

    Return Blaster.nat_not_lt_right_of_eq const expression and cache result.

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

      Return Blaster.nat_not_lt_left_of_eq const expression and cache result.

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

        Return Blaster.nat_not_eq_of_lt_left const expression and cache result.

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

          Return Blaster.nat_not_eq_of_lt_right const expression and cache result.

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

            Return Blaster.nat_not_zero_eq_of_zero_lt const expression and cache result.

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

              Return Blaster.nat_zero_lt_of_not_zero_eq const expression and cache result.

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

                Return Blaster.sub_min_nat_of_eq const expression and cache result.

                Equations
                Instances For