internlm/Lean-Github huggingface dataset:
Theorem: AIG.mkAtomCached_eval_eq_mkAtom_eval
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
assign : α → Bool
aig : AIG α
⊢ ⟦match aig.cache.find? (Decl.atom var) with
      | some hit =>
        { aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
      | none =>
        {
          aig :=
            { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
              inv := ⋯ },
          ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkAtom var, assign⟧
Tactic:
split
Proof state after:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
hit✝ : CacheHit aig.decls (Decl.atom var)
heq✝ : aig.cache.find? (Decl.atom var) = some hit✝
⊢ ⟦{ aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit✝.idx, hgate := ⋯ } }, assign⟧ =
    ⟦aig.mkAtom var, assign⟧

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

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
heq✝ : aig.cache.find? (Decl.atom var) = none
⊢ ⟦{
        aig :=
          { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
            inv := ⋯ },
        ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkAtom var, assign⟧
Tactic:
. next heq1 =>
  rw [denote_mkAtom_cached heq1]
Proof state after:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
heq✝ : aig.cache.find? (Decl.atom var) = none
⊢ ⟦{
        aig :=
          { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
            inv := ⋯ },
        ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkAtom var, assign⟧
Theorem: AIG.mkAtomCached_eval_eq_mkAtom_eval
Proof state before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
heq✝ : aig.cache.find? (Decl.atom var) = none
⊢ ⟦{
        aig :=
          { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
            inv := ⋯ },
        ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkAtom var, assign⟧
Tactic:
. simp [mkAtom, denote]
Proof state after:
no goals
Theorem: AIG.mkAtomCached_eval_eq_mkAtom_eval
Proof state before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
hit✝ : CacheHit aig.decls (Decl.atom var)
heq✝ : aig.cache.find? (Decl.atom var) = some hit✝
⊢ ⟦{ aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit✝.idx, hgate := ⋯ } }, assign⟧ =
    ⟦aig.mkAtom var, assign⟧
Tactic:
next heq1 =>
rw [denote_mkAtom_cached heq1]
Proof state after:
no goals
Theorem: AIG.mkAtomCached_eval_eq_mkAtom_eval
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
hit✝ : CacheHit aig.decls (Decl.atom var)
heq1 : aig.cache.find? (Decl.atom var) = some hit✝
⊢ ⟦{ aig := { decls := aig.decls, cache := aig.cache, inv := ⋯ }, ref := { gate := hit✝.idx, hgate := ⋯ } }, assign⟧ =
    ⟦aig.mkAtom var, assign⟧
Tactic:
rw [denote_mkAtom_cached heq1]
Proof state after:
no goals
Theorem: AIG.mkAtomCached_eval_eq_mkAtom_eval
Proof state before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
assign : α → Bool
aig : AIG α
x✝ : Option (CacheHit aig.decls (Decl.atom var))
heq✝ : aig.cache.find? (Decl.atom var) = none
⊢ ⟦{
        aig :=
          { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
            inv := ⋯ },
        ref := { gate := aig.decls.size, hgate := ⋯ } },
      assign⟧ =
    ⟦aig.mkAtom var, assign⟧
Tactic:
simp [mkAtom, denote]
Proof state after:
no goals
Theorem: AIG.denote_mkConst_cached
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
b : Bool
assign : α → Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.const b)
⊢ aig.cache.find? (Decl.const b) = some hit →
    ⟦{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }, assign⟧ = ⟦aig.mkConst b, assign⟧
Tactic:
have := hit.hvalid
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
b : Bool
assign : α → Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.const b)
this : aig.decls[hit.idx] = Decl.const b
⊢ aig.cache.find? (Decl.const b) = some hit →
    ⟦{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }, assign⟧ = ⟦aig.mkConst b, assign⟧
Theorem: AIG.denote_mkConst_cached
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
b : Bool
assign : α → Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.const b)
this : aig.decls[hit.idx] = Decl.const b
⊢ aig.cache.find? (Decl.const b) = some hit →
    ⟦{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }, assign⟧ = ⟦aig.mkConst b, assign⟧
Tactic:
simp only [denote_mkConst]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
b : Bool
assign : α → Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.const b)
this : aig.decls[hit.idx] = Decl.const b
⊢ aig.cache.find? (Decl.const b) = some hit → ⟦{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }, assign⟧ = b
Theorem: AIG.denote_mkConst_cached
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
b : Bool
assign : α → Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.const b)
this : aig.decls[hit.idx] = Decl.const b
⊢ aig.cache.find? (Decl.const b) = some hit → ⟦{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }, assign⟧ = b
Tactic:
unfold denote denote.go
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
b : Bool
assign : α → Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.const b)
this : aig.decls[hit.idx] = Decl.const b
⊢ aig.cache.find? (Decl.const b) = some hit →
    (match elem :
        { aig := aig,
                ref :=
                  { gate := hit.idx,
                    hgate := ⋯ } }.aig.decls[{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.ref.gate] with
      | Decl.const b_1 => b_1
      | 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) =
      b
Theorem: AIG.denote_mkConst_cached
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
b : Bool
assign : α → Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.const b)
this : aig.decls[hit.idx] = Decl.const b
⊢ aig.cache.find? (Decl.const b) = some hit →
    (match elem :
        { aig := aig,
                ref :=
                  { gate := hit.idx,
                    hgate := ⋯ } }.aig.decls[{ aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }.ref.gate] with
      | Decl.const b_1 => b_1
      | 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) =
      b
Tactic:
split <;> simp_all
Proof state after:
no goals
Theorem: AIG.mkConstCached_hit_aig
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.const val)
hcache : aig.cache.find? (Decl.const val) = some hit
⊢ (aig.mkConstCached val).aig = aig
Tactic:
simp only [mkConstCached]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.const val)
hcache : aig.cache.find? (Decl.const val) = some hit
⊢ (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 := ⋯ } }).aig =
    aig
Theorem: AIG.mkConstCached_hit_aig
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.const val)
hcache : aig.cache.find? (Decl.const val) = some hit
⊢ (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 := ⋯ } }).aig =
    aig
Tactic:
split <;> simp_all
Proof state after:
no goals
Theorem: AIG.mkConstCached_miss_aig
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
aig : AIG α
hcache : aig.cache.find? (Decl.const val) = none
⊢ (aig.mkConstCached val).aig.decls = aig.decls.push (Decl.const val)
Tactic:
simp only [mkConstCached]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
aig : AIG α
hcache : aig.cache.find? (Decl.const val) = none
⊢ (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 := ⋯ } }).aig.decls =
    aig.decls.push (Decl.const val)
Theorem: AIG.mkConstCached_miss_aig
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
aig : AIG α
hcache : aig.cache.find? (Decl.const val) = none
⊢ (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 := ⋯ } }).aig.decls =
    aig.decls.push (Decl.const val)
Tactic:
split <;> simp_all
Proof state after:
no goals
Theorem: AIG.mkConstCached_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkConstCached val).aig.decls.size
⊢ (aig.mkConstCached val).aig.decls[idx] = aig.decls[idx]
Tactic:
match hcache:aig.cache.find? (.const val) with
| some gate =>
  have := mkConstCached_hit_aig aig hcache
  simp [this]
| none =>
  have := mkConstCached_miss_aig aig hcache
  simp only [this, Array.get_push]
  split
  . rfl
  . contradiction
Proof state after:
no goals
Theorem: AIG.mkConstCached_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkConstCached val).aig.decls.size
gate : CacheHit aig.decls (Decl.const val)
hcache : aig.cache.find? (Decl.const val) = some gate
⊢ (aig.mkConstCached val).aig.decls[idx] = aig.decls[idx]
Tactic:
have := mkConstCached_hit_aig aig hcache
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkConstCached val).aig.decls.size
gate : CacheHit aig.decls (Decl.const val)
hcache : aig.cache.find? (Decl.const val) = some gate
this : (aig.mkConstCached val).aig = aig
⊢ (aig.mkConstCached val).aig.decls[idx] = aig.decls[idx]
Theorem: AIG.mkConstCached_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkConstCached val).aig.decls.size
gate : CacheHit aig.decls (Decl.const val)
hcache : aig.cache.find? (Decl.const val) = some gate
this : (aig.mkConstCached val).aig = aig
⊢ (aig.mkConstCached val).aig.decls[idx] = aig.decls[idx]
Tactic:
simp [this]
Proof state after:
no goals
Theorem: AIG.mkConstCached_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkConstCached val).aig.decls.size
hcache : aig.cache.find? (Decl.const val) = none
⊢ (aig.mkConstCached val).aig.decls[idx] = aig.decls[idx]
Tactic:
have := mkConstCached_miss_aig aig hcache
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkConstCached val).aig.decls.size
hcache : aig.cache.find? (Decl.const val) = none
this : (aig.mkConstCached val).aig.decls = aig.decls.push (Decl.const val)
⊢ (aig.mkConstCached val).aig.decls[idx] = aig.decls[idx]
Theorem: AIG.mkConstCached_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkConstCached val).aig.decls.size
hcache : aig.cache.find? (Decl.const val) = none
this : (aig.mkConstCached val).aig.decls = aig.decls.push (Decl.const val)
⊢ (aig.mkConstCached val).aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [this, Array.get_push]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkConstCached val).aig.decls.size
hcache : aig.cache.find? (Decl.const val) = none
this : (aig.mkConstCached val).aig.decls = aig.decls.push (Decl.const val)
⊢ (if h : idx < aig.decls.size then aig.decls[idx] else Decl.const val) = aig.decls[idx]
Theorem: AIG.mkConstCached_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkConstCached val).aig.decls.size
hcache : aig.cache.find? (Decl.const val) = none
this : (aig.mkConstCached val).aig.decls = aig.decls.push (Decl.const val)
⊢ (if h : idx < aig.decls.size then aig.decls[idx] else Decl.const val) = aig.decls[idx]
Tactic:
split
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkConstCached val).aig.decls.size
hcache : aig.cache.find? (Decl.const val) = none
this : (aig.mkConstCached val).aig.decls = aig.decls.push (Decl.const val)
h✝ : idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkConstCached val).aig.decls.size
hcache : aig.cache.find? (Decl.const val) = none
this : (aig.mkConstCached val).aig.decls = aig.decls.push (Decl.const val)
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Theorem: AIG.mkConstCached_decl_eq
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkConstCached val).aig.decls.size
hcache : aig.cache.find? (Decl.const val) = none
this : (aig.mkConstCached val).aig.decls = aig.decls.push (Decl.const val)
h✝ : idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkConstCached val).aig.decls.size
hcache : aig.cache.find? (Decl.const val) = none
this : (aig.mkConstCached val).aig.decls = aig.decls.push (Decl.const val)
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Tactic:
. rfl
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkConstCached val).aig.decls.size
hcache : aig.cache.find? (Decl.const val) = none
this : (aig.mkConstCached val).aig.decls = aig.decls.push (Decl.const val)
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Theorem: AIG.mkConstCached_decl_eq
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkConstCached val).aig.decls.size
hcache : aig.cache.find? (Decl.const val) = none
this : (aig.mkConstCached val).aig.decls = aig.decls.push (Decl.const val)
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Tactic:
. contradiction
Proof state after:
no goals
Theorem: AIG.mkConstCached_decl_eq
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkConstCached val).aig.decls.size
hcache : aig.cache.find? (Decl.const val) = none
this : (aig.mkConstCached val).aig.decls = aig.decls.push (Decl.const val)
h✝ : idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Tactic:
rfl
Proof state after:
no goals
Theorem: AIG.mkConstCached_decl_eq
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkConstCached val).aig.decls.size
hcache : aig.cache.find? (Decl.const val) = none
this : (aig.mkConstCached val).aig.decls = aig.decls.push (Decl.const val)
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Tactic:
contradiction
Proof state after:
no goals
Theorem: AIG.mkConstCached_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
⊢ aig.decls.size ≤ (aig.mkConstCached val).aig.decls.size
Tactic:
dsimp [mkConstCached]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
⊢ aig.decls.size ≤
    (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 := ⋯ } }).aig.decls.size
Theorem: AIG.mkConstCached_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
⊢ aig.decls.size ≤
    (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 := ⋯ } }).aig.decls.size
Tactic:
split
Proof state after:
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

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
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

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
Proof state after:
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
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