internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
case intro.right.intro.inr.intro.intro
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
h_base : motive 0 reducedToEmpty
h_inductive :
  ∀ (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)),
    motive (↑idx) res → motive (↑idx + 1) (reduce_fold_fn assignment res c_arr[idx])
h1 :
  Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToEmpty →
    ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < c_arr.size → ¬(p ⊨ c_arr[i])) ∨ ¬(p ⊨ assignment)
h2 :
  ∀ (l : Literal (PosFin n)),
    Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToUnit l →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → (∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])) → p ⊨ l
l : Literal (PosFin n)
hl : Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToUnit l
p : PosFin n → Bool
hp : p ⊨ assignment
i : PosFin n
pc1 : (i, true) ∈ c_arr.data
pc2 : decide (p i = true) = true
idx : Fin c_arr.size
hidx : c_arr[idx] = (i, true)
⊢ p ⊨ c_arr[idx]
Tactic:
rw [hidx]
Proof state after:
case intro.right.intro.inr.intro.intro
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
h_base : motive 0 reducedToEmpty
h_inductive :
  ∀ (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)),
    motive (↑idx) res → motive (↑idx + 1) (reduce_fold_fn assignment res c_arr[idx])
h1 :
  Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToEmpty →
    ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < c_arr.size → ¬(p ⊨ c_arr[i])) ∨ ¬(p ⊨ assignment)
h2 :
  ∀ (l : Literal (PosFin n)),
    Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToUnit l →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → (∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])) → p ⊨ l
l : Literal (PosFin n)
hl : Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToUnit l
p : PosFin n → Bool
hp : p ⊨ assignment
i : PosFin n
pc1 : (i, true) ∈ c_arr.data
pc2 : decide (p i = true) = true
idx : Fin c_arr.size
hidx : c_arr[idx] = (i, true)
⊢ p ⊨ (i, true)
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
case intro.right.intro.inr.intro.intro
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
h_base : motive 0 reducedToEmpty
h_inductive :
  ∀ (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)),
    motive (↑idx) res → motive (↑idx + 1) (reduce_fold_fn assignment res c_arr[idx])
h1 :
  Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToEmpty →
    ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < c_arr.size → ¬(p ⊨ c_arr[i])) ∨ ¬(p ⊨ assignment)
h2 :
  ∀ (l : Literal (PosFin n)),
    Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToUnit l →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → (∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])) → p ⊨ l
l : Literal (PosFin n)
hl : Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToUnit l
p : PosFin n → Bool
hp : p ⊨ assignment
i : PosFin n
pc1 : (i, true) ∈ c_arr.data
pc2 : decide (p i = true) = true
idx : Fin c_arr.size
hidx : c_arr[idx] = (i, true)
⊢ p i = true
Tactic:
exact of_decide_eq_true pc2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
h_base : motive 0 reducedToEmpty
h_inductive :
  ∀ (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)),
    motive (↑idx) res → motive (↑idx + 1) (reduce_fold_fn assignment res c_arr[idx])
h1 :
  Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToEmpty →
    ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < c_arr.size → ¬(p ⊨ c_arr[i])) ∨ ¬(p ⊨ assignment)
h2 :
  ∀ (l : Literal (PosFin n)),
    Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToUnit l →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → (∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])) → p ⊨ l
l : Literal (PosFin n)
hl : Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToUnit l
p : PosFin n → Bool
hp : p ⊨ assignment
i : PosFin n
pc1 : (i, true) ∈ c_arr.data
pc2 : decide (p i = true) = true
⊢ ∃ idx, c_arr[idx] = (i, true)
Tactic:
rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
Proof state after:
case intro
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
h_base : motive 0 reducedToEmpty
h_inductive :
  ∀ (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)),
    motive (↑idx) res → motive (↑idx + 1) (reduce_fold_fn assignment res c_arr[idx])
h1 :
  Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToEmpty →
    ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < c_arr.size → ¬(p ⊨ c_arr[i])) ∨ ¬(p ⊨ assignment)
h2 :
  ∀ (l : Literal (PosFin n)),
    Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToUnit l →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → (∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])) → p ⊨ l
l : Literal (PosFin n)
hl : Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToUnit l
p : PosFin n → Bool
hp : p ⊨ assignment
i : PosFin n
pc1 : (i, true) ∈ c_arr.data
pc2 : decide (p i = true) = true
idx : Fin c_arr.data.length
hidx : c_arr.data.get idx = (i, true)
⊢ ∃ idx, c_arr[idx] = (i, true)
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
case intro
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
h_base : motive 0 reducedToEmpty
h_inductive :
  ∀ (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)),
    motive (↑idx) res → motive (↑idx + 1) (reduce_fold_fn assignment res c_arr[idx])
h1 :
  Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToEmpty →
    ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < c_arr.size → ¬(p ⊨ c_arr[i])) ∨ ¬(p ⊨ assignment)
h2 :
  ∀ (l : Literal (PosFin n)),
    Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToUnit l →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → (∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])) → p ⊨ l
l : Literal (PosFin n)
hl : Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToUnit l
p : PosFin n → Bool
hp : p ⊨ assignment
i : PosFin n
pc1 : (i, true) ∈ c_arr.data
pc2 : decide (p i = true) = true
idx : Fin c_arr.data.length
hidx : c_arr.data.get idx = (i, true)
⊢ ∃ idx, c_arr[idx] = (i, true)
Tactic:
rw [← Array.getElem_fin_eq_data_get] at hidx
Proof state after:
case intro
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
h_base : motive 0 reducedToEmpty
h_inductive :
  ∀ (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)),
    motive (↑idx) res → motive (↑idx + 1) (reduce_fold_fn assignment res c_arr[idx])
h1 :
  Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToEmpty →
    ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < c_arr.size → ¬(p ⊨ c_arr[i])) ∨ ¬(p ⊨ assignment)
h2 :
  ∀ (l : Literal (PosFin n)),
    Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToUnit l →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → (∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])) → p ⊨ l
l : Literal (PosFin n)
hl : Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToUnit l
p : PosFin n → Bool
hp : p ⊨ assignment
i : PosFin n
pc1 : (i, true) ∈ c_arr.data
pc2 : decide (p i = true) = true
idx : Fin c_arr.data.length
hidx : c_arr[idx] = (i, true)
⊢ ∃ idx, c_arr[idx] = (i, true)
Theorem: LRAT.DefaultFormula.reduce_postcondition
Proof state before:
case intro
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
h_base : motive 0 reducedToEmpty
h_inductive :
  ∀ (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)),
    motive (↑idx) res → motive (↑idx + 1) (reduce_fold_fn assignment res c_arr[idx])
h1 :
  Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToEmpty →
    ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < c_arr.size → ¬(p ⊨ c_arr[i])) ∨ ¬(p ⊨ assignment)
h2 :
  ∀ (l : Literal (PosFin n)),
    Array.foldl (fun b => reduce_fold_fn assignment b) reducedToEmpty c_arr 0 = reducedToUnit l →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → (∃ i, ↑i < c_arr.size ∧ (p ⊨ c_arr[i])) → p ⊨ l
l : Literal (PosFin n)
hl : Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToUnit l
p : PosFin n → Bool
hp : p ⊨ assignment
i : PosFin n
pc1 : (i, true) ∈ c_arr.data
pc2 : decide (p i = true) = true
idx : Fin c_arr.data.length
hidx : c_arr[idx] = (i, true)
⊢ ∃ idx, c_arr[idx] = (i, true)
Tactic:
exact Exists.intro idx hidx
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
ih : f.confirmRupHint_fold_entails_hsat_motive (↑idx) acc
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
Tactic:
rcases ih with ⟨hsize, h1, h2⟩
Proof state after:
case intro.intro
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
case intro.intro
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
Tactic:
simp only [confirmRupHint, Bool.or_eq_true, Prod.mk.eta, Fin.getElem_fin]
Proof state after:
case intro.intro
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (if acc.2.2.snd = true ∨ acc.2.2.fst = true then acc
    else
      match f.clauses[rupHints[↑idx]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true))
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
case intro.intro
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (if acc.2.2.snd = true ∨ acc.2.2.fst = true then acc
    else
      match f.clauses[rupHints[↑idx]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true))
Tactic:
split
Proof state after:
case intro.intro.isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
h✝ : acc.2.2.snd = true ∨ acc.2.2.fst = true
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) acc

case intro.intro.isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
h✝ : ¬(acc.2.2.snd = true ∨ acc.2.2.fst = true)
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (match f.clauses[rupHints[↑idx]]? with
    | some (some c) =>
      match c.reduce acc.fst with
      | encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | reducedToNonunit => (acc.fst, acc.2.fst, false, true)
    | some none => (acc.fst, acc.2.fst, false, true)
    | none => (acc.fst, acc.2.fst, false, true))
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
case intro.intro.isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
h✝ : acc.2.2.snd = true ∨ acc.2.2.fst = true
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) acc

case intro.intro.isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
h✝ : ¬(acc.2.2.snd = true ∨ acc.2.2.fst = true)
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (match f.clauses[rupHints[↑idx]]? with
    | some (some c) =>
      match c.reduce acc.fst with
      | encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | reducedToNonunit => (acc.fst, acc.2.fst, false, true)
    | some none => (acc.fst, acc.2.fst, false, true)
    | none => (acc.fst, acc.2.fst, false, true))
Tactic:
. exact ⟨hsize, h1, h2⟩
Proof state after:
case intro.intro.isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
h✝ : ¬(acc.2.2.snd = true ∨ acc.2.2.fst = true)
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (match f.clauses[rupHints[↑idx]]? with
    | some (some c) =>
      match c.reduce acc.fst with
      | encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | reducedToNonunit => (acc.fst, acc.2.fst, false, true)
    | some none => (acc.fst, acc.2.fst, false, true)
    | none => (acc.fst, acc.2.fst, false, true))
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
case intro.intro.isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
h✝ : acc.2.2.snd = true ∨ acc.2.2.fst = true
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) acc
Tactic:
exact ⟨hsize, h1, h2⟩
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : ¬(acc.2.2.snd = true ∨ acc.2.2.fst = true)
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (match f.clauses[rupHints[↑idx]]? with
    | some (some c) =>
      match c.reduce acc.fst with
      | encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | reducedToNonunit => (acc.fst, acc.2.fst, false, true)
    | some none => (acc.fst, acc.2.fst, false, true)
    | none => (acc.fst, acc.2.fst, false, true))
Tactic:
simp only [not_or, Bool.not_eq_true] at acc2_eq_false
Proof state after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (match f.clauses[rupHints[↑idx]]? with
    | some (some c) =>
      match c.reduce acc.fst with
      | encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | reducedToNonunit => (acc.fst, acc.2.fst, false, true)
    | some none => (acc.fst, acc.2.fst, false, true)
    | none => (acc.fst, acc.2.fst, false, true))
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (match f.clauses[rupHints[↑idx]]? with
    | some (some c) =>
      match c.reduce acc.fst with
      | encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | reducedToNonunit => (acc.fst, acc.2.fst, false, true)
    | some none => (acc.fst, acc.2.fst, false, true)
    | none => (acc.fst, acc.2.fst, false, true))
Tactic:
split
Proof state after:
case h_1
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝ : f.clauses[rupHints[↑idx]]? = some (some c✝)
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (match c✝.reduce acc.fst with
    | encounteredBoth => (acc.fst, acc.2.fst, true, false)
    | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
    | reducedToUnit (l, b) =>
      if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
    | reducedToNonunit => (acc.fst, acc.2.fst, false, true))

case h_2
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
heq✝ : f.clauses[rupHints[↑idx]]? = some none
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, false, true)

case h_3
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
heq✝ : f.clauses[rupHints[↑idx]]? = none
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, false, true)