internlm/Lean-Github huggingface dataset:
Theorem: CNF.Clause.mem_lrat_of_mem
Proof state before:
case cons.h_2.isFalse.isFalse.tail.a.h1
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ l ∈ tl

case cons.h_2.isFalse.isFalse.tail.a.h2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ LRAT.DefaultClause.ofArray (List.toArray tl) = some acc✝
Tactic:
assumption
Proof state after:
case cons.h_2.isFalse.isFalse.tail.a.h2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ LRAT.DefaultClause.ofArray (List.toArray tl) = some acc✝
Theorem: CNF.Clause.mem_lrat_of_mem
Proof state before:
case cons.h_2.isFalse.isFalse.tail.a.h2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ LRAT.DefaultClause.ofArray (List.toArray tl) = some acc✝
Tactic:
unfold LRAT.DefaultClause.ofArray
Proof state after:
case cons.h_2.isFalse.isFalse.tail.a.h2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ (let fold_fn := fun l acc =>
      match acc with
      | none => none
      | some acc => acc.insert l;
    Array.foldr fold_fn (some LRAT.DefaultClause.empty) (List.toArray tl) (List.toArray tl).size) =
    some acc✝
Theorem: CNF.Clause.mem_lrat_of_mem
Proof state before:
case cons.h_2.isFalse.isFalse.tail.a.h2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ (let fold_fn := fun l acc =>
      match acc with
      | none => none
      | some acc => acc.insert l;
    Array.foldr fold_fn (some LRAT.DefaultClause.empty) (List.toArray tl) (List.toArray tl).size) =
    some acc✝
Tactic:
rw [Array.foldr_eq_foldr_data,Array.toArray_data]
Proof state after:
case cons.h_2.isFalse.isFalse.tail.a.h2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) { data := tl }.data =
    some acc✝
Theorem: CNF.Clause.mem_lrat_of_mem
Proof state before:
case cons.h_2.isFalse.isFalse.tail.a.h2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) { data := tl }.data =
    some acc✝
Tactic:
exact heq
Proof state after:
no goals
Theorem: CNF.Clause.convertLRAT_sat_of_sat
Proof state before:
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
⊢ eval assign clause = true → assign ⊨ lratClause
Tactic:
intro h2
Proof state after:
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
h2 : eval assign clause = true
⊢ assign ⊨ lratClause
Theorem: CNF.Clause.convertLRAT_sat_of_sat
Proof state before:
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
h2 : eval assign clause = true
⊢ assign ⊨ lratClause
Tactic:
simp only [CNF.Clause.eval, List.any_eq_true, bne_iff_ne, ne_eq] at h2
Proof state after:
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
h2 : ∃ x, x ∈ clause ∧ (assign x.fst == x.snd) = true
⊢ assign ⊨ lratClause
Theorem: CNF.Clause.convertLRAT_sat_of_sat
Proof state before:
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
h2 : ∃ x, x ∈ clause ∧ (assign x.fst == x.snd) = true
⊢ assign ⊨ lratClause
Tactic:
simp only [HSat.eval, List.any_eq_true, decide_eq_true_eq]
Proof state after:
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
h2 : ∃ x, x ∈ clause ∧ (assign x.fst == x.snd) = true
⊢ ∃ x, x ∈ LRAT.Clause.toList lratClause ∧ assign x.fst = x.snd
Theorem: CNF.Clause.convertLRAT_sat_of_sat
Proof state before:
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
h2 : ∃ x, x ∈ clause ∧ (assign x.fst == x.snd) = true
⊢ ∃ x, x ∈ LRAT.Clause.toList lratClause ∧ assign x.fst = x.snd
Tactic:
rcases h2 with ⟨lit, ⟨hlit1, hlit2⟩⟩
Proof state after:
case intro.intro
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
lit : PosFin n × Bool
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ ∃ x, x ∈ LRAT.Clause.toList lratClause ∧ assign x.fst = x.snd
Theorem: CNF.Clause.convertLRAT_sat_of_sat
Proof state before:
case intro.intro
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
lit : PosFin n × Bool
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ ∃ x, x ∈ LRAT.Clause.toList lratClause ∧ assign x.fst = x.snd
Tactic:
apply Exists.intro (lit.fst, lit.snd)
Proof state after:
case intro.intro
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
lit : PosFin n × Bool
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ (lit.fst, lit.snd) ∈ LRAT.Clause.toList lratClause ∧ assign (lit.fst, lit.snd).fst = (lit.fst, lit.snd).snd
Theorem: CNF.Clause.convertLRAT_sat_of_sat
Proof state before:
case intro.intro
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
lit : PosFin n × Bool
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ (lit.fst, lit.snd) ∈ LRAT.Clause.toList lratClause ∧ assign (lit.fst, lit.snd).fst = (lit.fst, lit.snd).snd
Tactic:
constructor
Proof state after:
case intro.intro.left
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
lit : PosFin n × Bool
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ (lit.fst, lit.snd) ∈ LRAT.Clause.toList lratClause

case intro.intro.right
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
lit : PosFin n × Bool
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ assign (lit.fst, lit.snd).fst = (lit.fst, lit.snd).snd
Theorem: CNF.Clause.convertLRAT_sat_of_sat
Proof state before:
case intro.intro.left
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
lit : PosFin n × Bool
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ (lit.fst, lit.snd) ∈ LRAT.Clause.toList lratClause

case intro.intro.right
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
lit : PosFin n × Bool
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ assign (lit.fst, lit.snd).fst = (lit.fst, lit.snd).snd
Tactic:
. simp[LRAT.Clause.toList, LRAT.DefaultClause.toList]
  simp[CNF.Clause.convertLRAT'] at h
  exact CNF.Clause.mem_lrat_of_mem clause hlit1 h
Proof state after:
case intro.intro.right
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
lit : PosFin n × Bool
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ assign (lit.fst, lit.snd).fst = (lit.fst, lit.snd).snd
Theorem: CNF.Clause.convertLRAT_sat_of_sat
Proof state before:
case intro.intro.right
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
lit : PosFin n × Bool
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ assign (lit.fst, lit.snd).fst = (lit.fst, lit.snd).snd
Tactic:
. simp_all
Proof state after:
no goals
Theorem: CNF.Clause.convertLRAT_sat_of_sat
Proof state before:
case intro.intro.left
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
lit : PosFin n × Bool
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ (lit.fst, lit.snd) ∈ LRAT.Clause.toList lratClause
Tactic:
simp[LRAT.Clause.toList, LRAT.DefaultClause.toList]
Proof state after:
case intro.intro.left
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
lit : PosFin n × Bool
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ lit ∈ lratClause.clause
Theorem: CNF.Clause.convertLRAT_sat_of_sat
Proof state before:
case intro.intro.left
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
lit : PosFin n × Bool
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ lit ∈ lratClause.clause
Tactic:
simp[CNF.Clause.convertLRAT'] at h
Proof state after:
case intro.intro.left
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : LRAT.DefaultClause.ofArray (List.toArray clause) = some lratClause
lit : PosFin n × Bool
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ lit ∈ lratClause.clause
Theorem: CNF.Clause.convertLRAT_sat_of_sat
Proof state before:
case intro.intro.left
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : LRAT.DefaultClause.ofArray (List.toArray clause) = some lratClause
lit : PosFin n × Bool
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ lit ∈ lratClause.clause
Tactic:
exact CNF.Clause.mem_lrat_of_mem clause hlit1 h
Proof state after:
no goals
Theorem: CNF.Clause.convertLRAT_sat_of_sat
Proof state before:
case intro.intro.right
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
lit : PosFin n × Bool
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ assign (lit.fst, lit.snd).fst = (lit.fst, lit.snd).snd
Tactic:
simp_all
Proof state after:
no goals
Theorem: CNF.convertLRAT_readfyForRupAdd
Proof state before:
cnf : CNF Nat
⊢ cnf.convertLRAT.readyForRupAdd
Tactic:
unfold CNF.convertLRAT
Proof state after:
cnf : CNF Nat
⊢ (let lifted := cnf.lift;
    let lratCnf := lifted.convertLRAT';
    LRAT.DefaultFormula.ofArray (List.toArray (none :: lratCnf))).readyForRupAdd
Theorem: CNF.convertLRAT_readfyForRupAdd
Proof state before:
cnf : CNF Nat
⊢ (let lifted := cnf.lift;
    let lratCnf := lifted.convertLRAT';
    LRAT.DefaultFormula.ofArray (List.toArray (none :: lratCnf))).readyForRupAdd
Tactic:
apply LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof state after:
no goals
Theorem: CNF.convertLRAT_readfyForRatAdd
Proof state before:
cnf : CNF Nat
⊢ cnf.convertLRAT.readyForRatAdd
Tactic:
unfold CNF.convertLRAT
Proof state after:
cnf : CNF Nat
⊢ (let lifted := cnf.lift;
    let lratCnf := lifted.convertLRAT';
    LRAT.DefaultFormula.ofArray (List.toArray (none :: lratCnf))).readyForRatAdd
Theorem: CNF.convertLRAT_readfyForRatAdd
Proof state before:
cnf : CNF Nat
⊢ (let lifted := cnf.lift;
    let lratCnf := lifted.convertLRAT';
    LRAT.DefaultFormula.ofArray (List.toArray (none :: lratCnf))).readyForRatAdd
Tactic:
apply LRAT.DefaultFormula.ofArray_readyForRatAdd
Proof state after:
no goals
Theorem: LRAT.unsat_of_cons_none_unsat
Proof state before:
n : Nat
clauses : List (Option (DefaultClause n))
⊢ unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses))) →
    unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray clauses))
Tactic:
intro h assign hassign
Proof state after:
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : assign ⊨ DefaultFormula.ofArray (List.toArray clauses)
⊢ False
Theorem: LRAT.unsat_of_cons_none_unsat
Proof state before:
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : assign ⊨ DefaultFormula.ofArray (List.toArray clauses)
⊢ False
Tactic:
apply h assign
Proof state after:
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : assign ⊨ DefaultFormula.ofArray (List.toArray clauses)
⊢ assign ⊨ DefaultFormula.ofArray (List.toArray (none :: clauses))
Theorem: LRAT.unsat_of_cons_none_unsat
Proof state before:
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : assign ⊨ DefaultFormula.ofArray (List.toArray clauses)
⊢ assign ⊨ DefaultFormula.ofArray (List.toArray (none :: clauses))
Tactic:
simp only [LRAT.Formula.formulaHSat_def, List.all_eq_true, decide_eq_true_eq] at *
Proof state after:
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray (List.toArray clauses)) → assign ⊨ x
⊢ ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray (List.toArray (none :: clauses))) → assign ⊨ x
Theorem: LRAT.unsat_of_cons_none_unsat
Proof state before:
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray (List.toArray clauses)) → assign ⊨ x
⊢ ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray (List.toArray (none :: clauses))) → assign ⊨ x
Tactic:
intro clause hclause
Proof state after:
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray (List.toArray clauses)) → assign ⊨ x
clause : DefaultClause n
hclause : clause ∈ Formula.toList (DefaultFormula.ofArray (List.toArray (none :: clauses)))
⊢ assign ⊨ clause
Theorem: LRAT.unsat_of_cons_none_unsat
Proof state before:
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray (List.toArray clauses)) → assign ⊨ x
clause : DefaultClause n
hclause : clause ∈ Formula.toList (DefaultFormula.ofArray (List.toArray (none :: clauses)))
⊢ assign ⊨ clause
Tactic:
simp_all[LRAT.DefaultFormula.ofArray, LRAT.Formula.toList, LRAT.DefaultFormula.toList]
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastConst.go_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
idx : Nat
s : aig.RefStream idx
val : BitVec w
hidx : idx ≤ w
⊢ aig.decls.size ≤ (go aig idx s val hidx).aig.decls.size
Tactic:
unfold go
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
idx : Nat
s : aig.RefStream idx
val : BitVec w
hidx : idx ≤ w
⊢ aig.decls.size ≤
    (if hidx : idx < w then
            let res := aig.mkConstCached (val.getLsb idx);
            let aig_1 := res.aig;
            let bitRef := res.ref;
            let s := s.cast ⋯;
            let s := s.pushRef bitRef;
            go aig_1 (idx + 1) s val ⋯
          else
            let_fun hidx := ⋯;
            { aig := aig, stream := hidx ▸ s }).aig.decls.size
Theorem: BVExpr.bitblast.blastConst.go_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
idx : Nat
s : aig.RefStream idx
val : BitVec w
hidx : idx ≤ w
⊢ aig.decls.size ≤
    (if hidx : idx < w then
            let res := aig.mkConstCached (val.getLsb idx);
            let aig_1 := res.aig;
            let bitRef := res.ref;
            let s := s.cast ⋯;
            let s := s.pushRef bitRef;
            go aig_1 (idx + 1) s val ⋯
          else
            let_fun hidx := ⋯;
            { aig := aig, stream := hidx ▸ s }).aig.decls.size
Tactic:
split
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
idx : Nat
s : aig.RefStream idx
val : BitVec w
hidx : idx ≤ w
h✝ : idx < w
⊢ aig.decls.size ≤
    (let res := aig.mkConstCached (val.getLsb idx);
          let aig_1 := res.aig;
          let bitRef := res.ref;
          let s := s.cast ⋯;
          let s := s.pushRef bitRef;
          go aig_1 (idx + 1) s val ⋯).aig.decls.size

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
idx : Nat
s : aig.RefStream idx
val : BitVec w
hidx : idx ≤ w
h✝ : ¬idx < w
⊢ aig.decls.size ≤
    (let_fun hidx := ⋯;
          { aig := aig, stream := hidx ▸ s }).aig.decls.size
Theorem: BVExpr.bitblast.blastConst.go_le_size
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
idx : Nat
s : aig.RefStream idx
val : BitVec w
hidx : idx ≤ w
h✝ : idx < w
⊢ aig.decls.size ≤
    (let res := aig.mkConstCached (val.getLsb idx);
          let aig_1 := res.aig;
          let bitRef := res.ref;
          let s := s.cast ⋯;
          let s := s.pushRef bitRef;
          go aig_1 (idx + 1) s val ⋯).aig.decls.size

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
idx : Nat
s : aig.RefStream idx
val : BitVec w
hidx : idx ≤ w
h✝ : ¬idx < w
⊢ aig.decls.size ≤
    (let_fun hidx := ⋯;
          { aig := aig, stream := hidx ▸ s }).aig.decls.size
Tactic:
. dsimp
  refine Nat.le_trans ?_ (by apply go_le_size)
  apply AIG.LawfulOperator.le_size
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
idx : Nat
s : aig.RefStream idx
val : BitVec w
hidx : idx ≤ w
h✝ : ¬idx < w
⊢ aig.decls.size ≤
    (let_fun hidx := ⋯;
          { aig := aig, stream := hidx ▸ s }).aig.decls.size
Theorem: BVExpr.bitblast.blastConst.go_le_size
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
idx : Nat
s : aig.RefStream idx
val : BitVec w
hidx : idx ≤ w
h✝ : ¬idx < w
⊢ aig.decls.size ≤
    (let_fun hidx := ⋯;
          { aig := aig, stream := hidx ▸ s }).aig.decls.size
Tactic:
. simp
Proof state after:
no goals