internlm/Lean-Github huggingface dataset:
Theorem: List.sizeOf_filter_lt_of_ne
Proof state before:
case cons
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : ¬filter f tail✝ = tail✝ → sizeOf (filter f tail✝) < sizeOf tail✝
h :
  ¬(match f head✝ with
      | true => head✝ :: filter f tail✝
      | false => filter f tail✝) =
      head✝ :: tail✝
⊢ sizeOf
      (match f head✝ with
      | true => head✝ :: filter f tail✝
      | false => filter f tail✝) <
    1 + sizeOf head✝ + sizeOf tail✝
Tactic:
next hd tl ih =>
split
next hHd =>
  simp [hHd] at h
  simp [_sizeOf_1]
  apply Nat.add_lt_add_left
  apply ih
  assumption
next hHd =>
  clear h hHd
  apply Nat.lt_of_le_of_lt (sizeOf_filter _ _)
  rw [Nat.add_comm, Nat.add_comm 1, Nat.add_one, Nat.add_succ]
  apply Nat.succ_le_succ
  apply Nat.le_add_right
Proof state after:
no goals
Theorem: List.sizeOf_filter_lt_of_ne
Proof state before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
⊢ sizeOf
      (match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) <
    1 + sizeOf hd + sizeOf tl
Tactic:
split
Proof state after:
case h_1
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
x✝ : Bool
heq✝ : f hd = true
⊢ sizeOf (hd :: filter f tl) < 1 + sizeOf hd + sizeOf tl

case h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
x✝ : Bool
heq✝ : f hd = false
⊢ sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl
Theorem: List.sizeOf_filter_lt_of_ne
Proof state before:
case h_1
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
x✝ : Bool
heq✝ : f hd = true
⊢ sizeOf (hd :: filter f tl) < 1 + sizeOf hd + sizeOf tl

case h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
x✝ : Bool
heq✝ : f hd = false
⊢ sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl
Tactic:
next hHd =>
  simp [hHd] at h
  simp [_sizeOf_1]
  apply Nat.add_lt_add_left
  apply ih
  assumption
Proof state after:
case h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
x✝ : Bool
heq✝ : f hd = false
⊢ sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl
Theorem: List.sizeOf_filter_lt_of_ne
Proof state before:
case h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
x✝ : Bool
heq✝ : f hd = false
⊢ sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl
Tactic:
next hHd =>
  clear h hHd
  apply Nat.lt_of_le_of_lt (sizeOf_filter _ _)
  rw [Nat.add_comm, Nat.add_comm 1, Nat.add_one, Nat.add_succ]
  apply Nat.succ_le_succ
  apply Nat.le_add_right
Proof state after:
no goals
Theorem: List.sizeOf_filter_lt_of_ne
Proof state before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
x✝ : Bool
hHd : f hd = true
⊢ sizeOf (hd :: filter f tl) < 1 + sizeOf hd + sizeOf tl
Tactic:
simp [hHd] at h
Proof state after:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
hHd : f hd = true
h : ¬filter f tl = tl
⊢ sizeOf (hd :: filter f tl) < 1 + sizeOf hd + sizeOf tl
Theorem: List.sizeOf_filter_lt_of_ne
Proof state before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
hHd : f hd = true
h : ¬filter f tl = tl
⊢ sizeOf (hd :: filter f tl) < 1 + sizeOf hd + sizeOf tl
Tactic:
simp [_sizeOf_1]
Proof state after:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
hHd : f hd = true
h : ¬filter f tl = tl
⊢ 1 + sizeOf hd + sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl
Theorem: List.sizeOf_filter_lt_of_ne
Proof state before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
hHd : f hd = true
h : ¬filter f tl = tl
⊢ 1 + sizeOf hd + sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl
Tactic:
apply Nat.add_lt_add_left
Proof state after:
case h
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
hHd : f hd = true
h : ¬filter f tl = tl
⊢ sizeOf (filter f tl) < sizeOf tl
Theorem: List.sizeOf_filter_lt_of_ne
Proof state before:
case h
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
hHd : f hd = true
h : ¬filter f tl = tl
⊢ sizeOf (filter f tl) < sizeOf tl
Tactic:
apply ih
Proof state after:
case h
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
hHd : f hd = true
h : ¬filter f tl = tl
⊢ ¬filter f tl = tl
Theorem: List.sizeOf_filter_lt_of_ne
Proof state before:
case h
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
hHd : f hd = true
h : ¬filter f tl = tl
⊢ ¬filter f tl = tl
Tactic:
assumption
Proof state after:
no goals
Theorem: List.sizeOf_filter_lt_of_ne
Proof state before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
x✝ : Bool
hHd : f hd = false
⊢ sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl
Tactic:
clear h hHd
Proof state after:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
⊢ sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl
Theorem: List.sizeOf_filter_lt_of_ne
Proof state before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
⊢ sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl
Tactic:
apply Nat.lt_of_le_of_lt (sizeOf_filter _ _)
Proof state after:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
⊢ sizeOf tl < 1 + sizeOf hd + sizeOf tl
Theorem: List.sizeOf_filter_lt_of_ne
Proof state before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
⊢ sizeOf tl < 1 + sizeOf hd + sizeOf tl
Tactic:
rw [Nat.add_comm, Nat.add_comm 1, Nat.add_one, Nat.add_succ]
Proof state after:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
⊢ sizeOf tl < Nat.succ (sizeOf tl + sizeOf hd)
Theorem: List.sizeOf_filter_lt_of_ne
Proof state before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
⊢ sizeOf tl < Nat.succ (sizeOf tl + sizeOf hd)
Tactic:
apply Nat.succ_le_succ
Proof state after:
case a
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
⊢ sizeOf tl ≤ sizeOf tl + sizeOf hd
Theorem: List.sizeOf_filter_lt_of_ne
Proof state before:
case a
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
⊢ sizeOf tl ≤ sizeOf tl + sizeOf hd
Tactic:
apply Nat.le_add_right
Proof state after:
no goals
Theorem: List.find?_map
Proof state before:
β : Type u_1
α : Type u_2
p : β → Bool
f : α → β
L : List α
⊢ find? p (map f L) = Option.map f (find? (p ∘ f) L)
Tactic:
induction L <;> simp [find?]
Proof state after:
case cons
β : Type u_1
α : Type u_2
p : β → Bool
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : find? p (map f tail✝) = Option.map f (find? (p ∘ f) tail✝)
⊢ (match p (f head✝) with
    | true => some (f head✝)
    | false => find? p (map f tail✝)) =
    Option.map f
      (match p (f head✝) with
      | true => some head✝
      | false => find? (p ∘ f) tail✝)
Theorem: List.find?_map
Proof state before:
case cons
β : Type u_1
α : Type u_2
p : β → Bool
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : find? p (map f tail✝) = Option.map f (find? (p ∘ f) tail✝)
⊢ (match p (f head✝) with
    | true => some (f head✝)
    | false => find? p (map f tail✝)) =
    Option.map f
      (match p (f head✝) with
      | true => some head✝
      | false => find? (p ∘ f) tail✝)
Tactic:
split <;> simp [*]
Proof state after:
no goals
Theorem: Std.AssocList.toList_ofList
Proof state before:
α : Type u_1
β : Type u_2
L : List (α × β)
⊢ toList (ofList L) = L
Tactic:
induction L <;> simp [*]
Proof state after:
no goals
Theorem: Array.ofFn_data
Proof state before:
n : Nat
α : Type u_1
f : Fin n → α
⊢ (ofFn f).data = List.map f (List.fins n)
Tactic:
ext i x
Proof state after:
case a.a
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ x ∈ List.get? (ofFn f).data i ↔ x ∈ List.get? (List.map f (List.fins n)) i
Theorem: Array.ofFn_data
Proof state before:
case a.a
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ x ∈ List.get? (ofFn f).data i ↔ x ∈ List.get? (List.map f (List.fins n)) i
Tactic:
simp [List.get?_eq_some]
Proof state after:
case a.a
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ h, List.get (ofFn f).data { val := i, isLt := h } = x) ↔ ∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x
Theorem: Array.ofFn_data
Proof state before:
case a.a
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ h, List.get (ofFn f).data { val := i, isLt := h } = x) ↔ ∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x
Tactic:
simp only [← Array.getElem_eq_data_get, Array.getElem_ofFn]
Proof state after:
case a.a
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ h, f { val := i, isLt := ⋯ } = x) ↔ ∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x
Theorem: Array.ofFn_data
Proof state before:
case a.a
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ h, f { val := i, isLt := ⋯ } = x) ↔ ∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x
Tactic:
refine ⟨?mp,?mpr⟩
Proof state after:
case mp
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ h, f { val := i, isLt := ⋯ } = x) → ∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x

case mpr
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x) → ∃ h, f { val := i, isLt := ⋯ } = x
Theorem: Array.ofFn_data
Proof state before:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ h, f { val := i, isLt := ⋯ } = x) → ∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x
Tactic:
case mp =>
  rintro ⟨h,rfl⟩
  refine ⟨_,?_,rfl⟩
  simpa using h
Proof state after:
no goals
Theorem: Array.ofFn_data
Proof state before:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x) → ∃ h, f { val := i, isLt := ⋯ } = x
Tactic:
case mpr =>
  rintro ⟨_,⟨h,rfl⟩,rfl⟩
  simpa using h
Proof state after:
no goals
Theorem: Array.ofFn_data
Proof state before:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ h, f { val := i, isLt := ⋯ } = x) → ∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x
Tactic:
rintro ⟨h,rfl⟩
Proof state after:
case intro
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < size (ofFn f)
⊢ ∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = f { val := i, isLt := ⋯ }
Theorem: Array.ofFn_data
Proof state before:
case intro
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < size (ofFn f)
⊢ ∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = f { val := i, isLt := ⋯ }
Tactic:
refine ⟨_,?_,rfl⟩
Proof state after:
case intro
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < size (ofFn f)
⊢ ∃ h_1, { val := i, isLt := ⋯ } = { val := i, isLt := ⋯ }
Theorem: Array.ofFn_data
Proof state before:
case intro
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < size (ofFn f)
⊢ ∃ h_1, { val := i, isLt := ⋯ } = { val := i, isLt := ⋯ }
Tactic:
simpa using h
Proof state after:
no goals
Theorem: Array.ofFn_data
Proof state before:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x) → ∃ h, f { val := i, isLt := ⋯ } = x
Tactic:
rintro ⟨_,⟨h,rfl⟩,rfl⟩
Proof state after:
case intro.intro.intro
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < List.length (List.fins n)
⊢ ∃ h_1, f { val := i, isLt := ⋯ } = f { val := i, isLt := ⋯ }
Theorem: Array.ofFn_data
Proof state before:
case intro.intro.intro
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < List.length (List.fins n)
⊢ ∃ h_1, f { val := i, isLt := ⋯ } = f { val := i, isLt := ⋯ }
Tactic:
simpa using h
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.encodesProp_equisatisfiable
Proof state before:
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
⊢ (∃ τ, τ ⊨ P) ↔ ∃ τ, τ ⊨ Cnf.toPropFun (toICnf e)
Tactic:
simp [toICnf, run, StateT.run]
Proof state after:
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
⊢ (∃ τ, P τ) ↔
    ∃ τ, τ ⊨ Cnf.toPropFun (↑e (LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv))).2.cnf
Theorem: LeanSAT.Encode.EncCNF.encodesProp_equisatisfiable
Proof state before:
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
⊢ (∃ τ, P τ) ↔
    ∃ τ, τ ⊨ Cnf.toPropFun (↑e (LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv))).2.cnf
Tactic:
generalize hls : LawfulState.new' _ _ = ls
Proof state after:
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun (↑e ls).2.cnf
Theorem: LeanSAT.Encode.EncCNF.encodesProp_equisatisfiable
Proof state before:
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun (↑e ls).2.cnf
Tactic:
have := h ls
Proof state after:
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
this :
  let s' := (↑e ls).2;
  s'.vMap = ls.vMap ∧
    s'.assumeVars = ls.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun (↑e ls).2.cnf
Theorem: LeanSAT.Encode.EncCNF.encodesProp_equisatisfiable
Proof state before:
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
this :
  let s' := (↑e ls).2;
  s'.vMap = ls.vMap ∧
    s'.assumeVars = ls.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun (↑e ls).2.cnf
Tactic:
generalize hls' : e.1 ls = ls' at this
Proof state after:
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
ls' : Id (α × LawfulState ν)
hls' : ↑e ls = ls'
this :
  let s' := ls'.2;
  s'.vMap = ls.vMap ∧
    s'.assumeVars = ls.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.2.cnf
Theorem: LeanSAT.Encode.EncCNF.encodesProp_equisatisfiable
Proof state before:
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
ls' : Id (α × LawfulState ν)
hls' : ↑e ls = ls'
this :
  let s' := ls'.2;
  s'.vMap = ls.vMap ∧
    s'.assumeVars = ls.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.2.cnf
Tactic:
rcases ls' with ⟨a,ls'⟩
Proof state after:
case mk
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
this :
  let s' := (a, ls').2;
  s'.vMap = ls.vMap ∧
    s'.assumeVars = ls.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun (a, ls').2.cnf
Theorem: LeanSAT.Encode.EncCNF.encodesProp_equisatisfiable
Proof state before:
case mk
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
this :
  let s' := (a, ls').2;
  s'.vMap = ls.vMap ∧
    s'.assumeVars = ls.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun (a, ls').2.cnf
Tactic:
simp only at this ⊢
Proof state after:
case mk
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
this :
  ls'.vMap = ls.vMap ∧
    ls'.assumeVars = ls.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp ls' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf
Theorem: LeanSAT.Encode.EncCNF.encodesProp_equisatisfiable
Proof state before:
case mk
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
this :
  ls'.vMap = ls.vMap ∧
    ls'.assumeVars = ls.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp ls' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf
Tactic:
rcases this with ⟨-,-,h3⟩
Proof state after:
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
h3 :
  ∀ (τ : PropAssignment ν),
    LawfulState.interp ls' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf
Theorem: LeanSAT.Encode.EncCNF.encodesProp_equisatisfiable
Proof state before:
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
h3 :
  ∀ (τ : PropAssignment ν),
    LawfulState.interp ls' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf
Tactic:
rw [←hls] at h3
Proof state after:
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
h3 :
  ∀ (τ : PropAssignment ν),
    LawfulState.interp ls' τ ↔
      LawfulState.interp (LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv)) τ ∧
        τ ⊨
          (fun τ =>
                τ ⊨
                  Clause.toPropFun
                    (LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv)).assumeVars)ᶜ ⇨
            P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf
Theorem: LeanSAT.Encode.EncCNF.encodesProp_equisatisfiable
Proof state before:
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
h3 :
  ∀ (τ : PropAssignment ν),
    LawfulState.interp ls' τ ↔
      LawfulState.interp (LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv)) τ ∧
        τ ⊨
          (fun τ =>
                τ ⊨
                  Clause.toPropFun
                    (LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv)).assumeVars)ᶜ ⇨
            P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf
Tactic:
simp [LawfulState.new', State.new, Clause.toPropFun] at h3
Proof state after:
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
h3 : ∀ (τ : PropAssignment ν), LawfulState.interp ls' τ ↔ P τ
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf
Theorem: LeanSAT.Encode.EncCNF.encodesProp_equisatisfiable
Proof state before:
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
h3 : ∀ (τ : PropAssignment ν), LawfulState.interp ls' τ ↔ P τ
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf
Tactic:
clear hls' hls
Proof state after:
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
a : α
ls' : LawfulState ν
h3 : ∀ (τ : PropAssignment ν), LawfulState.interp ls' τ ↔ P τ
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf