internlm/Lean-Github huggingface dataset:
Theorem: UInt.toNat_complement
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) < 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
have : toNat a + 1 < 2^length α := h
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this✝ : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) < 2 ^ length α
this : toNat a + 1 < 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Theorem: UInt.toNat_complement
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this✝ : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) < 2 ^ length α
this : toNat a + 1 < 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
have : 2^length α - (toNat a + 1) < 2^length α :=
  Nat.sub_lt_self (Nat.zero_lt_succ _) (toNat_lt a)
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this✝¹ : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) < 2 ^ length α
this✝ : toNat a + 1 < 2 ^ length α
this : 2 ^ length α - (toNat a + 1) < 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Theorem: UInt.toNat_complement
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this✝¹ : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) < 2 ^ length α
this✝ : toNat a + 1 < 2 ^ length α
this : 2 ^ length α - (toNat a + 1) < 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
rw [
  Nat.mod_eq_of_lt ‹toNat a + 1 < 2^length α›,
  Nat.mod_eq_of_lt ‹2^length α - (toNat a + 1) < 2^length α›
]
Proof state after:
no goals
Theorem: UInt.toNat_complement
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) = 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
have : toNat a + 1 = 2^length α := h
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this✝ : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) = 2 ^ length α
this : toNat a + 1 = 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Theorem: UInt.toNat_complement
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this✝ : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) = 2 ^ length α
this : toNat a + 1 = 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
simp [this]
Proof state after:
no goals
Theorem: UInt.toNat_of_length_eq_zero
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
h : length α = 0
a : α
⊢ toNat a = toNat (OfNat.ofNat (toNat a))
Tactic:
rw [UInt.ofNat_toNat]
Proof state after:
no goals
Theorem: UInt.toNat_of_length_eq_zero
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
h : length α = 0
a : α
⊢ toNat a % 2 ^ length α = toNat a % 1
Tactic:
rw [h, Nat.pow_zero]
Proof state after:
no goals
Theorem: UInt.eq_of_length_eq_zero
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ length α = 0 → ∀ (a b : α), a = b
Tactic:
intro h a b
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
h : length α = 0
a b : α
⊢ a = b
Theorem: UInt.eq_of_length_eq_zero
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
h : length α = 0
a b : α
⊢ a = b
Tactic:
apply UInt.toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
h : length α = 0
a b : α
⊢ toNat a = toNat b
Theorem: UInt.eq_of_length_eq_zero
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
h : length α = 0
a b : α
⊢ toNat a = toNat b
Tactic:
simp only [toNat_of_length_eq_zero h]
Proof state after:
no goals
Theorem: UInt.ofNat_add
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
m n : Nat
⊢ OfNat.ofNat m + OfNat.ofNat n = OfNat.ofNat (m + n)
Tactic:
apply UInt.toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
m n : Nat
⊢ toNat (OfNat.ofNat m + OfNat.ofNat n) = toNat (OfNat.ofNat (m + n))
Theorem: UInt.ofNat_add
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
m n : Nat
⊢ toNat (OfNat.ofNat m + OfNat.ofNat n) = toNat (OfNat.ofNat (m + n))
Tactic:
simp only [toNat_add, toNat_ofNat, Nat.mod_add_mod, Nat.add_mod_mod]
Proof state after:
no goals
Theorem: UInt.add_comm
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
⊢ a + b = b + a
Tactic:
apply toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
⊢ toNat (a + b) = toNat (b + a)
Theorem: UInt.add_comm
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
⊢ toNat (a + b) = toNat (b + a)
Tactic:
simp [toNat_add]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
⊢ (toNat a + toNat b) % 2 ^ length α = (toNat b + toNat a) % 2 ^ length α
Theorem: UInt.add_comm
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
⊢ (toNat a + toNat b) % 2 ^ length α = (toNat b + toNat a) % 2 ^ length α
Tactic:
rw [Nat.add_comm]
Proof state after:
no goals
Theorem: UInt.add_assoc
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ 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 : α
⊢ toNat (a + b + c) = toNat (a + (b + c))
Theorem: UInt.add_assoc
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat (a + b + c) = toNat (a + (b + c))
Tactic:
simp [toNat_add]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (toNat a + toNat b + toNat c) % 2 ^ length α = (toNat a + (toNat b + toNat c)) % 2 ^ length α
Theorem: UInt.add_assoc
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (toNat a + toNat b + toNat c) % 2 ^ length α = (toNat a + (toNat b + toNat c)) % 2 ^ length α
Tactic:
rw [Nat.add_assoc]
Proof state after:
no goals
Theorem: UInt.add_zero
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ a + 0 = a
Tactic:
apply toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (a + 0) = toNat a
Theorem: UInt.add_zero
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (a + 0) = toNat a
Tactic:
simp [toNat_add, toNat_zero]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat a % 2 ^ length α = toNat a
Theorem: UInt.add_zero
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat a % 2 ^ length α = toNat a
Tactic:
exact Nat.mod_eq_of_lt (toNat_lt a)
Proof state after:
no goals
Theorem: UInt.zero_add
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ 0 + a = a
Tactic:
apply toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (0 + a) = toNat a
Theorem: UInt.zero_add
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (0 + a) = toNat a
Tactic:
simp [toNat_add, toNat_zero]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat a % 2 ^ length α = toNat a
Theorem: UInt.zero_add
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat a % 2 ^ length α = toNat a
Tactic:
exact Nat.mod_eq_of_lt (toNat_lt a)
Proof state after:
no goals
Theorem: UInt.add_eq_xor
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
⊢ a &&& b = 0 → a + b = a ^^^ b
Tactic:
intro h
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
⊢ a + b = a ^^^ b
Theorem: UInt.add_eq_xor
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
⊢ a + b = a ^^^ b
Tactic:
apply toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
⊢ toNat (a + b) = toNat (a ^^^ b)
Theorem: UInt.add_eq_xor
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
⊢ toNat (a + b) = toNat (a ^^^ b)
Tactic:
simp [toNat_add, toNat_xor]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
⊢ (toNat a + toNat b) % 2 ^ length α = toNat a ^^^ toNat b
Theorem: UInt.add_eq_xor
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
⊢ (toNat a + toNat b) % 2 ^ length α = toNat a ^^^ toNat b
Tactic:
have : toNat a &&& toNat b = 0 :=
  toNat_land a b ▸ h ▸ toNat_zero
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
this : toNat a &&& toNat b = 0
⊢ (toNat a + toNat b) % 2 ^ length α = toNat a ^^^ toNat b
Theorem: UInt.add_eq_xor
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
this : toNat a &&& toNat b = 0
⊢ (toNat a + toNat b) % 2 ^ length α = toNat a ^^^ toNat b
Tactic:
rw [Nat.add_eq_xor this]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
this : toNat a &&& toNat b = 0
⊢ (toNat a ^^^ toNat b) % 2 ^ length α = toNat a ^^^ toNat b
Theorem: UInt.add_eq_xor
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
this : toNat a &&& toNat b = 0
⊢ (toNat a ^^^ toNat b) % 2 ^ length α = toNat a ^^^ toNat b
Tactic:
have : toNat a ^^^ toNat b < 2^length α
  := Nat.bitwise_lt_exp2 bne (toNat_lt a) (toNat_lt b)
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
this✝ : toNat a &&& toNat b = 0
this : toNat a ^^^ toNat b < 2 ^ length α
⊢ (toNat a ^^^ toNat b) % 2 ^ length α = toNat a ^^^ toNat b
Theorem: UInt.add_eq_xor
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : a &&& b = 0
this✝ : toNat a &&& toNat b = 0
this : toNat a ^^^ toNat b < 2 ^ length α
⊢ (toNat a ^^^ toNat b) % 2 ^ length α = toNat a ^^^ toNat b
Tactic:
rw [Nat.mod_eq_of_lt this]
Proof state after:
no goals
Theorem: UInt.sub_of_toNat_ge_toNat
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
⊢ toNat a ≥ toNat b → toNat (a - b) = toNat a - toNat b
Tactic:
intro hgt
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
hgt : toNat a ≥ toNat b
⊢ toNat (a - b) = toNat a - toNat b
Theorem: UInt.sub_of_toNat_ge_toNat
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
hgt : toNat a ≥ toNat b
⊢ toNat (a - b) = toNat a - toNat b
Tactic:
rw [
  UInt.toNat_sub,
  ←Nat.add_sub_assoc (Nat.le_of_lt $ UInt.toNat_lt b),
  Nat.sub_add_comm hgt,
  Nat.add_mod_right,
  Nat.mod_eq_of_lt (trans (Nat.sub_le ..) (UInt.toNat_lt a))
]
Proof state after:
no goals
Theorem: UInt.mul_comm
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
⊢ a * b = b * a
Tactic:
apply toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
⊢ toNat (a * b) = toNat (b * a)
Theorem: UInt.mul_comm
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
⊢ toNat (a * b) = toNat (b * a)
Tactic:
simp [toNat_mul]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
⊢ toNat a * toNat b % 2 ^ length α = toNat b * toNat a % 2 ^ length α
Theorem: UInt.mul_comm
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
⊢ toNat a * toNat b % 2 ^ length α = toNat b * toNat a % 2 ^ length α
Tactic:
rw [Nat.mul_comm]
Proof state after:
no goals
Theorem: UInt.mul_assoc
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ 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 : α
⊢ toNat (a * b * c) = toNat (a * (b * c))
Theorem: UInt.mul_assoc
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat (a * b * c) = toNat (a * (b * c))
Tactic:
simp [toNat_mul]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat a * toNat b % 2 ^ length α * toNat c % 2 ^ length α =
    toNat a * (toNat b * toNat c % 2 ^ length α) % 2 ^ length α
Theorem: UInt.mul_assoc
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat a * toNat b % 2 ^ length α * toNat c % 2 ^ length α =
    toNat a * (toNat b * toNat c % 2 ^ length α) % 2 ^ length α
Tactic:
conv => lhs; rw [Nat.mod_mul_mod]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat a * toNat b * toNat c % 2 ^ length α = toNat a * (toNat b * toNat c % 2 ^ length α) % 2 ^ length α
Theorem: UInt.mul_assoc
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat a * toNat b * toNat c % 2 ^ length α = toNat a * (toNat b * toNat c % 2 ^ length α) % 2 ^ length α
Tactic:
conv => rhs; rw [Nat.mul_comm, Nat.mod_mul_mod, Nat.mul_comm]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat a * toNat b * toNat c % 2 ^ length α = toNat a * (toNat b * toNat c) % 2 ^ length α
Theorem: UInt.mul_assoc
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat a * toNat b * toNat c % 2 ^ length α = toNat a * (toNat b * toNat c) % 2 ^ length α
Tactic:
rw [Nat.mul_assoc]
Proof state after:
no goals
Theorem: UInt.mul_zero
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ a * 0 = 0
Tactic:
apply toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (a * 0) = toNat 0
Theorem: UInt.mul_zero
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (a * 0) = toNat 0
Tactic:
simp [toNat_mul, toNat_zero]
Proof state after:
no goals
Theorem: UInt.zero_mul
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ 0 * a = 0
Tactic:
apply toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (0 * a) = toNat 0
Theorem: UInt.zero_mul
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (0 * a) = toNat 0
Tactic:
simp [toNat_mul, toNat_zero]
Proof state after:
no goals
Theorem: UInt.add_mul
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.add_mul
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_add, toNat_mul, Nat.mod_mul_mod, Nat.add_mul]
Proof state after:
no goals
Theorem: UInt.mul_add
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ a * (b + c) = a * b + a * 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 * b + a * c)
Theorem: UInt.mul_add
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat (a * (b + c)) = toNat (a * b + a * c)
Tactic:
simp [toNat_add, toNat_mul]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat a * ((toNat b + toNat c) % 2 ^ length α) % 2 ^ length α = (toNat a * toNat b + toNat a * toNat c) % 2 ^ length α
Theorem: UInt.mul_add
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat a * ((toNat b + toNat c) % 2 ^ length α) % 2 ^ length α = (toNat a * toNat b + toNat a * toNat c) % 2 ^ length α
Tactic:
conv => lhs; rw [Nat.mul_comm, Nat.mod_mul_mod, Nat.mul_comm, Nat.mul_add]
Proof state after:
no goals
Theorem: UInt.sub_self
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ a - a = 0
Tactic:
apply toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (a - a) = toNat 0
Theorem: UInt.sub_self
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (a - a) = toNat 0
Tactic:
simp [toNat_sub, toNat_zero]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ (toNat a + (2 ^ length α - toNat a)) % 2 ^ length α = 0
Theorem: UInt.sub_self
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ (toNat a + (2 ^ length α - toNat a)) % 2 ^ length α = 0
Tactic:
rw [ ←Nat.add_sub_assoc (Nat.le_of_lt (toNat_lt a))]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ (toNat a + 2 ^ length α - toNat a) % 2 ^ length α = 0
Theorem: UInt.sub_self
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ (toNat a + 2 ^ length α - toNat a) % 2 ^ length α = 0
Tactic:
rw [Nat.add_comm, Nat.add_sub_cancel, Nat.mod_self]
Proof state after:
no goals
Theorem: UInt.add_sub_assoc
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ 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 : α
⊢ toNat (a + b - c) = toNat (a + (b - c))
Theorem: UInt.add_sub_assoc
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat (a + b - c) = toNat (a + (b - c))
Tactic:
simp [toNat_add, toNat_sub, Nat.add_assoc]
Proof state after:
no goals
Theorem: UInt.add_neg
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
⊢ a + -b = a - b
Tactic:
rw [neg_eq, ←UInt.add_sub_assoc, UInt.add_zero]
Proof state after:
no goals
Theorem: UInt.neg_add
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
⊢ -a + b = b - a
Tactic:
rw [UInt.add_comm, UInt.add_neg]
Proof state after:
no goals
Theorem: UInt.neg_neg
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ - -a + 0 = - -a + (-a + a)
Tactic:
rw [UInt.neg_add_self]
Proof state after:
no goals
Theorem: UInt.neg_neg
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ - -a + (-a + a) = - -a + -a + a
Tactic:
rw [UInt.add_assoc]
Proof state after:
no goals
Theorem: UInt.neg_neg
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ - -a + -a + a = 0 + a
Tactic:
rw [UInt.neg_add_self]
Proof state after:
no goals
Theorem: UInt.lor_assoc
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ 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 : α
⊢ toNat (a ||| b ||| c) = toNat (a ||| (b ||| c))
Theorem: UInt.lor_assoc
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat (a ||| b ||| c) = toNat (a ||| (b ||| c))
Tactic:
simp [toNat_lor, Nat.lor_assoc]
Proof state after:
no goals
Theorem: UInt.land_assoc
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ 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 : α
⊢ toNat (a &&& b &&& c) = toNat (a &&& (b &&& c))
Theorem: UInt.land_assoc
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat (a &&& b &&& c) = toNat (a &&& (b &&& c))
Tactic:
simp [toNat_land, Nat.land_assoc]
Proof state after:
no goals
Theorem: UInt.xor_assoc
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ 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 : α
⊢ toNat (a ^^^ b ^^^ c) = toNat (a ^^^ (b ^^^ c))
Theorem: UInt.xor_assoc
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat (a ^^^ b ^^^ c) = toNat (a ^^^ (b ^^^ c))
Tactic:
simp [toNat_xor, Nat.xor_assoc]
Proof state after:
no goals
Theorem: UInt.land_xor
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ a &&& (b ^^^ c) = a &&& b ^^^ a &&& 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 &&& b ^^^ a &&& c)
Theorem: UInt.land_xor
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat (a &&& (b ^^^ c)) = toNat (a &&& b ^^^ a &&& c)
Tactic:
simp [toNat_land, toNat_xor]
Proof state after:
no goals
Theorem: UInt.xor_land
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_land
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_land, toNat_xor]
Proof state after:
no goals
Theorem: UInt.complement_complement
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ ~~~~~~a = a
Tactic:
apply toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (~~~~~~a) = toNat a
Theorem: UInt.complement_complement
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (~~~~~~a) = toNat a
Tactic:
simp [toNat_complement]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ 2 ^ length α - (2 ^ length α - (toNat a + 1) + 1) = toNat a
Theorem: UInt.complement_complement
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ 2 ^ length α - (2 ^ length α - (toNat a + 1) + 1) = toNat a
Tactic:
calc
  2^length α - (2^length α - (toNat a + 1) + 1)
    = 2^length α - (2^length α - toNat a - 1 + 1) := rfl
  _ = 2^length α - (2^length α - toNat a) := by rw [Nat.sub_add_cancel (Nat.sub_pos_of_lt (toNat_lt a))]
  _ = toNat a := Nat.sub_sub_self (Nat.le_of_lt (toNat_lt a))
Proof state after:
no goals
Theorem: UInt.complement_complement
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ 2 ^ length α - (2 ^ length α - toNat a - 1 + 1) = 2 ^ length α - (2 ^ length α - toNat a)
Tactic:
rw [Nat.sub_add_cancel (Nat.sub_pos_of_lt (toNat_lt a))]
Proof state after:
no goals
Theorem: UInt.complement_inj
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
⊢ ~~~a = ~~~b → a = b
Tactic:
intro h
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : ~~~a = ~~~b
⊢ a = b
Theorem: UInt.complement_inj
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
h : ~~~a = ~~~b
⊢ a = b
Tactic:
rw [←UInt.complement_complement a, ←UInt.complement_complement b, h]
Proof state after:
no goals
Theorem: UInt.shiftRight_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