internlm/Lean-Github huggingface dataset:
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
f : α → α × α → α → α × α := fun a₁ z m => (UInt.when (decide (a₁ &&& m ≠ 0)) z.snd ||| z.fst, z.snd <<< 1)
f' : α → Nat → α → α :=
  fun a₁ n x => UInt.when (decide (a₁ &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n) ||| x
a x : α
⊢ (Nat.fold (fun n z => (UInt.when (decide (a &&& bitmask (OfNat.ofNat n) ≠ 0)) z.snd ||| z.fst, z.snd <<< 1))
        (Nat.log2RU (length α)) (x, 1)).fst =
    Nat.fold (f' a) (Nat.log2RU (length α)) x
Tactic:
conv =>
  rhs; dsimp
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
f : α → α × α → α → α × α := fun a₁ z m => (UInt.when (decide (a₁ &&& m ≠ 0)) z.snd ||| z.fst, z.snd <<< 1)
f' : α → Nat → α → α :=
  fun a₁ n x => UInt.when (decide (a₁ &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n) ||| x
a x : α
⊢ (Nat.fold (fun n z => (UInt.when (decide (a &&& bitmask (OfNat.ofNat n) ≠ 0)) z.snd ||| z.fst, z.snd <<< 1))
        (Nat.log2RU (length α)) (x, 1)).fst =
    Nat.fold (fun n x => UInt.when (decide ¬a &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x)
      (Nat.log2RU (length α)) x
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
f : α → α × α → α → α × α := fun a₁ z m => (UInt.when (decide (a₁ &&& m ≠ 0)) z.snd ||| z.fst, z.snd <<< 1)
f' : α → Nat → α → α :=
  fun a₁ n x => UInt.when (decide (a₁ &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n) ||| x
a x : α
⊢ (Nat.fold (fun n z => (UInt.when (decide (a &&& bitmask (OfNat.ofNat n) ≠ 0)) z.snd ||| z.fst, z.snd <<< 1))
        (Nat.log2RU (length α)) (x, 1)).fst =
    Nat.fold (fun n x => UInt.when (decide ¬a &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x)
      (Nat.log2RU (length α)) x
Tactic:
clear f f'
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a x : α
⊢ (Nat.fold (fun n z => (UInt.when (decide (a &&& bitmask (OfNat.ofNat n) ≠ 0)) z.snd ||| z.fst, z.snd <<< 1))
        (Nat.log2RU (length α)) (x, 1)).fst =
    Nat.fold (fun n x => UInt.when (decide ¬a &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x)
      (Nat.log2RU (length α)) x
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a x : α
⊢ (Nat.fold (fun n z => (UInt.when (decide (a &&& bitmask (OfNat.ofNat n) ≠ 0)) z.snd ||| z.fst, z.snd <<< 1))
        (Nat.log2RU (length α)) (x, 1)).fst =
    Nat.fold (fun n x => UInt.when (decide ¬a &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x)
      (Nat.log2RU (length α)) x
Tactic:
suffices ∀ (f : Nat → α → α) (n : Nat) (y : α), n < length α → Nat.fold (λ (i : Nat) (z : α × α) => (f i z.2 ||| z.1, z.2 <<< 1)) n (x, y) = (Nat.fold (λ (i : Nat) (x : α) => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n) by
  if hlength : length α = 0
  then exact UInt.eq_of_length_eq_zero hlength ..
  else
  have := this
    (f:=λ i x => UInt.when (a &&& bitmask (OfNat.ofNat i) ≠ 0) x)
    (n:=Nat.log2RU $ length α) (y:=1)
    (Nat.log2RU_lt_self (length α) (Nat.zero_lt_of_ne_zero hlength))
  exact congrArg Prod.fst this
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a x : α
⊢ ∀ (f : Nat → α → α) (n : Nat) (y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a x : α
⊢ ∀ (f : Nat → α → α) (n : Nat) (y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
Tactic:
intro f n y hn
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a x : α
f : Nat → α → α
n : Nat
y : α
hn : n < length α
⊢ Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
    (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a x : α
f : Nat → α → α
n : Nat
y : α
hn : n < length α
⊢ Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
    (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
Tactic:
induction n generalizing x y
Proof state after:
case zero
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
x y : α
hn : Nat.zero < length α
⊢ Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) Nat.zero (x, y) =
    (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) Nat.zero x, y <<< OfNat.ofNat Nat.zero)

case succ
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n✝ : Nat
n_ih✝ :
  ∀ (x y : α),
    n✝ < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n✝ (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n✝ x, y <<< OfNat.ofNat n✝)
x y : α
hn : Nat.succ n✝ < length α
⊢ Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) (Nat.succ n✝) (x, y) =
    (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) (Nat.succ n✝) x, y <<< OfNat.ofNat (Nat.succ n✝))
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
x y : α
hn : Nat.zero < length α
⊢ Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) Nat.zero (x, y) =
    (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) Nat.zero x, y <<< OfNat.ofNat Nat.zero)
Tactic:
case zero => dsimp [Nat.fold]; rw [UInt.shiftLeft_zero]
Proof state after:
no goals
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
⊢ Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) (Nat.succ n) (x, y) =
    (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) (Nat.succ n) x, y <<< OfNat.ofNat (Nat.succ n))
Tactic:
case succ n h_ind =>
  dsimp [Nat.fold]
  have : n < length α := Nat.lt_of_succ_lt ‹n.succ < length α›
  simp only [h_ind x y this]
  suffices y <<< OfNat.ofNat n <<< 1 = y <<< OfNat.ofNat (n+1)
    from congrArg _ this
  have : toNat (OfNat.ofNat (α:=α) n) + toNat (α:=α) 1 = n+1 := by
    simp only [UInt.toNat_ofNat, UInt.toNat_ofNat 1]
    have : n % 2^length α = n := Nat.mod_eq_of_lt $ calc
      n < length α := ‹_›
      _ < 2^length α := Nat.exp_lt_pow _ .refl
    have : 1 % 2^length α = 1 := Nat.mod_eq_of_lt $ calc
      1 ≤ n+1 := Nat.le_add_left ..
      _ < length α := hn
      _ < 2^length α := Nat.exp_lt_pow _ .refl
    rw [‹n % 2^length α = n›, ‹1 % 2^length α = 1›]
  calc
    y <<< OfNat.ofNat n <<< 1
      = y <<< (OfNat.ofNat n + 1) := UInt.shiftLeft_shiftLeft y (OfNat.ofNat n) 1 (this ▸ ‹n.succ < length α›)
    _ = y <<< OfNat.ofNat (n+1) := by rw [UInt.ofNat_add]
Proof state after:
no goals
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a x : α
this :
  ∀ (f : Nat → α → α) (n : Nat) (y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
⊢ (Nat.fold (fun n z => (UInt.when (decide (a &&& bitmask (OfNat.ofNat n) ≠ 0)) z.snd ||| z.fst, z.snd <<< 1))
        (Nat.log2RU (length α)) (x, 1)).fst =
    Nat.fold (fun n x => UInt.when (decide ¬a &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x)
      (Nat.log2RU (length α)) x
Tactic:
if hlength : length α = 0
then exact UInt.eq_of_length_eq_zero hlength ..
else
have := this
  (f:=λ i x => UInt.when (a &&& bitmask (OfNat.ofNat i) ≠ 0) x)
  (n:=Nat.log2RU $ length α) (y:=1)
  (Nat.log2RU_lt_self (length α) (Nat.zero_lt_of_ne_zero hlength))
exact congrArg Prod.fst this
Proof state after:
no goals
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a x : α
this :
  ∀ (f : Nat → α → α) (n : Nat) (y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
hlength : length α = 0
⊢ (Nat.fold (fun n z => (UInt.when (decide (a &&& bitmask (OfNat.ofNat n) ≠ 0)) z.snd ||| z.fst, z.snd <<< 1))
        (Nat.log2RU (length α)) (x, 1)).fst =
    Nat.fold (fun n x => UInt.when (decide ¬a &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x)
      (Nat.log2RU (length α)) x
Tactic:
exact UInt.eq_of_length_eq_zero hlength ..
Proof state after:
no goals
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a x : α
this :
  ∀ (f : Nat → α → α) (n : Nat) (y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
hlength : ¬length α = 0
⊢ (Nat.fold (fun n z => (UInt.when (decide (a &&& bitmask (OfNat.ofNat n) ≠ 0)) z.snd ||| z.fst, z.snd <<< 1))
        (Nat.log2RU (length α)) (x, 1)).fst =
    Nat.fold (fun n x => UInt.when (decide ¬a &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x)
      (Nat.log2RU (length α)) x
Tactic:
have := this
  (f:=λ i x => UInt.when (a &&& bitmask (OfNat.ofNat i) ≠ 0) x)
  (n:=Nat.log2RU $ length α) (y:=1)
  (Nat.log2RU_lt_self (length α) (Nat.zero_lt_of_ne_zero hlength))
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a x : α
this✝ :
  ∀ (f : Nat → α → α) (n : Nat) (y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
hlength : ¬length α = 0
this :
  Nat.fold
      (fun i z =>
        ((fun i x => UInt.when (decide (a &&& bitmask (OfNat.ofNat i) ≠ 0)) x) i z.snd ||| z.fst, z.snd <<< 1))
      (Nat.log2RU (length α)) (x, 1) =
    (Nat.fold
        (fun i x => (fun i x => UInt.when (decide (a &&& bitmask (OfNat.ofNat i) ≠ 0)) x) i (1 <<< OfNat.ofNat i) ||| x)
        (Nat.log2RU (length α)) x,
      1 <<< OfNat.ofNat (Nat.log2RU (length α)))
⊢ (Nat.fold (fun n z => (UInt.when (decide (a &&& bitmask (OfNat.ofNat n) ≠ 0)) z.snd ||| z.fst, z.snd <<< 1))
        (Nat.log2RU (length α)) (x, 1)).fst =
    Nat.fold (fun n x => UInt.when (decide ¬a &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x)
      (Nat.log2RU (length α)) x
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a x : α
this✝ :
  ∀ (f : Nat → α → α) (n : Nat) (y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
hlength : ¬length α = 0
this :
  Nat.fold
      (fun i z =>
        ((fun i x => UInt.when (decide (a &&& bitmask (OfNat.ofNat i) ≠ 0)) x) i z.snd ||| z.fst, z.snd <<< 1))
      (Nat.log2RU (length α)) (x, 1) =
    (Nat.fold
        (fun i x => (fun i x => UInt.when (decide (a &&& bitmask (OfNat.ofNat i) ≠ 0)) x) i (1 <<< OfNat.ofNat i) ||| x)
        (Nat.log2RU (length α)) x,
      1 <<< OfNat.ofNat (Nat.log2RU (length α)))
⊢ (Nat.fold (fun n z => (UInt.when (decide (a &&& bitmask (OfNat.ofNat n) ≠ 0)) z.snd ||| z.fst, z.snd <<< 1))
        (Nat.log2RU (length α)) (x, 1)).fst =
    Nat.fold (fun n x => UInt.when (decide ¬a &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x)
      (Nat.log2RU (length α)) x
Tactic:
exact congrArg Prod.fst this
Proof state after:
no goals
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
x y : α
hn : Nat.zero < length α
⊢ Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) Nat.zero (x, y) =
    (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) Nat.zero x, y <<< OfNat.ofNat Nat.zero)
Tactic:
dsimp [Nat.fold]
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
x y : α
hn : Nat.zero < length α
⊢ (x, y) = (x, y <<< OfNat.ofNat 0)
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
x y : α
hn : Nat.zero < length α
⊢ (x, y) = (x, y <<< OfNat.ofNat 0)
Tactic:
rw [UInt.shiftLeft_zero]
Proof state after:
no goals
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
⊢ Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) (Nat.succ n) (x, y) =
    (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) (Nat.succ n) x, y <<< OfNat.ofNat (Nat.succ n))
Tactic:
dsimp [Nat.fold]
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
⊢ (f n (Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y)).snd |||
        (Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y)).fst,
      (Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y)).snd <<< 1) =
    (f n (y <<< OfNat.ofNat n) ||| Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x,
      y <<< OfNat.ofNat (Nat.succ n))
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
⊢ (f n (Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y)).snd |||
        (Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y)).fst,
      (Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y)).snd <<< 1) =
    (f n (y <<< OfNat.ofNat n) ||| Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x,
      y <<< OfNat.ofNat (Nat.succ n))
Tactic:
have : n < length α := Nat.lt_of_succ_lt ‹n.succ < length α›
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
this : n < length α
⊢ (f n (Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y)).snd |||
        (Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y)).fst,
      (Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y)).snd <<< 1) =
    (f n (y <<< OfNat.ofNat n) ||| Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x,
      y <<< OfNat.ofNat (Nat.succ n))
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
this : n < length α
⊢ (f n (Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y)).snd |||
        (Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y)).fst,
      (Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y)).snd <<< 1) =
    (f n (y <<< OfNat.ofNat n) ||| Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x,
      y <<< OfNat.ofNat (Nat.succ n))
Tactic:
simp only [h_ind x y this]
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
this : n < length α
⊢ (f n (y <<< OfNat.ofNat n) ||| Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n <<< 1) =
    (f n (y <<< OfNat.ofNat n) ||| Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x,
      y <<< OfNat.ofNat (Nat.succ n))
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
this : n < length α
⊢ (f n (y <<< OfNat.ofNat n) ||| Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n <<< 1) =
    (f n (y <<< OfNat.ofNat n) ||| Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x,
      y <<< OfNat.ofNat (Nat.succ n))
Tactic:
suffices y <<< OfNat.ofNat n <<< 1 = y <<< OfNat.ofNat (n+1)
  from congrArg _ this
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
this : n < length α
⊢ y <<< OfNat.ofNat n <<< 1 = y <<< OfNat.ofNat (n + 1)
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
this : n < length α
⊢ y <<< OfNat.ofNat n <<< 1 = y <<< OfNat.ofNat (n + 1)
Tactic:
have : toNat (OfNat.ofNat (α:=α) n) + toNat (α:=α) 1 = n+1 := by
  simp only [UInt.toNat_ofNat, UInt.toNat_ofNat 1]
  have : n % 2^length α = n := Nat.mod_eq_of_lt $ calc
    n < length α := ‹_›
    _ < 2^length α := Nat.exp_lt_pow _ .refl
  have : 1 % 2^length α = 1 := Nat.mod_eq_of_lt $ calc
    1 ≤ n+1 := Nat.le_add_left ..
    _ < length α := hn
    _ < 2^length α := Nat.exp_lt_pow _ .refl
  rw [‹n % 2^length α = n›, ‹1 % 2^length α = 1›]
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
this✝ : n < length α
this : toNat (OfNat.ofNat n) + toNat 1 = n + 1
⊢ y <<< OfNat.ofNat n <<< 1 = y <<< OfNat.ofNat (n + 1)
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
this✝ : n < length α
this : toNat (OfNat.ofNat n) + toNat 1 = n + 1
⊢ y <<< OfNat.ofNat n <<< 1 = y <<< OfNat.ofNat (n + 1)
Tactic:
calc
  y <<< OfNat.ofNat n <<< 1
    = y <<< (OfNat.ofNat n + 1) := UInt.shiftLeft_shiftLeft y (OfNat.ofNat n) 1 (this ▸ ‹n.succ < length α›)
  _ = y <<< OfNat.ofNat (n+1) := by rw [UInt.ofNat_add]
Proof state after:
no goals
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
this : n < length α
⊢ toNat (OfNat.ofNat n) + toNat 1 = n + 1
Tactic:
simp only [UInt.toNat_ofNat, UInt.toNat_ofNat 1]
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
this : n < length α
⊢ n % 2 ^ length α + 1 % 2 ^ length α = n + 1
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
this : n < length α
⊢ n % 2 ^ length α + 1 % 2 ^ length α = n + 1
Tactic:
have : n % 2^length α = n := Nat.mod_eq_of_lt $ calc
  n < length α := ‹_›
  _ < 2^length α := Nat.exp_lt_pow _ .refl
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
this✝ : n < length α
this : n % 2 ^ length α = n
⊢ n % 2 ^ length α + 1 % 2 ^ length α = n + 1
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
this✝ : n < length α
this : n % 2 ^ length α = n
⊢ n % 2 ^ length α + 1 % 2 ^ length α = n + 1
Tactic:
have : 1 % 2^length α = 1 := Nat.mod_eq_of_lt $ calc
  1 ≤ n+1 := Nat.le_add_left ..
  _ < length α := hn
  _ < 2^length α := Nat.exp_lt_pow _ .refl
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
this✝¹ : n < length α
this✝ : n % 2 ^ length α = n
this : 1 % 2 ^ length α = 1
⊢ n % 2 ^ length α + 1 % 2 ^ length α = n + 1