internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
case intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
h : ↑i ∈ (Array.map (fun x => x.fst) ratHints).data
j : Fin (Array.map (fun x => x.fst) ratHints).data.length
h' : (Array.map (fun x => x.fst) ratHints)[↑j] = ↑i
j_in_bounds : ↑j < ratHints.size
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Tactic:
simp only [Array.getElem_map] at h'
Proof state after:
case intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
h : ↑i ∈ (Array.map (fun x => x.fst) ratHints).data
j : Fin (Array.map (fun x => x.fst) ratHints).data.length
j_in_bounds : ↑j < ratHints.size
h' : ratHints[↑j].fst = ↑i
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
case intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
h : ↑i ∈ (Array.map (fun x => x.fst) ratHints).data
j : Fin (Array.map (fun x => x.fst) ratHints).data.length
j_in_bounds : ↑j < ratHints.size
h' : ratHints[↑j].fst = ↑i
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Tactic:
apply Exists.intro ⟨j.1, j_in_bounds⟩
Proof state after:
case intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
h : ↑i ∈ (Array.map (fun x => x.fst) ratHints).data
j : Fin (Array.map (fun x => x.fst) ratHints).data.length
j_in_bounds : ↑j < ratHints.size
h' : ratHints[↑j].fst = ↑i
⊢ f.clauses[ratHints[⟨↑j, j_in_bounds⟩].fst]! = some c'
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
case intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
h : ↑i ∈ (Array.map (fun x => x.fst) ratHints).data
j : Fin (Array.map (fun x => x.fst) ratHints).data.length
j_in_bounds : ↑j < ratHints.size
h' : ratHints[↑j].fst = ↑i
⊢ f.clauses[ratHints[⟨↑j, j_in_bounds⟩].fst]! = some c'
Tactic:
simp only [getElem!, Fin.getElem_fin, h', i_lt_f_clauses_size, dite_true]
Proof state after:
case intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
h : ↑i ∈ (Array.map (fun x => x.fst) ratHints).data
j : Fin (Array.map (fun x => x.fst) ratHints).data.length
j_in_bounds : ↑j < ratHints.size
h' : ratHints[↑j].fst = ↑i
⊢ f.clauses.get ⟨↑i, ⋯⟩ = some c'
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
case intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
h : ↑i ∈ (Array.map (fun x => x.fst) ratHints).data
j : Fin (Array.map (fun x => x.fst) ratHints).data.length
j_in_bounds : ↑j < ratHints.size
h' : ratHints[↑j].fst = ↑i
⊢ f.clauses.get ⟨↑i, ⋯⟩ = some c'
Tactic:
exact c'_in_f
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
⊢ ↑i < (Array.range f.clauses.size).size
Tactic:
rw [Array.range_size]
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
⊢ ↑i < f.clauses.size
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
⊢ ↑i < f.clauses.size
Tactic:
omega
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
⊢ ↑i < f.clauses.size
Tactic:
rw [Array.range_size] at i_in_bounds
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < f.clauses.size
⊢ ↑i < f.clauses.size
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < f.clauses.size
⊢ ↑i < f.clauses.size
Tactic:
exact i_in_bounds
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
⊢ ↑i ∈ (Array.map (fun x => x.fst) ratHints).data
Tactic:
rw [← of_decide_eq_true ratHintsExhaustive_eq_true]
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
⊢ ↑i ∈
    (Array.filter
        (fun i =>
          match f.clauses[i]! with
          | none => false
          | some c => c.contains pivot.negateLiteral)
        (Array.range f.clauses.size) 0).data
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
⊢ ↑i ∈
    (Array.filter
        (fun i =>
          match f.clauses[i]! with
          | none => false
          | some c => c.contains pivot.negateLiteral)
        (Array.range f.clauses.size) 0).data
Tactic:
have i_eq_range_i : i.1 = (Array.range f.clauses.size)[i.1]'i_in_bounds := by
  have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
  rw [Array.range_idx]
  conv => rhs; rw [f_clauses_rw, Array.size]
  exact i.2
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
i_eq_range_i : ↑i = (Array.range f.clauses.size)[↑i]
⊢ ↑i ∈
    (Array.filter
        (fun i =>
          match f.clauses[i]! with
          | none => false
          | some c => c.contains pivot.negateLiteral)
        (Array.range f.clauses.size) 0).data
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
i_eq_range_i : ↑i = (Array.range f.clauses.size)[↑i]
⊢ ↑i ∈
    (Array.filter
        (fun i =>
          match f.clauses[i]! with
          | none => false
          | some c => c.contains pivot.negateLiteral)
        (Array.range f.clauses.size) 0).data
Tactic:
rw [i_eq_range_i]
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
i_eq_range_i : ↑i = (Array.range f.clauses.size)[↑i]
⊢ (Array.range f.clauses.size)[↑i] ∈
    (Array.filter
        (fun i =>
          match f.clauses[i]! with
          | none => false
          | some c => c.contains pivot.negateLiteral)
        (Array.range f.clauses.size) 0).data
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
i_eq_range_i : ↑i = (Array.range f.clauses.size)[↑i]
⊢ (Array.range f.clauses.size)[↑i] ∈
    (Array.filter
        (fun i =>
          match f.clauses[i]! with
          | none => false
          | some c => c.contains pivot.negateLiteral)
        (Array.range f.clauses.size) 0).data
Tactic:
apply Misc.Array.mem_filter i.1 i_in_bounds
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
i_eq_range_i : ↑i = (Array.range f.clauses.size)[↑i]
⊢ (match f.clauses[(Array.range f.clauses.size)[↑i]]! with
    | none => false
    | some c => c.contains pivot.negateLiteral) =
    true
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
i_eq_range_i : ↑i = (Array.range f.clauses.size)[↑i]
⊢ (match f.clauses[(Array.range f.clauses.size)[↑i]]! with
    | none => false
    | some c => c.contains pivot.negateLiteral) =
    true
Tactic:
simp only [getElem!, Array.range_idx i_lt_f_clauses_size, i_lt_f_clauses_size, dite_true,
  c'_in_f, DefaultClause.contains_iff, Array.get_eq_getElem]
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
i_eq_range_i : ↑i = (Array.range f.clauses.size)[↑i]
⊢ pivot.negateLiteral ∈ c'.toList
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
i_eq_range_i : ↑i = (Array.range f.clauses.size)[↑i]
⊢ pivot.negateLiteral ∈ c'.toList
Tactic:
simp only [Clause.toList] at negPivot_in_c'
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ c'.toList
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
i_eq_range_i : ↑i = (Array.range f.clauses.size)[↑i]
⊢ pivot.negateLiteral ∈ c'.toList
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ c'.toList
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
i_eq_range_i : ↑i = (Array.range f.clauses.size)[↑i]
⊢ pivot.negateLiteral ∈ c'.toList
Tactic:
exact negPivot_in_c'
Proof state after:
no goals