Theorem: PropagateStruc.eval_sub (Lean4bits/lemmas.lean)

State before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
⊢ eval sub x = subSeq (x true) (x false)
Tactic:
dsimp [sub, eval]
State after:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
⊢ propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x =
    subSeq (x true) (x false)

State before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
⊢ propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x =
    subSeq (x true) (x false)
Tactic:
rw [sub_eq_propagate]
State after:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
⊢ propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      fun b => bif b then x true else x false

State before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
⊢ propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      fun b => bif b then x true else x false
Tactic:
funext b
State after:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
b : ℕ
⊢ propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x b =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x true else x false) b

State before:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
b : ℕ
⊢ propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x b =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x true else x false) b
Tactic:
cases b
State after:
case h.zero
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
⊢ propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x Nat.zero =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x true else x false) Nat.zero

case h.succ
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n✝ : ℕ
⊢ propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x (Nat.succ n✝) =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x true else x false) (Nat.succ n✝)

State before:
case h.zero
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
⊢ propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x Nat.zero =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x true else x false) Nat.zero

case h.succ
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n✝ : ℕ
⊢ propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x (Nat.succ n✝) =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x true else x false) (Nat.succ n✝)
Tactic:
rfl
State after:
case h.succ
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n✝ : ℕ
⊢ propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x (Nat.succ n✝) =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x true else x false) (Nat.succ n✝)

State before:
case h.succ
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n✝ : ℕ
⊢ propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x (Nat.succ n✝) =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x true else x false) (Nat.succ n✝)
Tactic:
congr
State after:
case h.succ.e_x
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n✝ : ℕ
⊢ x = fun b => bif b then x true else x false

State before:
case h.succ.e_x
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n✝ : ℕ
⊢ x = fun b => bif b then x true else x false
Tactic:
funext i
State after:
case h.succ.e_x.h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n✝ : ℕ
i : Bool
⊢ x i = bif i then x true else x false

State before:
case h.succ.e_x.h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n✝ : ℕ
i : Bool
⊢ x i = bif i then x true else x false
Tactic:
cases i <;> simp
State after:
no goals