internlm/Lean-Github huggingface dataset:
Theorem: AIG.mkConstCached_le_size
Proof state before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
x✝ : Option (CacheHit aig.decls (Decl.const val))
hit✝ : CacheHit aig.decls (Decl.const val)
heq✝ : aig.cache.find? (Decl.const val) = some hit✝
⊢ aig.decls.size ≤
    { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
            ref := { gate := hit✝.idx, hgate := ⋯ } }.aig.decls.size
Tactic:
simp
Proof state after:
no goals
Theorem: AIG.mkConstCached_le_size
Proof state before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
x✝ : Option (CacheHit aig.decls (Decl.const val))
heq✝ : aig.cache.find? (Decl.const val) = none
⊢ aig.decls.size ≤
    {
            aig :=
              { decls := aig.decls.push (Decl.const val), cache := Cache.insert aig.decls aig.cache (Decl.const val),
                inv := ⋯ },
            ref := { gate := aig.decls.size, hgate := ⋯ } }.aig.decls.size
Tactic:
simp_arith
Proof state after:
no goals
Theorem: AIG.mkConstCached_eval_eq_mkConst_eval
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
⊢ ⟦aig.mkConstCached val, assign⟧ = ⟦aig.mkConst val, assign⟧
Tactic:
simp only [mkConstCached]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
⊢ ⟦match aig.cache.find? (Decl.const val) with
      | some hit =>
        { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
      | none =>
        {
          aig :=
            { decls := aig.decls.push (Decl.const val), cache := Cache.insert aig.decls aig.cache (Decl.const val),
              inv := ⋯ },
          ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkConst val, assign⟧
Theorem: AIG.mkConstCached_eval_eq_mkConst_eval
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
⊢ ⟦match aig.cache.find? (Decl.const val) with
      | some hit =>
        { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
      | none =>
        {
          aig :=
            { decls := aig.decls.push (Decl.const val), cache := Cache.insert aig.decls aig.cache (Decl.const val),
              inv := ⋯ },
          ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkConst val, assign⟧
Tactic:
split
Proof state after:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.const val))
hit✝ : CacheHit aig.decls (Decl.const val)
heq✝ : aig.cache.find? (Decl.const val) = some hit✝
⊢ ⟦{ aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit✝.idx, hgate := ⋯ } }, assign⟧ =
    ⟦aig.mkConst val, assign⟧

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.const val))
heq✝ : aig.cache.find? (Decl.const val) = none
⊢ ⟦{
        aig :=
          { decls := aig.decls.push (Decl.const val), cache := Cache.insert aig.decls aig.cache (Decl.const val),
            inv := ⋯ },
        ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkConst val, assign⟧
Theorem: AIG.mkConstCached_eval_eq_mkConst_eval
Proof state before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.const val))
hit✝ : CacheHit aig.decls (Decl.const val)
heq✝ : aig.cache.find? (Decl.const val) = some hit✝
⊢ ⟦{ aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit✝.idx, hgate := ⋯ } }, assign⟧ =
    ⟦aig.mkConst val, assign⟧

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.const val))
heq✝ : aig.cache.find? (Decl.const val) = none
⊢ ⟦{
        aig :=
          { decls := aig.decls.push (Decl.const val), cache := Cache.insert aig.decls aig.cache (Decl.const val),
            inv := ⋯ },
        ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkConst val, assign⟧
Tactic:
. next heq1 =>
  rw [denote_mkConst_cached heq1]
Proof state after:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.const val))
heq✝ : aig.cache.find? (Decl.const val) = none
⊢ ⟦{
        aig :=
          { decls := aig.decls.push (Decl.const val), cache := Cache.insert aig.decls aig.cache (Decl.const val),
            inv := ⋯ },
        ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkConst val, assign⟧
Theorem: AIG.mkConstCached_eval_eq_mkConst_eval
Proof state before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.const val))
heq✝ : aig.cache.find? (Decl.const val) = none
⊢ ⟦{
        aig :=
          { decls := aig.decls.push (Decl.const val), cache := Cache.insert aig.decls aig.cache (Decl.const val),
            inv := ⋯ },
        ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkConst val, assign⟧
Tactic:
. simp [mkConst, denote]
Proof state after:
no goals
Theorem: AIG.mkConstCached_eval_eq_mkConst_eval
Proof state before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.const val))
hit✝ : CacheHit aig.decls (Decl.const val)
heq✝ : aig.cache.find? (Decl.const val) = some hit✝
⊢ ⟦{ aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit✝.idx, hgate := ⋯ } }, assign⟧ =
    ⟦aig.mkConst val, assign⟧
Tactic:
next heq1 =>
rw [denote_mkConst_cached heq1]
Proof state after:
no goals
Theorem: AIG.mkConstCached_eval_eq_mkConst_eval
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.const val))
hit✝ : CacheHit aig.decls (Decl.const val)
heq1 : aig.cache.find? (Decl.const val) = some hit✝
⊢ ⟦{ aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit✝.idx, hgate := ⋯ } }, assign⟧ =
    ⟦aig.mkConst val, assign⟧
Tactic:
rw [denote_mkConst_cached heq1]
Proof state after:
no goals
Theorem: AIG.mkConstCached_eval_eq_mkConst_eval
Proof state before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.const val))
heq✝ : aig.cache.find? (Decl.const val) = none
⊢ ⟦{
        aig :=
          { decls := aig.decls.push (Decl.const val), cache := Cache.insert aig.decls aig.cache (Decl.const val),
            inv := ⋯ },
        ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkConst val, assign⟧
Tactic:
simp [mkConst, denote]
Proof state after:
no goals
Theorem: AIG.denote_mkGate_cached
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
⊢ aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit →
    ⟦{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }, assign⟧ = ⟦aig.mkGate input, assign⟧
Tactic:
intros
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
a✝ : aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
⊢ ⟦{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }, assign⟧ = ⟦aig.mkGate input, assign⟧
Theorem: AIG.denote_mkGate_cached
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
a✝ : aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
⊢ ⟦{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }, assign⟧ = ⟦aig.mkGate input, assign⟧
Tactic:
have := hit.hvalid
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
a✝ : aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
this : aig.decls[hit.idx] = Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv
⊢ ⟦{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }, assign⟧ = ⟦aig.mkGate input, assign⟧
Theorem: AIG.denote_mkGate_cached
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
a✝ : aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
this : aig.decls[hit.idx] = Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv
⊢ ⟦{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }, assign⟧ = ⟦aig.mkGate input, assign⟧
Tactic:
simp only [denote_mkGate]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
a✝ : aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
this : aig.decls[hit.idx] = Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv
⊢ ⟦{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }, assign⟧ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Theorem: AIG.denote_mkGate_cached
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
a✝ : aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
this : aig.decls[hit.idx] = Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv
⊢ ⟦{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }, assign⟧ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
conv =>
  lhs
  unfold denote denote.go
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
a✝ : aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
this : aig.decls[hit.idx] = Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv
⊢ (match elem :
      { aig := aig,
              ref :=
                { gate := hit.idx,
                  hgate := ⋯ } }.aig.decls[{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.aig.decls assign ⋯ ⋯;
      xor lval linv && xor rval rinv) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Theorem: AIG.denote_mkGate_cached
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
hit : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
a✝ : aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
this : aig.decls[hit.idx] = Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv
⊢ (match elem :
      { aig := aig,
              ref :=
                { gate := hit.idx,
                  hgate := ⋯ } }.aig.decls[{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.aig.decls assign ⋯ ⋯;
      xor lval linv && xor rval rinv) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
split <;> simp_all[denote]
Proof state after:
no goals
Theorem: AIG.mkGateCached_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
⊢ aig.decls.size ≤ (aig.mkGateCached input).aig.decls.size
Tactic:
dsimp [mkGateCached]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
⊢ aig.decls.size ≤
    (match aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) with
          | some hit =>
            { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
          | none =>
            match aig.decls[input.lhs.ref.gate], aig.decls[input.rhs.ref.gate], input.lhs.inv, input.rhs.inv with
            | Decl.const true, x, true, x_1 => { decls := aig.decls, cache := aig.cache, inv := ⋯ }.mkConstCached false
            | Decl.const false, x, false, x_1 =>
              { decls := aig.decls, cache := aig.cache, inv := ⋯ }.mkConstCached false
            | x, Decl.const true, x_1, true => { decls := aig.decls, cache := aig.cache, inv := ⋯ }.mkConstCached false
            | x, Decl.const false, x_1, false =>
              { decls := aig.decls, cache := aig.cache, inv := ⋯ }.mkConstCached false
            | Decl.const true, x, false, false =>
              { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
                ref := { gate := input.rhs.ref.gate, hgate := ⋯ } }
            | Decl.const false, x, true, false =>
              { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
                ref := { gate := input.rhs.ref.gate, hgate := ⋯ } }
            | x, Decl.const true, false, false =>
              { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
                ref := { gate := input.lhs.ref.gate, hgate := ⋯ } }
            | x, Decl.const false, false, true =>
              { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
                ref := { gate := input.lhs.ref.gate, hgate := ⋯ } }
            | x, x_1, x_2, x_3 =>
              {
                aig :=
                  {
                    decls :=
                      aig.decls.push (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv),
                    cache :=
                      Cache.insert aig.decls aig.cache
                        (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv),
                    inv := ⋯ },
                ref := { gate := aig.decls.size, hgate := ⋯ } }).aig.decls.size
Theorem: AIG.mkGateCached_le_size
Proof state before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
x✝ : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝ : aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
⊢ aig.decls.size ≤
    (match aig.decls[input.lhs.ref.gate], aig.decls[input.rhs.ref.gate], input.lhs.inv, input.rhs.inv with
          | Decl.const true, x, true, x_1 => { decls := aig.decls, cache := aig.cache, inv := ⋯ }.mkConstCached false
          | Decl.const false, x, false, x_1 => { decls := aig.decls, cache := aig.cache, inv := ⋯ }.mkConstCached false
          | x, Decl.const true, x_1, true => { decls := aig.decls, cache := aig.cache, inv := ⋯ }.mkConstCached false
          | x, Decl.const false, x_1, false => { decls := aig.decls, cache := aig.cache, inv := ⋯ }.mkConstCached false
          | Decl.const true, x, false, false =>
            { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
              ref := { gate := input.rhs.ref.gate, hgate := ⋯ } }
          | Decl.const false, x, true, false =>
            { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
              ref := { gate := input.rhs.ref.gate, hgate := ⋯ } }
          | x, Decl.const true, false, false =>
            { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
              ref := { gate := input.lhs.ref.gate, hgate := ⋯ } }
          | x, Decl.const false, false, true =>
            { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
              ref := { gate := input.lhs.ref.gate, hgate := ⋯ } }
          | x, x_1, x_2, x_3 =>
            {
              aig :=
                { decls := aig.decls.push (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv),
                  cache :=
                    Cache.insert aig.decls aig.cache
                      (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv),
                  inv := ⋯ },
              ref := { gate := aig.decls.size, hgate := ⋯ } }).aig.decls.size
Tactic:
. split <;> simp_arith [mkConstCached_le_size]
Proof state after:
no goals
Theorem: AIG.mkGateCached_le_size
Proof state before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
x✝ : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
hit✝ : CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)
heq✝ : aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit✝
⊢ aig.decls.size ≤
    { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
            ref := { gate := hit✝.idx, hgate := ⋯ } }.aig.decls.size
Tactic:
simp
Proof state after:
no goals
Theorem: AIG.mkGateCached_le_size
Proof state before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
x✝ : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝ : aig.cache.find? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
⊢ aig.decls.size ≤
    (match aig.decls[input.lhs.ref.gate], aig.decls[input.rhs.ref.gate], input.lhs.inv, input.rhs.inv with
          | Decl.const true, x, true, x_1 => { decls := aig.decls, cache := aig.cache, inv := ⋯ }.mkConstCached false
          | Decl.const false, x, false, x_1 => { decls := aig.decls, cache := aig.cache, inv := ⋯ }.mkConstCached false
          | x, Decl.const true, x_1, true => { decls := aig.decls, cache := aig.cache, inv := ⋯ }.mkConstCached false
          | x, Decl.const false, x_1, false => { decls := aig.decls, cache := aig.cache, inv := ⋯ }.mkConstCached false
          | Decl.const true, x, false, false =>
            { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
              ref := { gate := input.rhs.ref.gate, hgate := ⋯ } }
          | Decl.const false, x, true, false =>
            { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
              ref := { gate := input.rhs.ref.gate, hgate := ⋯ } }
          | x, Decl.const true, false, false =>
            { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
              ref := { gate := input.lhs.ref.gate, hgate := ⋯ } }
          | x, Decl.const false, false, true =>
            { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ },
              ref := { gate := input.lhs.ref.gate, hgate := ⋯ } }
          | x, x_1, x_2, x_3 =>
            {
              aig :=
                { decls := aig.decls.push (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv),
                  cache :=
                    Cache.insert aig.decls aig.cache
                      (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv),
                  inv := ⋯ },
              ref := { gate := aig.decls.size, hgate := ⋯ } }).aig.decls.size
Tactic:
split <;> simp_arith [mkConstCached_le_size]
Proof state after:
no goals
Theorem: AIG.mkGateCached_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
⊢ ∀ (idx : Nat) (h1 : idx < (aig.mkGateCached input).aig.decls.size) (h2 : idx < aig.decls.size),
    (aig.mkGateCached input).aig.decls[idx] = aig.decls[idx]
Tactic:
generalize hres : mkGateCached aig input = res
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
res : Entrypoint α
hres : aig.mkGateCached input = res
⊢ ∀ (idx : Nat) (h1 : idx < res.aig.decls.size) (h2 : idx < aig.decls.size), res.aig.decls[idx] = aig.decls[idx]