Theorem: composeBinary_eval (Lean4bits/lemmas.lean)

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
State after:
no goals

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
State after:
no goals

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]
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)

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
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

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
State after:
no goals