Theorem: CNF.unsat_relabelFin (LeanSAT/Reflect/CNF/Decidable.lean)

State before:
g : CNF Nat
⊢ g.relabelFin.unsat ↔ g.unsat
Tactic:
dsimp [relabelFin]
State after:
g : CNF Nat
⊢ (if h : ∃ a, mem a g then relabel (fun i => if w : i < g.numLiterals then ⟨i, w⟩ else ⟨0, ⋯⟩) g
      else List.replicate (List.length g) []).unsat ↔
    g.unsat

State before:
g : CNF Nat
⊢ (if h : ∃ a, mem a g then relabel (fun i => if w : i < g.numLiterals then ⟨i, w⟩ else ⟨0, ⋯⟩) g
      else List.replicate (List.length g) []).unsat ↔
    g.unsat
Tactic:
split <;> rename_i h
State after:
case isTrue
g : CNF Nat
h : ∃ a, mem a g
⊢ (relabel (fun i => if w : i < g.numLiterals then ⟨i, w⟩ else ⟨0, ⋯⟩) g).unsat ↔ g.unsat

case isFalse
g : CNF Nat
h : ¬∃ a, mem a g
⊢ unsat (List.replicate (List.length g) []) ↔ g.unsat

State before:
case isTrue
g : CNF Nat
h : ∃ a, mem a g
⊢ (relabel (fun i => if w : i < g.numLiterals then ⟨i, w⟩ else ⟨0, ⋯⟩) g).unsat ↔ g.unsat
Tactic:
apply unsat_relabel_iff
State after:
case isTrue.w
g : CNF Nat
h : ∃ a, mem a g
⊢ ∀ {a b : Nat},
    mem a g →
      mem b g →
        ((if w : a < g.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < g.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b

State before:
case isTrue.w
g : CNF Nat
h : ∃ a, mem a g
⊢ ∀ {a b : Nat},
    mem a g →
      mem b g →
        ((if w : a < g.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < g.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b
Tactic:
intro a b ma mb
State after:
case isTrue.w
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
ma : mem a g
mb : mem b g
⊢ ((if w : a < g.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < g.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b

State before:
case isTrue.w
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
ma : mem a g
mb : mem b g
⊢ ((if w : a < g.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < g.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b
Tactic:
replace ma := lt_numLiterals ma
State after:
case isTrue.w
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
mb : mem b g
ma : a < g.numLiterals
⊢ ((if w : a < g.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < g.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b

State before:
case isTrue.w
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
mb : mem b g
ma : a < g.numLiterals
⊢ ((if w : a < g.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < g.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b
Tactic:
replace mb := lt_numLiterals mb
State after:
case isTrue.w
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
ma : a < g.numLiterals
mb : b < g.numLiterals
⊢ ((if w : a < g.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < g.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b

State before:
case isTrue.w
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
ma : a < g.numLiterals
mb : b < g.numLiterals
⊢ ((if w : a < g.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < g.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b
Tactic:
split <;> rename_i a_lt
State after:
case isTrue.w.isTrue
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
ma : a < g.numLiterals
mb : b < g.numLiterals
a_lt : a < g.numLiterals
⊢ ⟨a, a_lt⟩ = ⟨b, mb⟩ → a = b

case isTrue.w.isFalse
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
ma : a < g.numLiterals
mb : b < g.numLiterals
a_lt : ¬a < g.numLiterals
⊢ ⟨a, ma⟩ = ⟨b, mb⟩ → a = b

State before:
case isTrue.w.isTrue
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
ma : a < g.numLiterals
mb : b < g.numLiterals
a_lt : a < g.numLiterals
⊢ ⟨a, a_lt⟩ = ⟨b, mb⟩ → a = b
Tactic:
simp
State after:
no goals

State before:
case isTrue.w.isFalse
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
ma : a < g.numLiterals
mb : b < g.numLiterals
a_lt : ¬a < g.numLiterals
⊢ ⟨a, ma⟩ = ⟨b, mb⟩ → a = b
Tactic:
contradiction
State after:
no goals

State before:
case isFalse
g : CNF Nat
h : ¬∃ a, mem a g
⊢ unsat (List.replicate (List.length g) []) ↔ g.unsat
Tactic:
cases g with
| nil => simp
| cons c g =>
  simp only [not_mem_cons] at h
  obtain ⟨n, h⟩ := h
  cases n with
  | zero => simp at h
  | succ n =>
    simp_all
State after:
no goals

State before:
case isFalse.nil
h : ¬∃ a, mem a []
⊢ unsat (List.replicate [].length []) ↔ unsat []
Tactic:
simp
State after:
no goals

State before:
case isFalse.cons
c : Clause Nat
g : List (Clause Nat)
h : ¬∃ a, mem a (c :: g)
⊢ unsat (List.replicate (c :: g).length []) ↔ unsat (c :: g)
Tactic:
simp only [not_mem_cons] at h
State after:
case isFalse.cons
c : Clause Nat
g : List (Clause Nat)
h : ∃ n, c :: g = List.replicate n []
⊢ unsat (List.replicate (c :: g).length []) ↔ unsat (c :: g)

State before:
case isFalse.cons
c : Clause Nat
g : List (Clause Nat)
h : ∃ n, c :: g = List.replicate n []
⊢ unsat (List.replicate (c :: g).length []) ↔ unsat (c :: g)
Tactic:
obtain ⟨n, h⟩ := h
State after:
case isFalse.cons.intro
c : Clause Nat
g : List (Clause Nat)
n : Nat
h : c :: g = List.replicate n []
⊢ unsat (List.replicate (c :: g).length []) ↔ unsat (c :: g)

State before:
case isFalse.cons.intro
c : Clause Nat
g : List (Clause Nat)
n : Nat
h : c :: g = List.replicate n []
⊢ unsat (List.replicate (c :: g).length []) ↔ unsat (c :: g)
Tactic:
cases n with
| zero => simp at h
| succ n =>
  simp_all
State after:
no goals

State before:
case isFalse.cons.intro.zero
c : Clause Nat
g : List (Clause Nat)
h : c :: g = List.replicate 0 []
⊢ unsat (List.replicate (c :: g).length []) ↔ unsat (c :: g)
Tactic:
simp at h
State after:
no goals

State before:
case isFalse.cons.intro.succ
c : Clause Nat
g : List (Clause Nat)
n : Nat
h : c :: g = List.replicate (n + 1) []
⊢ unsat (List.replicate (c :: g).length []) ↔ unsat (c :: g)
Tactic:
simp_all
State after:
no goals