Theorem: UInt.toNat_lsb (Algdata/Classes/UInt.lean)

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]
State after:
no goals

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]
State after:
no goals

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
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)

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›
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)

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
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

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›]
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

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
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

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
State after:
no goals

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]
State after:
no goals

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
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)

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]
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)

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]
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)

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
State after:
no goals

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
State after:
no goals

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 ..
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

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]
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

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
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

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]
State after:
no goals

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))]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals