[GOAL]
p : Prop
as ps as₁ : List Prop
⊢ as = List.reverseAux as₁ ps → implies (mk as) p ps (List.length as₁) → p
[PROOFSTEP]
induction ps generalizing as₁ with
| nil => exact fun _ ↦ id
| cons a as ih =>
  refine fun e H ↦ @ih (a :: as₁) e (H ?_)
  subst e; clear ih H
  suffices ∀ n n', n' = List.length as₁ + n → ∀ bs, mk (as₁.reverseAux bs) n' ↔ mk bs n from this 0 _ rfl (a :: as)
  induction as₁ with simp
  | cons b as₁ ih => exact fun n bs ↦ ih (n + 1) _ (Nat.succ_add ..) _
[GOAL]
p : Prop
as ps as₁ : List Prop
⊢ as = List.reverseAux as₁ ps → implies (mk as) p ps (List.length as₁) → p
[PROOFSTEP]
induction ps generalizing as₁ with
| nil => exact fun _ ↦ id
| cons a as ih =>
  refine fun e H ↦ @ih (a :: as₁) e (H ?_)
  subst e; clear ih H
  suffices ∀ n n', n' = List.length as₁ + n → ∀ bs, mk (as₁.reverseAux bs) n' ↔ mk bs n from this 0 _ rfl (a :: as)
  induction as₁ with simp
  | cons b as₁ ih => exact fun n bs ↦ ih (n + 1) _ (Nat.succ_add ..) _
[GOAL]
case nil
p : Prop
as as₁ : List Prop
⊢ as = List.reverseAux as₁ [] → implies (mk as) p [] (List.length as₁) → p
[PROOFSTEP]

| nil => exact fun _ ↦ id
[GOAL]
case nil
p : Prop
as as₁ : List Prop
⊢ as = List.reverseAux as₁ [] → implies (mk as) p [] (List.length as₁) → p
[PROOFSTEP]
exact fun _ ↦ id
[GOAL]
case cons
p : Prop
as✝ : List Prop
a : Prop
as : List Prop
ih : ∀ (as₁ : List Prop), as✝ = List.reverseAux as₁ as → implies (mk as✝) p as (List.length as₁) → p
as₁ : List Prop
⊢ as✝ = List.reverseAux as₁ (a :: as) → implies (mk as✝) p (a :: as) (List.length as₁) → p
[PROOFSTEP]

| cons a as ih =>
  refine fun e H ↦ @ih (a :: as₁) e (H ?_)
  subst e; clear ih H
  suffices ∀ n n', n' = List.length as₁ + n → ∀ bs, mk (as₁.reverseAux bs) n' ↔ mk bs n from this 0 _ rfl (a :: as)
  induction as₁ with simp
  | cons b as₁ ih => exact fun n bs ↦ ih (n + 1) _ (Nat.succ_add ..) _
[GOAL]
case cons
p : Prop
as✝ : List Prop
a : Prop
as : List Prop
ih : ∀ (as₁ : List Prop), as✝ = List.reverseAux as₁ as → implies (mk as✝) p as (List.length as₁) → p
as₁ : List Prop
⊢ as✝ = List.reverseAux as₁ (a :: as) → implies (mk as✝) p (a :: as) (List.length as₁) → p
[PROOFSTEP]
refine fun e H ↦ @ih (a :: as₁) e (H ?_)
[GOAL]
case cons
p : Prop
as✝ : List Prop
a : Prop
as : List Prop
ih : ∀ (as₁ : List Prop), as✝ = List.reverseAux as₁ as → implies (mk as✝) p as (List.length as₁) → p
as₁ : List Prop
e : as✝ = List.reverseAux as₁ (a :: as)
H : implies (mk as✝) p (a :: as) (List.length as₁)
⊢ mk as✝ (List.length as₁) ↔ a
[PROOFSTEP]
subst e
[GOAL]
case cons
p a : Prop
as as₁ : List Prop
ih :
  ∀ (as₁_1 : List Prop),
    List.reverseAux as₁ (a :: as) = List.reverseAux as₁_1 as →
      implies (mk (List.reverseAux as₁ (a :: as))) p as (List.length as₁_1) → p
H : implies (mk (List.reverseAux as₁ (a :: as))) p (a :: as) (List.length as₁)
⊢ mk (List.reverseAux as₁ (a :: as)) (List.length as₁) ↔ a
[PROOFSTEP]
clear ih H
[GOAL]
case cons
p a : Prop
as as₁ : List Prop
⊢ mk (List.reverseAux as₁ (a :: as)) (List.length as₁) ↔ a
[PROOFSTEP]
suffices ∀ n n', n' = List.length as₁ + n → ∀ bs, mk (as₁.reverseAux bs) n' ↔ mk bs n from this 0 _ rfl (a :: as)
[GOAL]
case cons
p a : Prop
as as₁ : List Prop
⊢ ∀ (n n' : ℕ), n' = List.length as₁ + n → ∀ (bs : List Prop), mk (List.reverseAux as₁ bs) n' ↔ mk bs n
[PROOFSTEP]
induction as₁ with simp
| cons b as₁ ih => exact fun n bs ↦ ih (n + 1) _ (Nat.succ_add ..) _
[GOAL]
case cons
p a : Prop
as as₁ : List Prop
⊢ ∀ (n n' : ℕ), n' = List.length as₁ + n → ∀ (bs : List Prop), mk (List.reverseAux as₁ bs) n' ↔ mk bs n
[PROOFSTEP]
induction as₁ with simp
| cons b as₁ ih => exact fun n bs ↦ ih (n + 1) _ (Nat.succ_add ..) _
[GOAL]
case cons.cons
p a : Prop
as : List Prop
b : Prop
as₁ : List Prop
ih : ∀ (n n' : ℕ), n' = List.length as₁ + n → ∀ (bs : List Prop), mk (List.reverseAux as₁ bs) n' ↔ mk bs n
⊢ ∀ (n n' : ℕ), n' = List.length (b :: as₁) + n → ∀ (bs : List Prop), mk (List.reverseAux (b :: as₁) bs) n' ↔ mk bs n
[PROOFSTEP]
simp
[GOAL]
case cons.cons
p a : Prop
as : List Prop
b : Prop
as₁ : List Prop
ih : ∀ (n n' : ℕ), n' = List.length as₁ + n → ∀ (bs : List Prop), mk (List.reverseAux as₁ bs) n' ↔ mk bs n
⊢ ∀ (n : ℕ) (bs : List Prop), mk (List.reverseAux as₁ (b :: bs)) (Nat.succ (List.length as₁) + n) ↔ mk bs n
[PROOFSTEP]

| cons b as₁ ih => exact fun n bs ↦ ih (n + 1) _ (Nat.succ_add ..) _
[GOAL]
case cons.cons
p a : Prop
as : List Prop
b : Prop
as₁ : List Prop
ih : ∀ (n n' : ℕ), n' = List.length as₁ + n → ∀ (bs : List Prop), mk (List.reverseAux as₁ bs) n' ↔ mk bs n
⊢ ∀ (n : ℕ) (bs : List Prop), mk (List.reverseAux as₁ (b :: bs)) (Nat.succ (List.length as₁) + n) ↔ mk bs n
[PROOFSTEP]
exact fun n bs ↦ ih (n + 1) _ (Nat.succ_add ..) _
[GOAL]
case cons.nil
p a : Prop
as : List Prop
⊢ ∀ (n n' : ℕ), n' = List.length [] + n → ∀ (bs : List Prop), mk (List.reverseAux [] bs) n' ↔ mk bs n
[PROOFSTEP]
simp
[GOAL]
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
⊢ reify v (and f₁ f₂) (a ∨ b)
[PROOFSTEP]
refine ⟨fun H ↦ by_contra fun hn ↦ H ⟨fun c h ↦ by_contra fun hn' ↦ ?_⟩⟩
[GOAL]
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬Valuation.satisfies_fmla v (and f₁ f₂)
hn : ¬(a ∨ b)
c : Clause
h : c ∈ and f₁ f₂
hn' : ¬Valuation.satisfies v c
⊢ False
[PROOFSTEP]
rcases List.mem_append.1 h with h | h
[GOAL]
case inl
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬Valuation.satisfies_fmla v (and f₁ f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ and f₁ f₂
hn' : ¬Valuation.satisfies v c
h : c ∈ f₁
⊢ False
[PROOFSTEP]
exact hn $ Or.inl $ h₁.1 fun Hc ↦ hn' $ Hc.1 _ h
[GOAL]
case inr
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬Valuation.satisfies_fmla v (and f₁ f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ and f₁ f₂
hn' : ¬Valuation.satisfies v c
h : c ∈ f₂
⊢ False
[PROOFSTEP]
exact hn $ Or.inr $ h₂.1 fun Hc ↦ hn' $ Hc.1 _ h
