internlm/Lean-Github huggingface dataset:
Theorem: PropagateStruc.eval_one
Proof state before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Fin 0 → ℕ → Bool
⊢ eval one x = oneSeq
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Fin 0 → ℕ → Bool
n : ℕ
⊢ eval one x n = oneSeq n
Theorem: PropagateStruc.eval_one
Proof state before:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Fin 0 → ℕ → Bool
n : ℕ
⊢ eval one x n = oneSeq n
Tactic:
cases n <;> simp [one, oneSeq, eval, propagate_succ2, @eq_comm _ false]
Proof state after:
no goals
Theorem: PropagateStruc.eval_negOne
Proof state before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Fin 0 → ℕ → Bool
⊢ eval negOne x = negOneSeq
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Fin 0 → ℕ → Bool
n : ℕ
⊢ eval negOne x n = negOneSeq n
Theorem: PropagateStruc.eval_negOne
Proof state before:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Fin 0 → ℕ → Bool
n : ℕ
⊢ eval negOne x n = negOneSeq n
Tactic:
cases n <;> simp [negOne, negOneSeq, eval, propagate_succ2]
Proof state after:
no goals
Theorem: PropagateStruc.eval_ls
Proof state before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
⊢ eval ls x = lsSeq (x ())
Tactic:
ext n
Proof state after:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
n : ℕ
⊢ eval ls x n = lsSeq (x ()) n
Theorem: PropagateStruc.eval_ls
Proof state before:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
n : ℕ
⊢ eval ls x n = lsSeq (x ()) n
Tactic:
cases n <;> simp [ls, lsSeq, eval, propagate_succ2]
Proof state after:
no goals
Theorem: PropagateStruc.eval_var
Proof state before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
n : ℕ
x : Fin (n + 1) → ℕ → Bool
⊢ eval (var n) x = x (Fin.last n)
Tactic:
ext m
Proof state after:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
n : ℕ
x : Fin (n + 1) → ℕ → Bool
m : ℕ
⊢ eval (var n) x m = x (Fin.last n) m
Theorem: PropagateStruc.eval_var
Proof state before:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
n : ℕ
x : Fin (n + 1) → ℕ → Bool
m : ℕ
⊢ eval (var n) x m = x (Fin.last n) m
Tactic:
cases m <;> simp [var, eval, propagate_succ]
Proof state after:
no goals
Theorem: PropagateStruc.eval_incr
Proof state before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
⊢ eval incr x = incrSeq (x ())
Tactic:
dsimp [incr, 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 =
    incrSeq (x ())
Theorem: PropagateStruc.eval_incr
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 =
    incrSeq (x ())
Tactic:
rw [incr_eq_propagate]
Proof state after:
no goals
Theorem: PropagateStruc.eval_decr
Proof state before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
⊢ eval decr x = decrSeq (x ())
Tactic:
dsimp [decr, 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 =
    decrSeq (x ())
Theorem: PropagateStruc.eval_decr
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 =
    decrSeq (x ())
Tactic:
rw [decr_eq_propagate]
Proof state after:
no goals
Theorem: composeUnary_eval
Proof state before:
α β α' β' : Type
γ : β → Type
p : PropagateStruc Unit
t : Term
q : PropagateSolution t
x : Fin (arity t) → ℕ → Bool
⊢ PropagateStruc.eval (composeUnary p q) x = PropagateStruc.eval p fun x_1 => evalFin t x
Tactic:
rw [composeUnary, PropagateStruc.eval_compose, q.good]
Proof state after:
α β α' β' : Type
γ : β → Type
p : PropagateStruc Unit
t : Term
q : PropagateSolution t
x : Fin (arity t) → ℕ → Bool
⊢ (PropagateStruc.eval p fun a => PropagateStruc.eval q.toPropagateStruc fun i => x (id i)) =
    PropagateStruc.eval p fun x_1 => PropagateStruc.eval q.toPropagateStruc x
Theorem: composeUnary_eval
Proof state before:
α β α' β' : Type
γ : β → Type
p : PropagateStruc Unit
t : Term
q : PropagateSolution t
x : Fin (arity t) → ℕ → Bool
⊢ (PropagateStruc.eval p fun a => PropagateStruc.eval q.toPropagateStruc fun i => x (id i)) =
    PropagateStruc.eval p fun x_1 => PropagateStruc.eval q.toPropagateStruc x
Tactic:
rfl
Proof state after:
no goals
Theorem: composeBinary_eval
Proof state before:
α β α' β' : Type
γ : β → Type
p : PropagateStruc Bool
t₁ t₂ : Term
q₁ : PropagateSolution t₁
q₂ : PropagateSolution t₂
x : Fin (max (arity t₁) (arity t₂)) → ℕ → Bool
b : Bool
i : Fin (arity t₁)
⊢ arity t₁ ≤ max (arity t₁) (arity t₂)
Tactic:
simp
Proof state after:
no goals
Theorem: composeBinary_eval
Proof state before:
α β α' β' : Type
γ : β → Type
p : PropagateStruc Bool
t₁ t₂ : Term
q₁ : PropagateSolution t₁
q₂ : PropagateSolution t₂
x : Fin (max (arity t₁) (arity t₂)) → ℕ → Bool
b : Bool
i : Fin (arity t₂)
⊢ arity t₂ ≤ max (arity t₁) (arity t₂)
Tactic:
simp
Proof state after:
no goals
Theorem: composeBinary_eval
Proof state before:
α β α' β' : Type
γ : β → Type
p : PropagateStruc Bool
t₁ t₂ : Term
q₁ : PropagateSolution t₁
q₂ : PropagateSolution t₂
x : Fin (max (arity t₁) (arity t₂)) → ℕ → Bool
⊢ PropagateStruc.eval (composeBinary p q₁ q₂) x =
    PropagateStruc.eval p fun b =>
      bif b then evalFin t₁ fun i => x (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)
      else evalFin t₂ fun i => x (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)
Tactic:
rw [composeBinary, PropagateStruc.eval_compose, q₁.good, q₂.good]
Proof state after:
α β α' β' : Type
γ : β → Type
p : PropagateStruc Bool
t₁ t₂ : Term
q₁ : PropagateSolution t₁
q₂ : PropagateSolution t₂
x : Fin (max (arity t₁) (arity t₂)) → ℕ → Bool
⊢ (PropagateStruc.eval p fun a =>
      PropagateStruc.eval
        (match a with
        | true => q₁.toPropagateStruc
        | false => q₂.toPropagateStruc)
        fun i =>
        x (↑(Fin.castLe (_ : (bif a then arity t₁ else arity t₂) ≤ max (arity t₁) (arity t₂))).toEmbedding i)) =
    PropagateStruc.eval p fun b =>
      bif b then
        PropagateStruc.eval q₁.toPropagateStruc fun i =>
          x (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)
      else
        PropagateStruc.eval q₂.toPropagateStruc fun i =>
          x (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)
Theorem: composeBinary_eval
Proof state before:
α β α' β' : Type
γ : β → Type
p : PropagateStruc Bool
t₁ t₂ : Term
q₁ : PropagateSolution t₁
q₂ : PropagateSolution t₂
x : Fin (max (arity t₁) (arity t₂)) → ℕ → Bool
⊢ (PropagateStruc.eval p fun a =>
      PropagateStruc.eval
        (match a with
        | true => q₁.toPropagateStruc
        | false => q₂.toPropagateStruc)
        fun i =>
        x (↑(Fin.castLe (_ : (bif a then arity t₁ else arity t₂) ≤ max (arity t₁) (arity t₂))).toEmbedding i)) =
    PropagateStruc.eval p fun b =>
      bif b then
        PropagateStruc.eval q₁.toPropagateStruc fun i =>
          x (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)
      else
        PropagateStruc.eval q₂.toPropagateStruc fun i =>
          x (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)
Tactic:
ext b
Proof state after:
case h
α β α' β' : Type
γ : β → Type
p : PropagateStruc Bool
t₁ t₂ : Term
q₁ : PropagateSolution t₁
q₂ : PropagateSolution t₂
x : Fin (max (arity t₁) (arity t₂)) → ℕ → Bool
b : ℕ
⊢ PropagateStruc.eval p
      (fun a =>
        PropagateStruc.eval
          (match a with
          | true => q₁.toPropagateStruc
          | false => q₂.toPropagateStruc)
          fun i =>
          x (↑(Fin.castLe (_ : (bif a then arity t₁ else arity t₂) ≤ max (arity t₁) (arity t₂))).toEmbedding i))
      b =
    PropagateStruc.eval p
      (fun b =>
        bif b then
          PropagateStruc.eval q₁.toPropagateStruc fun i =>
            x (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)
        else
          PropagateStruc.eval q₂.toPropagateStruc fun i =>
            x (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i))
      b
Theorem: composeBinary_eval
Proof state before:
case h
α β α' β' : Type
γ : β → Type
p : PropagateStruc Bool
t₁ t₂ : Term
q₁ : PropagateSolution t₁
q₂ : PropagateSolution t₂
x : Fin (max (arity t₁) (arity t₂)) → ℕ → Bool
b : ℕ
⊢ PropagateStruc.eval p
      (fun a =>
        PropagateStruc.eval
          (match a with
          | true => q₁.toPropagateStruc
          | false => q₂.toPropagateStruc)
          fun i =>
          x (↑(Fin.castLe (_ : (bif a then arity t₁ else arity t₂) ≤ max (arity t₁) (arity t₂))).toEmbedding i))
      b =
    PropagateStruc.eval p
      (fun b =>
        bif b then
          PropagateStruc.eval q₁.toPropagateStruc fun i =>
            x (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)
        else
          PropagateStruc.eval q₂.toPropagateStruc fun i =>
            x (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i))
      b
Tactic:
cases b <;> dsimp <;> congr <;> funext b <;> cases b <;> simp
Proof state after:
no goals
Theorem: cond_propagate
Proof state before:
α✝ β✝ α'✝ β'✝ : Type
γ✝ : β✝ → Type
α α' β β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
init_carry' : α' → Bool
next_bit' : (α' → Bool) → (β' → Bool) → (α' → Bool) × Bool
γ : Type
fβ : β → γ
fβ' : β' → γ
x : γ → ℕ → Bool
b : Bool
⊢ (bif b then propagate init_carry next_bit fun b => x (fβ b) else propagate init_carry' next_bit' fun b => x (fβ' b)) =
    propagate
      (let_fun this := Bool.rec (motive := fun x => (bif x then α else α') → Bool) init_carry' init_carry b;
      this)
      (let_fun this :=
        Bool.rec (motive := fun x =>
          ((bif x then α else α') → Bool) → ((bif x then β else β') → Bool) → ((bif x then α else α') → Bool) × Bool)
          next_bit' next_bit b;
      this)
      (let_fun this :=
        Bool.rec (motive := fun x => (bif x then β else β') → ℕ → Bool) (fun b => x (fβ' b)) (fun b => x (fβ b)) b;
      this)
Tactic:
cases b <;> rfl
Proof state after:
no goals
Theorem: exists_repeat_carry
Proof state before:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
⊢ ∃ n m, propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m ∧ n < m
Tactic:
by_contra h
Proof state after:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
h : ¬∃ n m, propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m ∧ n < m
⊢ False
Theorem: exists_repeat_carry
Proof state before:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
h : ¬∃ n m, propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m ∧ n < m
⊢ False
Tactic:
haveI := Classical.decEq α
Proof state after:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
h : ¬∃ n m, propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m ∧ n < m
this : DecidableEq α
⊢ False
Theorem: exists_repeat_carry
Proof state before:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
h : ¬∃ n m, propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m ∧ n < m
this : DecidableEq α
⊢ False
Tactic:
push_neg at h
Proof state after:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
this : DecidableEq α
h :
  ∀ (n m : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m → m ≤ n
⊢ False
Theorem: exists_repeat_carry
Proof state before:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
this : DecidableEq α
h :
  ∀ (n m : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m → m ≤ n
⊢ False
Tactic:
have := λ a b hab => (le_antisymm (h a b hab) (h b a hab.symm)).symm
Proof state after:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
this✝ : DecidableEq α
h :
  ∀ (n m : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m → m ≤ n
this :
  ∀ (a b : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑a = propagateCarry2 init_carry next_carry seq ↑b → a = b
⊢ False
Theorem: exists_repeat_carry
Proof state before:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
this✝ : DecidableEq α
h :
  ∀ (n m : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m → m ≤ n
this :
  ∀ (a b : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑a = propagateCarry2 init_carry next_carry seq ↑b → a = b
⊢ False
Tactic:
have := Fintype.card_le_of_injective _ this
Proof state after:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
this✝¹ : DecidableEq α
h :
  ∀ (n m : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m → m ≤ n
this✝ :
  ∀ (a b : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑a = propagateCarry2 init_carry next_carry seq ↑b → a = b
this : card (Fin (2 ^ card α + 1)) ≤ card (α → Bool)
⊢ False
Theorem: exists_repeat_carry
Proof state before:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
this✝¹ : DecidableEq α
h :
  ∀ (n m : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m → m ≤ n
this✝ :
  ∀ (a b : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑a = propagateCarry2 init_carry next_carry seq ↑b → a = b
this : card (Fin (2 ^ card α + 1)) ≤ card (α → Bool)
⊢ False
Tactic:
simp at this
Proof state after:
no goals
Theorem: propagateCarry2_eq_of_seq_eq_lt
Proof state before:
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry✝ : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
i : ℕ
h : ∀ (b : β) (j : ℕ), j < i → seq₁ b j = seq₂ b j
⊢ propagateCarry2 init_carry next_carry seq₁ i = propagateCarry2 init_carry next_carry seq₂ i
Tactic:
induction' i with i ih
Proof state after:
case zero
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry✝ : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
i : ℕ
h✝ : ∀ (b : β) (j : ℕ), j < i → seq₁ b j = seq₂ b j
h : ∀ (b : β) (j : ℕ), j < Nat.zero → seq₁ b j = seq₂ b j
⊢ propagateCarry2 init_carry next_carry seq₁ Nat.zero = propagateCarry2 init_carry next_carry seq₂ Nat.zero

case succ
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry✝ : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
i✝ : ℕ
h✝ : ∀ (b : β) (j : ℕ), j < i✝ → seq₁ b j = seq₂ b j
i : ℕ
ih :
  (∀ (b : β) (j : ℕ), j < i → seq₁ b j = seq₂ b j) →
    propagateCarry2 init_carry next_carry seq₁ i = propagateCarry2 init_carry next_carry seq₂ i
h : ∀ (b : β) (j : ℕ), j < Nat.succ i → seq₁ b j = seq₂ b j
⊢ propagateCarry2 init_carry next_carry seq₁ (Nat.succ i) = propagateCarry2 init_carry next_carry seq₂ (Nat.succ i)
Theorem: propagateCarry2_eq_of_seq_eq_lt
Proof state before:
case zero
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry✝ : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
i : ℕ
h✝ : ∀ (b : β) (j : ℕ), j < i → seq₁ b j = seq₂ b j
h : ∀ (b : β) (j : ℕ), j < Nat.zero → seq₁ b j = seq₂ b j
⊢ propagateCarry2 init_carry next_carry seq₁ Nat.zero = propagateCarry2 init_carry next_carry seq₂ Nat.zero

case succ
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry✝ : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
i✝ : ℕ
h✝ : ∀ (b : β) (j : ℕ), j < i✝ → seq₁ b j = seq₂ b j
i : ℕ
ih :
  (∀ (b : β) (j : ℕ), j < i → seq₁ b j = seq₂ b j) →
    propagateCarry2 init_carry next_carry seq₁ i = propagateCarry2 init_carry next_carry seq₂ i
h : ∀ (b : β) (j : ℕ), j < Nat.succ i → seq₁ b j = seq₂ b j
⊢ propagateCarry2 init_carry next_carry seq₁ (Nat.succ i) = propagateCarry2 init_carry next_carry seq₂ (Nat.succ i)
Tactic:
{ simp [propagateCarry2] }
Proof state after:
case succ
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry✝ : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
i✝ : ℕ
h✝ : ∀ (b : β) (j : ℕ), j < i✝ → seq₁ b j = seq₂ b j
i : ℕ
ih :
  (∀ (b : β) (j : ℕ), j < i → seq₁ b j = seq₂ b j) →
    propagateCarry2 init_carry next_carry seq₁ i = propagateCarry2 init_carry next_carry seq₂ i
h : ∀ (b : β) (j : ℕ), j < Nat.succ i → seq₁ b j = seq₂ b j
⊢ propagateCarry2 init_carry next_carry seq₁ (Nat.succ i) = propagateCarry2 init_carry next_carry seq₂ (Nat.succ i)
Theorem: propagateCarry2_eq_of_seq_eq_lt
Proof state before:
case succ
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry✝ : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
i✝ : ℕ
h✝ : ∀ (b : β) (j : ℕ), j < i✝ → seq₁ b j = seq₂ b j
i : ℕ
ih :
  (∀ (b : β) (j : ℕ), j < i → seq₁ b j = seq₂ b j) →
    propagateCarry2 init_carry next_carry seq₁ i = propagateCarry2 init_carry next_carry seq₂ i
h : ∀ (b : β) (j : ℕ), j < Nat.succ i → seq₁ b j = seq₂ b j
⊢ propagateCarry2 init_carry next_carry seq₁ (Nat.succ i) = propagateCarry2 init_carry next_carry seq₂ (Nat.succ i)
Tactic:
{ simp only [propagateCarry2, h _ i (Nat.lt_succ_self i)]
  rw [ih]
  exact λ b j hj => h b j (Nat.lt_succ_of_lt hj) }
Proof state after:
no goals
Theorem: propagateCarry2_eq_of_seq_eq_lt
Proof state before:
case zero
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry✝ : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
i : ℕ
h✝ : ∀ (b : β) (j : ℕ), j < i → seq₁ b j = seq₂ b j
h : ∀ (b : β) (j : ℕ), j < Nat.zero → seq₁ b j = seq₂ b j
⊢ propagateCarry2 init_carry next_carry seq₁ Nat.zero = propagateCarry2 init_carry next_carry seq₂ Nat.zero
Tactic:
simp [propagateCarry2]
Proof state after:
no goals
Theorem: propagateCarry2_eq_of_seq_eq_lt
Proof state before:
case succ
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry✝ : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
i✝ : ℕ
h✝ : ∀ (b : β) (j : ℕ), j < i✝ → seq₁ b j = seq₂ b j
i : ℕ
ih :
  (∀ (b : β) (j : ℕ), j < i → seq₁ b j = seq₂ b j) →
    propagateCarry2 init_carry next_carry seq₁ i = propagateCarry2 init_carry next_carry seq₂ i
h : ∀ (b : β) (j : ℕ), j < Nat.succ i → seq₁ b j = seq₂ b j
⊢ propagateCarry2 init_carry next_carry seq₁ (Nat.succ i) = propagateCarry2 init_carry next_carry seq₂ (Nat.succ i)
Tactic:
simp only [propagateCarry2, h _ i (Nat.lt_succ_self i)]
Proof state after:
case succ
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry✝ : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
i✝ : ℕ
h✝ : ∀ (b : β) (j : ℕ), j < i✝ → seq₁ b j = seq₂ b j
i : ℕ
ih :
  (∀ (b : β) (j : ℕ), j < i → seq₁ b j = seq₂ b j) →
    propagateCarry2 init_carry next_carry seq₁ i = propagateCarry2 init_carry next_carry seq₂ i
h : ∀ (b : β) (j : ℕ), j < Nat.succ i → seq₁ b j = seq₂ b j
⊢ (next_carry (propagateCarry2 init_carry next_carry seq₁ i) fun i_1 => seq₂ i_1 i) =
    next_carry (propagateCarry2 init_carry next_carry seq₂ i) fun i_1 => seq₂ i_1 i