internlm/Lean-Github huggingface dataset:
Theorem: BVDecide.verifyCert_correct
Proof state before:
case intro.intro
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
action :
  LRAT.Action (LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)) (PosFin ((LratFormula.ofCnf c).numVars + 1))
wellFormedActions : { act // LRAT.wellFormedAction act }
left✝ :
  ∃ a,
    (∃ a_1, a_1 ∈ lratProof✝.toList ∧ LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1) a_1 = a) ∧
      (match a with
        | none => none
        | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
        | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
        | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
        | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
          if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
          else none) =
        some wellFormedActions
h2 : wellFormedActions.val = action
⊢ LRAT.wellFormedAction wellFormedActions.val
Tactic:
exact wellFormedActions.property
Proof state after:
no goals
Theorem: BVDecide.verifyCert_correct
Proof state before:
case h_1.a.intro.intro.h_1
c : CNF Nat
b : LratCert
x✝¹ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝¹ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
h3 : ∀ (x : CNF.Clause (PosFin (c.numLiterals + 1))), x ∈ c.lift → CNF.Clause.eval assignment x = true
x✝ : Option (LRAT.DefaultClause (c.numLiterals + 1))
foo✝ : LRAT.DefaultClause (c.numLiterals + 1)
heq✝ : reflectClause.convertLRAT' = some foo✝
hrclause2 : some (some foo✝) = some (some lratClause)
⊢ assignment ⊨ lratClause
Tactic:
next heq =>
rw [← heq] at hrclause2
simp only [Option.some.injEq] at hrclause2
simp [CNF.Clause.convertLRAT_sat_of_sat reflectClause hrclause2, h3 reflectClause hrclause1]
Proof state after:
no goals
Theorem: BVDecide.verifyCert_correct
Proof state before:
c : CNF Nat
b : LratCert
x✝¹ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
h3 : ∀ (x : CNF.Clause (PosFin (c.numLiterals + 1))), x ∈ c.lift → CNF.Clause.eval assignment x = true
x✝ : Option (LRAT.DefaultClause (c.numLiterals + 1))
foo✝ : LRAT.DefaultClause (c.numLiterals + 1)
heq : reflectClause.convertLRAT' = some foo✝
hrclause2 : reflectClause.convertLRAT' = some lratClause
⊢ assignment ⊨ lratClause
Tactic:
simp [CNF.Clause.convertLRAT_sat_of_sat reflectClause hrclause2, h3 reflectClause hrclause1]
Proof state after:
no goals
Theorem: BVDecide.verifyCert_correct
Proof state before:
case h_1.a.intro.intro.h_2
c : CNF Nat
b : LratCert
x✝¹ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝¹ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
h2✝ : unsatisfiable (PosFin ((LratFormula.ofCnf c).numVars + 1)) (LratFormula.ofCnf c).formula
assignment : PosFin (c.numLiterals + 1) → Bool
h2 : ¬(assignment ⊨ LRAT.DefaultFormula.ofArray (List.toArray c.lift.convertLRAT'))
lratClause : LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)
reflectClause : CNF.Clause (PosFin (c.numLiterals + 1))
hrclause1 : reflectClause ∈ c.lift
h3 : ∀ (x : CNF.Clause (PosFin (c.numLiterals + 1))), x ∈ c.lift → CNF.Clause.eval assignment x = true
x✝ : Option (LRAT.DefaultClause (c.numLiterals + 1))
heq✝ : reflectClause.convertLRAT' = none
hrclause2 : none = some (some lratClause)
⊢ assignment ⊨ lratClause
Tactic:
contradiction
Proof state after:
no goals
Theorem: BVDecide.verifyCert_correct
Proof state before:
case h_2
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = none
h1 : false = true
⊢ c.unsat
Tactic:
contradiction
Proof state after:
no goals
Theorem: bitvec_InstCombineShift__422_1
Proof state before:
⊢ ∀ (Y X C : BitVec 31), (Y + X >>> C) <<< C = Y <<< C + X &&& (-1) <<< C
Tactic:
intros
Proof state after:
Y✝ X✝ C✝ : BitVec 31
⊢ (Y✝ + X✝ >>> C✝) <<< C✝ = Y✝ <<< C✝ + X✝ &&& (-1) <<< C✝
Theorem: bitvec_InstCombineShift__422_1
Proof state before:
Y✝ X✝ C✝ : BitVec 31
⊢ (Y✝ + X✝ >>> C✝) <<< C✝ = Y✝ <<< C✝ + X✝ &&& (-1) <<< C✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: BVPred.blastGetLsb_denote_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
target : GetLsbTarget aig
assign : α → Bool
⊢ ⟦blastGetLsb aig target, assign⟧ =
    if h : target.idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef target.idx h }, assign⟧ else false
Tactic:
rcases target with ⟨expr, idx⟩
Proof state after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefStream w✝
idx : Nat
⊢ ⟦blastGetLsb aig (GetLsbTarget.mk expr idx), assign⟧ =
    if h : (GetLsbTarget.mk expr idx).idx < (GetLsbTarget.mk expr idx).w then
      ⟦{ aig := aig, ref := (GetLsbTarget.mk expr idx).stream.getRef (GetLsbTarget.mk expr idx).idx h }, assign⟧
    else false
Theorem: BVPred.blastGetLsb_denote_eq_eval_getLsb
Proof state before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefStream w✝
idx : Nat
⊢ ⟦blastGetLsb aig (GetLsbTarget.mk expr idx), assign⟧ =
    if h : (GetLsbTarget.mk expr idx).idx < (GetLsbTarget.mk expr idx).w then
      ⟦{ aig := aig, ref := (GetLsbTarget.mk expr idx).stream.getRef (GetLsbTarget.mk expr idx).idx h }, assign⟧
    else false
Tactic:
unfold blastGetLsb
Proof state after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefStream w✝
idx : Nat
⊢ ⟦if h : (GetLsbTarget.mk expr idx).idx < (GetLsbTarget.mk expr idx).w then
        { aig := aig, ref := (GetLsbTarget.mk expr idx).stream.getRef (GetLsbTarget.mk expr idx).idx h }
      else aig.mkConstCached false,
      assign⟧ =
    if h : (GetLsbTarget.mk expr idx).idx < (GetLsbTarget.mk expr idx).w then
      ⟦{ aig := aig, ref := (GetLsbTarget.mk expr idx).stream.getRef (GetLsbTarget.mk expr idx).idx h }, assign⟧
    else false
Theorem: BVPred.blastGetLsb_denote_eq_eval_getLsb
Proof state before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefStream w✝
idx : Nat
⊢ ⟦if h : (GetLsbTarget.mk expr idx).idx < (GetLsbTarget.mk expr idx).w then
        { aig := aig, ref := (GetLsbTarget.mk expr idx).stream.getRef (GetLsbTarget.mk expr idx).idx h }
      else aig.mkConstCached false,
      assign⟧ =
    if h : (GetLsbTarget.mk expr idx).idx < (GetLsbTarget.mk expr idx).w then
      ⟦{ aig := aig, ref := (GetLsbTarget.mk expr idx).stream.getRef (GetLsbTarget.mk expr idx).idx h }, assign⟧
    else false
Tactic:
dsimp
Proof state after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefStream w✝
idx : Nat
⊢ ⟦if h : idx < w✝ then { aig := aig, ref := expr.getRef idx h } else aig.mkConstCached false, assign⟧ =
    if h : idx < w✝ then ⟦{ aig := aig, ref := expr.getRef idx h }, assign⟧ else false
Theorem: BVPred.blastGetLsb_denote_eq_eval_getLsb
Proof state before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefStream w✝
idx : Nat
⊢ ⟦if h : idx < w✝ then { aig := aig, ref := expr.getRef idx h } else aig.mkConstCached false, assign⟧ =
    if h : idx < w✝ then ⟦{ aig := aig, ref := expr.getRef idx h }, assign⟧ else false
Tactic:
split <;> simp
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2486
Proof state before:
⊢ ∀ (x C : BitVec 64), x + C ^^^ -1 = -1 - C - x
Tactic:
intros
Proof state after:
x✝ C✝ : BitVec 64
⊢ x✝ + C✝ ^^^ -1 = -1 - C✝ - x✝
Theorem: bitvec_AndOrXor_2486
Proof state before:
x✝ C✝ : BitVec 64
⊢ x✝ + C✝ ^^^ -1 = -1 - C✝ - x✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_827
Proof state before:
⊢ ∀ (a b : BitVec 64), (a == 0 && b == 0) = (a ||| b == 0)
Tactic:
intros
Proof state after:
a✝ b✝ : BitVec 64
⊢ (a✝ == 0 && b✝ == 0) = (a✝ ||| b✝ == 0)
Theorem: bitvec_AndOrXor_827
Proof state before:
a✝ b✝ : BitVec 64
⊢ (a✝ == 0 && b✝ == 0) = (a✝ ||| b✝ == 0)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_1288_A__B__B__C__A___A__B__C
Proof state before:
⊢ ∀ (A C B : BitVec 64), (A ^^^ B) &&& (B ^^^ C ^^^ A) = (A ^^^ B) &&& (C ^^^ -1)
Tactic:
intros
Proof state after:
A✝ C✝ B✝ : BitVec 64
⊢ (A✝ ^^^ B✝) &&& (B✝ ^^^ C✝ ^^^ A✝) = (A✝ ^^^ B✝) &&& (C✝ ^^^ -1)
Theorem: bitvec_AndOrXor_1288_A__B__B__C__A___A__B__C
Proof state before:
A✝ C✝ B✝ : BitVec 64
⊢ (A✝ ^^^ B✝) &&& (B✝ ^^^ C✝ ^^^ A✝) = (A✝ ^^^ B✝) &&& (C✝ ^^^ -1)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: trace_unit_1
Proof state before:
x y : BitVec 64
⊢ x + y = y + x
Tactic:
bv_decide?
Proof state after:
no goals
Theorem: trace_unit_2
Proof state before:
x : BitVec 64
⊢ x = x
Tactic:
bv_decide?
Proof state after:
no goals
Theorem: trace_unit_1'
Proof state before:
x y : BitVec 64
⊢ x + y = y + x
Tactic:
bv_check "trace.lrat"
Proof state after:
no goals
Theorem: trace_unit_2'
Proof state before:
x : BitVec 64
⊢ x = x
Tactic:
bv_normalize
Proof state after:
no goals
Theorem: BoolExpr.size_pos
Proof state before:
α : Type
x : BoolExpr α
⊢ 0 < x.size
Tactic:
cases x <;> simp [size] <;> omega
Proof state after:
no goals
Theorem: BoolExpr.sat_and
Proof state before:
α : Type
x y : BoolExpr α
f : α → Bool
hx : x.sat f
hy : y.sat f
⊢ (gate Gate.and x y).sat f
Tactic:
simp only [sat] at *
Proof state after:
α : Type
x y : BoolExpr α
f : α → Bool
hx : eval f x = true
hy : eval f y = true
⊢ eval f (gate Gate.and x y) = true
Theorem: BoolExpr.sat_and
Proof state before:
α : Type
x y : BoolExpr α
f : α → Bool
hx : eval f x = true
hy : eval f y = true
⊢ eval f (gate Gate.and x y) = true
Tactic:
simp [hx, hy, Gate.eval]
Proof state after:
no goals
Theorem: List.all_append
Proof state before:
α : Type u_1
f : α → Bool
x y : List α
⊢ (x ++ y).all f = (x.all f && y.all f)
Tactic:
induction x with
| nil => rfl
| cons h t ih => simp_all [Bool.and_assoc]
Proof state after:
no goals
Theorem: List.all_append
Proof state before:
case nil
α : Type u_1
f : α → Bool
y : List α
⊢ ([] ++ y).all f = ([].all f && y.all f)
Tactic:
rfl
Proof state after:
no goals
Theorem: List.all_append
Proof state before:
case cons
α : Type u_1
f : α → Bool
y : List α
h : α
t : List α
ih : (t ++ y).all f = (t.all f && y.all f)
⊢ (h :: t ++ y).all f = ((h :: t).all f && y.all f)
Tactic:
simp_all [Bool.and_assoc]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_size
Proof state before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
⊢ (f.insertRatUnits units).fst.assignments.size = f.assignments.size
Tactic:
simp only [insertRatUnits, Prod.mk.eta]
Proof state after:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
⊢ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst.size = f.assignments.size
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_size
Proof state before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
⊢ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst.size = f.assignments.size
Tactic:
exact insertUnit_fold_preserves_size f.ratUnits f.assignments false
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_postcondition
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
assignments : Array Assignment := (f.insertRatUnits units).fst.assignments
⊢ assignments.size = n
Tactic:
rw [← hf.2]
Proof state after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
assignments : Array Assignment := (f.insertRatUnits units).fst.assignments
⊢ assignments.size = f.assignments.size
Theorem: LRAT.DefaultFormula.insertRatUnits_postcondition
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
assignments : Array Assignment := (f.insertRatUnits units).fst.assignments
⊢ assignments.size = f.assignments.size
Tactic:
exact insertRatUnits_preserves_assignments_size f units
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_postcondition
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
⊢ let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  insertUnit_invariant f.assignments ⋯ ratUnits assignments hsize
Tactic:
simp only [insertRatUnits]
Proof state after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
⊢ insertUnit_invariant f.assignments ⋯ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst ⋯
Theorem: LRAT.DefaultFormula.insertRatUnits_postcondition
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
⊢ insertUnit_invariant f.assignments ⋯ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst ⋯
Tactic:
have hsize : f.assignments.size = n := by rw [hf.2]
Proof state after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
⊢ insertUnit_invariant f.assignments ⋯ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst ⋯
Theorem: LRAT.DefaultFormula.insertRatUnits_postcondition
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
⊢ insertUnit_invariant f.assignments ⋯ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst ⋯
Tactic:
have h0 : insertUnit_invariant f.assignments hf.2 f.ratUnits f.assignments hsize := by
  intro i
  apply Or.inl
  simp only [Fin.getElem_fin, ne_eq, true_and, Bool.not_eq_true, exists_and_right]
  intro j
  simp only [hf.1, Array.size_toArray, List.length_nil] at j
  exact Fin.elim0 j
Proof state after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
h0 : insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments hsize
⊢ insertUnit_invariant f.assignments ⋯ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst ⋯
Theorem: LRAT.DefaultFormula.insertRatUnits_postcondition
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
h0 : insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments hsize
⊢ insertUnit_invariant f.assignments ⋯ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst ⋯
Tactic:
exact insertUnit_fold_preserves_invariant f.assignments hf.2 f.ratUnits f.assignments hsize false units h0
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_postcondition
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
⊢ f.assignments.size = n
Tactic:
rw [hf.2]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_postcondition
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
⊢ insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments hsize
Tactic:
intro i
Proof state after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
⊢ let assignments_i := f.assignments[↑i];
  let original_assignments_i := f.assignments[↑i];
  (assignments_i = original_assignments_i ∧ ∀ (j : Fin f.ratUnits.size), f.ratUnits[j].fst.val ≠ ↑i) ∨
    (∃ j b i_gt_zero,
        f.ratUnits[j] = (⟨↑i, ⋯⟩, b) ∧
          assignments_i = addAssignment b original_assignments_i ∧
            ¬hasAssignment b original_assignments_i = true ∧
              ∀ (k : Fin f.ratUnits.size), k ≠ j → f.ratUnits[k].fst.val ≠ ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        f.ratUnits[j1] = (⟨↑i, ⋯⟩, true) ∧
          f.ratUnits[j2] = (⟨↑i, ⋯⟩, false) ∧
            assignments_i = both ∧
              original_assignments_i = unassigned ∧
                ∀ (k : Fin f.ratUnits.size), k ≠ j1 → k ≠ j2 → f.ratUnits[k].fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.insertRatUnits_postcondition
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
⊢ let assignments_i := f.assignments[↑i];
  let original_assignments_i := f.assignments[↑i];
  (assignments_i = original_assignments_i ∧ ∀ (j : Fin f.ratUnits.size), f.ratUnits[j].fst.val ≠ ↑i) ∨
    (∃ j b i_gt_zero,
        f.ratUnits[j] = (⟨↑i, ⋯⟩, b) ∧
          assignments_i = addAssignment b original_assignments_i ∧
            ¬hasAssignment b original_assignments_i = true ∧
              ∀ (k : Fin f.ratUnits.size), k ≠ j → f.ratUnits[k].fst.val ≠ ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        f.ratUnits[j1] = (⟨↑i, ⋯⟩, true) ∧
          f.ratUnits[j2] = (⟨↑i, ⋯⟩, false) ∧
            assignments_i = both ∧
              original_assignments_i = unassigned ∧
                ∀ (k : Fin f.ratUnits.size), k ≠ j1 → k ≠ j2 → f.ratUnits[k].fst.val ≠ ↑i
Tactic:
apply Or.inl
Proof state after:
case h
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
⊢ f.assignments[↑i] = f.assignments[↑i] ∧ ∀ (j : Fin f.ratUnits.size), f.ratUnits[j].fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.insertRatUnits_postcondition
Proof state before:
case h
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
⊢ f.assignments[↑i] = f.assignments[↑i] ∧ ∀ (j : Fin f.ratUnits.size), f.ratUnits[j].fst.val ≠ ↑i
Tactic:
simp only [Fin.getElem_fin, ne_eq, true_and, Bool.not_eq_true, exists_and_right]
Proof state after:
case h
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
⊢ ∀ (j : Fin f.ratUnits.size), ¬f.ratUnits[↑j].fst.val = ↑i
Theorem: LRAT.DefaultFormula.insertRatUnits_postcondition
Proof state before:
case h
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
⊢ ∀ (j : Fin f.ratUnits.size), ¬f.ratUnits[↑j].fst.val = ↑i
Tactic:
intro j
Proof state after:
case h
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
i : Fin n
j : Fin f.ratUnits.size
⊢ ¬f.ratUnits[↑j].fst.val = ↑i