internlm/Lean-Github huggingface dataset:
Theorem: UInt.getBit_xor
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 bne (toNat x) (toNat y)).getBit i; rw [Nat.bitwise_getBit]
Proof state after:
no goals
Theorem: UInt.getBit_complement
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ ∀ (i : Nat), UInt.getBit (~~~x) i = (UInt.getBit x i != decide (i < length α))
Tactic:
intro i
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ UInt.getBit (~~~x) i = (UInt.getBit x i != decide (i < length α))
Theorem: UInt.getBit_complement
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ UInt.getBit (~~~x) i = (UInt.getBit x i != decide (i < length α))
Tactic:
unfold UInt.getBit
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ Nat.getBit (toNat (~~~x)) i = (Nat.getBit (toNat x) i != decide (i < length α))
Theorem: UInt.getBit_complement
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ Nat.getBit (toNat (~~~x)) i = (Nat.getBit (toNat x) i != decide (i < length α))
Tactic:
rw [UInt.toNat_complement, Nat.add_comm, Nat.sub_add_eq]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ Nat.getBit (2 ^ length α - 1 - toNat x) i = (Nat.getBit (toNat x) i != decide (i < length α))
Theorem: UInt.getBit_complement
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ Nat.getBit (2 ^ length α - 1 - toNat x) i = (Nat.getBit (toNat x) i != decide (i < length α))
Tactic:
have : 2^length α - 1 - UInt.toNat x = (2^length α - 1) ^^^ UInt.toNat x := by
  apply Nat.sub_eq_xor
  rw [Nat.land_comm, Nat.land_exp2_sub_one, Nat.mod_eq_of_lt (UInt.toNat_lt x)]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
this : 2 ^ length α - 1 - toNat x = 2 ^ length α - 1 ^^^ toNat x
⊢ Nat.getBit (2 ^ length α - 1 - toNat x) i = (Nat.getBit (toNat x) i != decide (i < length α))
Theorem: UInt.getBit_complement
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
this : 2 ^ length α - 1 - toNat x = 2 ^ length α - 1 ^^^ toNat x
⊢ Nat.getBit (2 ^ length α - 1 - toNat x) i = (Nat.getBit (toNat x) i != decide (i < length α))
Tactic:
rw [this, Nat.xor_getBit, Nat.getBit_pred_two_pow, Bool.bne_comm]
Proof state after:
no goals
Theorem: UInt.getBit_complement
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ 2 ^ length α - 1 - toNat x = 2 ^ length α - 1 ^^^ toNat x
Tactic:
apply Nat.sub_eq_xor
Proof state after:
case incl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ 2 ^ length α - 1 &&& toNat x = toNat x
Theorem: UInt.getBit_complement
Proof state before:
case incl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ 2 ^ length α - 1 &&& toNat x = toNat x
Tactic:
rw [Nat.land_comm, Nat.land_exp2_sub_one, Nat.mod_eq_of_lt (UInt.toNat_lt x)]
Proof state after:
no goals
Theorem: UInt.getBit_shiftLeft
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
⊢ ∀ (i : Nat),
    UInt.getBit (x <<< y) i =
      (decide (i < length α) && decide (i ≥ toNat y % length α) && UInt.getBit x (i - toNat y % length α))
Tactic:
intro i
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ UInt.getBit (x <<< y) i =
    (decide (i < length α) && decide (i ≥ toNat y % length α) && UInt.getBit x (i - toNat y % length α))
Theorem: UInt.getBit_shiftLeft
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ UInt.getBit (x <<< y) i =
    (decide (i < length α) && decide (i ≥ toNat y % length α) && UInt.getBit x (i - toNat y % length α))
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 =
    (decide (i < length α) && decide (i ≥ toNat y % length α) && Nat.getBit (toNat x) (i - toNat y % length α))
Theorem: UInt.getBit_shiftLeft
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat (x <<< y)) i =
    (decide (i < length α) && decide (i ≥ toNat y % length α) && Nat.getBit (toNat x) (i - toNat y % length α))
Tactic:
rw [UInt.toNat_shiftLeft, Nat.getBit_mod_two_pow, Nat.shiftLeft_getBit, Bool.and_assoc]
Proof state after:
no goals
Theorem: UInt.when_true_eq
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ UInt.when true a = a
Tactic:
unfold UInt.when
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ 0 - ofBool true &&& a = a
Theorem: UInt.when_true_eq
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ 0 - ofBool true &&& a = a
Tactic:
apply UInt.bitext
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ ∀ (i : Nat), i < length α → UInt.getBit (0 - ofBool true &&& a) i = UInt.getBit a i
Theorem: UInt.when_true_eq
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ ∀ (i : Nat), i < length α → UInt.getBit (0 - ofBool true &&& a) i = UInt.getBit a i
Tactic:
intro i hi
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
⊢ UInt.getBit (0 - ofBool true &&& a) i = UInt.getBit a i
Theorem: UInt.when_true_eq
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
⊢ UInt.getBit (0 - ofBool true &&& a) i = UInt.getBit a i
Tactic:
have : (0 : α) - 1 = ~~~(0 : α) := by
  rw [UInt.complement_eq, UInt.zero_add]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
this : 0 - 1 = ~~~0
⊢ UInt.getBit (0 - ofBool true &&& a) i = UInt.getBit a i
Theorem: UInt.when_true_eq
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
this : 0 - 1 = ~~~0
⊢ UInt.getBit (0 - ofBool true &&& a) i = UInt.getBit a i
Tactic:
rw [UInt.ofBool_true, this, UInt.getBit_land, UInt.getBit_complement]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
this : 0 - 1 = ~~~0
⊢ (UInt.getBit 0 i != decide (i < length α) && UInt.getBit a i) = UInt.getBit a i
Theorem: UInt.when_true_eq
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
this : 0 - 1 = ~~~0
⊢ (UInt.getBit 0 i != decide (i < length α) && UInt.getBit a i) = UInt.getBit a i
Tactic:
simp only [decide_eq_true hi, UInt.getBit_zero]
Proof state after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
this : 0 - 1 = ~~~0
⊢ (false != true && UInt.getBit a i) = UInt.getBit a i
Theorem: UInt.when_true_eq
Proof state before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
this : 0 - 1 = ~~~0
⊢ (false != true && UInt.getBit a i) = UInt.getBit a i
Tactic:
rfl
Proof state after:
no goals
Theorem: UInt.when_true_eq
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
⊢ 0 - 1 = ~~~0
Tactic:
rw [UInt.complement_eq, UInt.zero_add]
Proof state after:
no goals
Theorem: UInt.when_false_eq
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ UInt.when false a = 0
Tactic:
unfold UInt.when
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ 0 - ofBool false &&& a = 0
Theorem: UInt.when_false_eq
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ 0 - ofBool false &&& a = 0
Tactic:
rw [UInt.ofBool_false, UInt.sub_self, UInt.zero_land a]
Proof state after:
no goals
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
⊢ toNat n < length α → UInt.getBit (bitmask n) i = (decide (i < length α) && Nat.getBit i (toNat n))
Tactic:
intro hn
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
⊢ UInt.getBit (bitmask n) i = (decide (i < length α) && Nat.getBit i (toNat n))
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
⊢ UInt.getBit (bitmask n) i = (decide (i < length α) && Nat.getBit i (toNat n))
Tactic:
suffices ∀ k, k ≤ length α → UInt.getBit (bitmask.aux n k) i = (i < k && i.getBit (toNat n)) 
  from this (length α) Nat.le.refl
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
⊢ ∀ (k : Nat), k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
⊢ ∀ (k : Nat), k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
Tactic:
intro k hk
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
hk : k ≤ length α
⊢ UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
hk : k ≤ length α
⊢ UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
Tactic:
induction k
Proof state after:
case zero
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
hk : Nat.zero ≤ length α
⊢ UInt.getBit (bitmask.aux n Nat.zero) i = (decide (i < Nat.zero) && Nat.getBit i (toNat n))

case succ
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
n✝ : Nat
n_ih✝ : n✝ ≤ length α → UInt.getBit (bitmask.aux n n✝) i = (decide (i < n✝) && Nat.getBit i (toNat n))
hk : Nat.succ n✝ ≤ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ n✝)) i = (decide (i < Nat.succ n✝) && Nat.getBit i (toNat n))
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
hk : Nat.zero ≤ length α
⊢ UInt.getBit (bitmask.aux n Nat.zero) i = (decide (i < Nat.zero) && Nat.getBit i (toNat n))
Tactic:
case zero =>
  conv => lhs; dsimp [bitmask.aux, UInt.getBit]; rw [toNat_zero]
  simp [bitmask.aux, Nat.not_lt_zero i]
Proof state after:
no goals
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ k)) i = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
case succ k h_ind =>
  have : k < 2^length α := trans (Nat.le_of_succ_le hk) (Nat.exp_lt_pow _ Nat.le.refl)
  have : 2^toNat n < 2^length α := Nat.pow_lt_pow_right Nat.le.refl hn
  have : 1 < 2^length α := calc
    1 < 2^1 := by decide
    _ ≤ 2^k.succ := Nat.pow_le_pow_of_le_right (Nat.zero_lt_succ 1) (Nat.succ_le_succ k.zero_le)
    _ ≤ 2^length α := Nat.pow_le_pow_of_le_right (Nat.zero_lt_succ 1) hk
  conv =>
    lhs; simp only [UInt.getBit_xor, bitmask.aux]; rw [h_ind (Nat.le_of_succ_le hk)]
    unfold UInt.getBit
    simp only [toNat_shiftLeft, toNat_land, toNat_shiftRight, toNat_ofNat k, toNat_ofNat 1]
    rw [Nat.mod_eq_of_lt hn, Nat.mod_eq_of_lt ‹k < 2^length α›, Nat.mod_eq_of_lt hk, Nat.mod_eq_of_lt ‹1<2^length α›]
    tactic =>
      have : (k >>> toNat n &&& 1) <<< k < 2^length α :=
        calc (k >>> toNat n &&& 1) <<< k
          _ = (k >>> toNat n &&& 1) * 2^k := Nat.shiftLeft_eq _ k
          _ ≤ 1*2^k := Nat.mul_le_mul_right _ $ by rw [Nat.land_one]; exact Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ 1))
          _ = 2^k := Nat.one_mul _
          _ < 2^length α := Nat.pow_lt_pow_right Nat.le.refl hk
    rw [Nat.mod_eq_of_lt this]
    rhs; rw [Nat.shiftLeft_getBit, Nat.land_getBit, Nat.shiftRight_getBit]
    change decide (i ≥ k) && (k.getBit (i-k+toNat n) && Nat.getBit (2^0) (i-k))
    rw [Nat.getBit_two_pow, ←and_decideEq (λ x => Nat.getBit k (x + toNat n))]
    tactic =>
      have : 0 = i-k ↔ i ≤ k :=
        ⟨Nat.le_of_sub_eq_zero ∘ Eq.symm, Eq.symm ∘ Nat.sub_eq_zero_of_le⟩
      have : (i ≥ k ∧ i ≤ k) ↔ i = k :=
        ⟨λ h => Nat.le_antisymm h.right h.left, λ h => by cases h; exact ⟨Nat.le.refl, Nat.le.refl⟩⟩
    rw [decide_eq_decide.mpr ‹0=i-k ↔ i≤k›, Bool.and_comm _ (decide _), ←Bool.and_assoc]
    rw [decide_and_decide, decide_eq_decide.mpr ‹(i≥k ∧ i≤k) ↔ i=k›]
    rw [Nat.zero_add, ←decideEq_and (f:=λ x => Nat.getBit x (toNat n))]
  rw [←Bool.bne_and]
  cases Nat.lt_or_ge i k
  case inl hlt =>
    rw [decide_eq_true hlt, decide_eq_false (Nat.ne_of_lt hlt), decide_eq_true (Nat.lt_succ_of_lt hlt)]
    rfl
  case inr hge =>
    cases Nat.lt_or_eq_of_le hge
    case inl hgt =>
      rw [decide_eq_false (Nat.not_lt_of_le (Nat.le_of_lt hgt)), decide_eq_false (Nat.ne_of_gt hgt), decide_eq_false (Nat.not_lt_of_le hgt)]
      rfl
    case inr heq => cases heq; simp
Proof state after:
no goals
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
hk : Nat.zero ≤ length α
⊢ UInt.getBit (bitmask.aux n Nat.zero) i = (decide (i < Nat.zero) && Nat.getBit i (toNat n))
Tactic:
conv => lhs; dsimp [bitmask.aux, UInt.getBit]; rw [toNat_zero]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
hk : Nat.zero ≤ length α
⊢ Nat.getBit 0 i = (decide (i < Nat.zero) && Nat.getBit i (toNat n))
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
hk : Nat.zero ≤ length α
⊢ Nat.getBit 0 i = (decide (i < Nat.zero) && Nat.getBit i (toNat n))
Tactic:
simp [bitmask.aux, Nat.not_lt_zero i]
Proof state after:
no goals
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ k)) i = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
have : k < 2^length α := trans (Nat.le_of_succ_le hk) (Nat.exp_lt_pow _ Nat.le.refl)
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this : k < 2 ^ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ k)) i = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this : k < 2 ^ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ k)) i = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
have : 2^toNat n < 2^length α := Nat.pow_lt_pow_right Nat.le.refl hn
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝ : k < 2 ^ length α
this : 2 ^ toNat n < 2 ^ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ k)) i = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝ : k < 2 ^ length α
this : 2 ^ toNat n < 2 ^ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ k)) i = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
have : 1 < 2^length α := calc
  1 < 2^1 := by decide
  _ ≤ 2^k.succ := Nat.pow_le_pow_of_le_right (Nat.zero_lt_succ 1) (Nat.succ_le_succ k.zero_le)
  _ ≤ 2^length α := Nat.pow_le_pow_of_le_right (Nat.zero_lt_succ 1) hk
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ k)) i = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ UInt.getBit (bitmask.aux n (Nat.succ k)) i = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
conv =>
  lhs; simp only [UInt.getBit_xor, bitmask.aux]; rw [h_ind (Nat.le_of_succ_le hk)]
  unfold UInt.getBit
  simp only [toNat_shiftLeft, toNat_land, toNat_shiftRight, toNat_ofNat k, toNat_ofNat 1]
  rw [Nat.mod_eq_of_lt hn, Nat.mod_eq_of_lt ‹k < 2^length α›, Nat.mod_eq_of_lt hk, Nat.mod_eq_of_lt ‹1<2^length α›]
  tactic =>
    have : (k >>> toNat n &&& 1) <<< k < 2^length α :=
      calc (k >>> toNat n &&& 1) <<< k
        _ = (k >>> toNat n &&& 1) * 2^k := Nat.shiftLeft_eq _ k
        _ ≤ 1*2^k := Nat.mul_le_mul_right _ $ by rw [Nat.land_one]; exact Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ 1))
        _ = 2^k := Nat.one_mul _
        _ < 2^length α := Nat.pow_lt_pow_right Nat.le.refl hk
  rw [Nat.mod_eq_of_lt this]
  rhs; rw [Nat.shiftLeft_getBit, Nat.land_getBit, Nat.shiftRight_getBit]
  change decide (i ≥ k) && (k.getBit (i-k+toNat n) && Nat.getBit (2^0) (i-k))
  rw [Nat.getBit_two_pow, ←and_decideEq (λ x => Nat.getBit k (x + toNat n))]
  tactic =>
    have : 0 = i-k ↔ i ≤ k :=
      ⟨Nat.le_of_sub_eq_zero ∘ Eq.symm, Eq.symm ∘ Nat.sub_eq_zero_of_le⟩
    have : (i ≥ k ∧ i ≤ k) ↔ i = k :=
      ⟨λ h => Nat.le_antisymm h.right h.left, λ h => by cases h; exact ⟨Nat.le.refl, Nat.le.refl⟩⟩
  rw [decide_eq_decide.mpr ‹0=i-k ↔ i≤k›, Bool.and_comm _ (decide _), ←Bool.and_assoc]
  rw [decide_and_decide, decide_eq_decide.mpr ‹(i≥k ∧ i≤k) ↔ i=k›]
  rw [Nat.zero_add, ←decideEq_and (f:=λ x => Nat.getBit x (toNat n))]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ ((decide (i < k) && Nat.getBit i (toNat n)) != (decide (i = k) && Nat.getBit i (toNat n))) =
    (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ ((decide (i < k) && Nat.getBit i (toNat n)) != (decide (i = k) && Nat.getBit i (toNat n))) =
    (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
rw [←Bool.bne_and]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
cases Nat.lt_or_ge i k
Proof state after:
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
h✝ : i < k
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))

case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
h✝ : i ≥ k
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hlt : i < k
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
case inl hlt =>
  rw [decide_eq_true hlt, decide_eq_false (Nat.ne_of_lt hlt), decide_eq_true (Nat.lt_succ_of_lt hlt)]
  rfl
Proof state after:
no goals
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
case inr hge =>
  cases Nat.lt_or_eq_of_le hge
  case inl hgt =>
    rw [decide_eq_false (Nat.not_lt_of_le (Nat.le_of_lt hgt)), decide_eq_false (Nat.ne_of_gt hgt), decide_eq_false (Nat.not_lt_of_le hgt)]
    rfl
  case inr heq => cases heq; simp
Proof state after:
no goals
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝ : k < 2 ^ length α
this : 2 ^ toNat n < 2 ^ length α
⊢ 1 < 2 ^ 1
Tactic:
decide
Proof state after:
no goals