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

State before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst
Tactic:
let motive := fun (_ : Nat) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool) =>
  ∃ hsize : acc.1.size = n, derivedLits_invariant f f_assignments_size acc.1 hsize acc.2.1
State after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst

State before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst
Tactic:
have h_base : motive 0 (f.assignments, [], false, false) := by
  apply Exists.intro f_assignments_size
  intro i
  apply Or.inl
  constructor
  . rfl
  . intro l l_in_nil
    simp only [List.find?, List.not_mem_nil] at l_in_nil
State after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h_base : motive 0 (f.assignments, [], false, false)
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst

State before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h_base : motive 0 (f.assignments, [], false, false)
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst
Tactic:
have h_inductive (i : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool)
  (ih : motive i.1 acc) := confirmRupHint_preserves_invariant f f_assignments_size rupHints i acc ih
State after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (i : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑i) acc →
      let rupHint_res := confirmRupHint f.clauses acc rupHints[i];
      ∃ hsize, f.derivedLits_invariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst

State before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (i : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑i) acc →
      let rupHint_res := confirmRupHint f.clauses acc rupHints[i];
      ∃ hsize, f.derivedLits_invariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst
Tactic:
rcases Array.foldl_induction motive h_base h_inductive with ⟨_, h⟩
State after:
case intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (i : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑i) acc →
      let rupHint_res := confirmRupHint f.clauses acc rupHints[i];
      ∃ hsize, f.derivedLits_invariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst
w✝ : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
h :
  f.derivedLits_invariant f_assignments_size
    (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst w✝
    (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.fst
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst

State before:
case intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (i : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑i) acc →
      let rupHint_res := confirmRupHint f.clauses acc rupHints[i];
      ∃ hsize, f.derivedLits_invariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst
w✝ : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
h :
  f.derivedLits_invariant f_assignments_size
    (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst w✝
    (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.fst
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst
Tactic:
exact h
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ motive 0 (f.assignments, [], false, false)
Tactic:
apply Exists.intro f_assignments_size
State after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ f.derivedLits_invariant f_assignments_size (f.assignments, [], false, false).fst f_assignments_size
    (f.assignments, [], false, false).snd.fst

State before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ f.derivedLits_invariant f_assignments_size (f.assignments, [], false, false).fst f_assignments_size
    (f.assignments, [], false, false).snd.fst
Tactic:
intro i
State after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ let_fun i_lt_assignments_size := ⋯;
  let_fun i_lt_f_assignments_size := ⋯;
  let assignments_i := (f.assignments, [], false, false).fst[↑i];
  let fassignments_i := f.assignments[↑i];
  (assignments_i = fassignments_i ∧
      ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i) ∨
    (∃ j,
        ((f.assignments, [], false, false).snd.fst.get j).fst.val = ↑i ∧
          assignments_i = addAssignment ((f.assignments, [], false, false).snd.fst.get j).snd fassignments_i ∧
            ¬hasAssignment ((f.assignments, [], false, false).snd.fst.get j).snd fassignments_i = true ∧
              ∀ (k : Fin (f.assignments, [], false, false).snd.fst.length),
                k ≠ j → ((f.assignments, [], false, false).snd.fst.get k).fst.val ≠ ↑i) ∨
      ∃ j1 j2,
        ((f.assignments, [], false, false).snd.fst.get j1).fst.val = ↑i ∧
          ((f.assignments, [], false, false).snd.fst.get j2).fst.val = ↑i ∧
            ((f.assignments, [], false, false).snd.fst.get j1).snd = true ∧
              ((f.assignments, [], false, false).snd.fst.get j2).snd = false ∧
                assignments_i = both ∧
                  fassignments_i = unassigned ∧
                    ∀ (k : Fin (f.assignments, [], false, false).snd.fst.length),
                      k ≠ j1 → k ≠ j2 → ((f.assignments, [], false, false).snd.fst.get k).fst.val ≠ ↑i

State before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ let_fun i_lt_assignments_size := ⋯;
  let_fun i_lt_f_assignments_size := ⋯;
  let assignments_i := (f.assignments, [], false, false).fst[↑i];
  let fassignments_i := f.assignments[↑i];
  (assignments_i = fassignments_i ∧
      ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i) ∨
    (∃ j,
        ((f.assignments, [], false, false).snd.fst.get j).fst.val = ↑i ∧
          assignments_i = addAssignment ((f.assignments, [], false, false).snd.fst.get j).snd fassignments_i ∧
            ¬hasAssignment ((f.assignments, [], false, false).snd.fst.get j).snd fassignments_i = true ∧
              ∀ (k : Fin (f.assignments, [], false, false).snd.fst.length),
                k ≠ j → ((f.assignments, [], false, false).snd.fst.get k).fst.val ≠ ↑i) ∨
      ∃ j1 j2,
        ((f.assignments, [], false, false).snd.fst.get j1).fst.val = ↑i ∧
          ((f.assignments, [], false, false).snd.fst.get j2).fst.val = ↑i ∧
            ((f.assignments, [], false, false).snd.fst.get j1).snd = true ∧
              ((f.assignments, [], false, false).snd.fst.get j2).snd = false ∧
                assignments_i = both ∧
                  fassignments_i = unassigned ∧
                    ∀ (k : Fin (f.assignments, [], false, false).snd.fst.length),
                      k ≠ j1 → k ≠ j2 → ((f.assignments, [], false, false).snd.fst.get k).fst.val ≠ ↑i
Tactic:
apply Or.inl
State after:
case h
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ (f.assignments, [], false, false).fst[↑i] = f.assignments[↑i] ∧
    ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i

State before:
case h
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ (f.assignments, [], false, false).fst[↑i] = f.assignments[↑i] ∧
    ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i
Tactic:
constructor
State after:
case h.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ (f.assignments, [], false, false).fst[↑i] = f.assignments[↑i]

case h.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i

State before:
case h.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ (f.assignments, [], false, false).fst[↑i] = f.assignments[↑i]

case h.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i
Tactic:
. rfl
State after:
case h.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i

State before:
case h.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i
Tactic:
. intro l l_in_nil
  simp only [List.find?, List.not_mem_nil] at l_in_nil
State after:
no goals

State before:
case h.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ (f.assignments, [], false, false).fst[↑i] = f.assignments[↑i]
Tactic:
rfl
State after:
no goals

State before:
case h.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i
Tactic:
intro l l_in_nil
State after:
case h.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
l : Literal (PosFin n)
l_in_nil : l ∈ (f.assignments, [], false, false).snd.fst
⊢ l.fst.val ≠ ↑i

State before:
case h.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
l : Literal (PosFin n)
l_in_nil : l ∈ (f.assignments, [], false, false).snd.fst
⊢ l.fst.val ≠ ↑i
Tactic:
simp only [List.find?, List.not_mem_nil] at l_in_nil
State after:
no goals