internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.eval_signExtend
Proof state before:
assign : Assignment
v a✝ : Nat
expr : BVExpr a✝
⊢ eval assign (signExtend v expr) = BitVec.signExtend v (eval assign expr)
Tactic:
rfl
Proof state after:
no goals
Theorem: BVBinPred.eval_eq
Proof state before:
w : Nat
⊢ eq.eval = fun x x_1 => x == x_1
Tactic:
rfl
Proof state after:
no goals
Theorem: BVBinPred.eval_ult
Proof state before:
w : Nat
⊢ ult.eval = BitVec.ult
Tactic:
rfl
Proof state after:
no goals
Theorem: BVPred.eval_bin
Proof state before:
assign : BVExpr.Assignment
a✝ : Nat
lhs : BVExpr a✝
op : BVBinPred
rhs : BVExpr a✝
⊢ eval assign (bin lhs op rhs) = op.eval (BVExpr.eval assign lhs) (BVExpr.eval assign rhs)
Tactic:
rfl
Proof state after:
no goals
Theorem: BVPred.eval_getLsb
Proof state before:
assign : BVExpr.Assignment
a✝ : Nat
expr : BVExpr a✝
idx : Nat
⊢ eval assign (getLsb expr idx) = (BVExpr.eval assign expr).getLsb idx
Tactic:
rfl
Proof state after:
no goals
Theorem: BVLogicalExpr.sat_and
Proof state before:
x y : BVLogicalExpr
assign : BVExpr.Assignment
hx : x.sat assign
hy : y.sat assign
⊢ sat (BoolExpr.gate Gate.and x y) assign
Tactic:
simp only [sat] at *
Proof state after:
x y : BVLogicalExpr
assign : BVExpr.Assignment
hx : eval assign x = true
hy : eval assign y = true
⊢ eval assign (BoolExpr.gate Gate.and x y) = true
Theorem: BVLogicalExpr.sat_and
Proof state before:
x y : BVLogicalExpr
assign : BVExpr.Assignment
hx : eval assign x = true
hy : eval assign y = true
⊢ eval assign (BoolExpr.gate Gate.and x y) = true
Tactic:
simp [hx, hy, Gate.eval]
Proof state after:
no goals
Theorem: bitvec_290__292
Proof state before:
⊢ ∀ (Y Op1 : BitVec 64), 1#64 <<< Y * Op1 = Op1 <<< Y
Tactic:
intros
Proof state after:
Y✝ Op1✝ : BitVec 64
⊢ 1#64 <<< Y✝ * Op1✝ = Op1✝ <<< Y✝
Theorem: bitvec_290__292
Proof state before:
Y✝ Op1✝ : BitVec 64
⊢ 1#64 <<< Y✝ * Op1✝ = Op1✝ <<< Y✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_InstCombineShift__458
Proof state before:
⊢ ∀ (Y X C : BitVec 31), (X.sshiftRight C.toNat - Y) <<< C = X - Y <<< C &&& (-1) <<< C
Tactic:
intros
Proof state after:
Y✝ X✝ C✝ : BitVec 31
⊢ (X✝.sshiftRight C✝.toNat - Y✝) <<< C✝ = X✝ - Y✝ <<< C✝ &&& (-1) <<< C✝
Theorem: bitvec_InstCombineShift__458
Proof state before:
Y✝ X✝ C✝ : BitVec 31
⊢ (X✝.sshiftRight C✝.toNat - Y✝) <<< C✝ = X✝ - Y✝ <<< C✝ &&& (-1) <<< C✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_709
Proof state before:
⊢ ∀ (a b d : BitVec 64), (a &&& b == b && a &&& d == d) = (a &&& (b ||| d) == b ||| d)
Tactic:
intros
Proof state after:
a✝ b✝ d✝ : BitVec 64
⊢ (a✝ &&& b✝ == b✝ && a✝ &&& d✝ == d✝) = (a✝ &&& (b✝ ||| d✝) == b✝ ||| d✝)
Theorem: bitvec_AndOrXor_709
Proof state before:
a✝ b✝ d✝ : BitVec 64
⊢ (a✝ &&& b✝ == b✝ && a✝ &&& d✝ == d✝) = (a✝ &&& (b✝ ||| d✝) == b✝ ||| d✝)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2265
Proof state before:
⊢ ∀ (A B : BitVec 64), A &&& B ||| A ^^^ B = A ||| B
Tactic:
intros
Proof state after:
A✝ B✝ : BitVec 64
⊢ A✝ &&& B✝ ||| A✝ ^^^ B✝ = A✝ ||| B✝
Theorem: bitvec_AndOrXor_2265
Proof state before:
A✝ B✝ : BitVec 64
⊢ A✝ &&& B✝ ||| A✝ ^^^ B✝ = A✝ ||| B✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.mem_of_necessary_assignment
Proof state before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p_entails_c : ∃ a, (a, false) ∈ Clause.toList c ∧ p a = false ∨ (a, true) ∈ Clause.toList c ∧ p a = true
p'_not_entails_c :
  ¬∃ a,
      (a, false) ∈ Clause.toList c ∧ (if a = l.fst then l.snd else p a) = false ∨
        (a, true) ∈ Clause.toList c ∧ (if a = l.fst then l.snd else p a) = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
simp only [not_exists, not_or, not_and] at p'_not_entails_c
Proof state after:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p_entails_c : ∃ a, (a, false) ∈ Clause.toList c ∧ p a = false ∨ (a, true) ∈ Clause.toList c ∧ p a = true
p'_not_entails_c :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = false) ∧
      ((x, true) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = true)
⊢ l.negateLiteral ∈ Clause.toList c
Theorem: LRAT.DefaultFormula.mem_of_necessary_assignment
Proof state before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p_entails_c : ∃ a, (a, false) ∈ Clause.toList c ∧ p a = false ∨ (a, true) ∈ Clause.toList c ∧ p a = true
p'_not_entails_c :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = false) ∧
      ((x, true) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = true)
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
rcases p_entails_c with ⟨v, ⟨v_in_c, pv⟩ | ⟨v_in_c, pv⟩⟩
Proof state after:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p'_not_entails_c :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = false) ∧
      ((x, true) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = true)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
⊢ l.negateLiteral ∈ Clause.toList c

case intro.inr.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p'_not_entails_c :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = false) ∧
      ((x, true) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = true)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
⊢ l.negateLiteral ∈ Clause.toList c
Theorem: LRAT.DefaultFormula.mem_of_necessary_assignment
Proof state before:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p'_not_entails_c :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = false) ∧
      ((x, true) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = true)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
specialize p'_not_entails_c v
Proof state after:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
⊢ l.negateLiteral ∈ Clause.toList c
Theorem: LRAT.DefaultFormula.mem_of_necessary_assignment
Proof state before:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
have h := p'_not_entails_c.1 v_in_c
Proof state after:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h : ¬(if v = l.fst then l.snd else p v) = false
⊢ l.negateLiteral ∈ Clause.toList c
Theorem: LRAT.DefaultFormula.mem_of_necessary_assignment
Proof state before:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h : ¬(if v = l.fst then l.snd else p v) = false
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
simp only [HSat.eval, Bool.not_eq_false] at h
Proof state after:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h : (if v = l.fst then l.snd else p v) = true
⊢ l.negateLiteral ∈ Clause.toList c
Theorem: LRAT.DefaultFormula.mem_of_necessary_assignment
Proof state before:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h : (if v = l.fst then l.snd else p v) = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
split at h
Proof state after:
case intro.inl.intro.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : v = l.fst
h : l.snd = true
⊢ l.negateLiteral ∈ Clause.toList c

case intro.inl.intro.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : ¬v = l.fst
h : p v = true
⊢ l.negateLiteral ∈ Clause.toList c
Theorem: LRAT.DefaultFormula.mem_of_necessary_assignment
Proof state before:
case intro.inl.intro.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : v = l.fst
h : l.snd = true
⊢ l.negateLiteral ∈ Clause.toList c

case intro.inl.intro.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : ¬v = l.fst
h : p v = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
. next heq => simp [negateLiteral, ← heq, h, v_in_c]
Proof state after:
case intro.inl.intro.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : ¬v = l.fst
h : p v = true
⊢ l.negateLiteral ∈ Clause.toList c
Theorem: LRAT.DefaultFormula.mem_of_necessary_assignment
Proof state before:
case intro.inl.intro.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : v = l.fst
h : l.snd = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
next heq => simp [negateLiteral, ← heq, h, v_in_c]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.mem_of_necessary_assignment
Proof state before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
heq : v = l.fst
h : l.snd = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
simp [negateLiteral, ← heq, h, v_in_c]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.mem_of_necessary_assignment
Proof state before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
hne : ¬v = l.fst
h : p v = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
exfalso
Proof state after:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
hne : ¬v = l.fst
h : p v = true
⊢ False
Theorem: LRAT.DefaultFormula.mem_of_necessary_assignment
Proof state before:
case intro.inr.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p'_not_entails_c :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = false) ∧
      ((x, true) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = true)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
specialize p'_not_entails_c v
Proof state after:
case intro.inr.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
⊢ l.negateLiteral ∈ Clause.toList c
Theorem: LRAT.DefaultFormula.mem_of_necessary_assignment
Proof state before:
case intro.inr.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
have h := p'_not_entails_c.2 v_in_c
Proof state after:
case intro.inr.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h : ¬(if v = l.fst then l.snd else p v) = true
⊢ l.negateLiteral ∈ Clause.toList c
Theorem: LRAT.DefaultFormula.mem_of_necessary_assignment
Proof state before:
case intro.inr.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h : ¬(if v = l.fst then l.snd else p v) = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
split at h
Proof state after:
case intro.inr.intro.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : v = l.fst
h : ¬l.snd = true
⊢ l.negateLiteral ∈ Clause.toList c

case intro.inr.intro.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : ¬v = l.fst
h : ¬p v = true
⊢ l.negateLiteral ∈ Clause.toList c
Theorem: LRAT.DefaultFormula.mem_of_necessary_assignment
Proof state before:
case intro.inr.intro.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : v = l.fst
h : ¬l.snd = true
⊢ l.negateLiteral ∈ Clause.toList c

case intro.inr.intro.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : ¬v = l.fst
h : ¬p v = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
. next heq => simp [negateLiteral, ← heq, h, v_in_c]
Proof state after:
case intro.inr.intro.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : ¬v = l.fst
h : ¬p v = true
⊢ l.negateLiteral ∈ Clause.toList c
Theorem: LRAT.DefaultFormula.mem_of_necessary_assignment
Proof state before:
case intro.inr.intro.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : v = l.fst
h : ¬l.snd = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
next heq => simp [negateLiteral, ← heq, h, v_in_c]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.mem_of_necessary_assignment
Proof state before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
heq : v = l.fst
h : ¬l.snd = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
simp [negateLiteral, ← heq, h, v_in_c]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.mem_of_necessary_assignment
Proof state before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
hne : ¬v = l.fst
h : ¬p v = true
⊢ l.negateLiteral ∈ Clause.toList c
Tactic:
exfalso
Proof state after:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
hne : ¬v = l.fst
h : ¬p v = true
⊢ False
Theorem: LRAT.DefaultFormula.entails_of_irrelevant_assignment
Proof state before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p_entails_cl :
  ∃ a,
    ((a, false) ≠ l.negateLiteral ∧ (a, false) ∈ c.toList) ∧ p a = false ∨
      ((a, true) ≠ l.negateLiteral ∧ (a, true) ∈ c.toList) ∧ p a = true
⊢ ∃ a,
    (a, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if a = l.fst then l.snd else p a) = false ∨
      (a, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if a = l.fst then l.snd else p a) = true
Tactic:
rcases p_entails_cl with ⟨v, ⟨⟨negl_ne_v, v_in_c_del_l⟩, pv⟩ | ⟨⟨negl_ne_v, v_in_c_del_l⟩, pv⟩⟩
  <;> [
      (apply Exists.intro v; apply Or.inl);
      (apply Exists.intro v; apply Or.inr)
    ]
Proof state after:
case intro.inl.intro.intro.h
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negateLiteral
v_in_c_del_l : (v, false) ∈ c.toList
⊢ (v, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = false

case intro.inr.intro.intro.h
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = true
Theorem: LRAT.DefaultFormula.entails_of_irrelevant_assignment
Proof state before:
case intro.inl.intro.intro.h
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negateLiteral
v_in_c_del_l : (v, false) ∈ c.toList
⊢ (v, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = false

case intro.inr.intro.intro.h
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = true
Tactic:
all_goals
  constructor
  . simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l]
  . split
    . next heq =>
      simp only [heq, negateLiteral, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
      split at negl_ne_v <;> simp_all
    . next hne =>
      exact pv
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.entails_of_irrelevant_assignment
Proof state before:
case intro.inl.intro.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negateLiteral
v_in_c_del_l : (v, false) ∈ c.toList
⊢ ∃ a,
    (a, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if a = l.fst then l.snd else p a) = false ∨
      (a, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if a = l.fst then l.snd else p a) = true
Tactic:
apply Exists.intro v
Proof state after:
case intro.inl.intro.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negateLiteral
v_in_c_del_l : (v, false) ∈ c.toList
⊢ (v, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = false ∨
    (v, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = true
Theorem: LRAT.DefaultFormula.entails_of_irrelevant_assignment
Proof state before:
case intro.inl.intro.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negateLiteral
v_in_c_del_l : (v, false) ∈ c.toList
⊢ (v, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = false ∨
    (v, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = true
Tactic:
apply Or.inl
Proof state after:
case intro.inl.intro.intro.h
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negateLiteral
v_in_c_del_l : (v, false) ∈ c.toList
⊢ (v, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = false