Theorem: CNF.unsat_relabel_iff (LeanSAT/Reflect/CNF/Relabel.lean)

State before:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
⊢ (relabel f x).unsat ↔ x.unsat
Tactic:
rcases nonempty_or_impossible x with (⟨⟨a₀⟩⟩ | ⟨n, rfl⟩)
State after:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
⊢ (relabel f x).unsat ↔ x.unsat

case inr.intro
α β : Type
f : α → β
n : Nat
w : ∀ {a b : α}, mem a (List.replicate n []) → mem b (List.replicate n []) → f a = f b → a = b
⊢ (relabel f (List.replicate n [])).unsat ↔ unsat (List.replicate n [])

State before:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
⊢ (relabel f x).unsat ↔ x.unsat
Tactic:
refine ⟨fun h => ?_, unsat_relabel f⟩
State after:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
⊢ x.unsat

State before:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
⊢ x.unsat
Tactic:
have em := Classical.propDecidable
State after:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
⊢ x.unsat

State before:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
⊢ x.unsat
Tactic:
let g : β → α := fun b =>
  if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
State after:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
⊢ x.unsat

State before:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
⊢ x.unsat
Tactic:
have h' := unsat_relabel g h
State after:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
⊢ x.unsat

State before:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
⊢ x.unsat
Tactic:
suffices w : relabel g (relabel f x) = x by
  rwa [w] at h'
State after:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
⊢ relabel g (relabel f x) = x

State before:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
this : ∀ (a : α), mem a x → g (f a) = a
⊢ relabel g (relabel f x) = x
Tactic:
rw [relabel_relabel, relabel_congr, relabel_id]
State after:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
this : ∀ (a : α), mem a x → g (f a) = a
⊢ ∀ (a : α), mem a x → (g ∘ f) a = id a

State before:
case inl.intro
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
this : ∀ (a : α), mem a x → g (f a) = a
⊢ ∀ (a : α), mem a x → (g ∘ f) a = id a
Tactic:
exact this
State after:
no goals

State before:
α β : Type
x : CNF α
f : α → β
w✝ : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
w : relabel g (relabel f x) = x
⊢ x.unsat
Tactic:
rwa [w] at h'
State after:
no goals

State before:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
⊢ ∀ (a : α), mem a x → g (f a) = a
Tactic:
intro a h
State after:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ g (f a) = a

State before:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ g (f a) = a
Tactic:
dsimp [g]
State after:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ (if h : ∃ a_1, mem a_1 x ∧ f a_1 = f a then h.choose else a₀) = a

State before:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ (if h : ∃ a_1, mem a_1 x ∧ f a_1 = f a then h.choose else a₀) = a
Tactic:
rw [dif_pos ⟨a, h, rfl⟩]
State after:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ ⋯.choose = a

State before:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ ⋯.choose = a
Tactic:
apply w _ h
State after:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ f ⋯.choose = f a

α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ mem ⋯.choose x

State before:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ f ⋯.choose = f a
Tactic:
exact (Exists.choose_spec (⟨a, h, rfl⟩ : ∃ a', mem a' x ∧ f a' = f a)).2
State after:
no goals

State before:
α β : Type
x : CNF α
f : α → β
w : ∀ {a b : α}, mem a x → mem b x → f a = f b → a = b
a₀ : α
h✝ : (relabel f x).unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
h' : (relabel g (relabel f x)).unsat
a : α
h : mem a x
⊢ mem ⋯.choose x
Tactic:
exact (Exists.choose_spec (⟨a, h, rfl⟩ : ∃ a', mem a' x ∧ f a' = f a)).1
State after:
no goals

State before:
case inr.intro
α β : Type
f : α → β
n : Nat
w : ∀ {a b : α}, mem a (List.replicate n []) → mem b (List.replicate n []) → f a = f b → a = b
⊢ (relabel f (List.replicate n [])).unsat ↔ unsat (List.replicate n [])
Tactic:
cases n <;> simp [unsat, relabel, Clause.relabel]
State after:
no goals