Theorem: AIG.mkConst_decl_eq (LeanSAT/AIG/Lemmas.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
this : aig.decls.size ≤ (aig.mkConst val).aig.decls.size
⊢ idx < (aig.mkConst val).aig.decls.size
Tactic:
omega
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
⊢ let_fun this := ⋯;
  (aig.mkConst val).aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [mkConst, Array.get_push]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
⊢ (if h : idx < aig.decls.size then aig.decls[idx] else Decl.const val) = aig.decls[idx]

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
⊢ (if h : idx < aig.decls.size then aig.decls[idx] else Decl.const val) = aig.decls[idx]
Tactic:
split
State after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h 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
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

State before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h 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
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Tactic:
. rfl
State after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

State before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Tactic:
. contradiction
State after:
no goals

State before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h h✝ : idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Tactic:
rfl
State after:
no goals

State before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Tactic:
contradiction
State after:
no goals