internlm/Lean-Github huggingface dataset:
Theorem: propagateCarry_changeVars
Proof state before:
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
x : β' → ℕ → Bool
i : ℕ
changeVars : β → β'
⊢ propagateCarry init_carry next_bit (fun b => x (changeVars b)) i =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x i
Tactic:
induction i
Proof state after:
case zero
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
x : β' → ℕ → Bool
changeVars : β → β'
⊢ propagateCarry init_carry next_bit (fun b => x (changeVars b)) Nat.zero =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x Nat.zero

case succ
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
x : β' → ℕ → Bool
changeVars : β → β'
n✝ : ℕ
n_ih✝ :
  propagateCarry init_carry next_bit (fun b => x (changeVars b)) n✝ =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x n✝
⊢ propagateCarry init_carry next_bit (fun b => x (changeVars b)) (Nat.succ n✝) =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x (Nat.succ n✝)
Theorem: propagateCarry_changeVars
Proof state before:
case zero
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
x : β' → ℕ → Bool
changeVars : β → β'
⊢ propagateCarry init_carry next_bit (fun b => x (changeVars b)) Nat.zero =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x Nat.zero

case succ
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
x : β' → ℕ → Bool
changeVars : β → β'
n✝ : ℕ
n_ih✝ :
  propagateCarry init_carry next_bit (fun b => x (changeVars b)) n✝ =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x n✝
⊢ propagateCarry init_carry next_bit (fun b => x (changeVars b)) (Nat.succ n✝) =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x (Nat.succ n✝)
Tactic:
. simp
Proof state after:
case succ
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
x : β' → ℕ → Bool
changeVars : β → β'
n✝ : ℕ
n_ih✝ :
  propagateCarry init_carry next_bit (fun b => x (changeVars b)) n✝ =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x n✝
⊢ propagateCarry init_carry next_bit (fun b => x (changeVars b)) (Nat.succ n✝) =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x (Nat.succ n✝)
Theorem: propagateCarry_changeVars
Proof state before:
case succ
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
x : β' → ℕ → Bool
changeVars : β → β'
n✝ : ℕ
n_ih✝ :
  propagateCarry init_carry next_bit (fun b => x (changeVars b)) n✝ =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x n✝
⊢ propagateCarry init_carry next_bit (fun b => x (changeVars b)) (Nat.succ n✝) =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x (Nat.succ n✝)
Tactic:
. simp [*]
Proof state after:
no goals
Theorem: propagate_changeVars
Proof state before:
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β' → ℕ → Bool
i : ℕ
changeVars : β → β'
⊢ propagate init_carry next_bit (fun b => x (changeVars b)) i =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x i
Tactic:
induction' i with i ih
Proof state after:
case zero
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β' → ℕ → Bool
changeVars : β → β'
⊢ propagate init_carry next_bit (fun b => x (changeVars b)) Nat.zero =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x Nat.zero

case succ
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β' → ℕ → Bool
changeVars : β → β'
i : ℕ
ih :
  propagate init_carry next_bit (fun b => x (changeVars b)) i =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x i
⊢ propagate init_carry next_bit (fun b => x (changeVars b)) (Nat.succ i) =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x (Nat.succ i)
Theorem: propagate_changeVars
Proof state before:
case zero
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β' → ℕ → Bool
changeVars : β → β'
⊢ propagate init_carry next_bit (fun b => x (changeVars b)) Nat.zero =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x Nat.zero

case succ
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β' → ℕ → Bool
changeVars : β → β'
i : ℕ
ih :
  propagate init_carry next_bit (fun b => x (changeVars b)) i =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x i
⊢ propagate init_carry next_bit (fun b => x (changeVars b)) (Nat.succ i) =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x (Nat.succ i)
Tactic:
. rfl
Proof state after:
case succ
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β' → ℕ → Bool
changeVars : β → β'
i : ℕ
ih :
  propagate init_carry next_bit (fun b => x (changeVars b)) i =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x i
⊢ propagate init_carry next_bit (fun b => x (changeVars b)) (Nat.succ i) =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x (Nat.succ i)
Theorem: propagate_changeVars
Proof state before:
case succ
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β' → ℕ → Bool
changeVars : β → β'
i : ℕ
ih :
  propagate init_carry next_bit (fun b => x (changeVars b)) i =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x i
⊢ propagate init_carry next_bit (fun b => x (changeVars b)) (Nat.succ i) =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x (Nat.succ i)
Tactic:
. simp only [propagate_succ, propagateCarry_changeVars, ih]
Proof state after:
no goals
Theorem: evalFin_eq_eval
Proof state before:
α β α' β' : Type
γ : β → Type
t : Term
vars : ℕ → ℕ → Bool
⊢ (evalFin t fun i => vars ↑i) = eval t vars
Tactic:
induction t <;>
dsimp [Term.evalFin, Term.eval, arity] at * <;> simp [*]
Proof state after:
no goals
Theorem: id_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
⊢ x = propagate Empty.elim (fun x y => (Empty.elim, y ())) fun x_1 => x
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ x n = propagate Empty.elim (fun x y => (Empty.elim, y ())) (fun x_1 => x) n
Theorem: id_eq_propagate
Proof state before:
case h
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ x n = propagate Empty.elim (fun x y => (Empty.elim, y ())) (fun x_1 => x) n
Tactic:
cases n <;> rfl
Proof state after:
no goals
Theorem: zero_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
⊢ zeroSeq = propagate Empty.elim (fun x x => (Empty.elim, false)) Empty.elim
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
n : ℕ
⊢ zeroSeq n = propagate Empty.elim (fun x x => (Empty.elim, false)) Empty.elim n
Theorem: zero_eq_propagate
Proof state before:
case h
α β α' β' : Type
γ : β → Type
n : ℕ
⊢ zeroSeq n = propagate Empty.elim (fun x x => (Empty.elim, false)) Empty.elim n
Tactic:
cases n <;> rfl
Proof state after:
no goals
Theorem: one_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
⊢ oneSeq = propagate (fun x => true) (fun f x => (fun x => false, f ())) Empty.elim
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
n : ℕ
⊢ oneSeq n = propagate (fun x => true) (fun f x => (fun x => false, f ())) Empty.elim n
Theorem: one_eq_propagate
Proof state before:
case h
α β α' β' : Type
γ : β → Type
n : ℕ
⊢ oneSeq n = propagate (fun x => true) (fun f x => (fun x => false, f ())) Empty.elim n
Tactic:
match n with
| 0 => rfl
| 1 => rfl
| n+2 => simp [oneSeq, propagate_succ]
Proof state after:
no goals
Theorem: one_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
n : ℕ
⊢ oneSeq 0 = propagate (fun x => true) (fun f x => (fun x => false, f ())) Empty.elim 0
Tactic:
rfl
Proof state after:
no goals
Theorem: one_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
n : ℕ
⊢ oneSeq 1 = propagate (fun x => true) (fun f x => (fun x => false, f ())) Empty.elim 1
Tactic:
rfl
Proof state after:
no goals
Theorem: one_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
n✝ n : ℕ
⊢ oneSeq (n + 2) = propagate (fun x => true) (fun f x => (fun x => false, f ())) Empty.elim (n + 2)
Tactic:
simp [oneSeq, propagate_succ]
Proof state after:
no goals
Theorem: and_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
⊢ andSeq x y = propagate Empty.elim (fun x y => (Empty.elim, y true && y false)) fun b => bif b then x else y
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ andSeq x y n = propagate Empty.elim (fun x y => (Empty.elim, y true && y false)) (fun b => bif b then x else y) n
Theorem: and_eq_propagate
Proof state before:
case h
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ andSeq x y n = propagate Empty.elim (fun x y => (Empty.elim, y true && y false)) (fun b => bif b then x else y) n
Tactic:
cases n <;> simp [propagate, propagateAux, andSeq]
Proof state after:
no goals
Theorem: or_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
⊢ orSeq x y = propagate Empty.elim (fun x y => (Empty.elim, y true || y false)) fun b => bif b then x else y
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ orSeq x y n = propagate Empty.elim (fun x y => (Empty.elim, y true || y false)) (fun b => bif b then x else y) n
Theorem: or_eq_propagate
Proof state before:
case h
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ orSeq x y n = propagate Empty.elim (fun x y => (Empty.elim, y true || y false)) (fun b => bif b then x else y) n
Tactic:
cases n <;> simp [propagate, propagateAux, orSeq]
Proof state after:
no goals
Theorem: xor_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
⊢ xorSeq x y =
    propagate Empty.elim (fun x y => (Empty.elim, _root_.xor (y true) (y false))) fun b => bif b then x else y
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ xorSeq x y n =
    propagate Empty.elim (fun x y => (Empty.elim, _root_.xor (y true) (y false))) (fun b => bif b then x else y) n
Theorem: xor_eq_propagate
Proof state before:
case h
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ xorSeq x y n =
    propagate Empty.elim (fun x y => (Empty.elim, _root_.xor (y true) (y false))) (fun b => bif b then x else y) n
Tactic:
cases n <;> simp [propagate, propagateAux, xorSeq]
Proof state after:
no goals
Theorem: not_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
⊢ notSeq x = propagate Empty.elim (fun x y => (Empty.elim, !y ())) fun x_1 => x
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ notSeq x n = propagate Empty.elim (fun x y => (Empty.elim, !y ())) (fun x_1 => x) n
Theorem: not_eq_propagate
Proof state before:
case h
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ notSeq x n = propagate Empty.elim (fun x y => (Empty.elim, !y ())) (fun x_1 => x) n
Tactic:
cases n <;> simp [propagate, propagateAux, notSeq]
Proof state after:
no goals
Theorem: ls_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
⊢ lsSeq x = propagate (fun x => false) (fun carry x => (x, carry ())) fun x_1 => x
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ lsSeq x n = propagate (fun x => false) (fun carry x => (x, carry ())) (fun x_1 => x) n
Theorem: ls_eq_propagate
Proof state before:
case h
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ lsSeq x n = propagate (fun x => false) (fun carry x => (x, carry ())) (fun x_1 => x) n
Tactic:
match n with
| 0 => rfl
| 1 => rfl
| n+2 => simp [lsSeq, propagate_succ]
Proof state after:
no goals
Theorem: ls_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ lsSeq x 0 = propagate (fun x => false) (fun carry x => (x, carry ())) (fun x_1 => x) 0
Tactic:
rfl
Proof state after:
no goals
Theorem: ls_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ lsSeq x 1 = propagate (fun x => false) (fun carry x => (x, carry ())) (fun x_1 => x) 1
Tactic:
rfl
Proof state after:
no goals
Theorem: ls_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n✝ n : ℕ
⊢ lsSeq x (n + 2) = propagate (fun x => false) (fun carry x => (x, carry ())) (fun x_1 => x) (n + 2)
Tactic:
simp [lsSeq, propagate_succ]
Proof state after:
no goals
Theorem: addSeqAux_eq_propagateCarry
Proof state before:
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ (addSeqAux x y n).snd =
    propagateCarry (fun x => false)
      (fun carry bits x => bits true && bits false || bits false && carry () || bits true && carry ())
      (fun b => bif b then x else y) n ()
Tactic:
induction n <;> simp [addSeqAux, *]
Proof state after:
no goals
Theorem: add_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
⊢ addSeq x y =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => bits true && bits false || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      fun b => bif b then x else y
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ addSeq x y n =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => bits true && bits false || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x else y) n
Theorem: add_eq_propagate
Proof state before:
case h
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ addSeq x y n =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => bits true && bits false || bits false && carry () || bits true && 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 [addSeq, addSeqAux]
| 1 => simp [addSeq, addSeqAux, propagate, propagateAux]
| n+2 => simp [addSeq, addSeqAux, addSeqAux_eq_propagateCarry, propagate_succ]
Proof state after:
no goals
Theorem: add_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ addSeq x y 0 =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => bits true && bits false || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x else y) 0
Tactic:
simp [addSeq, addSeqAux]
Proof state after:
no goals
Theorem: add_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ addSeq x y 1 =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => bits true && bits false || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x else y) 1
Tactic:
simp [addSeq, addSeqAux, propagate, propagateAux]
Proof state after:
no goals
Theorem: add_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n✝ n : ℕ
⊢ addSeq x y (n + 2) =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => bits true && bits false || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x else y) (n + 2)
Tactic:
simp [addSeq, addSeqAux, addSeqAux_eq_propagateCarry, propagate_succ]
Proof state after:
no goals
Theorem: subSeqAux_eq_propagateCarry
Proof state before:
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ (subSeqAux x y n).snd =
    propagateCarry (fun x => false)
      (fun carry bits x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry ())
      (fun b => bif b then x else y) n ()
Tactic:
induction n <;> simp [subSeqAux, *]
Proof state after:
no goals
Theorem: sub_eq_propagate
Proof 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
Proof 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
Theorem: sub_eq_propagate
Proof 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]
Proof state after:
no goals
Theorem: sub_eq_propagate
Proof 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]
Proof state after:
no goals
Theorem: sub_eq_propagate
Proof 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]
Proof state after:
no goals
Theorem: sub_eq_propagate
Proof 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]
Proof state after:
no goals
Theorem: negSeqAux_eq_propagateCarry
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ (negSeqAux x n).snd = propagateCarry (fun x => true) (fun carry bits x => !bits () && carry ()) (fun x_1 => x) n ()
Tactic:
induction n <;> simp [negSeqAux, *]
Proof state after:
no goals
Theorem: neg_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
⊢ negSeq x =
    propagate (fun x => true) (fun carry bits => (fun x => !bits () && carry (), _root_.xor (!bits ()) (carry ())))
      fun x_1 => x
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ negSeq x n =
    propagate (fun x => true) (fun carry bits => (fun x => !bits () && carry (), _root_.xor (!bits ()) (carry ())))
      (fun x_1 => x) n
Theorem: neg_eq_propagate
Proof state before:
case h
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ negSeq x n =
    propagate (fun x => true) (fun carry bits => (fun x => !bits () && carry (), _root_.xor (!bits ()) (carry ())))
      (fun x_1 => x) n
Tactic:
match n with
| 0 => simp [negSeq, negSeqAux]
| 1 => simp [negSeq, negSeqAux, propagate, propagateAux]
| n+2 => simp [negSeq, negSeqAux, negSeqAux_eq_propagateCarry, propagate_succ]
Proof state after:
no goals
Theorem: neg_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ negSeq x 0 =
    propagate (fun x => true) (fun carry bits => (fun x => !bits () && carry (), _root_.xor (!bits ()) (carry ())))
      (fun x_1 => x) 0
Tactic:
simp [negSeq, negSeqAux]
Proof state after:
no goals
Theorem: neg_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ negSeq x 1 =
    propagate (fun x => true) (fun carry bits => (fun x => !bits () && carry (), _root_.xor (!bits ()) (carry ())))
      (fun x_1 => x) 1
Tactic:
simp [negSeq, negSeqAux, propagate, propagateAux]
Proof state after:
no goals
Theorem: neg_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n✝ n : ℕ
⊢ negSeq x (n + 2) =
    propagate (fun x => true) (fun carry bits => (fun x => !bits () && carry (), _root_.xor (!bits ()) (carry ())))
      (fun x_1 => x) (n + 2)
Tactic:
simp [negSeq, negSeqAux, negSeqAux_eq_propagateCarry, propagate_succ]
Proof state after:
no goals
Theorem: incrSeqAux_eq_propagateCarry
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ (incrSeqAux x n).snd = propagateCarry (fun x => true) (fun carry bits x => bits () && carry ()) (fun x_1 => x) n ()
Tactic:
induction n <;> simp [incrSeqAux, *]
Proof state after:
no goals
Theorem: incr_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
⊢ incrSeq x =
    propagate (fun x => true) (fun carry bits => (fun x => bits () && carry (), _root_.xor (bits ()) (carry ())))
      fun x_1 => x
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ incrSeq x n =
    propagate (fun x => true) (fun carry bits => (fun x => bits () && carry (), _root_.xor (bits ()) (carry ())))
      (fun x_1 => x) n
Theorem: incr_eq_propagate
Proof state before:
case h
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ incrSeq x n =
    propagate (fun x => true) (fun carry bits => (fun x => bits () && carry (), _root_.xor (bits ()) (carry ())))
      (fun x_1 => x) n
Tactic:
match n with
| 0 => simp [incrSeq, incrSeqAux]
| 1 => simp [incrSeq, incrSeqAux, propagate, propagateAux]
| n+2 => simp [incrSeq, incrSeqAux, incrSeqAux_eq_propagateCarry, propagate_succ]
Proof state after:
no goals
Theorem: incr_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ incrSeq x 0 =
    propagate (fun x => true) (fun carry bits => (fun x => bits () && carry (), _root_.xor (bits ()) (carry ())))
      (fun x_1 => x) 0
Tactic:
simp [incrSeq, incrSeqAux]
Proof state after:
no goals
Theorem: incr_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ incrSeq x 1 =
    propagate (fun x => true) (fun carry bits => (fun x => bits () && carry (), _root_.xor (bits ()) (carry ())))
      (fun x_1 => x) 1
Tactic:
simp [incrSeq, incrSeqAux, propagate, propagateAux]
Proof state after:
no goals
Theorem: incr_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n✝ n : ℕ
⊢ incrSeq x (n + 2) =
    propagate (fun x => true) (fun carry bits => (fun x => bits () && carry (), _root_.xor (bits ()) (carry ())))
      (fun x_1 => x) (n + 2)
Tactic:
simp [incrSeq, incrSeqAux, incrSeqAux_eq_propagateCarry, propagate_succ]
Proof state after:
no goals