internlm/Lean-Github huggingface dataset:
Theorem: UInt.bitcnt_eq
Proof state before:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
⊢ 1 <<< OfNat.ofNat (i + 1) <<< 1 = 1 <<< OfNat.ofNat (i + 1 + 1)
Tactic:
rw [UInt.shiftLeft_shiftLeft 1 (OfNat.ofNat (i+1)) 1, UInt.ofNat_add]
Proof state after:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
⊢ toNat (OfNat.ofNat (i + 1)) + toNat 1 < length α
Theorem: UInt.bitcnt_eq
Proof state before:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
⊢ toNat (OfNat.ofNat (i + 1)) + toNat 1 < length α
Tactic:
. simp only [UInt.toNat_ofNat, UInt.toNat_ofNat 1]
  have : length α > 0 :=
    hn |> (length α).rec (λ (hn : 0 = n) => nomatch (trans h hn.symm)) (λ l _ _ => l.zero_lt_succ)
  have : n < length α := hn ▸ Nat.log2RU_lt_self _ ‹length α > 0›
  have : n < 2^length α := trans this (Nat.exp_lt_pow (length α) .refl)
  rw [
      Nat.mod_eq_of_lt (trans h this),
      Nat.mod_eq_of_lt (trans (trans (Nat.le_add_left 1 i) h) this)
  ]
  exact trans (r:=LE.le) (h : i+2 ≤ n) ‹n < length α›
Proof state after:
no goals
Theorem: UInt.bitcnt_eq
Proof state before:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
⊢ toNat (OfNat.ofNat (i + 1)) + toNat 1 < length α
Tactic:
simp only [UInt.toNat_ofNat, UInt.toNat_ofNat 1]
Proof state after:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
⊢ (i + 1) % 2 ^ length α + 1 % 2 ^ length α < length α
Theorem: UInt.bitcnt_eq
Proof state before:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
⊢ (i + 1) % 2 ^ length α + 1 % 2 ^ length α < length α
Tactic:
have : length α > 0 :=
  hn |> (length α).rec (λ (hn : 0 = n) => nomatch (trans h hn.symm)) (λ l _ _ => l.zero_lt_succ)
Proof state after:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
this : length α > 0
⊢ (i + 1) % 2 ^ length α + 1 % 2 ^ length α < length α
Theorem: UInt.bitcnt_eq
Proof state before:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
this : length α > 0
⊢ (i + 1) % 2 ^ length α + 1 % 2 ^ length α < length α
Tactic:
have : n < length α := hn ▸ Nat.log2RU_lt_self _ ‹length α > 0›
Proof state after:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
this✝ : length α > 0
this : n < length α
⊢ (i + 1) % 2 ^ length α + 1 % 2 ^ length α < length α
Theorem: UInt.bitcnt_eq
Proof state before:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
this✝ : length α > 0
this : n < length α
⊢ (i + 1) % 2 ^ length α + 1 % 2 ^ length α < length α
Tactic:
have : n < 2^length α := trans this (Nat.exp_lt_pow (length α) .refl)
Proof state after:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
this✝¹ : length α > 0
this✝ : n < length α
this : n < 2 ^ length α
⊢ (i + 1) % 2 ^ length α + 1 % 2 ^ length α < length α
Theorem: UInt.bitcnt_eq
Proof state before:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
this✝¹ : length α > 0
this✝ : n < length α
this : n < 2 ^ length α
⊢ (i + 1) % 2 ^ length α + 1 % 2 ^ length α < length α
Tactic:
rw [
    Nat.mod_eq_of_lt (trans h this),
    Nat.mod_eq_of_lt (trans (trans (Nat.le_add_left 1 i) h) this)
]
Proof state after:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
this✝¹ : length α > 0
this✝ : n < length α
this : n < 2 ^ length α
⊢ i + 1 + 1 < length α
Theorem: UInt.bitcnt_eq
Proof state before:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
this✝¹ : length α > 0
this✝ : n < length α
this : n < 2 ^ length α
⊢ i + 1 + 1 < length α
Tactic:
exact trans (r:=LE.le) (h : i+2 ≤ n) ‹n < length α›
Proof state after:
no goals
Theorem: UInt.bitcnt_eq
Proof state before:
case h.mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
a✝ : i < n
x k : α
⊢ ((x, k).fst &&& ~~~bitmask (OfNat.ofNat i)) + ((x, k).fst &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i) =
    (match (x, k) with
      | (x, snd) =>
        ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
          1 <<< OfNat.ofNat (i + 1))).fst
Tactic:
rfl
Proof state after:
no goals
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (UInt.lsb a) = Nat.lsb (toNat a)
Tactic:
if hlength : length α = 0
then simp only [UInt.toNat_of_length_eq_zero hlength]
else
have hlength : length α > 0 := Nat.pos_of_ne_zero hlength
have : 1 % 2^length α = 1 :=
  Nat.mod_eq_of_lt $ calc
    1 = 2^0 := Eq.symm $ Nat.pow_zero 2
    _ < 2^length α := Nat.pow_lt_pow_right (n:=2) .refl ‹length α > 0›
suffices (UInt.toNat a &&& UInt.toNat (a-1)) = (UInt.toNat a &&& (UInt.toNat a - 1)) by
  unfold UInt.lsb; simp only [UInt.toNat_xor, UInt.toNat_land]
  rw [this]; rfl
rw [UInt.toNat_sub, UInt.toNat_ofNat, ‹1%2^length α = 1›]
cases ha : UInt.toNat a
case zero => simp
case succ n =>
  have := calc
    n.succ + (2^length α - 1)
      = n.succ + 2^length α - 1 :=
        by rw [Nat.add_sub_assoc (Nat.pos_pow_of_pos (n:=2) (length α) (by decide))]
    _ = (n + 2^length α).succ - 1 := by rw [Nat.succ_add]
    _ = n + 2^length α := Nat.succ_sub_one ..
  rw [this, Nat.add_mod_right]
  have := calc
    n < n.succ := n.lt_succ_self
    _ = toNat a := ha.symm
    _ < 2^length α := UInt.toNat_lt a
  simp only [Nat.mod_eq_of_lt this, Nat.succ_sub_one]
Proof state after:
no goals
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength : length α = 0
⊢ toNat (UInt.lsb a) = Nat.lsb (toNat a)
Tactic:
simp only [UInt.toNat_of_length_eq_zero hlength]
Proof state after:
no goals
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength : ¬length α = 0
⊢ toNat (UInt.lsb a) = Nat.lsb (toNat a)
Tactic:
have hlength : length α > 0 := Nat.pos_of_ne_zero hlength
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
⊢ toNat (UInt.lsb a) = Nat.lsb (toNat a)
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
⊢ toNat (UInt.lsb a) = Nat.lsb (toNat a)
Tactic:
have : 1 % 2^length α = 1 :=
  Nat.mod_eq_of_lt $ calc
    1 = 2^0 := Eq.symm $ Nat.pow_zero 2
    _ < 2^length α := Nat.pow_lt_pow_right (n:=2) .refl ‹length α > 0›
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this : 1 % 2 ^ length α = 1
⊢ toNat (UInt.lsb a) = Nat.lsb (toNat a)
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this : 1 % 2 ^ length α = 1
⊢ toNat (UInt.lsb a) = Nat.lsb (toNat a)
Tactic:
suffices (UInt.toNat a &&& UInt.toNat (a-1)) = (UInt.toNat a &&& (UInt.toNat a - 1)) by
  unfold UInt.lsb; simp only [UInt.toNat_xor, UInt.toNat_land]
  rw [this]; rfl
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this : 1 % 2 ^ length α = 1
⊢ toNat a &&& toNat (a - 1) = toNat a &&& toNat a - 1
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this : 1 % 2 ^ length α = 1
⊢ toNat a &&& toNat (a - 1) = toNat a &&& toNat a - 1
Tactic:
rw [UInt.toNat_sub, UInt.toNat_ofNat, ‹1%2^length α = 1›]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this : 1 % 2 ^ length α = 1
⊢ toNat a &&& (toNat a + (2 ^ length α - 1)) % 2 ^ length α = toNat a &&& toNat a - 1
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this : 1 % 2 ^ length α = 1
⊢ toNat a &&& (toNat a + (2 ^ length α - 1)) % 2 ^ length α = toNat a &&& toNat a - 1
Tactic:
cases ha : UInt.toNat a
Proof state after:
case zero
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this : 1 % 2 ^ length α = 1
ha : toNat a = Nat.zero
⊢ Nat.zero &&& (Nat.zero + (2 ^ length α - 1)) % 2 ^ length α = Nat.zero &&& Nat.zero - 1

case succ
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this : 1 % 2 ^ length α = 1
n✝ : Nat
ha : toNat a = Nat.succ n✝
⊢ Nat.succ n✝ &&& (Nat.succ n✝ + (2 ^ length α - 1)) % 2 ^ length α = Nat.succ n✝ &&& Nat.succ n✝ - 1
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this : 1 % 2 ^ length α = 1
ha : toNat a = Nat.zero
⊢ Nat.zero &&& (Nat.zero + (2 ^ length α - 1)) % 2 ^ length α = Nat.zero &&& Nat.zero - 1
Tactic:
case zero => simp
Proof state after:
no goals
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this : 1 % 2 ^ length α = 1
n : Nat
ha : toNat a = Nat.succ n
⊢ Nat.succ n &&& (Nat.succ n + (2 ^ length α - 1)) % 2 ^ length α = Nat.succ n &&& Nat.succ n - 1
Tactic:
case succ n =>
  have := calc
    n.succ + (2^length α - 1)
      = n.succ + 2^length α - 1 :=
        by rw [Nat.add_sub_assoc (Nat.pos_pow_of_pos (n:=2) (length α) (by decide))]
    _ = (n + 2^length α).succ - 1 := by rw [Nat.succ_add]
    _ = n + 2^length α := Nat.succ_sub_one ..
  rw [this, Nat.add_mod_right]
  have := calc
    n < n.succ := n.lt_succ_self
    _ = toNat a := ha.symm
    _ < 2^length α := UInt.toNat_lt a
  simp only [Nat.mod_eq_of_lt this, Nat.succ_sub_one]
Proof state after:
no goals
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this✝ : 1 % 2 ^ length α = 1
this : toNat a &&& toNat (a - 1) = toNat a &&& toNat a - 1
⊢ toNat (UInt.lsb a) = Nat.lsb (toNat a)
Tactic:
unfold UInt.lsb
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this✝ : 1 % 2 ^ length α = 1
this : toNat a &&& toNat (a - 1) = toNat a &&& toNat a - 1
⊢ toNat (a ^^^ a &&& a - 1) = Nat.lsb (toNat a)
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this✝ : 1 % 2 ^ length α = 1
this : toNat a &&& toNat (a - 1) = toNat a &&& toNat a - 1
⊢ toNat (a ^^^ a &&& a - 1) = Nat.lsb (toNat a)
Tactic:
simp only [UInt.toNat_xor, UInt.toNat_land]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this✝ : 1 % 2 ^ length α = 1
this : toNat a &&& toNat (a - 1) = toNat a &&& toNat a - 1
⊢ toNat a ^^^ toNat a &&& toNat (a - 1) = Nat.lsb (toNat a)
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this✝ : 1 % 2 ^ length α = 1
this : toNat a &&& toNat (a - 1) = toNat a &&& toNat a - 1
⊢ toNat a ^^^ toNat a &&& toNat (a - 1) = Nat.lsb (toNat a)
Tactic:
rw [this]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this✝ : 1 % 2 ^ length α = 1
this : toNat a &&& toNat (a - 1) = toNat a &&& toNat a - 1
⊢ toNat a ^^^ toNat a &&& toNat a - 1 = Nat.lsb (toNat a)
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this✝ : 1 % 2 ^ length α = 1
this : toNat a &&& toNat (a - 1) = toNat a &&& toNat a - 1
⊢ toNat a ^^^ toNat a &&& toNat a - 1 = Nat.lsb (toNat a)
Tactic:
rfl
Proof state after:
no goals
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this : 1 % 2 ^ length α = 1
ha : toNat a = Nat.zero
⊢ Nat.zero &&& (Nat.zero + (2 ^ length α - 1)) % 2 ^ length α = Nat.zero &&& Nat.zero - 1
Tactic:
simp
Proof state after:
no goals
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this : 1 % 2 ^ length α = 1
n : Nat
ha : toNat a = Nat.succ n
⊢ Nat.succ n &&& (Nat.succ n + (2 ^ length α - 1)) % 2 ^ length α = Nat.succ n &&& Nat.succ n - 1
Tactic:
have := calc
  n.succ + (2^length α - 1)
    = n.succ + 2^length α - 1 :=
      by rw [Nat.add_sub_assoc (Nat.pos_pow_of_pos (n:=2) (length α) (by decide))]
  _ = (n + 2^length α).succ - 1 := by rw [Nat.succ_add]
  _ = n + 2^length α := Nat.succ_sub_one ..
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this✝ : 1 % 2 ^ length α = 1
n : Nat
ha : toNat a = Nat.succ n
this : Nat.succ n + (2 ^ length α - 1) = n + 2 ^ length α
⊢ Nat.succ n &&& (Nat.succ n + (2 ^ length α - 1)) % 2 ^ length α = Nat.succ n &&& Nat.succ n - 1
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this✝ : 1 % 2 ^ length α = 1
n : Nat
ha : toNat a = Nat.succ n
this : Nat.succ n + (2 ^ length α - 1) = n + 2 ^ length α
⊢ Nat.succ n &&& (Nat.succ n + (2 ^ length α - 1)) % 2 ^ length α = Nat.succ n &&& Nat.succ n - 1
Tactic:
rw [this, Nat.add_mod_right]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this✝ : 1 % 2 ^ length α = 1
n : Nat
ha : toNat a = Nat.succ n
this : Nat.succ n + (2 ^ length α - 1) = n + 2 ^ length α
⊢ Nat.succ n &&& n % 2 ^ length α = Nat.succ n &&& Nat.succ n - 1
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this✝ : 1 % 2 ^ length α = 1
n : Nat
ha : toNat a = Nat.succ n
this : Nat.succ n + (2 ^ length α - 1) = n + 2 ^ length α
⊢ Nat.succ n &&& n % 2 ^ length α = Nat.succ n &&& Nat.succ n - 1
Tactic:
have := calc
  n < n.succ := n.lt_succ_self
  _ = toNat a := ha.symm
  _ < 2^length α := UInt.toNat_lt a
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this✝¹ : 1 % 2 ^ length α = 1
n : Nat
ha : toNat a = Nat.succ n
this✝ : Nat.succ n + (2 ^ length α - 1) = n + 2 ^ length α
this : n < 2 ^ length α
⊢ Nat.succ n &&& n % 2 ^ length α = Nat.succ n &&& Nat.succ n - 1
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this✝¹ : 1 % 2 ^ length α = 1
n : Nat
ha : toNat a = Nat.succ n
this✝ : Nat.succ n + (2 ^ length α - 1) = n + 2 ^ length α
this : n < 2 ^ length α
⊢ Nat.succ n &&& n % 2 ^ length α = Nat.succ n &&& Nat.succ n - 1
Tactic:
simp only [Nat.mod_eq_of_lt this, Nat.succ_sub_one]
Proof state after:
no goals
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this : 1 % 2 ^ length α = 1
n : Nat
ha : toNat a = Nat.succ n
⊢ Nat.succ n + (2 ^ length α - 1) = Nat.succ n + 2 ^ length α - 1
Tactic:
rw [Nat.add_sub_assoc (Nat.pos_pow_of_pos (n:=2) (length α) (by decide))]
Proof state after:
no goals
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this : 1 % 2 ^ length α = 1
n : Nat
ha : toNat a = Nat.succ n
⊢ 0 < 2
Tactic:
decide
Proof state after:
no goals
Theorem: UInt.toNat_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
hlength✝ : ¬length α = 0
hlength : length α > 0
this : 1 % 2 ^ length α = 1
n : Nat
ha : toNat a = Nat.succ n
⊢ Nat.succ n + 2 ^ length α - 1 = Nat.succ (n + 2 ^ length α) - 1
Tactic:
rw [Nat.succ_add]
Proof state after:
no goals
Theorem: UInt.getBit_lsb_iff
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ UInt.getBit (UInt.lsb a) i = true ↔ UInt.getBit a i = true ∧ ∀ (j : Nat), j < i → UInt.getBit a j = false
Tactic:
unfold UInt.getBit
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ Nat.getBit (toNat (UInt.lsb a)) i = true ↔
    Nat.getBit (toNat a) i = true ∧ ∀ (j : Nat), j < i → Nat.getBit (toNat a) j = false
Theorem: UInt.getBit_lsb_iff
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ Nat.getBit (toNat (UInt.lsb a)) i = true ↔
    Nat.getBit (toNat a) i = true ∧ ∀ (j : Nat), j < i → Nat.getBit (toNat a) j = false
Tactic:
rw [UInt.toNat_lsb]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ Nat.getBit (Nat.lsb (toNat a)) i = true ↔
    Nat.getBit (toNat a) i = true ∧ ∀ (j : Nat), j < i → Nat.getBit (toNat a) j = false
Theorem: UInt.getBit_lsb_iff
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ Nat.getBit (Nat.lsb (toNat a)) i = true ↔
    Nat.getBit (toNat a) i = true ∧ ∀ (j : Nat), j < i → Nat.getBit (toNat a) j = false
Tactic:
exact Nat.lsb_getBit_iff ..
Proof state after:
no goals
Theorem: UInt.getBit_of_getBit_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ UInt.getBit (UInt.lsb a) i = true → UInt.getBit a i = true
Tactic:
intro h
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
h : UInt.getBit (UInt.lsb a) i = true
⊢ UInt.getBit a i = true
Theorem: UInt.getBit_of_getBit_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
h : UInt.getBit (UInt.lsb a) i = true
⊢ UInt.getBit a i = true
Tactic:
exact And.left $ (UInt.getBit_lsb_iff a).mp h
Proof state after:
no goals
Theorem: UInt.getBit_lower_of_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ UInt.getBit (UInt.lsb a) i = true → ∀ {j : Nat}, j < i → UInt.getBit a j = false
Tactic:
intro h j
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
h : UInt.getBit (UInt.lsb a) i = true
j : Nat
⊢ j < i → UInt.getBit a j = false
Theorem: UInt.getBit_lower_of_lsb
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
h : UInt.getBit (UInt.lsb a) i = true
j : Nat
⊢ j < i → UInt.getBit a j = false
Tactic:
exact (And.right $ (UInt.getBit_lsb_iff a).mp h) j
Proof state after:
no goals
Theorem: UInt.lsb_zero
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ UInt.lsb 0 = 0
Tactic:
unfold UInt.lsb
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ 0 ^^^ 0 &&& 0 - 1 = 0
Theorem: UInt.lsb_zero
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ 0 ^^^ 0 &&& 0 - 1 = 0
Tactic:
rw [UInt.zero_land, UInt.zero_xor]
Proof state after:
no goals
Theorem: UInt.eq_zero_of_lsb_eq_zero
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ UInt.lsb a = 0 → a = 0
Tactic:
intro h
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
⊢ a = 0
Theorem: UInt.eq_zero_of_lsb_eq_zero
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
⊢ a = 0
Tactic:
suffices UInt.toNat a = 0 by
  apply UInt.toNat_inj; rw [UInt.toNat_ofNat, Nat.zero_mod]; exact this
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
⊢ toNat a = 0
Theorem: UInt.eq_zero_of_lsb_eq_zero
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
⊢ toNat a = 0
Tactic:
have : (UInt.toNat a).lsb = 0 := by
  rw [←UInt.toNat_lsb, h, UInt.toNat_ofNat, Nat.zero_mod]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
this : Nat.lsb (toNat a) = 0
⊢ toNat a = 0
Theorem: UInt.eq_zero_of_lsb_eq_zero
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
this : Nat.lsb (toNat a) = 0
⊢ toNat a = 0
Tactic:
exact Nat.eq_zero_of_lsb_eq_zero this
Proof state after:
no goals
Theorem: UInt.eq_zero_of_lsb_eq_zero
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
this : toNat a = 0
⊢ a = 0
Tactic:
apply UInt.toNat_inj
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
this : toNat a = 0
⊢ toNat a = toNat 0
Theorem: UInt.eq_zero_of_lsb_eq_zero
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
this : toNat a = 0
⊢ toNat a = toNat 0
Tactic:
rw [UInt.toNat_ofNat, Nat.zero_mod]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
this : toNat a = 0
⊢ toNat a = 0
Theorem: UInt.eq_zero_of_lsb_eq_zero
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
this : toNat a = 0
⊢ toNat a = 0
Tactic:
exact this
Proof state after:
no goals
Theorem: UInt.eq_zero_of_lsb_eq_zero
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
h : UInt.lsb a = 0
⊢ Nat.lsb (toNat a) = 0
Tactic:
rw [←UInt.toNat_lsb, h, UInt.toNat_ofNat, Nat.zero_mod]
Proof state after:
no goals
Theorem: UInt.lsb_singleton
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ a ≠ 0 → ∃ i, ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i = j)
Tactic:
intro ha
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
⊢ ∃ i, ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i = j)
Theorem: UInt.lsb_singleton
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
this : ∃ i, UInt.getBit (UInt.lsb a) i = true
⊢ ∃ i, ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i = j)
Tactic:
cases this with | intro i hi =>
suffices ∀ j, UInt.getBit (UInt.lsb a) j = decide (i = j) from ⟨i, this⟩
intro j
if hij : i = j
then exact Eq.trans (hij ▸ hi) (decide_eq_true hij).symm
else
  suffices UInt.getBit (UInt.lsb a) j ≠ true
    by rw [decide_eq_false hij]; exact eq_false_of_ne_true this
  intro hcontra
  cases Nat.lt_or_ge i j
  . have : i < j := ‹_›
    have : UInt.getBit a i = false :=
      ((UInt.getBit_lsb_iff a).mp hcontra).right i this
    have : UInt.getBit a i = true :=
      ((UInt.getBit_lsb_iff a).mp hi).left
    cases Eq.trans ‹UInt.getBit a i = false›.symm ‹UInt.getBit a i = true›
  . have : i > j := Nat.lt_of_le_of_ne ‹i ≥ j› (hij ∘ Eq.symm)
    have : UInt.getBit a j = false :=
      And.right ((UInt.getBit_lsb_iff a).mp hi) j this
    have : UInt.getBit a j = true :=
      ((UInt.getBit_lsb_iff a).mp hcontra).left
    cases Eq.trans ‹UInt.getBit a j = false›.symm ‹UInt.getBit a j = true›
Proof state after:
no goals