Documentation

Init.Grind.Offset

@[reducible, inline]
abbrev Lean.Grind.isLt (x y : Nat) :
Equations
    Instances For
      @[reducible, inline]
      abbrev Lean.Grind.isLE (x y : Nat) :
      Equations
        Instances For

          Theorems for transitivity.

          theorem Lean.Grind.Nat.le_ro (u w v k : Nat) :
          u ww v + ku v + k
          theorem Lean.Grind.Nat.le_lo (u w v k : Nat) :
          u ww + k vu + k v
          theorem Lean.Grind.Nat.lo_le (u w v k : Nat) :
          u + k ww vu + k v
          theorem Lean.Grind.Nat.lo_lo (u w v k₁ k₂ : Nat) :
          u + k₁ ww + k₂ vu + (k₁ + k₂) v
          theorem Lean.Grind.Nat.lo_ro_1 (u w v k₁ k₂ : Nat) :
          isLt k₂ k₁ = trueu + k₁ ww v + k₂u + (k₁ - k₂) v
          theorem Lean.Grind.Nat.lo_ro_2 (u w v k₁ k₂ : Nat) :
          u + k₁ ww v + k₂u v + (k₂ - k₁)
          theorem Lean.Grind.Nat.ro_le (u w v k : Nat) :
          u w + kw vu v + k
          theorem Lean.Grind.Nat.ro_lo_1 (u w v k₁ k₂ : Nat) :
          u w + k₁w + k₂ vu v + (k₁ - k₂)
          theorem Lean.Grind.Nat.ro_lo_2 (u w v k₁ k₂ : Nat) :
          isLt k₁ k₂ = trueu w + k₁w + k₂ vu + (k₂ - k₁) v
          theorem Lean.Grind.Nat.ro_ro (u w v k₁ k₂ : Nat) :
          u w + k₁w v + k₂u v + (k₁ + k₂)

          Theorems for negating constraints.

          theorem Lean.Grind.Nat.of_le_eq_false (u v : Nat) :
          (u v) = Falsev + 1 u
          theorem Lean.Grind.Nat.of_lo_eq_false_1 (u v : Nat) :
          (u + 1 v) = Falsev u
          theorem Lean.Grind.Nat.of_lo_eq_false (u v k : Nat) :
          (u + k v) = Falsev u + (k - 1)
          theorem Lean.Grind.Nat.of_ro_eq_false (u v k : Nat) :
          (u v + k) = Falsev + (k + 1) u

          Theorems for closing a goal.

          theorem Lean.Grind.Nat.unsat_le_lo (u v k : Nat) :
          isLt 0 k = trueu vv + k uFalse
          theorem Lean.Grind.Nat.unsat_lo_lo (u v k₁ k₂ : Nat) :
          isLt 0 (k₁ + k₂) = trueu + k₁ vv + k₂ uFalse
          theorem Lean.Grind.Nat.unsat_lo_ro (u v k₁ k₂ : Nat) :
          isLt k₂ k₁ = trueu + k₁ vv u + k₂False

          Theorems for propagating constraints to True

          theorem Lean.Grind.Nat.lo_eq_true_of_lo (u v k₁ k₂ : Nat) :
          isLE k₂ k₁ = trueu + k₁ v → (u + k₂ v) = True
          theorem Lean.Grind.Nat.le_eq_true_of_lo (u v k : Nat) :
          u + k v → (u v) = True
          theorem Lean.Grind.Nat.le_eq_true_of_le (u v : Nat) :
          u v → (u v) = True
          theorem Lean.Grind.Nat.ro_eq_true_of_lo (u v k₁ k₂ : Nat) :
          u + k₁ v → (u v + k₂) = True
          theorem Lean.Grind.Nat.ro_eq_true_of_le (u v k : Nat) :
          u v → (u v + k) = True
          theorem Lean.Grind.Nat.ro_eq_true_of_ro (u v k₁ k₂ : Nat) :
          isLE k₁ k₂ = trueu v + k₁ → (u v + k₂) = True

          Theorems for propagating constraints to False. They are variants of the theorems for closing a goal.

          theorem Lean.Grind.Nat.lo_eq_false_of_le (u v k : Nat) :
          isLt 0 k = trueu v → (v + k u) = False
          theorem Lean.Grind.Nat.le_eq_false_of_lo (u v k : Nat) :
          isLt 0 k = trueu + k v → (v u) = False
          theorem Lean.Grind.Nat.lo_eq_false_of_lo (u v k₁ k₂ : Nat) :
          isLt 0 (k₁ + k₂) = trueu + k₁ v → (v + k₂ u) = False
          theorem Lean.Grind.Nat.ro_eq_false_of_lo (u v k₁ k₂ : Nat) :
          isLt k₂ k₁ = trueu + k₁ v → (v u + k₂) = False
          theorem Lean.Grind.Nat.lo_eq_false_of_ro (u v k₁ k₂ : Nat) :
          isLt k₁ k₂ = trueu v + k₁ → (v + k₂ u) = False

          Helper theorems for equality propagation

          theorem Lean.Grind.Nat.le_of_eq_1 (u v : Nat) :
          u = vu v
          theorem Lean.Grind.Nat.le_of_eq_2 (u v : Nat) :
          u = vv u
          theorem Lean.Grind.Nat.eq_of_le_of_le (u v : Nat) :
          u vv uu = v
          theorem Lean.Grind.Nat.le_offset (a k : Nat) :
          k a + k