-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/RelabelFin.lean
theorem unsat_relabelFin {f : CNF Nat} : Unsat f.relabelFin ↔ Unsat f

Proof state:
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 [List.replicate_succ]

Result:
no goals

Proof state:
case isFalse
f : CNF Nat
h : ¬∃ v, Mem v f
⊢ Unsat (List.replicate (List.length f) []) ↔ f.Unsat

Tactic:
cases f with
| nil => simp
| cons c g =>
  simp only [not_exists_mem] at h
  obtain ⟨n, h⟩ := h
  cases n with
  | zero => simp at h
  | succ n => simp_all [List.replicate_succ]

Result:
no goals

Proof state:
case isFalse.nil
h : ¬∃ v, Mem v []
⊢ Unsat (List.replicate [].length []) ↔ Unsat []

Tactic:
simp

Result:
no goals

Proof state:
case isTrue.hw
f : CNF Nat
h : ∃ v, Mem v f
a b : Nat
mb : Mem b f
ma : a < f.numLiterals
⊢ ((if w : a < f.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < f.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b

Tactic:
replace mb := lt_numLiterals mb

Result:
case isTrue.hw
f : CNF Nat
h : ∃ v, Mem v f
a b : Nat
ma : a < f.numLiterals
mb : b < f.numLiterals
⊢ ((if w : a < f.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < f.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b

Proof state:
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

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

Proof state:
case isTrue
f : CNF Nat
h : ∃ v, Mem v f
⊢ (relabel (fun i => if w : i < f.numLiterals then ⟨i, w⟩ else ⟨0, ⋯⟩) f).Unsat ↔ f.Unsat

Tactic:
apply unsat_relabel_iff

Result:
case isTrue.hw
f : CNF Nat
h : ∃ v, Mem v f
⊢ ∀ {v1 v2 : Nat},
    Mem v1 f →
      Mem v2 f →
        ((if w : v1 < f.numLiterals then ⟨v1, w⟩ else ⟨0, ⋯⟩) = if w : v2 < f.numLiterals then ⟨v2, w⟩ else ⟨0, ⋯⟩) →
          v1 = v2

Proof state:
f : CNF Nat
⊢ (if h : ∃ v, Mem v f then relabel (fun i => if w : i < f.numLiterals then ⟨i, w⟩ else ⟨0, ⋯⟩) f
      else List.replicate (List.length f) []).Unsat ↔
    f.Unsat

Tactic:
split <;> rename_i h

Result:
case isTrue
f : CNF Nat
h : ∃ v, Mem v f
⊢ (relabel (fun i => if w : i < f.numLiterals then ⟨i, w⟩ else ⟨0, ⋯⟩) f).Unsat ↔ f.Unsat

case isFalse
f : CNF Nat
h : ¬∃ v, Mem v f
⊢ Unsat (List.replicate (List.length f) []) ↔ f.Unsat

Proof state:
case isFalse.cons
c : Clause Nat
g : List (Clause Nat)
h : ¬∃ v, Mem v (c :: g)
⊢ Unsat (List.replicate (c :: g).length []) ↔ Unsat (c :: g)

Tactic:
simp only [not_exists_mem] at h

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

Proof state:
case isTrue.hw
f : CNF Nat
h : ∃ v, Mem v f
a b : Nat
ma : a < f.numLiterals
mb : b < f.numLiterals
⊢ ((if w : a < f.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < f.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b

Tactic:
split <;> rename_i a_lt

Result:
case isTrue.hw.isTrue
f : CNF Nat
h : ∃ v, Mem v f
a b : Nat
ma : a < f.numLiterals
mb : b < f.numLiterals
a_lt : a < f.numLiterals
⊢ ⟨a, a_lt⟩ = ⟨b, mb⟩ → a = b

case isTrue.hw.isFalse
f : CNF Nat
h : ∃ v, Mem v f
a b : Nat
ma : a < f.numLiterals
mb : b < f.numLiterals
a_lt : ¬a < f.numLiterals
⊢ ⟨a, ma⟩ = ⟨b, mb⟩ → a = b

Proof state:
case isTrue.hw
f : CNF Nat
h : ∃ v, Mem v f
⊢ ∀ {v1 v2 : Nat},
    Mem v1 f →
      Mem v2 f →
        ((if w : v1 < f.numLiterals then ⟨v1, w⟩ else ⟨0, ⋯⟩) = if w : v2 < f.numLiterals then ⟨v2, w⟩ else ⟨0, ⋯⟩) →
          v1 = v2

Tactic:
intro a b ma mb

Result:
case isTrue.hw
f : CNF Nat
h : ∃ v, Mem v f
a b : Nat
ma : Mem a f
mb : Mem b f
⊢ ((if w : a < f.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < f.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b

Proof state:
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

Result:
no goals

Proof state:
f : CNF Nat
⊢ f.relabelFin.Unsat ↔ f.Unsat

Tactic:
dsimp [relabelFin]

Result:
f : CNF Nat
⊢ (if h : ∃ v, Mem v f then relabel (fun i => if w : i < f.numLiterals then ⟨i, w⟩ else ⟨0, ⋯⟩) f
      else List.replicate (List.length f) []).Unsat ↔
    f.Unsat

Proof state:
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 [List.replicate_succ]

Result:
no goals

Proof state:
case isTrue.hw.isFalse
f : CNF Nat
h : ∃ v, Mem v f
a b : Nat
ma : a < f.numLiterals
mb : b < f.numLiterals
a_lt : ¬a < f.numLiterals
⊢ ⟨a, ma⟩ = ⟨b, mb⟩ → a = b

Tactic:
contradiction

Result:
no goals

Proof state:
case isTrue.hw
f : CNF Nat
h : ∃ v, Mem v f
a b : Nat
ma : Mem a f
mb : Mem b f
⊢ ((if w : a < f.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < f.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b

Tactic:
replace ma := lt_numLiterals ma

Result:
case isTrue.hw
f : CNF Nat
h : ∃ v, Mem v f
a b : Nat
mb : Mem b f
ma : a < f.numLiterals
⊢ ((if w : a < f.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < f.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b

Proof state:
case isTrue.hw.isTrue
f : CNF Nat
h : ∃ v, Mem v f
a b : Nat
ma : a < f.numLiterals
mb : b < f.numLiterals
a_lt : a < f.numLiterals
⊢ ⟨a, a_lt⟩ = ⟨b, mb⟩ → a = b

Tactic:
simp

Result:
no goals