internlm/Lean-Github huggingface dataset:
Theorem: AIG.mkImpCached_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.BinaryInput
h : idx < aig.decls.size
h2 : idx < (aig.mkImpCached input).aig.decls.size
⊢ ((aig.mkGateCached (input.asGateInput false true)).aig.mkConstCached true).aig.decls[idx] = aig.decls[idx]

case h1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.BinaryInput
h : idx < aig.decls.size
h2 : idx < (aig.mkImpCached input).aig.decls.size
⊢ idx < ((aig.mkGateCached (input.asGateInput false true)).aig.mkConstCached true).aig.decls.size
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.BinaryInput
h : idx < aig.decls.size
h2 : idx < (aig.mkImpCached input).aig.decls.size
⊢ (aig.mkGateCached (input.asGateInput false true)).aig.decls[idx] = aig.decls[idx]

case h1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.BinaryInput
h : idx < aig.decls.size
h2 : idx < (aig.mkImpCached input).aig.decls.size
⊢ idx < (aig.mkGateCached (input.asGateInput false true)).aig.decls.size

case h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.BinaryInput
h : idx < aig.decls.size
h2 : idx < (aig.mkImpCached input).aig.decls.size
⊢ idx < ((aig.mkGateCached (input.asGateInput false true)).aig.mkConstCached true).aig.decls.size
Theorem: AIG.mkImpCached_decl_eq
Proof state before:
case h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.BinaryInput
h : idx < aig.decls.size
h2 : idx < (aig.mkImpCached input).aig.decls.size
⊢ idx < ((aig.mkGateCached (input.asGateInput false true)).aig.mkConstCached true).aig.decls.size
Tactic:
. apply LawfulOperator.lt_size_of_lt_aig_size (f := mkConstCached)
  apply LawfulOperator.lt_size_of_lt_aig_size
  assumption
Proof state after:
no goals
Theorem: AIG.mkImpCached_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.BinaryInput
h : idx < aig.decls.size
h2 : idx < (aig.mkImpCached input).aig.decls.size
⊢ (aig.mkGateCached (input.asGateInput false true)).aig.decls[idx] = aig.decls[idx]
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
Proof state after:
case h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.BinaryInput
h : idx < aig.decls.size
h2 : idx < (aig.mkImpCached input).aig.decls.size
⊢ idx < (aig.mkGateCached (input.asGateInput false true)).aig.decls.size
Theorem: AIG.mkImpCached_decl_eq
Proof state before:
case h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.BinaryInput
h : idx < aig.decls.size
h2 : idx < (aig.mkImpCached input).aig.decls.size
⊢ idx < (aig.mkGateCached (input.asGateInput false true)).aig.decls.size
Tactic:
apply LawfulOperator.lt_size_of_lt_aig_size
Proof state after:
case h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.BinaryInput
h : idx < aig.decls.size
h2 : idx < (aig.mkImpCached input).aig.decls.size
⊢ idx < aig.decls.size
Theorem: AIG.mkImpCached_decl_eq
Proof state before:
case h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.BinaryInput
h : idx < aig.decls.size
h2 : idx < (aig.mkImpCached input).aig.decls.size
⊢ idx < aig.decls.size
Tactic:
assumption
Proof state after:
no goals
Theorem: AIG.mkImpCached_decl_eq
Proof state before:
case h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.BinaryInput
h : idx < aig.decls.size
h2 : idx < (aig.mkImpCached input).aig.decls.size
⊢ idx < ((aig.mkGateCached (input.asGateInput false true)).aig.mkConstCached true).aig.decls.size
Tactic:
apply LawfulOperator.lt_size_of_lt_aig_size (f := mkConstCached)
Proof state after:
case h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.BinaryInput
h : idx < aig.decls.size
h2 : idx < (aig.mkImpCached input).aig.decls.size
⊢ idx < (aig.mkGateCached (input.asGateInput false true)).aig.decls.size
Theorem: AIG.mkImpCached_decl_eq
Proof state before:
case h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.BinaryInput
h : idx < aig.decls.size
h2 : idx < (aig.mkImpCached input).aig.decls.size
⊢ idx < (aig.mkGateCached (input.asGateInput false true)).aig.decls.size
Tactic:
apply LawfulOperator.lt_size_of_lt_aig_size
Proof state after:
case h2.h.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.BinaryInput
h : idx < aig.decls.size
h2 : idx < (aig.mkImpCached input).aig.decls.size
⊢ idx < aig.decls.size
Theorem: AIG.mkImpCached_decl_eq
Proof state before:
case h2.h.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.BinaryInput
h : idx < aig.decls.size
h2 : idx < (aig.mkImpCached input).aig.decls.size
⊢ idx < aig.decls.size
Tactic:
assumption
Proof state after:
no goals
Theorem: AIG.denote_mkImpCached
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦aig.mkImpCached input, assign⟧ =
    (!⟦{ aig := aig, ref := { gate := input.lhs.gate, hgate := ⋯ } }, assign⟧ ||
      ⟦{ aig := aig, ref := { gate := input.rhs.gate, hgate := ⋯ } }, assign⟧)
Tactic:
rw [← imp_as_aig]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦aig.mkImpCached input, assign⟧ =
    !(⟦{ aig := aig, ref := { gate := input.lhs.gate, hgate := ⋯ } }, assign⟧ &&
        !⟦{ aig := aig, ref := { gate := input.rhs.gate, hgate := ⋯ } }, assign⟧)
Theorem: AIG.denote_mkImpCached
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦aig.mkImpCached input, assign⟧ =
    !(⟦{ aig := aig, ref := { gate := input.lhs.gate, hgate := ⋯ } }, assign⟧ &&
        !⟦{ aig := aig, ref := { gate := input.rhs.gate, hgate := ⋯ } }, assign⟧)
Tactic:
simp [mkImpCached, LawfulOperator.denote_input_entry (f := mkConstCached)]
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2429
Proof state before:
⊢ ∀ (y x : BitVec 64), x &&& y ^^^ -1 = x ^^^ -1 ||| y ^^^ -1
Tactic:
intros
Proof state after:
y✝ x✝ : BitVec 64
⊢ x✝ &&& y✝ ^^^ -1 = x✝ ^^^ -1 ||| y✝ ^^^ -1
Theorem: bitvec_AndOrXor_2429
Proof state before:
y✝ x✝ : BitVec 64
⊢ x✝ &&& y✝ ^^^ -1 = x✝ ^^^ -1 ||| y✝ ^^^ -1
Tactic:
bv_decide
Proof state after:
no goals
Theorem: AIG.RefStream.LawfulMapOperator.denote_prefix_cast_ref
Proof state before:
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
assign : α → Bool
aig : AIG α
input1 input2 : aig.Ref
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
h : aig.decls.size ≤ (f aig input1).aig.decls.size
⊢ ⟦f (f aig input1).aig (input2.cast h), assign⟧ = ⟦f aig input2, assign⟧
Tactic:
rw [LawfulMapOperator.chainable]
Proof state after:
no goals
Theorem: AIG.RefStream.LawfulZipOperator.denote_prefix_cast_ref
Proof state before:
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
assign : α → Bool
aig : AIG α
input1 input2 : aig.BinaryInput
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝¹ : LawfulOperator α BinaryInput f
inst✝ : LawfulZipOperator α f
h : aig.decls.size ≤ (f aig input1).aig.decls.size
⊢ ⟦f (f aig input1).aig (input2.cast h), assign⟧ = ⟦f aig input2, assign⟧
Tactic:
rw [LawfulZipOperator.chainable]
Proof state after:
no goals
Theorem: AIG.RefStream.map.go_le_size
Proof state before:
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
idx : Nat
hidx : idx ≤ len
s : aig.RefStream idx
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
⊢ aig.decls.size ≤ (go aig idx hidx s input f).aig.decls.size
Tactic:
unfold go
Proof state after:
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
idx : Nat
hidx : idx ≤ len
s : aig.RefStream idx
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
⊢ aig.decls.size ≤
    (if hidx : idx < len then
            let res := f aig (input.getRef idx hidx);
            let aig_1 := res.aig;
            let newRef := res.ref;
            let_fun this := ⋯;
            let input_1 := input.cast this;
            let s := s.cast this;
            let s := s.pushRef newRef;
            go aig_1 (idx + 1) ⋯ s input_1 f
          else
            let_fun this := ⋯;
            { aig := aig, stream := this ▸ s }).aig.decls.size
Theorem: AIG.RefStream.map.go_le_size
Proof state before:
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
idx : Nat
hidx : idx ≤ len
s : aig.RefStream idx
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
⊢ aig.decls.size ≤
    (if hidx : idx < len then
            let res := f aig (input.getRef idx hidx);
            let aig_1 := res.aig;
            let newRef := res.ref;
            let_fun this := ⋯;
            let input_1 := input.cast this;
            let s := s.cast this;
            let s := s.pushRef newRef;
            go aig_1 (idx + 1) ⋯ s input_1 f
          else
            let_fun this := ⋯;
            { aig := aig, stream := this ▸ s }).aig.decls.size
Tactic:
split
Proof state after:
case isTrue
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
idx : Nat
hidx : idx ≤ len
s : aig.RefStream idx
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
h✝ : idx < len
⊢ aig.decls.size ≤
    (let res := f aig (input.getRef idx h✝);
          let aig_1 := res.aig;
          let newRef := res.ref;
          let_fun this := ⋯;
          let input_1 := input.cast this;
          let s := s.cast this;
          let s := s.pushRef newRef;
          go aig_1 (idx + 1) ⋯ s input_1 f).aig.decls.size

case isFalse
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
idx : Nat
hidx : idx ≤ len
s : aig.RefStream idx
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
h✝ : ¬idx < len
⊢ aig.decls.size ≤
    (let_fun this := ⋯;
          { aig := aig, stream := this ▸ s }).aig.decls.size
Theorem: AIG.RefStream.map.go_le_size
Proof state before:
case isTrue
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
idx : Nat
hidx : idx ≤ len
s : aig.RefStream idx
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
h✝ : idx < len
⊢ aig.decls.size ≤
    (let res := f aig (input.getRef idx h✝);
          let aig_1 := res.aig;
          let newRef := res.ref;
          let_fun this := ⋯;
          let input_1 := input.cast this;
          let s := s.cast this;
          let s := s.pushRef newRef;
          go aig_1 (idx + 1) ⋯ s input_1 f).aig.decls.size

case isFalse
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
idx : Nat
hidx : idx ≤ len
s : aig.RefStream idx
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
h✝ : ¬idx < len
⊢ aig.decls.size ≤
    (let_fun this := ⋯;
          { aig := aig, stream := this ▸ s }).aig.decls.size
Tactic:
. next h =>
  dsimp
  refine Nat.le_trans ?_ (by apply map.go_le_size)
  apply LawfulOperator.le_size
Proof state after:
case isFalse
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
idx : Nat
hidx : idx ≤ len
s : aig.RefStream idx
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
h✝ : ¬idx < len
⊢ aig.decls.size ≤
    (let_fun this := ⋯;
          { aig := aig, stream := this ▸ s }).aig.decls.size
Theorem: AIG.RefStream.map.go_le_size
Proof state before:
case isFalse
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
idx : Nat
hidx : idx ≤ len
s : aig.RefStream idx
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
h✝ : ¬idx < len
⊢ aig.decls.size ≤
    (let_fun this := ⋯;
          { aig := aig, stream := this ▸ s }).aig.decls.size
Tactic:
. simp
Proof state after:
no goals
Theorem: AIG.RefStream.map.go_le_size
Proof state before:
case isTrue
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
idx : Nat
hidx : idx ≤ len
s : aig.RefStream idx
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
h✝ : idx < len
⊢ aig.decls.size ≤
    (let res := f aig (input.getRef idx h✝);
          let aig_1 := res.aig;
          let newRef := res.ref;
          let_fun this := ⋯;
          let input_1 := input.cast this;
          let s := s.cast this;
          let s := s.pushRef newRef;
          go aig_1 (idx + 1) ⋯ s input_1 f).aig.decls.size
Tactic:
next h =>
dsimp
refine Nat.le_trans ?_ (by apply map.go_le_size)
apply LawfulOperator.le_size
Proof state after:
no goals
Theorem: AIG.RefStream.map.go_le_size
Proof state before:
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
idx : Nat
hidx : idx ≤ len
s : aig.RefStream idx
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
h : idx < len
⊢ aig.decls.size ≤
    (let res := f aig (input.getRef idx h);
          let aig_1 := res.aig;
          let newRef := res.ref;
          let_fun this := ⋯;
          let input_1 := input.cast this;
          let s := s.cast this;
          let s := s.pushRef newRef;
          go aig_1 (idx + 1) ⋯ s input_1 f).aig.decls.size
Tactic:
dsimp
Proof state after:
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
idx : Nat
hidx : idx ≤ len
s : aig.RefStream idx
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
h : idx < len
⊢ aig.decls.size ≤
    (go (f aig (input.getRef idx h)).aig (idx + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef idx h)).ref)
            (input.cast ⋯) f).aig.decls.size
Theorem: AIG.RefStream.map.go_le_size
Proof state before:
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
idx : Nat
hidx : idx ≤ len
s : aig.RefStream idx
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
h : idx < len
⊢ aig.decls.size ≤
    (go (f aig (input.getRef idx h)).aig (idx + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef idx h)).ref)
            (input.cast ⋯) f).aig.decls.size
Tactic:
refine Nat.le_trans ?_ (by apply map.go_le_size)
Proof state after:
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
idx : Nat
hidx : idx ≤ len
s : aig.RefStream idx
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
h : idx < len
⊢ aig.decls.size ≤ (f aig (input.getRef idx h)).aig.decls.size
Theorem: AIG.RefStream.map.go_le_size
Proof state before:
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
idx : Nat
hidx : idx ≤ len
s : aig.RefStream idx
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
h : idx < len
⊢ aig.decls.size ≤ (f aig (input.getRef idx h)).aig.decls.size
Tactic:
apply LawfulOperator.le_size
Proof state after:
no goals
Theorem: AIG.RefStream.map.go_le_size
Proof state before:
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
idx : Nat
hidx : idx ≤ len
s : aig.RefStream idx
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
h : idx < len
⊢ ?m.26457 ≤
    (go (f aig (input.getRef idx h)).aig (idx + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef idx h)).ref)
            (input.cast ⋯) f).aig.decls.size
Tactic:
apply map.go_le_size
Proof state after:
no goals
Theorem: AIG.RefStream.map.go_le_size
Proof state before:
case isFalse
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
idx : Nat
hidx : idx ≤ len
s : aig.RefStream idx
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
h✝ : ¬idx < len
⊢ aig.decls.size ≤
    (let_fun this := ⋯;
          { aig := aig, stream := this ▸ s }).aig.decls.size
Tactic:
simp
Proof state after:
no goals
Theorem: AIG.RefStream.map_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
target : MapTarget aig len
⊢ aig.decls.size ≤ (map aig target).aig.decls.size
Tactic:
unfold map
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
target : MapTarget aig len
⊢ aig.decls.size ≤ (map.go aig 0 ⋯ empty target.stream target.func).aig.decls.size
Theorem: AIG.RefStream.map_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
target : MapTarget aig len
⊢ aig.decls.size ≤ (map.go aig 0 ⋯ empty target.stream target.func).aig.decls.size
Tactic:
apply map.go_le_size
Proof state after:
no goals
Theorem: AIG.RefStream.map.go_decl_eq
Proof state before:
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
i : Nat
hi : i ≤ len
s : aig.RefStream i
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig i hi s input f).aig.decls.size),
    (go aig i hi s input f).aig.decls[idx] = aig.decls[idx]
Tactic:
generalize hgo : go aig i hi s input f = res
Proof state after:
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
i : Nat
hi : i ≤ len
s : aig.RefStream i
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
res : RefStreamEntry α len
hgo : go aig i hi s input f = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: AIG.RefStream.map.go_decl_eq
Proof state before:
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
i : Nat
hi : i ≤ len
s : aig.RefStream i
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
res : RefStreamEntry α len
hgo : go aig i hi s input f = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
unfold go at hgo
Proof state after:
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
i : Nat
hi : i ≤ len
s : aig.RefStream i
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
res : RefStreamEntry α len
hgo :
  (if hidx : i < len then
      let res := f aig (input.getRef i hidx);
      let aig_1 := res.aig;
      let newRef := res.ref;
      let_fun this := ⋯;
      let input_1 := input.cast this;
      let s := s.cast this;
      let s := s.pushRef newRef;
      go aig_1 (i + 1) ⋯ s input_1 f
    else
      let_fun this := ⋯;
      { aig := aig, stream := this ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: AIG.RefStream.map.go_decl_eq
Proof state before:
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
i : Nat
hi : i ≤ len
s : aig.RefStream i
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
res : RefStreamEntry α len
hgo :
  (if hidx : i < len then
      let res := f aig (input.getRef i hidx);
      let aig_1 := res.aig;
      let newRef := res.ref;
      let_fun this := ⋯;
      let input_1 := input.cast this;
      let s := s.cast this;
      let s := s.pushRef newRef;
      go aig_1 (i + 1) ⋯ s input_1 f
    else
      let_fun this := ⋯;
      { aig := aig, stream := this ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
split at hgo
Proof state after:
case isTrue
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
i : Nat
hi : i ≤ len
s : aig.RefStream i
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
res : RefStreamEntry α len
h✝ : i < len
hgo :
  (let res := f aig (input.getRef i h✝);
    let aig_1 := res.aig;
    let newRef := res.ref;
    let_fun this := ⋯;
    let input_1 := input.cast this;
    let s := s.cast this;
    let s := s.pushRef newRef;
    go aig_1 (i + 1) ⋯ s input_1 f) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

case isFalse
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
i : Nat
hi : i ≤ len
s : aig.RefStream i
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
res : RefStreamEntry α len
h✝ : ¬i < len
hgo :
  (let_fun this := ⋯;
    { aig := aig, stream := this ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]