-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Fold.lean
theorem denote_fold_and {aig : AIG α} (s : RefVec aig len) :
    ⟦(fold aig (FoldTarget.mkAnd s)), assign⟧
      ↔
    (∀ (idx : Nat) (hidx : idx < len), ⟦aig, s.get idx hidx, assign⟧)

Proof state:
case mp
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
idx : Nat
hidx : idx < len
h : ⟦assign, { aig := (aig.mkConstCached true).aig, ref := { gate := (s.get idx hidx).gate, hgate := ⋯ } }⟧ = true
⊢ ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true

Tactic:
rw [AIG.LawfulOperator.denote_mem_prefix (f := mkConstCached)] at h

Result:
case mp
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
idx : Nat
hidx : idx < len
h✝ : ⟦assign, { aig := (aig.mkConstCached true).aig, ref := { gate := (s.get idx hidx).gate, hgate := ⋯ } }⟧ = true
h : ⟦assign, { aig := aig, ref := { gate := (s.get idx hidx).gate, hgate := ?mp } }⟧ = true
⊢ ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true

case mp
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
idx : Nat
hidx : idx < len
h : ⟦assign, { aig := (aig.mkConstCached true).aig, ref := { gate := (s.get idx hidx).gate, hgate := ⋯ } }⟧ = true
⊢ (s.get idx hidx).gate < aig.decls.size

Proof state:
case mpr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
idx : Nat
hidx : idx < len
h : ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true
⊢ ⟦assign, { aig := aig, ref := { gate := (s.get idx hidx).gate, hgate := ?mpr } }⟧ = true

Tactic:
simp only [← h]

Result:
no goals

Proof state:
case mpr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
h : ∀ (idx : Nat) (hidx : idx < len), ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true
idx : Nat
hidx : idx < len
⊢ ⟦assign, { aig := (aig.mkConstCached true).aig, ref := { gate := (s.get idx hidx).gate, hgate := ⋯ } }⟧ = true

Tactic:
specialize h idx hidx

Result:
case mpr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
idx : Nat
hidx : idx < len
h : ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true
⊢ ⟦assign, { aig := (aig.mkConstCached true).aig, ref := { gate := (s.get idx hidx).gate, hgate := ⋯ } }⟧ = true

Proof state:
case mp
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
idx : Nat
hidx : idx < len
h✝ : ⟦assign, { aig := (aig.mkConstCached true).aig, ref := { gate := (s.get idx hidx).gate, hgate := ⋯ } }⟧ = true
h : ⟦assign, { aig := aig, ref := { gate := (s.get idx hidx).gate, hgate := ?mp } }⟧ = true
⊢ ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true

case mp
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
idx : Nat
hidx : idx < len
h : ⟦assign, { aig := (aig.mkConstCached true).aig, ref := { gate := (s.get idx hidx).gate, hgate := ⋯ } }⟧ = true
⊢ (s.get idx hidx).gate < aig.decls.size

Tactic:
rw [← h]

Result:
no goals

Proof state:
case mpr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
idx : Nat
hidx : idx < len
h : ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true
⊢ (s.get idx hidx).gate < aig.decls.size

Tactic:
apply RefVec.hrefs

Result:
case mpr.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
idx : Nat
hidx : idx < len
h : ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true
⊢ idx < len

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
⊢ ⟦assign, fold.go (aig.mkConstCached true).aig (aig.mkConstCached true).ref 0 len (s.cast ⋯) mkAndCached⟧ = true ↔
    ∀ (idx : Nat) (hidx : idx < len), ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true

Tactic:
rw [fold.denote_go_and]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
⊢ (⟦assign, { aig := (aig.mkConstCached true).aig, ref := (aig.mkConstCached true).ref }⟧ = true ∧
      ∀ (idx : Nat) (hidx1 : idx < len),
        0 ≤ idx → ⟦assign, { aig := (aig.mkConstCached true).aig, ref := (s.cast ⋯).get idx hidx1 }⟧ = true) ↔
    ∀ (idx : Nat) (hidx : idx < len), ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true

case hcurr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
⊢ 0 ≤ len

Proof state:
case hcurr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
s : aig.RefVec len
⊢ 0 ≤ len

Tactic:
omega

Result:
no goals