internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.blastSignExtend_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧
Tactic:
rw [← hg]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ ⟦{ aig := { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty }.aig,
        ref :=
          { aig := aig,
                  stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty }.stream.getRef
            idx hidx },
      assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastSignExtend_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ ⟦{ aig := { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty }.aig,
        ref :=
          { aig := aig,
                  stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty }.stream.getRef
            idx hidx },
      assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧
Tactic:
dsimp
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ ⟦{ aig := aig, ref := (blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty).getRef idx hidx },
      assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastSignExtend_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ ⟦{ aig := aig, ref := (blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty).getRef idx hidx },
      assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧
Tactic:
rw [blastSignExtend.go_getRef]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ ⟦{ aig := aig,
        ref := if hidx2 : idx < target.w then target.stream.getRef idx ⋯ else target.stream.getRef (target.w - 1) ⋯ },
      assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ 0 ≤ idx
Theorem: BVExpr.bitblast.blastSignExtend_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ ⟦{ aig := aig,
        ref := if hidx2 : idx < target.w then target.stream.getRef idx ⋯ else target.stream.getRef (target.w - 1) ⋯ },
      assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ 0 ≤ idx
Tactic:
. split <;> simp only
Proof state after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ 0 ≤ idx
Theorem: BVExpr.bitblast.blastSignExtend_eq_eval_getLsb
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ 0 ≤ idx
Tactic:
. omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastSignExtend_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
hg :
  (if hw : target.w = 0 then blastZeroExtend aig { w := target.w, stream := target.stream }
    else { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty }) =
    res
⊢ ¬target.w = 0
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastSignExtend_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ ⟦{ aig := aig,
        ref := if hidx2 : idx < target.w then target.stream.getRef idx ⋯ else target.stream.getRef (target.w - 1) ⋯ },
      assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧
Tactic:
split <;> simp only
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastSignExtend_eq_eval_getLsb
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
this : ¬target.w = 0
hg : { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty } = res
⊢ 0 ≤ idx
Tactic:
omega
Proof state after:
no goals
Theorem: AIGStress.t1
Proof state before:
x : Bool
x✝ : x = true
⊢ (x && x) = true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: AIGStress.t2
Proof state before:
x : Bool
x✝ : x = true
⊢ (x && x && (x && x)) = true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: AIGStress.t3
Proof state before:
x : Bool
x✝ : x = true
⊢ (x && x && (x && x) && (x && x && (x && x))) = true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: AIGStress.t4
Proof state before:
x : Bool
x✝ : x = true
⊢ (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) = true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: AIGStress.t5
Proof state before:
x : Bool
x✝ : x = true
⊢ (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
      (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))))) =
    true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: AIGStress.t6
Proof state before:
x : Bool
x✝ : x = true
⊢ (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
        (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
      (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
        (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))))) =
    true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: AIGStress.t7
Proof state before:
x : Bool
x✝ : x = true
⊢ (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
          (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
        (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
          (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))))) &&
      (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
          (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
        (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
          (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))))))) =
    true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: AIGStress.t8
Proof state before:
x : Bool
x✝ : x = true
⊢ (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
            (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
          (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
            (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))))) &&
        (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
            (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
          (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
            (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))))) &&
      (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
            (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
          (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
            (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))))) &&
        (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
            (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
          (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
            (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))))))) =
    true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AddSub_1164
Proof state before:
⊢ ∀ (a b : BitVec 64), 0 - a + b = b - a
Tactic:
intros
Proof state after:
a✝ b✝ : BitVec 64
⊢ 0 - a✝ + b✝ = b✝ - a✝
Theorem: bitvec_AddSub_1164
Proof state before:
a✝ b✝ : BitVec 64
⊢ 0 - a✝ + b✝ = b✝ - a✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: LRAT.Literal.sat_iff
Proof state before:
α : Type u_1
p : α → Bool
a : α
b : Bool
⊢ p ⊨ (a, b) ↔ p a = b
Tactic:
simp only [HSat.eval]
Proof state after:
no goals
Theorem: LRAT.Literal.sat_negate_iff_not_sat
Proof state before:
α : Type u_1
p : α → Bool
l : Literal α
⊢ p ⊨ l.negateLiteral ↔ ¬(p ⊨ l)
Tactic:
simp only [negateLiteral, sat_iff]
Proof state after:
α : Type u_1
p : α → Bool
l : Literal α
⊢ p l.fst = !l.snd ↔ ¬(p ⊨ l)
Theorem: LRAT.Literal.sat_negate_iff_not_sat
Proof state before:
α : Type u_1
p : α → Bool
l : Literal α
⊢ p l.fst = !l.snd ↔ ¬(p ⊨ l)
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
p : α → Bool
l : Literal α
⊢ p l.fst = !l.snd → ¬(p ⊨ l)

case mpr
α : Type u_1
p : α → Bool
l : Literal α
⊢ ¬(p ⊨ l) → p l.fst = !l.snd
Theorem: LRAT.Literal.sat_negate_iff_not_sat
Proof state before:
case mp
α : Type u_1
p : α → Bool
l : Literal α
⊢ p l.fst = !l.snd → ¬(p ⊨ l)

case mpr
α : Type u_1
p : α → Bool
l : Literal α
⊢ ¬(p ⊨ l) → p l.fst = !l.snd
Tactic:
. intro h pl
  rw [sat_iff, h, not] at pl
  split at pl <;> simp_all
Proof state after:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
⊢ ¬(p ⊨ l) → p l.fst = !l.snd
Theorem: LRAT.Literal.sat_negate_iff_not_sat
Proof state before:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
⊢ ¬(p ⊨ l) → p l.fst = !l.snd
Tactic:
. intro h
  rw [sat_iff] at h
  rw [not]
  split <;> simp_all
Proof state after:
no goals
Theorem: LRAT.Literal.sat_negate_iff_not_sat
Proof state before:
case mp
α : Type u_1
p : α → Bool
l : Literal α
⊢ p l.fst = !l.snd → ¬(p ⊨ l)
Tactic:
intro h pl
Proof state after:
case mp
α : Type u_1
p : α → Bool
l : Literal α
h : p l.fst = !l.snd
pl : p ⊨ l
⊢ False
Theorem: LRAT.Literal.sat_negate_iff_not_sat
Proof state before:
case mp
α : Type u_1
p : α → Bool
l : Literal α
h : p l.fst = !l.snd
pl : p ⊨ l
⊢ False
Tactic:
rw [sat_iff, h, not] at pl
Proof state after:
case mp
α : Type u_1
p : α → Bool
l : Literal α
h : p l.fst = !l.snd
pl :
  (match l.snd with
    | true => false
    | false => true) =
    l.snd
⊢ False
Theorem: LRAT.Literal.sat_negate_iff_not_sat
Proof state before:
case mp
α : Type u_1
p : α → Bool
l : Literal α
h : p l.fst = !l.snd
pl :
  (match l.snd with
    | true => false
    | false => true) =
    l.snd
⊢ False
Tactic:
split at pl <;> simp_all
Proof state after:
no goals
Theorem: LRAT.Literal.sat_negate_iff_not_sat
Proof state before:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
⊢ ¬(p ⊨ l) → p l.fst = !l.snd
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
h : ¬(p ⊨ l)
⊢ p l.fst = !l.snd
Theorem: LRAT.Literal.sat_negate_iff_not_sat
Proof state before:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
h : ¬(p ⊨ l)
⊢ p l.fst = !l.snd
Tactic:
rw [sat_iff] at h
Proof state after:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
h : ¬p l.fst = l.snd
⊢ p l.fst = !l.snd
Theorem: LRAT.Literal.sat_negate_iff_not_sat
Proof state before:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
h : ¬p l.fst = l.snd
⊢ p l.fst = !l.snd
Tactic:
rw [not]
Proof state after:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
h : ¬p l.fst = l.snd
⊢ p l.fst =
    match l.snd with
    | true => false
    | false => true
Theorem: LRAT.Literal.sat_negate_iff_not_sat
Proof state before:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
h : ¬p l.fst = l.snd
⊢ p l.fst =
    match l.snd with
    | true => false
    | false => true
Tactic:
split <;> simp_all
Proof state after:
no goals
Theorem: LRAT.Literal.unsat_of_limplies_complement
Proof state before:
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
⊢ limplies α x l → limplies α x l.negateLiteral → unsatisfiable α x
Tactic:
intro h1 h2 p px
Proof state after:
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
h1 : limplies α x l
h2 : limplies α x l.negateLiteral
p : α → Bool
px : p ⊨ x
⊢ False
Theorem: LRAT.Literal.unsat_of_limplies_complement
Proof state before:
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
h1 : limplies α x l
h2 : limplies α x l.negateLiteral
p : α → Bool
px : p ⊨ x
⊢ False
Tactic:
specialize h1 p px
Proof state after:
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
h2 : limplies α x l.negateLiteral
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
⊢ False
Theorem: LRAT.Literal.unsat_of_limplies_complement
Proof state before:
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
h2 : limplies α x l.negateLiteral
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
⊢ False
Tactic:
specialize h2 p px
Proof state after:
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
h2 : p ⊨ l.negateLiteral
⊢ False
Theorem: LRAT.Literal.unsat_of_limplies_complement
Proof state before:
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
h2 : p ⊨ l.negateLiteral
⊢ False
Tactic:
rw [sat_negate_iff_not_sat] at h2
Proof state after:
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
h2 : ¬(p ⊨ l)
⊢ False
Theorem: LRAT.Literal.unsat_of_limplies_complement
Proof state before:
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
h2 : ¬(p ⊨ l)
⊢ False
Tactic:
exact h2 h1
Proof state after:
no goals
Theorem: LRAT.Clause.sat_iff_exists
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Clause α β
p : α → Bool
c : β
⊢ ((toList c).any fun l => decide (p l.fst = l.snd)) = true ↔ ∃ l, l ∈ toList c ∧ p l.fst = l.snd
Tactic:
simp only [List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool]
Proof state after:
no goals
Theorem: LRAT.Clause.limplies_iff_mem
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ limplies α l c ↔ l ∈ toList c
Tactic:
simp only [limplies, sat_iff_exists, Prod.exists, Bool.exists_bool]
Proof state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ (∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))) ↔
    l ∈ toList c
Theorem: LRAT.Clause.limplies_iff_mem
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ (∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))) ↔
    l ∈ toList c
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ (∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))) →
    l ∈ toList c

case mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ l ∈ toList c →
    ∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
Theorem: LRAT.Clause.limplies_iff_mem
Proof state before:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ l ∈ toList c →
    ∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
Tactic:
. intro h p pl
  apply Exists.intro l.1
  by_cases hl : l.2
  . apply Or.inr
    rw [← hl]
    exact ⟨h, pl⟩
  . apply Or.inl
    simp only [Bool.not_eq_true] at hl
    rw [← hl]
    exact ⟨h, pl⟩
Proof state after:
no goals
Theorem: LRAT.Clause.limplies_iff_mem
Proof state before:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ (∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))) →
    l ∈ toList c
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : ∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
⊢ l ∈ toList c
Theorem: LRAT.Clause.limplies_iff_mem
Proof state before:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : ∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
⊢ l ∈ toList c
Tactic:
let p := fun x : α => if x = l.1 then l.2 else (x, false) ∈ toList c
Proof state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : ∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
⊢ l ∈ toList c
Theorem: LRAT.Clause.limplies_iff_mem
Proof state before:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : ∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
⊢ l ∈ toList c
Tactic:
specialize h p pl
Proof state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
h : ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
⊢ l ∈ toList c
Theorem: LRAT.Clause.limplies_iff_mem
Proof state before:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
h : ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
⊢ l ∈ toList c
Tactic:
rcases h with ⟨v, ⟨h1, h2⟩ | ⟨h1, h2⟩⟩
Proof state after:
case mp.intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
h2 : p ⊨ (v, false)
⊢ l ∈ toList c

case mp.intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
h2 : p ⊨ (v, true)
⊢ l ∈ toList c