internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.a.mpr.intro.intro.refl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ ∃ σ,
    PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ' =
        PropAssignment.map (State.withTemps.vMap s.toState) σ ∧
      σ ⊨ Cnf.toPropFun s.cnf
Tactic:
simp [PropAssignment.map] at h2 ⊢
Proof state after:
case h.a.mpr.intro.intro.refl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ ∃ σ, σ' ∘ State.withTemps.vMap s.toState = σ ∘ State.withTemps.vMap s.toState ∧ σ ⊨ Cnf.toPropFun s.cnf
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ σ' ∘ State.withTemps.vMap s.toState =
      PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState ∧
    PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ⊨
      Cnf.toPropFun s.cnf
Tactic:
constructor
Proof state after:
case h.left
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ σ' ∘ State.withTemps.vMap s.toState =
    PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
      State.withTemps.vMap s.toState

case h.right
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ⊨
    Cnf.toPropFun s.cnf
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.left
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ σ' ∘ State.withTemps.vMap s.toState =
    PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
      State.withTemps.vMap s.toState
Tactic:
ext vot
Proof state after:
case h.left.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
vot : ν ⊕ Fin n
⊢ (σ' ∘ State.withTemps.vMap s.toState) vot =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      vot
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.left.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
vot : ν ⊕ Fin n
⊢ (σ' ∘ State.withTemps.vMap s.toState) vot =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      vot
Tactic:
rcases vot with (v|t)
Proof state after:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ (σ' ∘ State.withTemps.vMap s.toState) (Sum.inl v) =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      (Sum.inl v)

case h.left.h.inr
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
t : Fin n
⊢ (σ' ∘ State.withTemps.vMap s.toState) (Sum.inr t) =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      (Sum.inr t)
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ (σ' ∘ State.withTemps.vMap s.toState) (Sum.inl v) =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      (Sum.inl v)
Tactic:
have := congrFun h1 v
Proof state after:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
this :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') v =
    PropAssignment.map s.vMap σ v
⊢ (σ' ∘ State.withTemps.vMap s.toState) (Sum.inl v) =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      (Sum.inl v)
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
this :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') v =
    PropAssignment.map s.vMap σ v
⊢ (σ' ∘ State.withTemps.vMap s.toState) (Sum.inl v) =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      (Sum.inl v)
Tactic:
simp at this
Proof state after:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
this : σ' (State.withTemps.vMap s.toState (Sum.inl v)) = σ (s.vMap v)
⊢ (σ' ∘ State.withTemps.vMap s.toState) (Sum.inl v) =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      (Sum.inl v)
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
this : σ' (State.withTemps.vMap s.toState (Sum.inl v)) = σ (s.vMap v)
⊢ (σ' ∘ State.withTemps.vMap s.toState) (Sum.inl v) =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      (Sum.inl v)
Tactic:
simp [this]
Proof state after:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
this : σ' (State.withTemps.vMap s.toState (Sum.inl v)) = σ (s.vMap v)
⊢ σ (s.vMap v) =
    PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ'
      (State.withTemps.vMap s.toState (Sum.inl v))
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
this : σ' (State.withTemps.vMap s.toState (Sum.inl v)) = σ (s.vMap v)
⊢ σ (s.vMap v) =
    PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ'
      (State.withTemps.vMap s.toState (Sum.inl v))
Tactic:
clear this h2
Proof state after:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ σ (s.vMap v) =
    PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ'
      (State.withTemps.vMap s.toState (Sum.inl v))
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ σ (s.vMap v) =
    PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ'
      (State.withTemps.vMap s.toState (Sum.inl v))
Tactic:
simp [withTemps, State.withTemps, State.withTemps.vMap]
Proof state after:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ σ (s.vMap v) =
    PropAssignment.setMany σ (Finset.image (fun x => { val := ↑s.nextVar + ↑x, property := ⋯ }) Finset.univ) σ'
      (s.vMap v)
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ σ (s.vMap v) =
    PropAssignment.setMany σ (Finset.image (fun x => { val := ↑s.nextVar + ↑x, property := ⋯ }) Finset.univ) σ'
      (s.vMap v)
Tactic:
rw [PropAssignment.setMany_not_mem]
Proof state after:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ s.vMap v ∉ Finset.image (fun x => { val := ↑s.nextVar + ↑x, property := ⋯ }) Finset.univ
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ s.vMap v ∉ Finset.image (fun x => { val := ↑s.nextVar + ↑x, property := ⋯ }) Finset.univ
Tactic:
simp
Proof state after:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ ∀ (x : Fin n), ¬{ val := ↑s.nextVar + ↑x, property := ⋯ } = s.vMap v
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ ∀ (x : Fin n), ¬{ val := ↑s.nextVar + ↑x, property := ⋯ } = s.vMap v
Tactic:
intro x
Proof state after:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
⊢ ¬{ val := ↑s.nextVar + ↑x, property := ⋯ } = s.vMap v
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
⊢ ¬{ val := ↑s.nextVar + ↑x, property := ⋯ } = s.vMap v
Tactic:
have := s.vMapLt v
Proof state after:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : s.vMap v < s.nextVar
⊢ ¬{ val := ↑s.nextVar + ↑x, property := ⋯ } = s.vMap v
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : s.vMap v < s.nextVar
⊢ ¬{ val := ↑s.nextVar + ↑x, property := ⋯ } = s.vMap v
Tactic:
rw [←Subtype.val_inj]
Proof state after:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : s.vMap v < s.nextVar
⊢ ¬↑{ val := ↑s.nextVar + ↑x, property := ⋯ } = ↑(s.vMap v)
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : s.vMap v < s.nextVar
⊢ ¬↑{ val := ↑s.nextVar + ↑x, property := ⋯ } = ↑(s.vMap v)
Tactic:
rw [← PNat.coe_lt_coe] at this
Proof state after:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : ↑(s.vMap v) < ↑s.nextVar
⊢ ¬↑{ val := ↑s.nextVar + ↑x, property := ⋯ } = ↑(s.vMap v)
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : ↑(s.vMap v) < ↑s.nextVar
⊢ ¬↑{ val := ↑s.nextVar + ↑x, property := ⋯ } = ↑(s.vMap v)
Tactic:
simp
Proof state after:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : ↑(s.vMap v) < ↑s.nextVar
⊢ ¬↑s.nextVar + ↑x = ↑(s.vMap v)
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : ↑(s.vMap v) < ↑s.nextVar
⊢ ¬↑s.nextVar + ↑x = ↑(s.vMap v)
Tactic:
apply Nat.ne_of_gt
Proof state after:
case h.left.h.inl.h.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : ↑(s.vMap v) < ↑s.nextVar
⊢ ↑(s.vMap v) < ↑s.nextVar + ↑x
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.left.h.inl.h.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : ↑(s.vMap v) < ↑s.nextVar
⊢ ↑(s.vMap v) < ↑s.nextVar + ↑x
Tactic:
exact Nat.lt_add_right _ this
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.left.h.inr
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
t : Fin n
⊢ (σ' ∘ State.withTemps.vMap s.toState) (Sum.inr t) =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      (Sum.inr t)
Tactic:
simp [State.withTemps.vMap]
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.right
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ⊨
    Cnf.toPropFun s.cnf
Tactic:
apply (Model.PropFun.agreeOn_semVars _).mpr h2
Proof state after:
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ PropAssignment.agreeOn (↑(PropFun.semVars (Cnf.toPropFun s.cnf)))
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ') σ
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ PropAssignment.agreeOn (↑(PropFun.semVars (Cnf.toPropFun s.cnf)))
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ') σ
Tactic:
intro v hv
Proof state after:
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ ↑(PropFun.semVars (Cnf.toPropFun s.cnf))
⊢ PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' v = σ v
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ ↑(PropFun.semVars (Cnf.toPropFun s.cnf))
⊢ PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' v = σ v
Tactic:
simp at hv
Proof state after:
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
⊢ PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' v = σ v
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
⊢ PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' v = σ v
Tactic:
have := semVars_toPropFun_cnf_lt _ _ hv
Proof state after:
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
⊢ PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' v = σ v
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
⊢ PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' v = σ v
Tactic:
rw [PropAssignment.setMany_not_mem]
Proof state after:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
⊢ v ∉ Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ