internlm/Lean-Github huggingface dataset:
Theorem: UInt.shiftRight_zero
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (a >>> 0) = toNat a
Tactic:
simp only [UInt.toNat_shiftRight, UInt.toNat_ofNat 0, Nat.zero_mod]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat a >>> 0 = toNat a
Theorem: UInt.shiftRight_zero
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat a >>> 0 = toNat a
Tactic:
rfl
Proof state after:
no goals
Theorem: UInt.shiftLeft_zero
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ a <<< 0 = a
Tactic:
apply UInt.toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (a <<< 0) = toNat a
Theorem: UInt.shiftLeft_zero
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (a <<< 0) = toNat a
Tactic:
simp only [UInt.toNat_shiftLeft, UInt.toNat_ofNat 0]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat a <<< (0 % 2 ^ length α % length α) % 2 ^ length α = toNat a
Theorem: UInt.shiftLeft_zero
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat a <<< (0 % 2 ^ length α % length α) % 2 ^ length α = toNat a
Tactic:
simp only [Nat.zero_mod, Nat.shiftLeft_zero, Nat.mod_eq_of_lt (UInt.toNat_lt a)]
Proof state after:
no goals
Theorem: UInt.shiftRight_shiftRight
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat b + toNat c < length α → a >>> b >>> c = a >>> (b + c)
Tactic:
intro h
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
h : toNat b + toNat c < length α
⊢ a >>> b >>> c = a >>> (b + c)
Theorem: UInt.shiftRight_shiftRight
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
h : toNat b + toNat c < length α
⊢ a >>> b >>> c = a >>> (b + c)
Tactic:
apply toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
h : toNat b + toNat c < length α
⊢ toNat (a >>> b >>> c) = toNat (a >>> (b + c))
Theorem: UInt.shiftRight_shiftRight
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
h : toNat b + toNat c < length α
⊢ toNat (a >>> b >>> c) = toNat (a >>> (b + c))
Tactic:
simp [toNat_shiftRight, toNat_add]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
h : toNat b + toNat c < length α
⊢ toNat a >>> (toNat b % length α + toNat c % length α) = toNat a >>> ((toNat b + toNat c) % 2 ^ length α % length α)
Theorem: UInt.shiftRight_shiftRight
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
h : toNat b + toNat c < length α
⊢ toNat a >>> (toNat b % length α + toNat c % length α) = toNat a >>> ((toNat b + toNat c) % 2 ^ length α % length α)
Tactic:
rw [
  Nat.mod_eq_of_lt (trans (Nat.le_add_right (toNat b) (toNat c)) h),
  Nat.mod_eq_of_lt (trans (Nat.le_add_left (toNat c) (toNat b)) h),
  Nat.mod_eq_of_lt (trans h (Nat.exp_lt_pow _ (by decide))),
  Nat.mod_eq_of_lt h
]
Proof state after:
no goals
Theorem: UInt.shiftRight_shiftRight
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
h : toNat b + toNat c < length α
⊢ 2 ≥ 2
Tactic:
decide
Proof state after:
no goals
Theorem: UInt.shiftLeft_shiftLeft
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat b + toNat c < length α → a <<< b <<< c = a <<< (b + c)
Tactic:
intro h
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
h : toNat b + toNat c < length α
⊢ a <<< b <<< c = a <<< (b + c)
Theorem: UInt.shiftLeft_shiftLeft
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
h : toNat b + toNat c < length α
⊢ a <<< b <<< c = a <<< (b + c)
Tactic:
apply toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
h : toNat b + toNat c < length α
⊢ toNat (a <<< b <<< c) = toNat (a <<< (b + c))
Theorem: UInt.shiftLeft_shiftLeft
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
h : toNat b + toNat c < length α
⊢ toNat (a <<< b <<< c) = toNat (a <<< (b + c))
Tactic:
simp [toNat_shiftLeft, toNat_add]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
h : toNat b + toNat c < length α
⊢ toNat a * 2 ^ (toNat b % length α) % 2 ^ length α * 2 ^ (toNat c % length α) % 2 ^ length α =
    toNat a * 2 ^ ((toNat b + toNat c) % 2 ^ length α % length α) % 2 ^ length α
Theorem: UInt.shiftLeft_shiftLeft
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
h : toNat b + toNat c < length α
⊢ toNat a * 2 ^ (toNat b % length α) % 2 ^ length α * 2 ^ (toNat c % length α) % 2 ^ length α =
    toNat a * 2 ^ ((toNat b + toNat c) % 2 ^ length α % length α) % 2 ^ length α
Tactic:
rw [
  Nat.mod_eq_of_lt (trans (Nat.le_add_right (toNat b) (toNat c)) h),
  Nat.mod_eq_of_lt (trans (Nat.le_add_left (toNat c) (toNat b)) h),
  Nat.mod_eq_of_lt (trans h (Nat.exp_lt_pow _ (by decide))),
  Nat.mod_eq_of_lt h,
  Nat.mod_mul_mod,
  Nat.mul_assoc (toNat a),
  Nat.pow_add
]
Proof state after:
no goals
Theorem: UInt.shiftLeft_shiftLeft
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
h : toNat b + toNat c < length α
⊢ 2 ≥ 2
Tactic:
decide
Proof state after:
no goals
Theorem: UInt.shiftLeft_shiftLeft_comm
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ a <<< b <<< c = a <<< c <<< b
Tactic:
apply toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat (a <<< b <<< c) = toNat (a <<< c <<< b)
Theorem: UInt.shiftLeft_shiftLeft_comm
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat (a <<< b <<< c) = toNat (a <<< c <<< b)
Tactic:
simp [toNat_shiftLeft, toNat_add]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat a * 2 ^ (toNat b % length α) % 2 ^ length α * 2 ^ (toNat c % length α) % 2 ^ length α =
    toNat a * 2 ^ (toNat c % length α) % 2 ^ length α * 2 ^ (toNat b % length α) % 2 ^ length α
Theorem: UInt.shiftLeft_shiftLeft_comm
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat a * 2 ^ (toNat b % length α) % 2 ^ length α * 2 ^ (toNat c % length α) % 2 ^ length α =
    toNat a * 2 ^ (toNat c % length α) % 2 ^ length α * 2 ^ (toNat b % length α) % 2 ^ length α
Tactic:
simp only [Nat.mod_mul_mod, Nat.mul_assoc]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat a * (2 ^ (toNat b % length α) * 2 ^ (toNat c % length α)) % 2 ^ length α =
    toNat a * (2 ^ (toNat c % length α) * 2 ^ (toNat b % length α)) % 2 ^ length α
Theorem: UInt.shiftLeft_shiftLeft_comm
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat a * (2 ^ (toNat b % length α) * 2 ^ (toNat c % length α)) % 2 ^ length α =
    toNat a * (2 ^ (toNat c % length α) * 2 ^ (toNat b % length α)) % 2 ^ length α
Tactic:
rw [Nat.mul_comm (2^(toNat b % length α))]
Proof state after:
no goals
Theorem: UInt.lor_shiftRight
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (a ||| b) >>> c = a >>> c ||| b >>> c
Tactic:
apply toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat ((a ||| b) >>> c) = toNat (a >>> c ||| b >>> c)
Theorem: UInt.lor_shiftRight
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat ((a ||| b) >>> c) = toNat (a >>> c ||| b >>> c)
Tactic:
simp [toNat_shiftRight, toNat_lor]
Proof state after:
no goals
Theorem: UInt.land_shiftRight
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (a &&& b) >>> c = a >>> c &&& b >>> c
Tactic:
apply toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat ((a &&& b) >>> c) = toNat (a >>> c &&& b >>> c)
Theorem: UInt.land_shiftRight
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat ((a &&& b) >>> c) = toNat (a >>> c &&& b >>> c)
Tactic:
simp [toNat_shiftRight, toNat_land]
Proof state after:
no goals
Theorem: UInt.xor_shiftRight
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (a ^^^ b) >>> c = a >>> c ^^^ b >>> c
Tactic:
apply toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat ((a ^^^ b) >>> c) = toNat (a >>> c ^^^ b >>> c)
Theorem: UInt.xor_shiftRight
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat ((a ^^^ b) >>> c) = toNat (a >>> c ^^^ b >>> c)
Tactic:
simp [toNat_shiftRight, toNat_xor]
Proof state after:
no goals
Theorem: UInt.lor_shiftLeft
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (a ||| b) <<< c = a <<< c ||| b <<< c
Tactic:
apply toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat ((a ||| b) <<< c) = toNat (a <<< c ||| b <<< c)
Theorem: UInt.lor_shiftLeft
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat ((a ||| b) <<< c) = toNat (a <<< c ||| b <<< c)
Tactic:
simp only [toNat_shiftLeft, toNat_lor]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (toNat a ||| toNat b) <<< (toNat c % length α) % 2 ^ length α =
    toNat a <<< (toNat c % length α) % 2 ^ length α ||| toNat b <<< (toNat c % length α) % 2 ^ length α
Theorem: UInt.lor_shiftLeft
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (toNat a ||| toNat b) <<< (toNat c % length α) % 2 ^ length α =
    toNat a <<< (toNat c % length α) % 2 ^ length α ||| toNat b <<< (toNat c % length α) % 2 ^ length α
Tactic:
conv =>
  lhs; change (toNat a ||| toNat b) <<< (toNat c % length α) % 2^length α
  rw [Nat.lor_shiftLeft]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (toNat a <<< (toNat c % length α) ||| toNat b <<< (toNat c % length α)) % 2 ^ length α =
    toNat a <<< (toNat c % length α) % 2 ^ length α ||| toNat b <<< (toNat c % length α) % 2 ^ length α
Theorem: UInt.lor_shiftLeft
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (toNat a <<< (toNat c % length α) ||| toNat b <<< (toNat c % length α)) % 2 ^ length α =
    toNat a <<< (toNat c % length α) % 2 ^ length α ||| toNat b <<< (toNat c % length α) % 2 ^ length α
Tactic:
simp [Nat.lor_mod_two_pow]
Proof state after:
no goals
Theorem: UInt.land_shiftLeft
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (a &&& b) <<< c = a <<< c &&& b <<< c
Tactic:
apply toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat ((a &&& b) <<< c) = toNat (a <<< c &&& b <<< c)
Theorem: UInt.land_shiftLeft
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat ((a &&& b) <<< c) = toNat (a <<< c &&& b <<< c)
Tactic:
simp only [toNat_shiftLeft, toNat_land]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (toNat a &&& toNat b) <<< (toNat c % length α) % 2 ^ length α =
    toNat a <<< (toNat c % length α) % 2 ^ length α &&& toNat b <<< (toNat c % length α) % 2 ^ length α
Theorem: UInt.land_shiftLeft
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (toNat a &&& toNat b) <<< (toNat c % length α) % 2 ^ length α =
    toNat a <<< (toNat c % length α) % 2 ^ length α &&& toNat b <<< (toNat c % length α) % 2 ^ length α
Tactic:
conv =>
  lhs; change (toNat a &&& toNat b) <<< (toNat c % length α) % 2^length α
  rw [Nat.land_shiftLeft]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (toNat a <<< (toNat c % length α) &&& toNat b <<< (toNat c % length α)) % 2 ^ length α =
    toNat a <<< (toNat c % length α) % 2 ^ length α &&& toNat b <<< (toNat c % length α) % 2 ^ length α
Theorem: UInt.land_shiftLeft
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (toNat a <<< (toNat c % length α) &&& toNat b <<< (toNat c % length α)) % 2 ^ length α =
    toNat a <<< (toNat c % length α) % 2 ^ length α &&& toNat b <<< (toNat c % length α) % 2 ^ length α
Tactic:
simp [Nat.land_mod_two_pow]
Proof state after:
no goals
Theorem: UInt.xor_shiftLeft
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (a ^^^ b) <<< c = a <<< c ^^^ b <<< c
Tactic:
apply toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat ((a ^^^ b) <<< c) = toNat (a <<< c ^^^ b <<< c)
Theorem: UInt.xor_shiftLeft
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat ((a ^^^ b) <<< c) = toNat (a <<< c ^^^ b <<< c)
Tactic:
simp only [toNat_shiftLeft, toNat_xor]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (toNat a ^^^ toNat b) <<< (toNat c % length α) % 2 ^ length α =
    toNat a <<< (toNat c % length α) % 2 ^ length α ^^^ toNat b <<< (toNat c % length α) % 2 ^ length α
Theorem: UInt.xor_shiftLeft
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (toNat a ^^^ toNat b) <<< (toNat c % length α) % 2 ^ length α =
    toNat a <<< (toNat c % length α) % 2 ^ length α ^^^ toNat b <<< (toNat c % length α) % 2 ^ length α
Tactic:
conv =>
  lhs; change (toNat a ^^^ toNat b) <<< (toNat c % length α) % 2^length α
  rw [Nat.xor_shiftLeft]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (toNat a <<< (toNat c % length α) ^^^ toNat b <<< (toNat c % length α)) % 2 ^ length α =
    toNat a <<< (toNat c % length α) % 2 ^ length α ^^^ toNat b <<< (toNat c % length α) % 2 ^ length α
Theorem: UInt.xor_shiftLeft
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (toNat a <<< (toNat c % length α) ^^^ toNat b <<< (toNat c % length α)) % 2 ^ length α =
    toNat a <<< (toNat c % length α) % 2 ^ length α ^^^ toNat b <<< (toNat c % length α) % 2 ^ length α
Tactic:
simp [Nat.xor_mod_two_pow]
Proof state after:
no goals
Theorem: UInt.getBit_zero
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ ∀ (i : Nat), UInt.getBit 0 i = false
Tactic:
unfold UInt.getBit
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ ∀ (i : Nat), Nat.getBit (toNat 0) i = false
Theorem: UInt.getBit_zero
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ ∀ (i : Nat), Nat.getBit (toNat 0) i = false
Tactic:
simp [toNat_zero]
Proof state after:
no goals
Theorem: UInt.getBit_one
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ ∀ (i : Nat), UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))
Tactic:
intro i
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))
Theorem: UInt.getBit_one
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))
Tactic:
cases Nat.eq_zero_or_pos (length α)
Proof state after:
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
h✝ : length α = 0
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))

case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
h✝ : length α > 0
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))
Theorem: UInt.getBit_one
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hzero : length α = 0
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))
Tactic:
case inl hzero =>
  simp only [hzero, decide_eq_false, Bool.false_and]
  calc
    UInt.getBit (α:=α) 1 i
      = UInt.getBit (α:=α) 0 i := by rw [UInt.eq_of_length_eq_zero hzero 1 0]
    _ = false := UInt.getBit_zero i
Proof state after:
no goals
Theorem: UInt.getBit_one
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))
Tactic:
case inr hpos =>
  rw [decide_eq_true hpos, Bool.true_and]
  dsimp [UInt.getBit]; rw [UInt.toNat_ofNat]
  have := calc
    1 ≤ length α := hpos
    _ < 2^length α := Nat.exp_lt_pow _ .refl
  rw [Nat.mod_eq_of_lt this]
  calc
    Nat.getBit 1 i = decide (0 = i) := Nat.getBit_two_pow 0 i
    _              = decide (i = 0) := decide_eq_decide.mpr ⟨Eq.symm, Eq.symm⟩
Proof state after:
no goals
Theorem: UInt.getBit_one
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hzero : length α = 0
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))
Tactic:
simp only [hzero, decide_eq_false, Bool.false_and]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hzero : length α = 0
⊢ UInt.getBit 1 i = false
Theorem: UInt.getBit_one
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hzero : length α = 0
⊢ UInt.getBit 1 i = false
Tactic:
calc
  UInt.getBit (α:=α) 1 i
    = UInt.getBit (α:=α) 0 i := by rw [UInt.eq_of_length_eq_zero hzero 1 0]
  _ = false := UInt.getBit_zero i
Proof state after:
no goals
Theorem: UInt.getBit_one
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hzero : length α = 0
⊢ UInt.getBit 1 i = UInt.getBit 0 i
Tactic:
rw [UInt.eq_of_length_eq_zero hzero 1 0]
Proof state after:
no goals
Theorem: UInt.getBit_one
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))
Tactic:
rw [decide_eq_true hpos, Bool.true_and]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ UInt.getBit 1 i = decide (i = 0)
Theorem: UInt.getBit_one
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ UInt.getBit 1 i = decide (i = 0)
Tactic:
dsimp [UInt.getBit]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ Nat.getBit (toNat 1) i = decide (i = 0)
Theorem: UInt.getBit_one
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ Nat.getBit (toNat 1) i = decide (i = 0)
Tactic:
rw [UInt.toNat_ofNat]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ Nat.getBit (1 % 2 ^ length α) i = decide (i = 0)
Theorem: UInt.getBit_one
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ Nat.getBit (1 % 2 ^ length α) i = decide (i = 0)
Tactic:
have := calc
  1 ≤ length α := hpos
  _ < 2^length α := Nat.exp_lt_pow _ .refl
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
this : 1 < 2 ^ length α
⊢ Nat.getBit (1 % 2 ^ length α) i = decide (i = 0)
Theorem: UInt.getBit_one
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
this : 1 < 2 ^ length α
⊢ Nat.getBit (1 % 2 ^ length α) i = decide (i = 0)
Tactic:
rw [Nat.mod_eq_of_lt this]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
this : 1 < 2 ^ length α
⊢ Nat.getBit 1 i = decide (i = 0)
Theorem: UInt.getBit_one
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
this : 1 < 2 ^ length α
⊢ Nat.getBit 1 i = decide (i = 0)
Tactic:
calc
  Nat.getBit 1 i = decide (0 = i) := Nat.getBit_two_pow 0 i
  _              = decide (i = 0) := decide_eq_decide.mpr ⟨Eq.symm, Eq.symm⟩
Proof state after:
no goals
Theorem: UInt.getBit_lor
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
⊢ ∀ (i : Nat), UInt.getBit (x ||| y) i = (UInt.getBit x i || UInt.getBit y i)
Tactic:
intro i
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ UInt.getBit (x ||| y) i = (UInt.getBit x i || UInt.getBit y i)
Theorem: UInt.getBit_lor
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ UInt.getBit (x ||| y) i = (UInt.getBit x i || UInt.getBit y i)
Tactic:
unfold UInt.getBit
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat (x ||| y)) i = (Nat.getBit (toNat x) i || Nat.getBit (toNat y) i)
Theorem: UInt.getBit_lor
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat (x ||| y)) i = (Nat.getBit (toNat x) i || Nat.getBit (toNat y) i)
Tactic:
rw [toNat_lor]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat x ||| toNat y) i = (Nat.getBit (toNat x) i || Nat.getBit (toNat y) i)
Theorem: UInt.getBit_lor
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat x ||| toNat y) i = (Nat.getBit (toNat x) i || Nat.getBit (toNat y) i)
Tactic:
conv => lhs; change (Nat.bitwise or (toNat x) (toNat y)).getBit i; rw [Nat.bitwise_getBit]
Proof state after:
no goals
Theorem: UInt.getBit_land
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
⊢ ∀ (i : Nat), UInt.getBit (x &&& y) i = (UInt.getBit x i && UInt.getBit y i)
Tactic:
intro i
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ UInt.getBit (x &&& y) i = (UInt.getBit x i && UInt.getBit y i)
Theorem: UInt.getBit_land
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ UInt.getBit (x &&& y) i = (UInt.getBit x i && UInt.getBit y i)
Tactic:
unfold UInt.getBit
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat (x &&& y)) i = (Nat.getBit (toNat x) i && Nat.getBit (toNat y) i)
Theorem: UInt.getBit_land
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat (x &&& y)) i = (Nat.getBit (toNat x) i && Nat.getBit (toNat y) i)
Tactic:
rw [toNat_land]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat x &&& toNat y) i = (Nat.getBit (toNat x) i && Nat.getBit (toNat y) i)
Theorem: UInt.getBit_land
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat x &&& toNat y) i = (Nat.getBit (toNat x) i && Nat.getBit (toNat y) i)
Tactic:
conv => lhs; change (Nat.bitwise and (toNat x) (toNat y)).getBit i; rw [Nat.bitwise_getBit]
Proof state after:
no goals
Theorem: UInt.getBit_xor
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
⊢ ∀ (i : Nat), UInt.getBit (x ^^^ y) i = (UInt.getBit x i != UInt.getBit y i)
Tactic:
intro i
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ UInt.getBit (x ^^^ y) i = (UInt.getBit x i != UInt.getBit y i)
Theorem: UInt.getBit_xor
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ UInt.getBit (x ^^^ y) i = (UInt.getBit x i != UInt.getBit y i)
Tactic:
unfold UInt.getBit
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat (x ^^^ y)) i = (Nat.getBit (toNat x) i != Nat.getBit (toNat y) i)
Theorem: UInt.getBit_xor
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat (x ^^^ y)) i = (Nat.getBit (toNat x) i != Nat.getBit (toNat y) i)
Tactic:
rw [toNat_xor]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat x ^^^ toNat y) i = (Nat.getBit (toNat x) i != Nat.getBit (toNat y) i)