Theorem: LRAT.DefaultFormula.delete_readyForRupAdd (LeanSAT/LRAT/Formula/Basic.lean)

State before:
n : Nat
f : DefaultFormula n
arr : Array Nat
⊢ f.readyForRupAdd → (f.delete arr).readyForRupAdd
Tactic:
intro h
State after:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (f.delete arr).readyForRupAdd

State before:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (f.delete arr).readyForRupAdd
Tactic:
rw [delete, Array.foldl_eq_foldl_data]
State after:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).readyForRupAdd

State before:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).readyForRupAdd
Tactic:
constructor
State after:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).rupUnits = #[]

case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant

State before:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).rupUnits = #[]

case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant
Tactic:
. have hb : f.rupUnits = #[] := h.1
  have hl (acc : DefaultFormula n) (ih : acc.rupUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.data) :
    (deleteOne acc id).rupUnits = #[] := by rw [deleteOne_preserves_rupUnits, ih]
  exact List.foldlRecOn arr.data deleteOne f hb hl
State after:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant

State before:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant
Tactic:
. have hb : strong_assignments_invariant f := h.2
  have hl (acc : DefaultFormula n) (ih : strong_assignments_invariant acc) (id : Nat) (_id_in_arr : id ∈ arr.data) :
    strong_assignments_invariant (deleteOne acc id) := deleteOne_preserves_strong_assignments_invariant acc id ih
  exact List.foldlRecOn arr.data deleteOne f hb hl
State after:
no goals

State before:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).rupUnits = #[]
Tactic:
have hb : f.rupUnits = #[] := h.1
State after:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.rupUnits = #[]
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).rupUnits = #[]

State before:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.rupUnits = #[]
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).rupUnits = #[]
Tactic:
have hl (acc : DefaultFormula n) (ih : acc.rupUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.data) :
  (deleteOne acc id).rupUnits = #[] := by rw [deleteOne_preserves_rupUnits, ih]
State after:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.rupUnits = #[]
hl : ∀ (acc : DefaultFormula n), acc.rupUnits = #[] → ∀ (id : Nat), id ∈ arr.data → (acc.deleteOne id).rupUnits = #[]
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).rupUnits = #[]

State before:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.rupUnits = #[]
hl : ∀ (acc : DefaultFormula n), acc.rupUnits = #[] → ∀ (id : Nat), id ∈ arr.data → (acc.deleteOne id).rupUnits = #[]
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).rupUnits = #[]
Tactic:
exact List.foldlRecOn arr.data deleteOne f hb hl
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.rupUnits = #[]
acc : DefaultFormula n
ih : acc.rupUnits = #[]
id : Nat
_id_in_arr : id ∈ arr.data
⊢ (acc.deleteOne id).rupUnits = #[]
Tactic:
rw [deleteOne_preserves_rupUnits, ih]
State after:
no goals

State before:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant
Tactic:
have hb : strong_assignments_invariant f := h.2
State after:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.strong_assignments_invariant
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant

State before:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.strong_assignments_invariant
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant
Tactic:
have hl (acc : DefaultFormula n) (ih : strong_assignments_invariant acc) (id : Nat) (_id_in_arr : id ∈ arr.data) :
  strong_assignments_invariant (deleteOne acc id) := deleteOne_preserves_strong_assignments_invariant acc id ih
State after:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.strong_assignments_invariant
hl :
  ∀ (acc : DefaultFormula n),
    acc.strong_assignments_invariant → ∀ (id : Nat), id ∈ arr.data → (acc.deleteOne id).strong_assignments_invariant
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant

State before:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.strong_assignments_invariant
hl :
  ∀ (acc : DefaultFormula n),
    acc.strong_assignments_invariant → ∀ (id : Nat), id ∈ arr.data → (acc.deleteOne id).strong_assignments_invariant
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant
Tactic:
exact List.foldlRecOn arr.data deleteOne f hb hl
State after:
no goals