-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem cons_append_append (x : BitVec w₁) (y : BitVec w₂) (z : BitVec w₃) (a : Bool) :
    (cons a x) ++ y ++ z = (cons a (x ++ y ++ z)).cast (by omega)

Proof state:
case neg
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : ¬i < w₁ + w₂ + w₃
⊢ (if i < w₃ then z.getLsbD i else if i - w₃ < w₂ then y.getLsbD (i - w₃) else a) = a

Tactic:
by_cases h₂ : i < w₃

Result:
case pos
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : ¬i < w₁ + w₂ + w₃
h₂ : i < w₃
⊢ (if i < w₃ then z.getLsbD i else if i - w₃ < w₂ then y.getLsbD (i - w₃) else a) = a

case neg
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : ¬i < w₁ + w₂ + w₃
h₂ : ¬i < w₃
⊢ (if i < w₃ then z.getLsbD i else if i - w₃ < w₂ then y.getLsbD (i - w₃) else a) = a

Proof state:
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
⊢ w₁ + w₂ + w₃ + 1 = w₁ + 1 + w₂ + w₃

Tactic:
omega

Result:
no goals

Proof state:
case neg
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : i < w₁ + w₂ + w₃
h₁ : ¬i < w₃
h₂ : ¬i - w₃ < w₂
⊢ (if i - w₃ < w₂ then y.getLsbD (i - w₃)
    else if i - w₃ - w₂ < w₁ then x.getLsbD (i - w₃ - w₂) else decide (i - w₃ - w₂ - w₁ = 0) && a) =
    if i - w₃ < w₂ then y.getLsbD (i - w₃) else x.getLsbD (i - w₃ - w₂)

Tactic:
simp [h₂]

Result:
case neg
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : i < w₁ + w₂ + w₃
h₁ : ¬i < w₃
h₂ : ¬i - w₃ < w₂
⊢ w₁ ≤ i - w₃ - w₂ → (decide (i - w₃ - w₂ - w₁ = 0) && a) = x.getLsbD (i - w₃ - w₂)

Proof state:
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
⊢ cons a x ++ y ++ z = BitVec.cast ⋯ (cons a (x ++ y ++ z))

Tactic:
ext i h

Result:
case pred
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
⊢ (cons a x ++ y ++ z).getLsbD i = (BitVec.cast ⋯ (cons a (x ++ y ++ z))).getLsbD i

Proof state:
case pred
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
⊢ (cons a x ++ y ++ z).getLsbD i = (BitVec.cast ⋯ (cons a (x ++ y ++ z))).getLsbD i

Tactic:
simp only [cons, getLsbD_append, getLsbD_cast, getLsbD_ofBool, cast_cast]

Result:
case pred
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
⊢ (if i < w₃ then z.getLsbD i
    else
      if i - w₃ < w₂ then y.getLsbD (i - w₃)
      else if i - w₃ - w₂ < w₁ then x.getLsbD (i - w₃ - w₂) else decide (i - w₃ - w₂ - w₁ = 0) && a) =
    if i < w₁ + w₂ + w₃ then
      if i < w₃ then z.getLsbD i else if i - w₃ < w₂ then y.getLsbD (i - w₃) else x.getLsbD (i - w₃ - w₂)
    else decide (i - (w₁ + w₂ + w₃) = 0) && a

Proof state:
case pos
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : i < w₁ + w₂ + w₃
⊢ (if i < w₃ then z.getLsbD i
    else
      if i - w₃ < w₂ then y.getLsbD (i - w₃)
      else if i - w₃ - w₂ < w₁ then x.getLsbD (i - w₃ - w₂) else decide (i - w₃ - w₂ - w₁ = 0) && a) =
    if i < w₃ then z.getLsbD i else if i - w₃ < w₂ then y.getLsbD (i - w₃) else x.getLsbD (i - w₃ - w₂)

Tactic:
by_cases h₁ : i < w₃

Result:
case pos
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : i < w₁ + w₂ + w₃
h₁ : i < w₃
⊢ (if i < w₃ then z.getLsbD i
    else
      if i - w₃ < w₂ then y.getLsbD (i - w₃)
      else if i - w₃ - w₂ < w₁ then x.getLsbD (i - w₃ - w₂) else decide (i - w₃ - w₂ - w₁ = 0) && a) =
    if i < w₃ then z.getLsbD i else if i - w₃ < w₂ then y.getLsbD (i - w₃) else x.getLsbD (i - w₃ - w₂)

case neg
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : i < w₁ + w₂ + w₃
h₁ : ¬i < w₃
⊢ (if i < w₃ then z.getLsbD i
    else
      if i - w₃ < w₂ then y.getLsbD (i - w₃)
      else if i - w₃ - w₂ < w₁ then x.getLsbD (i - w₃ - w₂) else decide (i - w₃ - w₂ - w₁ = 0) && a) =
    if i < w₃ then z.getLsbD i else if i - w₃ < w₂ then y.getLsbD (i - w₃) else x.getLsbD (i - w₃ - w₂)

Proof state:
case pos
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : i < w₁ + w₂ + w₃
h₁ : i < w₃
⊢ (if i < w₃ then z.getLsbD i
    else
      if i - w₃ < w₂ then y.getLsbD (i - w₃)
      else if i - w₃ - w₂ < w₁ then x.getLsbD (i - w₃ - w₂) else decide (i - w₃ - w₂ - w₁ = 0) && a) =
    if i < w₃ then z.getLsbD i else if i - w₃ < w₂ then y.getLsbD (i - w₃) else x.getLsbD (i - w₃ - w₂)

Tactic:
simp [h₁]

Result:
no goals

Proof state:
case neg
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : i < w₁ + w₂ + w₃
h₁ : ¬i < w₃
h₂ : ¬i - w₃ < w₂
⊢ w₁ ≤ i - w₃ - w₂ → (decide (i - w₃ - w₂ - w₁ = 0) && a) = x.getLsbD (i - w₃ - w₂)

Tactic:
omega

Result:
no goals

Proof state:
case pos
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : i < w₁ + w₂ + w₃
h₁ : ¬i < w₃
h₂ : i - w₃ < w₂
⊢ (if i - w₃ < w₂ then y.getLsbD (i - w₃)
    else if i - w₃ - w₂ < w₁ then x.getLsbD (i - w₃ - w₂) else decide (i - w₃ - w₂ - w₁ = 0) && a) =
    if i - w₃ < w₂ then y.getLsbD (i - w₃) else x.getLsbD (i - w₃ - w₂)

Tactic:
simp [h₂]

Result:
no goals

Proof state:
case neg
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : i < w₁ + w₂ + w₃
h₁ : ¬i < w₃
⊢ (if i < w₃ then z.getLsbD i
    else
      if i - w₃ < w₂ then y.getLsbD (i - w₃)
      else if i - w₃ - w₂ < w₁ then x.getLsbD (i - w₃ - w₂) else decide (i - w₃ - w₂ - w₁ = 0) && a) =
    if i < w₃ then z.getLsbD i else if i - w₃ < w₂ then y.getLsbD (i - w₃) else x.getLsbD (i - w₃ - w₂)

Tactic:
simp only [h₁, ↓reduceIte]

Result:
case neg
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : i < w₁ + w₂ + w₃
h₁ : ¬i < w₃
⊢ (if i - w₃ < w₂ then y.getLsbD (i - w₃)
    else if i - w₃ - w₂ < w₁ then x.getLsbD (i - w₃ - w₂) else decide (i - w₃ - w₂ - w₁ = 0) && a) =
    if i - w₃ < w₂ then y.getLsbD (i - w₃) else x.getLsbD (i - w₃ - w₂)

Proof state:
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : ¬i < w₁ + w₂ + w₃
⊢ i - w₃ - w₂ - w₁ = 0

Tactic:
omega

Result:
no goals

Proof state:
case neg
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : ¬i < w₁ + w₂ + w₃
⊢ (if i < w₃ then z.getLsbD i
    else
      if i - w₃ < w₂ then y.getLsbD (i - w₃)
      else if i - w₃ - w₂ < w₁ then x.getLsbD (i - w₃ - w₂) else decide (i - w₃ - w₂ - w₁ = 0) && a) =
    if i < w₁ + w₂ + w₃ then
      if i < w₃ then z.getLsbD i else if i - w₃ < w₂ then y.getLsbD (i - w₃) else x.getLsbD (i - w₃ - w₂)
    else decide (i - (w₁ + w₂ + w₃) = 0) && a

Tactic:
simp only [show ¬i - w₃ - w₂ < w₁ by omega, ↓reduceIte, show i - w₃ - w₂ - w₁ = 0 by omega,
  decide_true, Bool.true_and, h₀, show i - (w₁ + w₂ + w₃) = 0 by omega]

Result:
case neg
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : ¬i < w₁ + w₂ + w₃
⊢ (if i < w₃ then z.getLsbD i else if i - w₃ < w₂ then y.getLsbD (i - w₃) else a) = a

Proof state:
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : ¬i < w₁ + w₂ + w₃
⊢ ¬i - w₃ - w₂ < w₁

Tactic:
omega

Result:
no goals