internlm/Lean-Github huggingface dataset:
Theorem: decrSeqAux_eq_propagateCarry
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ (decrSeqAux x n).snd = propagateCarry (fun x => true) (fun carry bits x => !bits () && carry ()) (fun x_1 => x) n ()
Tactic:
induction n <;> simp [decrSeqAux, *]
Proof state after:
no goals
Theorem: decr_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
⊢ decrSeq 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 : ℕ
⊢ decrSeq x n =
    propagate (fun x => true) (fun carry bits => (fun x => !bits () && carry (), _root_.xor (bits ()) (carry ())))
      (fun x_1 => x) n
Theorem: decr_eq_propagate
Proof state before:
case h
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ decrSeq 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 [decrSeq, decrSeqAux]
| 1 => simp [decrSeq, decrSeqAux, propagate, propagateAux]
| n+2 => simp [decrSeq, decrSeqAux, decrSeqAux_eq_propagateCarry, propagate_succ]
Proof state after:
no goals
Theorem: decr_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ decrSeq x 0 =
    propagate (fun x => true) (fun carry bits => (fun x => !bits () && carry (), _root_.xor (bits ()) (carry ())))
      (fun x_1 => x) 0
Tactic:
simp [decrSeq, decrSeqAux]
Proof state after:
no goals
Theorem: decr_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ decrSeq x 1 =
    propagate (fun x => true) (fun carry bits => (fun x => !bits () && carry (), _root_.xor (bits ()) (carry ())))
      (fun x_1 => x) 1
Tactic:
simp [decrSeq, decrSeqAux, propagate, propagateAux]
Proof state after:
no goals
Theorem: decr_eq_propagate
Proof state before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n✝ n : ℕ
⊢ decrSeq 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 [decrSeq, decrSeqAux, decrSeqAux_eq_propagateCarry, propagate_succ]
Proof state after:
no goals
Theorem: PropagateStruc.eval_compose
Proof state before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
inst✝ : Fintype arity
new_arity : Type
q_arity : arity → Type
vars : (a : arity) → q_arity a → new_arity
q : (a : arity) → PropagateStruc (q_arity a)
x : new_arity → ℕ → Bool
⊢ eval (compose p new_arity q_arity vars q) x = eval p fun a => eval (q a) fun i => x (vars a i)
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
inst✝ : Fintype arity
new_arity : Type
q_arity : arity → Type
vars : (a : arity) → q_arity a → new_arity
q : (a : arity) → PropagateStruc (q_arity a)
x : new_arity → ℕ → Bool
n : ℕ
⊢ eval (compose p new_arity q_arity vars q) x n = eval p (fun a => eval (q a) fun i => x (vars a i)) n
Theorem: PropagateStruc.eval_compose
Proof state before:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
inst✝ : Fintype arity
new_arity : Type
q_arity : arity → Type
vars : (a : arity) → q_arity a → new_arity
q : (a : arity) → PropagateStruc (q_arity a)
x : new_arity → ℕ → Bool
n : ℕ
⊢ eval (compose p new_arity q_arity vars q) x n = eval p (fun a => eval (q a) fun i => x (vars a i)) n
Tactic:
simp only [eval, compose, propagate_propagate]
Proof state after:
no goals
Theorem: PropagateStruc.eval_and
Proof state before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
⊢ eval and x = andSeq (x true) (x false)
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n : ℕ
⊢ eval and x n = andSeq (x true) (x false) n
Theorem: PropagateStruc.eval_and
Proof state before:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n : ℕ
⊢ eval and x n = andSeq (x true) (x false) n
Tactic:
cases n <;> simp [and, andSeq, eval, propagate_succ]
Proof state after:
no goals
Theorem: PropagateStruc.eval_or
Proof state before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
⊢ eval or x = orSeq (x true) (x false)
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n : ℕ
⊢ eval or x n = orSeq (x true) (x false) n
Theorem: PropagateStruc.eval_or
Proof state before:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n : ℕ
⊢ eval or x n = orSeq (x true) (x false) n
Tactic:
cases n <;> simp [or, orSeq, eval, propagate_succ]
Proof state after:
no goals
Theorem: PropagateStruc.eval_xor
Proof state before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
⊢ eval xor x = xorSeq (x true) (x false)
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n : ℕ
⊢ eval xor x n = xorSeq (x true) (x false) n
Theorem: PropagateStruc.eval_xor
Proof state before:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n : ℕ
⊢ eval xor x n = xorSeq (x true) (x false) n
Tactic:
cases n <;> simp [xor, xorSeq, eval, propagate_succ]
Proof state after:
no goals
Theorem: PropagateStruc.eval_add
Proof state before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
⊢ eval add x = addSeq (x true) (x false)
Tactic:
dsimp [add, eval]
Proof 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 || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x =
    addSeq (x true) (x false)
Theorem: PropagateStruc.eval_add
Proof 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 || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x =
    addSeq (x true) (x false)
Tactic:
rw [add_eq_propagate]
Proof 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 || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x =
    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 true else x false
Theorem: PropagateStruc.eval_add
Proof 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 || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x =
    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 true else x false
Tactic:
funext b
Proof 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 || bits false && carry () || bits true && 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 || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x true else x false) b
Theorem: PropagateStruc.eval_add
Proof 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 || bits false && carry () || bits true && 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 || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x true else x false) b
Tactic:
cases b
Proof 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 || bits false && carry () || bits true && 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 || bits false && carry () || bits true && 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 || bits false && carry () || bits true && 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 || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x true else x false) (Nat.succ n✝)
Theorem: PropagateStruc.eval_add
Proof 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 || bits false && carry () || bits true && 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 || bits false && carry () || bits true && 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 || bits false && carry () || bits true && 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 || bits false && carry () || bits true && 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
Proof 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 || bits false && carry () || bits true && 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 || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x true else x false) (Nat.succ n✝)
Theorem: PropagateStruc.eval_add
Proof 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 || bits false && carry () || bits true && 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 || bits false && carry () || bits true && 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
Proof 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
Theorem: PropagateStruc.eval_add
Proof 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
Proof 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
Theorem: PropagateStruc.eval_add
Proof 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
Proof state after:
no goals
Theorem: PropagateStruc.eval_sub
Proof state before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
⊢ eval sub x = subSeq (x true) (x false)
Tactic:
dsimp [sub, eval]
Proof 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)
Theorem: PropagateStruc.eval_sub
Proof 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]
Proof 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
Theorem: PropagateStruc.eval_sub
Proof 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
Proof 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
Theorem: PropagateStruc.eval_sub
Proof 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
Proof 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✝)
Theorem: PropagateStruc.eval_sub
Proof 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
Proof 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✝)
Theorem: PropagateStruc.eval_sub
Proof 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
Proof 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
Theorem: PropagateStruc.eval_sub
Proof 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
Proof 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
Theorem: PropagateStruc.eval_sub
Proof 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
Proof state after:
no goals
Theorem: PropagateStruc.eval_neg
Proof state before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
⊢ eval neg x = negSeq (x ())
Tactic:
dsimp [neg, eval]
Proof state after:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
⊢ propagate (fun x => true) (fun carry bits => (fun x => !bits () && carry (), _root_.xor (!bits ()) (carry ()))) x =
    negSeq (x ())
Theorem: PropagateStruc.eval_neg
Proof state before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
⊢ propagate (fun x => true) (fun carry bits => (fun x => !bits () && carry (), _root_.xor (!bits ()) (carry ()))) x =
    negSeq (x ())
Tactic:
rw [neg_eq_propagate]
Proof state after:
no goals
Theorem: PropagateStruc.eval_not
Proof state before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
⊢ eval not x = notSeq (x ())
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
n : ℕ
⊢ eval not x n = notSeq (x ()) n
Theorem: PropagateStruc.eval_not
Proof state before:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
n : ℕ
⊢ eval not x n = notSeq (x ()) n
Tactic:
cases n <;> simp [not, notSeq, eval, propagate_succ]
Proof state after:
no goals
Theorem: PropagateStruc.eval_zero
Proof state before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Fin 0 → ℕ → Bool
⊢ eval zero x = zeroSeq
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Fin 0 → ℕ → Bool
n : ℕ
⊢ eval zero x n = zeroSeq n
Theorem: PropagateStruc.eval_zero
Proof state before:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Fin 0 → ℕ → Bool
n : ℕ
⊢ eval zero x n = zeroSeq n
Tactic:
cases n <;> simp [zero, zeroSeq, eval, propagate_succ]
Proof state after:
no goals