internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.blastZeroExtend.go_eq_eval_getLsb
Proof state before:
case isTrue.inr.isFalse.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
assign : α → Bool
idx : Nat
hidx1 : idx < newWidth
hidx2 : curr ≤ idx
res : RefStreamEntry α newWidth
h✝³ : curr < newWidth
h✝² : curr < idx
h✝¹ : ¬curr < w
hgo :
  go (aig.mkConstCached false).aig w (input.cast ⋯) newWidth (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
h✝ : ¬idx < w
⊢ false = false
Tactic:
. rfl
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastZeroExtend.go_eq_eval_getLsb
Proof state before:
case isTrue.inr.isFalse.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
assign : α → Bool
idx : Nat
hidx1 : idx < newWidth
hidx2 : curr ≤ idx
res : RefStreamEntry α newWidth
h✝³ : curr < newWidth
h✝² : curr < idx
h✝¹ : ¬curr < w
hgo :
  go (aig.mkConstCached false).aig w (input.cast ⋯) newWidth (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
h✝ : idx < w
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRef idx h✝ }, assign⟧ =
    ⟦{ aig := aig, ref := input.getRef idx h✝ }, assign⟧
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastZeroExtend.go_eq_eval_getLsb
Proof state before:
case isTrue.inr.isFalse.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
assign : α → Bool
idx : Nat
hidx1 : idx < newWidth
hidx2 : curr ≤ idx
res : RefStreamEntry α newWidth
h✝³ : curr < newWidth
h✝² : curr < idx
h✝¹ : ¬curr < w
hgo :
  go (aig.mkConstCached false).aig w (input.cast ⋯) newWidth (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
h✝ : ¬idx < w
⊢ false = false
Tactic:
rfl
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastZeroExtend.go_eq_eval_getLsb
Proof state before:
case isTrue.inr.isFalse.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
assign : α → Bool
idx : Nat
hidx1 : idx < newWidth
hidx2 : curr ≤ idx
res : RefStreamEntry α newWidth
h✝² : curr < newWidth
h✝¹ : curr < idx
h✝ : ¬curr < w
hgo :
  go (aig.mkConstCached false).aig w (input.cast ⋯) newWidth (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
⊢ curr + 1 ≤ idx
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastZeroExtend.go_eq_eval_getLsb
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
assign : α → Bool
idx : Nat
hidx1 : idx < newWidth
hidx2 : curr ≤ idx
res : RefStreamEntry α newWidth
h✝ : ¬curr < newWidth
hgo :
  (let_fun hcurr := ⋯;
    { aig := aig, stream := hcurr ▸ s }) =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx1 }, assign⟧ =
    if hidx : idx < w then ⟦{ aig := aig, ref := input.getRef idx hidx }, assign⟧ else false
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastZeroExtend_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
⊢ ∀ (idx : Nat) (hidx : idx < newWidth),
    ⟦{ aig := (blastZeroExtend aig target).aig, ref := (blastZeroExtend aig target).stream.getRef idx hidx }, assign⟧ =
      if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧ else false
Tactic:
intro idx hidx
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
⊢ ⟦{ aig := (blastZeroExtend aig target).aig, ref := (blastZeroExtend aig target).stream.getRef idx hidx }, assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧ else false
Theorem: BVExpr.bitblast.blastZeroExtend_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
⊢ ⟦{ aig := (blastZeroExtend aig target).aig, ref := (blastZeroExtend aig target).stream.getRef idx hidx }, assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧ else false
Tactic:
unfold blastZeroExtend
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
⊢ ⟦{
        aig :=
          (match target with
            | { w := width, stream := input } => blastZeroExtend.go aig width input newWidth 0 ⋯ RefStream.empty).aig,
        ref :=
          (match target with
                | { w := width, stream := input } =>
                  blastZeroExtend.go aig width input newWidth 0 ⋯ RefStream.empty).stream.getRef
            idx hidx },
      assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧ else false
Theorem: BVExpr.bitblast.blastZeroExtend_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
⊢ ⟦{
        aig :=
          (match target with
            | { w := width, stream := input } => blastZeroExtend.go aig width input newWidth 0 ⋯ RefStream.empty).aig,
        ref :=
          (match target with
                | { w := width, stream := input } =>
                  blastZeroExtend.go aig width input newWidth 0 ⋯ RefStream.empty).stream.getRef
            idx hidx },
      assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧ else false
Tactic:
apply blastZeroExtend.go_eq_eval_getLsb
Proof state after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
⊢ 0 ≤ idx
Theorem: BVExpr.bitblast.blastZeroExtend_eq_eval_getLsb
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
⊢ 0 ≤ idx
Tactic:
omega
Proof state after:
no goals
Theorem: List.length_ofFn_go
Proof state before:
n : Nat
α : Type u_1
f : Fin n → α
i j : Nat
h : i + j = n
⊢ (ofFn.go f i j h).length = i
Tactic:
induction i generalizing j with
| zero => simp[ofFn.go]
| succ n ih =>
  dsimp [ofFn.go]
  rw [ih]
Proof state after:
no goals
Theorem: List.length_ofFn_go
Proof state before:
case zero
n : Nat
α : Type u_1
f : Fin n → α
j : Nat
h : 0 + j = n
⊢ (ofFn.go f 0 j h).length = 0
Tactic:
simp[ofFn.go]
Proof state after:
no goals
Theorem: List.length_ofFn_go
Proof state before:
case succ
n✝ : Nat
α : Type u_1
f : Fin n✝ → α
n : Nat
ih : ∀ {j : Nat} {h : n + j = n✝}, (ofFn.go f n j h).length = n
j : Nat
h : n + 1 + j = n✝
⊢ (ofFn.go f (n + 1) j h).length = n + 1
Tactic:
dsimp [ofFn.go]
Proof state after:
case succ
n✝ : Nat
α : Type u_1
f : Fin n✝ → α
n : Nat
ih : ∀ {j : Nat} {h : n + j = n✝}, (ofFn.go f n j h).length = n
j : Nat
h : n + 1 + j = n✝
⊢ (ofFn.go f n (j + 1) ⋯).length + 1 = n + 1
Theorem: List.length_ofFn_go
Proof state before:
case succ
n✝ : Nat
α : Type u_1
f : Fin n✝ → α
n : Nat
ih : ∀ {j : Nat} {h : n + j = n✝}, (ofFn.go f n j h).length = n
j : Nat
h : n + 1 + j = n✝
⊢ (ofFn.go f n (j + 1) ⋯).length + 1 = n + 1
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: List.length_ofFn
Proof state before:
k : Nat
α : Type u_1
f : Fin k → α
⊢ (ofFn f).length = k
Tactic:
simp [ofFn, length_ofFn_go]
Proof state after:
no goals
Theorem: List.get_Array_data
Proof state before:
x : Array ?m.919
i : Fin x.data.length
⊢ x.data.length = x.size
Tactic:
simp
Proof state after:
no goals
Theorem: List.get_Array_data
Proof state before:
α✝ : Type u_1
x : Array α✝
i : Fin x.data.length
⊢ x.data.get i = x.get (Fin.cast ⋯ i)
Tactic:
rfl
Proof state after:
no goals
Theorem: List.get_ofFn_go
Proof state before:
k✝ : Nat
α : Type ?u.1010
f : Fin k✝ → α
i j k : Nat
h : i + j = k✝
hk : k < (ofFn.go f i j h).length
⊢ j + k < k✝
Tactic:
simp[length_ofFn_go] at hk
Proof state after:
k✝ : Nat
α : Type ?u.1010
f : Fin k✝ → α
i j k : Nat
h : i + j = k✝
hk : k < i
⊢ j + k < k✝
Theorem: List.get_ofFn_go
Proof state before:
k✝ : Nat
α : Type ?u.1010
f : Fin k✝ → α
i j k : Nat
h : i + j = k✝
hk : k < i
⊢ j + k < k✝
Tactic:
omega
Proof state after:
no goals
Theorem: List.get_ofFn_go
Proof state before:
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i j k : Nat
h : i + j = k✝
hk : k < (ofFn.go f i j h).length
⊢ (ofFn.go f i j h).get ⟨k, hk⟩ = f ⟨j + k, ⋯⟩
Tactic:
let i+1 := i
Proof state after:
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i✝ j k i : Nat
h : i + 1 + j = k✝
hk : k < (ofFn.go f (i + 1) j h).length
⊢ (ofFn.go f (i + 1) j h).get ⟨k, hk⟩ = f ⟨j + k, ⋯⟩
Theorem: List.get_ofFn_go
Proof state before:
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i✝ j k i : Nat
h : i + 1 + j = k✝
hk : k < (ofFn.go f (i + 1) j h).length
⊢ (ofFn.go f (i + 1) j h).get ⟨k, hk⟩ = f ⟨j + k, ⋯⟩
Tactic:
cases k with
| zero => dsimp [ofFn.go]
| succ k =>
  dsimp [ofFn.go]
  rw [get_ofFn_go]
  congr 2
  simp_arith
Proof state after:
no goals
Theorem: List.get_ofFn_go
Proof state before:
case zero
k : Nat
α : Type u_1
f : Fin k → α
i✝ j i : Nat
h : i + 1 + j = k
hk : 0 < (ofFn.go f (i + 1) j h).length
⊢ (ofFn.go f (i + 1) j h).get ⟨0, hk⟩ = f ⟨j + 0, ⋯⟩
Tactic:
dsimp [ofFn.go]
Proof state after:
no goals
Theorem: List.get_ofFn_go
Proof state before:
case succ
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i✝ j i : Nat
h : i + 1 + j = k✝
k : Nat
hk : k + 1 < (ofFn.go f (i + 1) j h).length
⊢ (ofFn.go f (i + 1) j h).get ⟨k + 1, hk⟩ = f ⟨j + (k + 1), ⋯⟩
Tactic:
dsimp [ofFn.go]
Proof state after:
case succ
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i✝ j i : Nat
h : i + 1 + j = k✝
k : Nat
hk : k + 1 < (ofFn.go f (i + 1) j h).length
⊢ (ofFn.go f i (j + 1) ⋯).get ⟨k, ⋯⟩ = f ⟨j + (k + 1), ⋯⟩
Theorem: List.get_ofFn_go
Proof state before:
case succ
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i✝ j i : Nat
h : i + 1 + j = k✝
k : Nat
hk : k + 1 < (ofFn.go f (i + 1) j h).length
⊢ (ofFn.go f i (j + 1) ⋯).get ⟨k, ⋯⟩ = f ⟨j + (k + 1), ⋯⟩
Tactic:
rw [get_ofFn_go]
Proof state after:
case succ
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i✝ j i : Nat
h : i + 1 + j = k✝
k : Nat
hk : k + 1 < (ofFn.go f (i + 1) j h).length
⊢ f ⟨j + 1 + k, ⋯⟩ = f ⟨j + (k + 1), ⋯⟩
Theorem: List.get_ofFn_go
Proof state before:
case succ
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i✝ j i : Nat
h : i + 1 + j = k✝
k : Nat
hk : k + 1 < (ofFn.go f (i + 1) j h).length
⊢ f ⟨j + 1 + k, ⋯⟩ = f ⟨j + (k + 1), ⋯⟩
Tactic:
congr 2
Proof state after:
case succ.e_a.e_val
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i✝ j i : Nat
h : i + 1 + j = k✝
k : Nat
hk : k + 1 < (ofFn.go f (i + 1) j h).length
⊢ j + 1 + k = j + (k + 1)
Theorem: List.get_ofFn_go
Proof state before:
case succ.e_a.e_val
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i✝ j i : Nat
h : i + 1 + j = k✝
k : Nat
hk : k + 1 < (ofFn.go f (i + 1) j h).length
⊢ j + 1 + k = j + (k + 1)
Tactic:
simp_arith
Proof state after:
no goals
Theorem: List.get_ofFn
Proof state before:
k : Nat
α : Type ?u.7201
f : Fin k → α
i : Fin (ofFn f).length
⊢ (ofFn f).length = k
Tactic:
simp
Proof state after:
no goals
Theorem: List.get_ofFn
Proof state before:
k : Nat
α : Type u_1
f : Fin k → α
i : Fin (ofFn f).length
⊢ (ofFn f).get i = f (Fin.cast ⋯ i)
Tactic:
rcases i with ⟨i, hi⟩
Proof state after:
case mk
k : Nat
α : Type u_1
f : Fin k → α
i : Nat
hi : i < (ofFn f).length
⊢ (ofFn f).get ⟨i, hi⟩ = f (Fin.cast ⋯ ⟨i, hi⟩)
Theorem: List.get_ofFn
Proof state before:
case mk
k : Nat
α : Type u_1
f : Fin k → α
i : Nat
hi : i < (ofFn f).length
⊢ (ofFn f).get ⟨i, hi⟩ = f (Fin.cast ⋯ ⟨i, hi⟩)
Tactic:
simp [ofFn, get_ofFn_go]
Proof state after:
no goals
Theorem: List.getD_ofFn
Proof state before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
⊢ (ofFn f).getD i d = if h : i < k then f ⟨i, h⟩ else d
Tactic:
simp [List.getD]
Proof state after:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
⊢ ((ofFn f).get? i).getD d = if h : i < k then f ⟨i, h⟩ else d
Theorem: List.getD_ofFn
Proof state before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
⊢ ((ofFn f).get? i).getD d = if h : i < k then f ⟨i, h⟩ else d
Tactic:
if h : i < (ofFn f).length then
  rw [get?_eq_get h]
  rw [length_ofFn] at h
  rw [dif_pos h]
  simp
else
  rw [get?_eq_none.mpr (by simpa using h)]
  rw [length_ofFn] at h
  rw [dif_neg h]
  rfl
Proof state after:
no goals
Theorem: List.getD_ofFn
Proof state before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : i < (ofFn f).length
⊢ ((ofFn f).get? i).getD d = if h : i < k then f ⟨i, h⟩ else d
Tactic:
rw [get?_eq_get h]
Proof state after:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : i < (ofFn f).length
⊢ (some ((ofFn f).get ⟨i, h⟩)).getD d = if h : i < k then f ⟨i, h⟩ else d
Theorem: List.getD_ofFn
Proof state before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : i < (ofFn f).length
⊢ (some ((ofFn f).get ⟨i, h⟩)).getD d = if h : i < k then f ⟨i, h⟩ else d
Tactic:
rw [length_ofFn] at h
Proof state after:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h✝ : i < (ofFn f).length
h : i < k
⊢ (some ((ofFn f).get ⟨i, h✝⟩)).getD d = if h : i < k then f ⟨i, h⟩ else d
Theorem: List.getD_ofFn
Proof state before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h✝ : i < (ofFn f).length
h : i < k
⊢ (some ((ofFn f).get ⟨i, h✝⟩)).getD d = if h : i < k then f ⟨i, h⟩ else d
Tactic:
rw [dif_pos h]
Proof state after:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h✝ : i < (ofFn f).length
h : i < k
⊢ (some ((ofFn f).get ⟨i, h✝⟩)).getD d = f ⟨i, h⟩
Theorem: List.getD_ofFn
Proof state before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h✝ : i < (ofFn f).length
h : i < k
⊢ (some ((ofFn f).get ⟨i, h✝⟩)).getD d = f ⟨i, h⟩
Tactic:
simp
Proof state after:
no goals
Theorem: List.getD_ofFn
Proof state before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : ¬i < (ofFn f).length
⊢ ((ofFn f).get? i).getD d = if h : i < k then f ⟨i, h⟩ else d
Tactic:
rw [get?_eq_none.mpr (by simpa using h)]
Proof state after:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : ¬i < (ofFn f).length
⊢ none.getD d = if h : i < k then f ⟨i, h⟩ else d
Theorem: List.getD_ofFn
Proof state before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : ¬i < (ofFn f).length
⊢ none.getD d = if h : i < k then f ⟨i, h⟩ else d
Tactic:
rw [length_ofFn] at h
Proof state after:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : ¬i < k
⊢ none.getD d = if h : i < k then f ⟨i, h⟩ else d
Theorem: List.getD_ofFn
Proof state before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : ¬i < k
⊢ none.getD d = if h : i < k then f ⟨i, h⟩ else d
Tactic:
rw [dif_neg h]
Proof state after:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : ¬i < k
⊢ none.getD d = d
Theorem: List.getD_ofFn
Proof state before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : ¬i < k
⊢ none.getD d = d
Tactic:
rfl
Proof state after:
no goals
Theorem: List.getD_ofFn
Proof state before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : ¬i < (ofFn f).length
⊢ (ofFn f).length ≤ i
Tactic:
simpa using h
Proof state after:
no goals
Theorem: BoolExprNat.sat_and
Proof state before:
x y : BoolExprNat
f : List Bool
hx : x.sat f
hy : y.sat f
⊢ (gate Gate.and x y).sat f
Tactic:
simp only [sat] at *
Proof state after:
x y : BoolExprNat
f : List Bool
hx : eval f x = true
hy : eval f y = true
⊢ eval f (gate Gate.and x y) = true
Theorem: BoolExprNat.sat_and
Proof state before:
x y : BoolExprNat
f : List Bool
hx : eval f x = true
hy : eval f y = true
⊢ eval f (gate Gate.and x y) = true
Tactic:
simp [hx, hy, Gate.eval]
Proof state after:
no goals
Theorem: BoolExprNat.eval_toBoolExpr
Proof state before:
x : BoolExprNat
f : List Bool
⊢ BoolExpr.eval (fun x => f.getD x false) x.toBoolExpr = eval f x
Tactic:
induction x with
| literal a => rfl
| const b => rfl
| not x ih => simp [eval, ih, toBoolExpr]
| gate g x y ihx ihy => simp [eval, ihx, ihy, toBoolExpr]
Proof state after:
no goals
Theorem: BoolExprNat.eval_toBoolExpr
Proof state before:
case literal
f : List Bool
a : Nat
⊢ BoolExpr.eval (fun x => f.getD x false) (literal a).toBoolExpr = eval f (literal a)
Tactic:
rfl
Proof state after:
no goals
Theorem: BoolExprNat.eval_toBoolExpr
Proof state before:
case const
f : List Bool
b : Bool
⊢ BoolExpr.eval (fun x => f.getD x false) (const b).toBoolExpr = eval f (const b)
Tactic:
rfl
Proof state after:
no goals
Theorem: BoolExprNat.eval_toBoolExpr
Proof state before:
case not
f : List Bool
x : BoolExprNat
ih : BoolExpr.eval (fun x => f.getD x false) x.toBoolExpr = eval f x
⊢ BoolExpr.eval (fun x => f.getD x false) x.not.toBoolExpr = eval f x.not
Tactic:
simp [eval, ih, toBoolExpr]
Proof state after:
no goals
Theorem: BoolExprNat.eval_toBoolExpr
Proof state before:
case gate
f : List Bool
g : Gate
x y : BoolExprNat
ihx : BoolExpr.eval (fun x => f.getD x false) x.toBoolExpr = eval f x
ihy : BoolExpr.eval (fun x => f.getD x false) y.toBoolExpr = eval f y
⊢ BoolExpr.eval (fun x => f.getD x false) (gate g x y).toBoolExpr = eval f (gate g x y)
Tactic:
simp [eval, ihx, ihy, toBoolExpr]
Proof state after:
no goals
Theorem: BoolExprNat.eval_ofFn
Proof state before:
k : Nat
x : BoolExprNat
f : Fin k → Bool
⊢ eval (List.ofFn f) x = BoolExpr.eval (fun i => if h : i < k then f ⟨i, h⟩ else false) x.toBoolExpr
Tactic:
match x with
| literal a => simp [toBoolExpr, List.getD_ofFn]
| const b => rfl
| not x => simp [eval, toBoolExpr, eval_ofFn]
| gate g x y => simp [eval, toBoolExpr, eval_ofFn]
Proof state after:
no goals
Theorem: BoolExprNat.eval_ofFn
Proof state before:
k : Nat
x : BoolExprNat
f : Fin k → Bool
a : Nat
⊢ eval (List.ofFn f) (literal a) = BoolExpr.eval (fun i => if h : i < k then f ⟨i, h⟩ else false) (literal a).toBoolExpr
Tactic:
simp [toBoolExpr, List.getD_ofFn]
Proof state after:
no goals
Theorem: BoolExprNat.eval_ofFn
Proof state before:
k : Nat
x : BoolExprNat
f : Fin k → Bool
b : Bool
⊢ eval (List.ofFn f) (const b) = BoolExpr.eval (fun i => if h : i < k then f ⟨i, h⟩ else false) (const b).toBoolExpr
Tactic:
rfl
Proof state after:
no goals
Theorem: BoolExprNat.eval_ofFn
Proof state before:
k : Nat
x✝ : BoolExprNat
f : Fin k → Bool
x : BoolExprNat
⊢ eval (List.ofFn f) x.not = BoolExpr.eval (fun i => if h : i < k then f ⟨i, h⟩ else false) x.not.toBoolExpr
Tactic:
simp [eval, toBoolExpr, eval_ofFn]
Proof state after:
no goals
Theorem: BoolExprNat.eval_ofFn
Proof state before:
k : Nat
x✝ : BoolExprNat
f : Fin k → Bool
g : Gate
x y : BoolExprNat
⊢ eval (List.ofFn f) (gate g x y) =
    BoolExpr.eval (fun i => if h : i < k then f ⟨i, h⟩ else false) (gate g x y).toBoolExpr
Tactic:
simp [eval, toBoolExpr, eval_ofFn]
Proof state after:
no goals
Theorem: BoolExprNat.eval_if
Proof state before:
x : BoolExprNat
f : List Bool
a : Nat
⊢ BoolExpr.eval (fun i => decide (i < (literal a).toBoolExpr.vars) && f.getD i false) (literal a).toBoolExpr =
    eval f (literal a)
Tactic:
simp [toBoolExpr]
Proof state after:
no goals
Theorem: BoolExprNat.eval_if
Proof state before:
x : BoolExprNat
f : List Bool
b : Bool
⊢ BoolExpr.eval (fun i => decide (i < (const b).toBoolExpr.vars) && f.getD i false) (const b).toBoolExpr =
    eval f (const b)
Tactic:
rfl
Proof state after:
no goals
Theorem: BoolExprNat.eval_if
Proof state before:
x✝ : BoolExprNat
f : List Bool
x : BoolExprNat
⊢ BoolExpr.eval (fun i => decide (i < x.not.toBoolExpr.vars) && f.getD i false) x.not.toBoolExpr = eval f x.not
Tactic:
simp [toBoolExpr, eval_if]
Proof state after:
no goals
Theorem: BoolExprNat.eval_if
Proof state before:
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
⊢ BoolExpr.eval (fun i => decide (i < (gate g x y).toBoolExpr.vars) && f.getD i false) (gate g x y).toBoolExpr =
    eval f (gate g x y)
Tactic:
simp [toBoolExpr]
Proof state after:
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
⊢ g.eval (BoolExpr.eval (fun i => decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) x.toBoolExpr)
      (BoolExpr.eval (fun i => decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) y.toBoolExpr) =
    g.eval (eval f x) (eval f y)
Theorem: BoolExprNat.eval_if
Proof state before:
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
⊢ g.eval (BoolExpr.eval (fun i => decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) x.toBoolExpr)
      (BoolExpr.eval (fun i => decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) y.toBoolExpr) =
    g.eval (eval f x) (eval f y)
Tactic:
rw [BoolExpr.eval_congr, eval_if f, BoolExpr.eval_congr, eval_if f]
Proof state after:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
⊢ ∀ (i : Nat),
    i < y.toBoolExpr.vars →
      (decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) =
        (decide (i < y.toBoolExpr.vars) && f.getD i false)

case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
⊢ ∀ (i : Nat),
    i < x.toBoolExpr.vars →
      (decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) =
        (decide (i < x.toBoolExpr.vars) && f.getD i false)
Theorem: BoolExprNat.eval_if
Proof state before:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
⊢ ∀ (i : Nat),
    i < y.toBoolExpr.vars →
      (decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) =
        (decide (i < y.toBoolExpr.vars) && f.getD i false)
Tactic:
intro i h
Proof state after:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
i : Nat
h : i < y.toBoolExpr.vars
⊢ (decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) =
    (decide (i < y.toBoolExpr.vars) && f.getD i false)
Theorem: BoolExprNat.eval_if
Proof state before:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
i : Nat
h : i < y.toBoolExpr.vars
⊢ (decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) =
    (decide (i < y.toBoolExpr.vars) && f.getD i false)
Tactic:
simp only [h, decide_True, Bool.true_and, Bool.and_iff_right_iff_imp, decide_eq_true_eq]
Proof state after:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
i : Nat
h : i < y.toBoolExpr.vars
⊢ f.getD i false = true → i < max x.toBoolExpr.vars y.toBoolExpr.vars
Theorem: BoolExprNat.eval_if
Proof state before:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
i : Nat
h : i < y.toBoolExpr.vars
⊢ f.getD i false = true → i < max x.toBoolExpr.vars y.toBoolExpr.vars
Tactic:
omega
Proof state after:
no goals
Theorem: BoolExprNat.eval_if
Proof state before:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
⊢ ∀ (i : Nat),
    i < x.toBoolExpr.vars →
      (decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) =
        (decide (i < x.toBoolExpr.vars) && f.getD i false)
Tactic:
intro i h
Proof state after:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
i : Nat
h : i < x.toBoolExpr.vars
⊢ (decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) =
    (decide (i < x.toBoolExpr.vars) && f.getD i false)
Theorem: BoolExprNat.eval_if
Proof state before:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
i : Nat
h : i < x.toBoolExpr.vars
⊢ (decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) =
    (decide (i < x.toBoolExpr.vars) && f.getD i false)
Tactic:
simp only [h, decide_True, Bool.true_and, Bool.and_iff_right_iff_imp, decide_eq_true_eq]
Proof state after:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
i : Nat
h : i < x.toBoolExpr.vars
⊢ f.getD i false = true → i < max x.toBoolExpr.vars y.toBoolExpr.vars