Theorem: sub_eq_propagate (Lean4bits/lemmas.lean)

State before:
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
⊢ subSeq x y =
    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 else y
Tactic:
ext n
State after:
case h
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ subSeq x y 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 else y) n

State before:
case h
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ subSeq x y 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 else y) n
Tactic:
match n with
| 0 => simp [subSeq, subSeqAux]
| 1 => simp [subSeq, subSeqAux, propagate, propagateAux]
| n+2 => simp [subSeq, subSeqAux, subSeqAux_eq_propagateCarry, propagate_succ]
State after:
no goals

State before:
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ subSeq x y 0 =
    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 else y) 0
Tactic:
simp [subSeq, subSeqAux]
State after:
no goals

State before:
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ subSeq x y 1 =
    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 else y) 1
Tactic:
simp [subSeq, subSeqAux, propagate, propagateAux]
State after:
no goals

State before:
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n✝ n : ℕ
⊢ subSeq x y (n + 2) =
    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 else y) (n + 2)
Tactic:
simp [subSeq, subSeqAux, subSeqAux_eq_propagateCarry, propagate_succ]
State after:
no goals