Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_assignments_size (LeanSAT/LRAT/Formula/RupAddResult.lean)

State before:
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
⊢ (confirmRupHint clauses (assignments, derivedLits, b1, b2) id).fst.size = assignments.size
Tactic:
simp only [confirmRupHint]
State after:
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
⊢ (if (b2 || b1) = true then (assignments, derivedLits, b1, b2)
        else
          match clauses[id]? with
          | some (some c) =>
            match c.reduce assignments with
            | ReduceResult.encounteredBoth => (assignments, derivedLits, true, false)
            | ReduceResult.reducedToEmpty => (assignments, derivedLits, true, false)
            | ReduceResult.reducedToUnit (l, b) =>
              if hasAssignment b assignments[l.val]! = true then (assignments, derivedLits, false, false)
              else (assignments.modify l.val (addAssignment b), (l, b) :: derivedLits, false, false)
            | ReduceResult.reducedToNonunit => (assignments, derivedLits, false, true)
          | some none => (assignments, derivedLits, false, true)
          | none => (assignments, derivedLits, false, true)).fst.size =
    assignments.size

State before:
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
⊢ (if (b2 || b1) = true then (assignments, derivedLits, b1, b2)
        else
          match clauses[id]? with
          | some (some c) =>
            match c.reduce assignments with
            | ReduceResult.encounteredBoth => (assignments, derivedLits, true, false)
            | ReduceResult.reducedToEmpty => (assignments, derivedLits, true, false)
            | ReduceResult.reducedToUnit (l, b) =>
              if hasAssignment b assignments[l.val]! = true then (assignments, derivedLits, false, false)
              else (assignments.modify l.val (addAssignment b), (l, b) :: derivedLits, false, false)
            | ReduceResult.reducedToNonunit => (assignments, derivedLits, false, true)
          | some none => (assignments, derivedLits, false, true)
          | none => (assignments, derivedLits, false, true)).fst.size =
    assignments.size
Tactic:
repeat first
  | rfl
  | simp only [Array.modify_preserves_size]
  | split
State after:
no goals

State before:
case isFalse.h_3
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size
Tactic:
first
| rfl
| simp only [Array.modify_preserves_size]
| split
State after:
no goals

State before:
case isFalse.h_3
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size
Tactic:
rfl
State after:
no goals

State before:
case isFalse.h_1.h_3.isFalse
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝¹ : ¬(b2 || b1) = true
x✝¹ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝¹ : clauses[id]? = some (some c✝)
x✝ : ReduceResult (PosFin n)
l✝ : PosFin n
b✝ : Bool
heq✝ : c✝.reduce assignments = ReduceResult.reducedToUnit (l✝, b✝)
h✝ : ¬hasAssignment b✝ assignments[l✝.val]! = true
⊢ (assignments.modify l✝.val (addAssignment b✝), (l✝, b✝) :: derivedLits, false, false).fst.size = assignments.size

case isFalse.h_1.h_4
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝¹ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝¹ : clauses[id]? = some (some c✝)
x✝ : ReduceResult (PosFin n)
heq✝ : c✝.reduce assignments = ReduceResult.reducedToNonunit
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_2
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = some none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_3
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size
Tactic:
simp only [Array.modify_preserves_size]
State after:
case isFalse.h_1.h_4
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝¹ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝¹ : clauses[id]? = some (some c✝)
x✝ : ReduceResult (PosFin n)
heq✝ : c✝.reduce assignments = ReduceResult.reducedToNonunit
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_2
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = some none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_3
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

State before:
case isFalse.h_1.h_3
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝¹ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝¹ : clauses[id]? = some (some c✝)
x✝ : ReduceResult (PosFin n)
l✝ : PosFin n
b✝ : Bool
heq✝ : c✝.reduce assignments = ReduceResult.reducedToUnit (l✝, b✝)
⊢ (if hasAssignment b✝ assignments[l✝.val]! = true then (assignments, derivedLits, false, false)
        else (assignments.modify l✝.val (addAssignment b✝), (l✝, b✝) :: derivedLits, false, false)).fst.size =
    assignments.size

case isFalse.h_1.h_4
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝¹ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝¹ : clauses[id]? = some (some c✝)
x✝ : ReduceResult (PosFin n)
heq✝ : c✝.reduce assignments = ReduceResult.reducedToNonunit
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_2
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = some none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_3
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size
Tactic:
split
State after:
case isFalse.h_1.h_3.isTrue
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝¹ : ¬(b2 || b1) = true
x✝¹ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝¹ : clauses[id]? = some (some c✝)
x✝ : ReduceResult (PosFin n)
l✝ : PosFin n
b✝ : Bool
heq✝ : c✝.reduce assignments = ReduceResult.reducedToUnit (l✝, b✝)
h✝ : hasAssignment b✝ assignments[l✝.val]! = true
⊢ (assignments, derivedLits, false, false).fst.size = assignments.size

case isFalse.h_1.h_3.isFalse
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝¹ : ¬(b2 || b1) = true
x✝¹ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝¹ : clauses[id]? = some (some c✝)
x✝ : ReduceResult (PosFin n)
l✝ : PosFin n
b✝ : Bool
heq✝ : c✝.reduce assignments = ReduceResult.reducedToUnit (l✝, b✝)
h✝ : ¬hasAssignment b✝ assignments[l✝.val]! = true
⊢ (assignments.modify l✝.val (addAssignment b✝), (l✝, b✝) :: derivedLits, false, false).fst.size = assignments.size

case isFalse.h_1.h_4
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝¹ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝¹ : clauses[id]? = some (some c✝)
x✝ : ReduceResult (PosFin n)
heq✝ : c✝.reduce assignments = ReduceResult.reducedToNonunit
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_2
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = some none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_3
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size