internlm/Lean-Github huggingface dataset:
Theorem: AIG.RefStream.map.denote_go
Proof state before:
case isTrue.inl
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
heq : curr = idx
⊢ ⟦{
        aig :=
          (go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
              (input.cast ⋯) f).aig,
        ref := (f aig (input.getRef curr h✝)).ref.cast ⋯ },
      assign⟧ =
    ⟦f aig (input.getRef curr ⋯), assign⟧
Tactic:
rw [go_denote_mem_prefix]
Proof state after:
case isTrue.inl
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
heq : curr = idx
⊢ ⟦{ aig := (f aig (input.getRef curr h✝)).aig,
        ref := { gate := ((f aig (input.getRef curr h✝)).ref.cast ⋯).gate, hgate := ?isTrue.inl.hstart } },
      assign⟧ =
    ⟦f aig (input.getRef curr ⋯), assign⟧

case isTrue.inl.hstart
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
heq : curr = idx
⊢ ((f aig (input.getRef curr h✝)).ref.cast ⋯).gate < (f aig (input.getRef curr h✝)).aig.decls.size
Theorem: AIG.RefStream.map.denote_go
Proof state before:
case isTrue.inl
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
heq : curr = idx
⊢ ⟦{ aig := (f aig (input.getRef curr h✝)).aig,
        ref := { gate := ((f aig (input.getRef curr h✝)).ref.cast ⋯).gate, hgate := ?isTrue.inl.hstart } },
      assign⟧ =
    ⟦f aig (input.getRef curr ⋯), assign⟧

case isTrue.inl.hstart
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
heq : curr = idx
⊢ ((f aig (input.getRef curr h✝)).ref.cast ⋯).gate < (f aig (input.getRef curr h✝)).aig.decls.size
Tactic:
. simp
Proof state after:
case isTrue.inl.hstart
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
heq : curr = idx
⊢ ((f aig (input.getRef curr h✝)).ref.cast ⋯).gate < (f aig (input.getRef curr h✝)).aig.decls.size
Theorem: AIG.RefStream.map.denote_go
Proof state before:
case isTrue.inl.hstart
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
heq : curr = idx
⊢ ((f aig (input.getRef curr h✝)).ref.cast ⋯).gate < (f aig (input.getRef curr h✝)).aig.decls.size
Tactic:
. simp [Ref.hgate]
Proof state after:
no goals
Theorem: AIG.RefStream.map.denote_go
Proof state before:
case isTrue.inl
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
heq : curr = idx
⊢ ⟦{ aig := (f aig (input.getRef curr h✝)).aig,
        ref := { gate := ((f aig (input.getRef curr h✝)).ref.cast ⋯).gate, hgate := ?isTrue.inl.hstart } },
      assign⟧ =
    ⟦f aig (input.getRef curr ⋯), assign⟧
Tactic:
simp
Proof state after:
no goals
Theorem: AIG.RefStream.map.denote_go
Proof state before:
case isTrue.inl.hstart
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
heq : curr = idx
⊢ ((f aig (input.getRef curr h✝)).ref.cast ⋯).gate < (f aig (input.getRef curr h✝)).aig.decls.size
Tactic:
simp [Ref.hgate]
Proof state after:
no goals
Theorem: AIG.RefStream.map.denote_go
Proof state before:
case isTrue.inl.hidx
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
heq : curr = idx
⊢ idx = curr
Tactic:
rw [heq]
Proof state after:
no goals
Theorem: AIG.RefStream.map.denote_go
Proof state before:
case isTrue.inr
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
hlt : curr < idx
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx1 }, assign⟧ = ⟦f aig (input.getRef idx hidx1), assign⟧
Tactic:
rw [← hgo]
Proof state after:
case isTrue.inr
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
hlt : curr < idx
⊢ ⟦{
        aig :=
          (go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
              (input.cast ⋯) f).aig,
        ref :=
          (go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
                  (input.cast ⋯) f).stream.getRef
            idx hidx1 },
      assign⟧ =
    ⟦f aig (input.getRef idx hidx1), assign⟧
Theorem: AIG.RefStream.map.denote_go
Proof state before:
case isTrue.inr
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
hlt : curr < idx
⊢ ⟦{
        aig :=
          (go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
              (input.cast ⋯) f).aig,
        ref :=
          (go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
                  (input.cast ⋯) f).stream.getRef
            idx hidx1 },
      assign⟧ =
    ⟦f aig (input.getRef idx hidx1), assign⟧
Tactic:
rw [denote_go]
Proof state after:
case isTrue.inr
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
hlt : curr < idx
⊢ ⟦f (f aig (input.getRef curr h✝)).aig ((input.cast ⋯).getRef idx hidx1), assign⟧ =
    ⟦f aig (input.getRef idx hidx1), assign⟧

case isTrue.inr.a
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
hlt : curr < idx
⊢ curr + 1 ≤ idx
Theorem: AIG.RefStream.map.denote_go
Proof state before:
case isTrue.inr
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
hlt : curr < idx
⊢ ⟦f (f aig (input.getRef curr h✝)).aig ((input.cast ⋯).getRef idx hidx1), assign⟧ =
    ⟦f aig (input.getRef idx hidx1), assign⟧

case isTrue.inr.a
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
hlt : curr < idx
⊢ curr + 1 ≤ idx
Tactic:
. simp [getRef_cast, -Ref_cast']
Proof state after:
case isTrue.inr.a
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
hlt : curr < idx
⊢ curr + 1 ≤ idx
Theorem: AIG.RefStream.map.denote_go
Proof state before:
case isTrue.inr.a
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
hlt : curr < idx
⊢ curr + 1 ≤ idx
Tactic:
. omega
Proof state after:
no goals
Theorem: AIG.RefStream.map.denote_go
Proof state before:
case isTrue.inr
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
hlt : curr < idx
⊢ ⟦f (f aig (input.getRef curr h✝)).aig ((input.cast ⋯).getRef idx hidx1), assign⟧ =
    ⟦f aig (input.getRef idx hidx1), assign⟧
Tactic:
simp [getRef_cast, -Ref_cast']
Proof state after:
no goals
Theorem: AIG.RefStream.map.denote_go
Proof state before:
case isTrue.inr.a
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
hlt : curr < idx
⊢ curr + 1 ≤ idx
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.RefStream.map.denote_go
Proof state before:
case isFalse
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : ¬curr < len
hgo :
  (let_fun this := ⋯;
    { aig := aig, stream := this ▸ s }) =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx1 }, assign⟧ = ⟦f aig (input.getRef idx hidx1), assign⟧
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.RefStream.denote_map
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
target : MapTarget aig len
⊢ ∀ (idx : Nat) (hidx : idx < len),
    ⟦{ aig := (map aig target).aig, ref := (map aig target).stream.getRef idx hidx }, assign⟧ =
      ⟦target.func aig (target.stream.getRef idx hidx), assign⟧
Tactic:
intro idx hidx
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
target : MapTarget aig len
idx : Nat
hidx : idx < len
⊢ ⟦{ aig := (map aig target).aig, ref := (map aig target).stream.getRef idx hidx }, assign⟧ =
    ⟦target.func aig (target.stream.getRef idx hidx), assign⟧
Theorem: AIG.RefStream.denote_map
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
target : MapTarget aig len
idx : Nat
hidx : idx < len
⊢ ⟦{ aig := (map aig target).aig, ref := (map aig target).stream.getRef idx hidx }, assign⟧ =
    ⟦target.func aig (target.stream.getRef idx hidx), assign⟧
Tactic:
unfold map
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
target : MapTarget aig len
idx : Nat
hidx : idx < len
⊢ ⟦{ aig := (map.go aig 0 ⋯ empty target.stream target.func).aig,
        ref := (map.go aig 0 ⋯ empty target.stream target.func).stream.getRef idx hidx },
      assign⟧ =
    ⟦target.func aig (target.stream.getRef idx hidx), assign⟧
Theorem: AIG.RefStream.denote_map
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
target : MapTarget aig len
idx : Nat
hidx : idx < len
⊢ ⟦{ aig := (map.go aig 0 ⋯ empty target.stream target.func).aig,
        ref := (map.go aig 0 ⋯ empty target.stream target.func).stream.getRef idx hidx },
      assign⟧ =
    ⟦target.func aig (target.stream.getRef idx hidx), assign⟧
Tactic:
apply map.denote_go
Proof state after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
target : MapTarget aig len
idx : Nat
hidx : idx < len
⊢ 0 ≤ idx
Theorem: AIG.RefStream.denote_map
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
target : MapTarget aig len
idx : Nat
hidx : idx < len
⊢ 0 ≤ idx
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.RefStream.zip.go_getRef_aux
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
lhs rhs : aig.RefStream len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
idx : Nat
hidx : idx < curr
hfoo : aig.decls.size ≤ (go aig curr s hcurr lhs rhs f).aig.decls.size
⊢ idx < len
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.RefStream.zip.go_getRef_aux
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
lhs rhs : aig.RefStream len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
⊢ ∀ (idx : Nat) (hidx : idx < curr) (hfoo : aig.decls.size ≤ (go aig curr s hcurr lhs rhs f).aig.decls.size),
    (go aig curr s hcurr lhs rhs f).stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
intro idx hidx
Proof state after:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
lhs rhs : aig.RefStream len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
idx : Nat
hidx : idx < curr
⊢ ∀ (hfoo : aig.decls.size ≤ (go aig curr s hcurr lhs rhs f).aig.decls.size),
    (go aig curr s hcurr lhs rhs f).stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Theorem: AIG.RefStream.zip.go_getRef_aux
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
lhs rhs : aig.RefStream len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
idx : Nat
hidx : idx < curr
⊢ ∀ (hfoo : aig.decls.size ≤ (go aig curr s hcurr lhs rhs f).aig.decls.size),
    (go aig curr s hcurr lhs rhs f).stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
generalize hgo : go aig curr s hcurr lhs rhs f = res
Proof state after:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
lhs rhs : aig.RefStream len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
idx : Nat
hidx : idx < curr
res : RefStreamEntry α len
hgo : go aig curr s hcurr lhs rhs f = res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Theorem: AIG.RefStream.zip.go_getRef_aux
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
lhs rhs : aig.RefStream len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
idx : Nat
hidx : idx < curr
res : RefStreamEntry α len
hgo : go aig curr s hcurr lhs rhs f = res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
unfold go at hgo
Proof state after:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
lhs rhs : aig.RefStream len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
idx : Nat
hidx : idx < curr
res : RefStreamEntry α len
hgo :
  (if hidx : curr < len then
      let res := f aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx };
      let aig_1 := res.aig;
      let newRef := res.ref;
      let_fun this := ⋯;
      let s := s.cast this;
      let s := s.pushRef newRef;
      go aig_1 (curr + 1) s ⋯ (lhs.cast this) (rhs.cast this) f
    else
      let_fun this := ⋯;
      { aig := aig, stream := this ▸ s }) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo