Theorem: CNF.Clause.convertLRAT_sat_of_sat (LeanSAT/Reflect/Glue.lean)

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
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

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
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

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]
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

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⟩⟩
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

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)
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

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
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

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
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

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
State after:
no goals

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]
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

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
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

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
State after:
no goals

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
State after:
no goals