internlm/Lean-Github huggingface dataset:
Theorem: Smt.Reconstruct.Prop.deMorganSmall₂
Proof state before:
p q : Prop
h : ¬p ∧ ¬q
⊢ ¬(p ∨ q)
Tactic:
have ⟨np, nq⟩ := h
Proof state after:
p q : Prop
h : ¬p ∧ ¬q
np : ¬p
nq : ¬q
⊢ ¬(p ∨ q)
Theorem: Smt.Reconstruct.Prop.deMorganSmall₂
Proof state before:
p q : Prop
h : ¬p ∧ ¬q
np : ¬p
nq : ¬q
⊢ ¬(p ∨ q)
Tactic:
exact match Classical.em p, Classical.em q with
| Or.inl pp,  _   => False.elim (np pp)
| _        ,  Or.inl pq  => False.elim (nq pq)
| Or.inr npp, Or.inr npq => λ h₂ =>
                               match h₂ with
                               | Or.inl pp => False.elim (npp pp)
                               | Or.inr pq => False.elim (npq pq)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.deMorganSmall₃
Proof state before:
⊢ ∀ {p q : Prop}, ¬(p ∧ q) → ¬p ∨ ¬q
Tactic:
intros p q h
Proof state after:
p q : Prop
h : ¬(p ∧ q)
⊢ ¬p ∨ ¬q
Theorem: Smt.Reconstruct.Prop.deMorganSmall₃
Proof state before:
p q : Prop
h : ¬(p ∧ q)
⊢ ¬p ∨ ¬q
Tactic:
match Classical.em p, Classical.em q with
| Or.inl hp, Or.inl hq  => exact False.elim (h (And.intro hp hq))
| _,         Or.inr hnq => exact Or.inr hnq
| Or.inr hnp, _        => exact Or.inl hnp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.deMorganSmall₃
Proof state before:
p q : Prop
h : ¬(p ∧ q)
hp : p
hq : q
⊢ ¬p ∨ ¬q
Tactic:
exact False.elim (h (And.intro hp hq))
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.deMorganSmall₃
Proof state before:
p q : Prop
h : ¬(p ∧ q)
x✝ : p ∨ ¬p
hnq : ¬q
⊢ ¬p ∨ ¬q
Tactic:
exact Or.inr hnq
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.deMorganSmall₃
Proof state before:
p q : Prop
h : ¬(p ∧ q)
hnp : ¬p
x✝ : q ∨ ¬q
⊢ ¬p ∨ ¬q
Tactic:
exact Or.inl hnp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.notNotElim
Proof state before:
⊢ ∀ {p : Prop}, ¬¬p → p
Tactic:
intros p h
Proof state after:
p : Prop
h : ¬¬p
⊢ p
Theorem: Smt.Reconstruct.Prop.notNotElim
Proof state before:
p : Prop
h : ¬¬p
⊢ p
Tactic:
exact match Classical.em p with
| Or.inl pp => pp
| Or.inr np => False.elim (h (λ p => np p))
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.deMorgan
Proof state before:
⊢ ∀ {l : List Prop}, ¬orN (notList l) → andN l
Tactic:
intros l h
Proof state after:
l : List Prop
h : ¬orN (notList l)
⊢ andN l
Theorem: Smt.Reconstruct.Prop.deMorgan
Proof state before:
l : List Prop
h : ¬orN (notList l)
⊢ andN l
Tactic:
exact match l with
| []   => True.intro
| [t]  => by
  simp only [andN]
  simp only [notList, orN, map] at h
  cases Classical.em t with
  | inl tt  => exact tt
  | inr ntt => exact False.elim (h ntt)
| h₁::h₂::t => by
  simp only [orN, notList, map] at h
  have ⟨ t₁, t₂ ⟩ := deMorganSmall h
  have ih := @deMorgan (h₂::t) t₂
  simp [andN]
  have t₁' := notNotElim t₁
  exact ⟨ t₁', ih ⟩
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.deMorgan
Proof state before:
l : List Prop
t : Prop
h : ¬orN (notList [t])
⊢ andN [t]
Tactic:
simp only [andN]
Proof state after:
l : List Prop
t : Prop
h : ¬orN (notList [t])
⊢ t
Theorem: Smt.Reconstruct.Prop.deMorgan
Proof state before:
l : List Prop
t : Prop
h : ¬orN (notList [t])
⊢ t
Tactic:
simp only [notList, orN, map] at h
Proof state after:
l : List Prop
t : Prop
h : ¬¬t
⊢ t
Theorem: Smt.Reconstruct.Prop.deMorgan
Proof state before:
l : List Prop
t : Prop
h : ¬¬t
⊢ t
Tactic:
cases Classical.em t with
| inl tt  => exact tt
| inr ntt => exact False.elim (h ntt)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.deMorgan
Proof state before:
case inl
l : List Prop
t : Prop
h : ¬¬t
tt : t
⊢ t
Tactic:
exact tt
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.deMorgan
Proof state before:
case inr
l : List Prop
t : Prop
h : ¬¬t
ntt : ¬t
⊢ t
Tactic:
exact False.elim (h ntt)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.deMorgan
Proof state before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : ¬orN (notList (h₁ :: h₂ :: t))
⊢ andN (h₁ :: h₂ :: t)
Tactic:
simp only [orN, notList, map] at h
Proof state after:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : ¬(¬h₁ ∨ orN ((¬h₂) :: map Not t))
⊢ andN (h₁ :: h₂ :: t)
Theorem: Smt.Reconstruct.Prop.deMorgan
Proof state before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : ¬(¬h₁ ∨ orN ((¬h₂) :: map Not t))
⊢ andN (h₁ :: h₂ :: t)
Tactic:
have ⟨ t₁, t₂ ⟩ := deMorganSmall h
Proof state after:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : ¬(¬h₁ ∨ orN ((¬h₂) :: map Not t))
t₁ : ¬¬h₁
t₂ : ¬orN ((¬h₂) :: map Not t)
⊢ andN (h₁ :: h₂ :: t)
Theorem: Smt.Reconstruct.Prop.deMorgan
Proof state before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : ¬(¬h₁ ∨ orN ((¬h₂) :: map Not t))
t₁ : ¬¬h₁
t₂ : ¬orN ((¬h₂) :: map Not t)
⊢ andN (h₁ :: h₂ :: t)
Tactic:
have ih := @deMorgan (h₂::t) t₂
Proof state after:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : ¬(¬h₁ ∨ orN ((¬h₂) :: map Not t))
t₁ : ¬¬h₁
t₂ : ¬orN ((¬h₂) :: map Not t)
ih : andN (h₂ :: t)
⊢ andN (h₁ :: h₂ :: t)
Theorem: Smt.Reconstruct.Prop.deMorgan
Proof state before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : ¬(¬h₁ ∨ orN ((¬h₂) :: map Not t))
t₁ : ¬¬h₁
t₂ : ¬orN ((¬h₂) :: map Not t)
ih : andN (h₂ :: t)
⊢ andN (h₁ :: h₂ :: t)
Tactic:
simp [andN]
Proof state after:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : ¬(¬h₁ ∨ orN ((¬h₂) :: map Not t))
t₁ : ¬¬h₁
t₂ : ¬orN ((¬h₂) :: map Not t)
ih : andN (h₂ :: t)
⊢ h₁ ∧ andN (h₂ :: t)
Theorem: Smt.Reconstruct.Prop.deMorgan
Proof state before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : ¬(¬h₁ ∨ orN ((¬h₂) :: map Not t))
t₁ : ¬¬h₁
t₂ : ¬orN ((¬h₂) :: map Not t)
ih : andN (h₂ :: t)
⊢ h₁ ∧ andN (h₂ :: t)
Tactic:
have t₁' := notNotElim t₁
Proof state after:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : ¬(¬h₁ ∨ orN ((¬h₂) :: map Not t))
t₁ : ¬¬h₁
t₂ : ¬orN ((¬h₂) :: map Not t)
ih : andN (h₂ :: t)
t₁' : h₁
⊢ h₁ ∧ andN (h₂ :: t)
Theorem: Smt.Reconstruct.Prop.deMorgan
Proof state before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : ¬(¬h₁ ∨ orN ((¬h₂) :: map Not t))
t₁ : ¬¬h₁
t₂ : ¬orN ((¬h₂) :: map Not t)
ih : andN (h₂ :: t)
t₁' : h₁
⊢ h₁ ∧ andN (h₂ :: t)
Tactic:
exact ⟨ t₁', ih ⟩
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.deMorgan₂
Proof state before:
⊢ ∀ {l : List Prop}, andN l → ¬orN (notList l)
Tactic:
intros l h
Proof state after:
l : List Prop
h : andN l
⊢ ¬orN (notList l)
Theorem: Smt.Reconstruct.Prop.deMorgan₂
Proof state before:
l : List Prop
h : andN l
⊢ ¬orN (notList l)
Tactic:
exact match l with
| [] => by
  simp [orN, notList]
| [t] => by
  simp only [orN, notList]
  simp [andN] at h
  exact notNotIntro h
| h₁::h₂::t => by
  simp only [orN, notList, map]
  simp [andN] at h
  apply deMorganSmall₂
  have nnh₁ := notNotIntro (And.left h)
  have ih := @deMorgan₂ (h₂::t) (And.right h)
  exact ⟨nnh₁, ih⟩
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.deMorgan₂
Proof state before:
l : List Prop
h : andN []
⊢ ¬orN (notList [])
Tactic:
simp [orN, notList]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.deMorgan₂
Proof state before:
l : List Prop
t : Prop
h : andN [t]
⊢ ¬orN (notList [t])
Tactic:
simp only [orN, notList]
Proof state after:
l : List Prop
t : Prop
h : andN [t]
⊢ ¬¬t
Theorem: Smt.Reconstruct.Prop.deMorgan₂
Proof state before:
l : List Prop
t : Prop
h : andN [t]
⊢ ¬¬t
Tactic:
simp [andN] at h
Proof state after:
l : List Prop
t : Prop
h : t
⊢ ¬¬t
Theorem: Smt.Reconstruct.Prop.deMorgan₂
Proof state before:
l : List Prop
t : Prop
h : t
⊢ ¬¬t
Tactic:
exact notNotIntro h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.deMorgan₂
Proof state before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : andN (h₁ :: h₂ :: t)
⊢ ¬orN (notList (h₁ :: h₂ :: t))
Tactic:
simp only [orN, notList, map]
Proof state after:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : andN (h₁ :: h₂ :: t)
⊢ ¬(¬h₁ ∨ orN ((¬h₂) :: map Not t))
Theorem: Smt.Reconstruct.Prop.deMorgan₂
Proof state before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : andN (h₁ :: h₂ :: t)
⊢ ¬(¬h₁ ∨ orN ((¬h₂) :: map Not t))
Tactic:
simp [andN] at h
Proof state after:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∧ andN (h₂ :: t)
⊢ ¬(¬h₁ ∨ orN ((¬h₂) :: map Not t))
Theorem: Smt.Reconstruct.Prop.deMorgan₂
Proof state before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∧ andN (h₂ :: t)
⊢ ¬(¬h₁ ∨ orN ((¬h₂) :: map Not t))
Tactic:
apply deMorganSmall₂
Proof state after:
case a
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∧ andN (h₂ :: t)
⊢ ¬¬h₁ ∧ ¬orN ((¬h₂) :: map Not t)
Theorem: Smt.Reconstruct.Prop.deMorgan₂
Proof state before:
case a
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∧ andN (h₂ :: t)
⊢ ¬¬h₁ ∧ ¬orN ((¬h₂) :: map Not t)
Tactic:
have nnh₁ := notNotIntro (And.left h)
Proof state after:
case a
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∧ andN (h₂ :: t)
nnh₁ : ¬¬h₁
⊢ ¬¬h₁ ∧ ¬orN ((¬h₂) :: map Not t)
Theorem: Smt.Reconstruct.Prop.deMorgan₂
Proof state before:
case a
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∧ andN (h₂ :: t)
nnh₁ : ¬¬h₁
⊢ ¬¬h₁ ∧ ¬orN ((¬h₂) :: map Not t)
Tactic:
have ih := @deMorgan₂ (h₂::t) (And.right h)
Proof state after:
case a
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∧ andN (h₂ :: t)
nnh₁ : ¬¬h₁
ih : ¬orN (notList (h₂ :: t))
⊢ ¬¬h₁ ∧ ¬orN ((¬h₂) :: map Not t)
Theorem: Smt.Reconstruct.Prop.deMorgan₂
Proof state before:
case a
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∧ andN (h₂ :: t)
nnh₁ : ¬¬h₁
ih : ¬orN (notList (h₂ :: t))
⊢ ¬¬h₁ ∧ ¬orN ((¬h₂) :: map Not t)
Tactic:
exact ⟨nnh₁, ih⟩
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.deMorgan₃
Proof state before:
⊢ ∀ {l : List Prop}, ¬orN l → andN (notList l)
Tactic:
intros l h
Proof state after:
l : List Prop
h : ¬orN l
⊢ andN (notList l)
Theorem: Smt.Reconstruct.Prop.deMorgan₃
Proof state before:
l : List Prop
h : ¬orN l
⊢ andN (notList l)
Tactic:
exact match l with
| [] => True.intro
| [t] => by
  simp only [andN, notList, map]
  simp only [orN, Not] at h
  exact h
| h₁::h₂::t => by
  simp only [orN, Not] at h
  have ⟨t₁, t₂⟩ := deMorganSmall h
  simp only [orN, Not] at t₂
  simp [andN, notList, map]
  have ih := @deMorgan₃ (h₂::t) t₂
  exact ⟨t₁, ih⟩
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.deMorgan₃
Proof state before:
l : List Prop
t : Prop
h : ¬orN [t]
⊢ andN (notList [t])
Tactic:
simp only [andN, notList, map]
Proof state after:
l : List Prop
t : Prop
h : ¬orN [t]
⊢ ¬t
Theorem: Smt.Reconstruct.Prop.deMorgan₃
Proof state before:
l : List Prop
t : Prop
h : ¬orN [t]
⊢ ¬t
Tactic:
simp only [orN, Not] at h
Proof state after:
l : List Prop
t : Prop
h : t → False
⊢ ¬t
Theorem: Smt.Reconstruct.Prop.deMorgan₃
Proof state before:
l : List Prop
t : Prop
h : t → False
⊢ ¬t
Tactic:
exact h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.deMorgan₃
Proof state before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : ¬orN (h₁ :: h₂ :: t)
⊢ andN (notList (h₁ :: h₂ :: t))
Tactic:
simp only [orN, Not] at h
Proof state after:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∨ orN (h₂ :: t) → False
⊢ andN (notList (h₁ :: h₂ :: t))
Theorem: Smt.Reconstruct.Prop.deMorgan₃
Proof state before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∨ orN (h₂ :: t) → False
⊢ andN (notList (h₁ :: h₂ :: t))
Tactic:
have ⟨t₁, t₂⟩ := deMorganSmall h
Proof state after:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∨ orN (h₂ :: t) → False
t₁ : ¬h₁
t₂ : ¬orN (h₂ :: t)
⊢ andN (notList (h₁ :: h₂ :: t))
Theorem: Smt.Reconstruct.Prop.deMorgan₃
Proof state before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∨ orN (h₂ :: t) → False
t₁ : ¬h₁
t₂ : ¬orN (h₂ :: t)
⊢ andN (notList (h₁ :: h₂ :: t))
Tactic:
simp only [orN, Not] at t₂
Proof state after:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∨ orN (h₂ :: t) → False
t₁ : ¬h₁
t₂ : orN (h₂ :: t) → False
⊢ andN (notList (h₁ :: h₂ :: t))
Theorem: Smt.Reconstruct.Prop.deMorgan₃
Proof state before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∨ orN (h₂ :: t) → False
t₁ : ¬h₁
t₂ : orN (h₂ :: t) → False
⊢ andN (notList (h₁ :: h₂ :: t))
Tactic:
simp [andN, notList, map]
Proof state after:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∨ orN (h₂ :: t) → False
t₁ : ¬h₁
t₂ : orN (h₂ :: t) → False
⊢ ¬h₁ ∧ andN ((¬h₂) :: map Not t)
Theorem: Smt.Reconstruct.Prop.deMorgan₃
Proof state before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∨ orN (h₂ :: t) → False
t₁ : ¬h₁
t₂ : orN (h₂ :: t) → False
⊢ ¬h₁ ∧ andN ((¬h₂) :: map Not t)
Tactic:
have ih := @deMorgan₃ (h₂::t) t₂
Proof state after:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∨ orN (h₂ :: t) → False
t₁ : ¬h₁
t₂ : orN (h₂ :: t) → False
ih : andN (notList (h₂ :: t))
⊢ ¬h₁ ∧ andN ((¬h₂) :: map Not t)
Theorem: Smt.Reconstruct.Prop.deMorgan₃
Proof state before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∨ orN (h₂ :: t) → False
t₁ : ¬h₁
t₂ : orN (h₂ :: t) → False
ih : andN (notList (h₂ :: t))
⊢ ¬h₁ ∧ andN ((¬h₂) :: map Not t)
Tactic:
exact ⟨t₁, ih⟩
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfAndNeg'
Proof state before:
⊢ ∀ (l : List Prop), andN l ∨ orN (notList l)
Tactic:
intro l
Proof state after:
l : List Prop
⊢ andN l ∨ orN (notList l)
Theorem: Smt.Reconstruct.Prop.cnfAndNeg'
Proof state before:
l : List Prop
⊢ andN l ∨ orN (notList l)
Tactic:
apply orComm
Proof state after:
case a
l : List Prop
⊢ orN (notList l) ∨ andN l
Theorem: Smt.Reconstruct.Prop.cnfAndNeg'
Proof state before:
case a
l : List Prop
⊢ orN (notList l) ∨ andN l
Tactic:
apply orImplies
Proof state after:
case a.a
l : List Prop
⊢ ¬orN (notList l) → andN l
Theorem: Smt.Reconstruct.Prop.cnfAndNeg'
Proof state before:
case a.a
l : List Prop
⊢ ¬orN (notList l) → andN l
Tactic:
intro h
Proof state after:
case a.a
l : List Prop
h : ¬orN (notList l)
⊢ andN l
Theorem: Smt.Reconstruct.Prop.cnfAndNeg'
Proof state before:
case a.a
l : List Prop
h : ¬orN (notList l)
⊢ andN l
Tactic:
exact deMorgan h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfAndNeg
Proof state before:
l : List Prop
⊢ orN (andN l :: notList l)
Tactic:
cases l with
| nil => trivial
| cons l ls =>
  simp only [orN]
  apply cnfAndNeg'
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfAndNeg
Proof state before:
case nil

⊢ orN (andN [] :: notList [])
Tactic:
trivial
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfAndNeg
Proof state before:
case cons
l : Prop
ls : List Prop
⊢ orN (andN (l :: ls) :: notList (l :: ls))
Tactic:
simp only [orN]
Proof state after:
case cons
l : Prop
ls : List Prop
⊢ andN (l :: ls) ∨ orN ((¬l) :: map Not ls)
Theorem: Smt.Reconstruct.Prop.cnfAndNeg
Proof state before:
case cons
l : Prop
ls : List Prop
⊢ andN (l :: ls) ∨ orN ((¬l) :: map Not ls)
Tactic:
apply cnfAndNeg'
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfAndPos
Proof state before:
⊢ ∀ (l : List Prop) (i : Nat), ¬andN l ∨ l.getD i True
Tactic:
intros l i
Proof state after:
l : List Prop
i : Nat
⊢ ¬andN l ∨ l.getD i True
Theorem: Smt.Reconstruct.Prop.cnfAndPos
Proof state before:
l : List Prop
i : Nat
⊢ ¬andN l ∨ l.getD i True
Tactic:
apply orImplies
Proof state after:
case a
l : List Prop
i : Nat
⊢ ¬¬andN l → l.getD i True
Theorem: Smt.Reconstruct.Prop.cnfAndPos
Proof state before:
case a
l : List Prop
i : Nat
⊢ ¬¬andN l → l.getD i True
Tactic:
intro h
Proof state after:
case a
l : List Prop
i : Nat
h : ¬¬andN l
⊢ l.getD i True
Theorem: Smt.Reconstruct.Prop.cnfAndPos
Proof state before:
case a
l : List Prop
i : Nat
h : ¬¬andN l
⊢ l.getD i True
Tactic:
have h' := notNotElim h
Proof state after:
case a
l : List Prop
i : Nat
h : ¬¬andN l
h' : andN l
⊢ l.getD i True
Theorem: Smt.Reconstruct.Prop.cnfAndPos
Proof state before:
case a
l : List Prop
i : Nat
h : ¬¬andN l
h' : andN l
⊢ l.getD i True
Tactic:
match l with
| [] => exact True.intro
| [p] =>
  match i with
  | 0 => exact h'
  | _ + 1 => exact True.intro
| p₁::p₂::ps =>
  match i with
  | 0 => exact And.left h'
  | i' + 1 =>
    have IH :=  cnfAndPos (p₂::ps) i'
    exact orImplies₂ IH (And.right h')
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfAndPos
Proof state before:
l : List Prop
i : Nat
h : ¬¬andN []
h' : andN []
⊢ [].getD i True
Tactic:
exact True.intro
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfAndPos
Proof state before:
l : List Prop
i : Nat
p : Prop
h : ¬¬andN [p]
h' : andN [p]
⊢ [p].getD i True
Tactic:
match i with
| 0 => exact h'
| _ + 1 => exact True.intro
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfAndPos
Proof state before:
l : List Prop
i : Nat
p : Prop
h : ¬¬andN [p]
h' : andN [p]
⊢ [p].getD 0 True
Tactic:
exact h'
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfAndPos
Proof state before:
l : List Prop
i : Nat
p : Prop
h : ¬¬andN [p]
h' : andN [p]
n✝ : Nat
⊢ [p].getD (n✝ + 1) True
Tactic:
exact True.intro
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfAndPos
Proof state before:
l : List Prop
i : Nat
p₁ p₂ : Prop
ps : List Prop
h : ¬¬andN (p₁ :: p₂ :: ps)
h' : andN (p₁ :: p₂ :: ps)
⊢ (p₁ :: p₂ :: ps).getD i True
Tactic:
match i with
| 0 => exact And.left h'
| i' + 1 =>
  have IH :=  cnfAndPos (p₂::ps) i'
  exact orImplies₂ IH (And.right h')
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfAndPos
Proof state before:
l : List Prop
i : Nat
p₁ p₂ : Prop
ps : List Prop
h : ¬¬andN (p₁ :: p₂ :: ps)
h' : andN (p₁ :: p₂ :: ps)
⊢ (p₁ :: p₂ :: ps).getD 0 True
Tactic:
exact And.left h'
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfAndPos
Proof state before:
l : List Prop
i : Nat
p₁ p₂ : Prop
ps : List Prop
h : ¬¬andN (p₁ :: p₂ :: ps)
h' : andN (p₁ :: p₂ :: ps)
i' : Nat
⊢ (p₁ :: p₂ :: ps).getD (i' + 1) True
Tactic:
have IH :=  cnfAndPos (p₂::ps) i'
Proof state after:
l : List Prop
i : Nat
p₁ p₂ : Prop
ps : List Prop
h : ¬¬andN (p₁ :: p₂ :: ps)
h' : andN (p₁ :: p₂ :: ps)
i' : Nat
IH : ¬andN (p₂ :: ps) ∨ (p₂ :: ps).getD i' True
⊢ (p₁ :: p₂ :: ps).getD (i' + 1) True
Theorem: Smt.Reconstruct.Prop.cnfAndPos
Proof state before:
l : List Prop
i : Nat
p₁ p₂ : Prop
ps : List Prop
h : ¬¬andN (p₁ :: p₂ :: ps)
h' : andN (p₁ :: p₂ :: ps)
i' : Nat
IH : ¬andN (p₂ :: ps) ∨ (p₂ :: ps).getD i' True
⊢ (p₁ :: p₂ :: ps).getD (i' + 1) True
Tactic:
exact orImplies₂ IH (And.right h')
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfOrNeg
Proof state before:
⊢ ∀ (l : List Prop) (i : Nat), orN l ∨ ¬l.getD i False
Tactic:
intros l i
Proof state after:
l : List Prop
i : Nat
⊢ orN l ∨ ¬l.getD i False
Theorem: Smt.Reconstruct.Prop.cnfOrNeg
Proof state before:
l : List Prop
i : Nat
⊢ orN l ∨ ¬l.getD i False
Tactic:
apply orImplies
Proof state after:
case a
l : List Prop
i : Nat
⊢ ¬orN l → ¬l.getD i False
Theorem: Smt.Reconstruct.Prop.cnfOrNeg
Proof state before:
case a
l : List Prop
i : Nat
⊢ ¬orN l → ¬l.getD i False
Tactic:
intros orNl p
Proof state after:
case a
l : List Prop
i : Nat
orNl : ¬orN l
p : l.getD i False
⊢ False
Theorem: Smt.Reconstruct.Prop.cnfOrNeg
Proof state before:
case a
l : List Prop
i : Nat
orNl : ¬orN l
p : l.getD i False
⊢ False
Tactic:
have andNotl := @deMorgan₃ l orNl
Proof state after:
case a
l : List Prop
i : Nat
orNl : ¬orN l
p : l.getD i False
andNotl : andN (notList l)
⊢ False
Theorem: Smt.Reconstruct.Prop.cnfOrNeg
Proof state before:
case a
l : List Prop
i : Nat
orNl : ¬orN l
p : l.getD i False
andNotl : andN (notList l)
⊢ False
Tactic:
match l with
| [] => exact False.elim p
| [h] =>
  match i with
  | 0 => exact absurd p orNl
  | _ + 1 => exact False.elim p
| h₁::h₂::hs =>
  match i with
  | 0 => have ⟨nh₁p, _⟩ := andNotl
         exact absurd p nh₁p
  | i' + 1 =>
    have IH := cnfOrNeg (h₂::hs) i'
    have orNTail := orImplies₂ (orComm IH) p
    have ⟨_, notOrNTail⟩ := deMorganSmall orNl
    exact absurd orNTail notOrNTail
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfOrNeg
Proof state before:
l : List Prop
i : Nat
orNl : ¬orN []
p : [].getD i False
andNotl : andN (notList [])
⊢ False
Tactic:
exact False.elim p
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfOrNeg
Proof state before:
l : List Prop
i : Nat
h : Prop
orNl : ¬orN [h]
p : [h].getD i False
andNotl : andN (notList [h])
⊢ False
Tactic:
match i with
| 0 => exact absurd p orNl
| _ + 1 => exact False.elim p
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfOrNeg
Proof state before:
l : List Prop
i : Nat
h : Prop
orNl : ¬orN [h]
andNotl : andN (notList [h])
p : [h].getD 0 False
⊢ False
Tactic:
exact absurd p orNl
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfOrNeg
Proof state before:
l : List Prop
i : Nat
h : Prop
orNl : ¬orN [h]
andNotl : andN (notList [h])
n✝ : Nat
p : [h].getD (n✝ + 1) False
⊢ False
Tactic:
exact False.elim p
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfOrNeg
Proof state before:
l : List Prop
i : Nat
h₁ h₂ : Prop
hs : List Prop
orNl : ¬orN (h₁ :: h₂ :: hs)
p : (h₁ :: h₂ :: hs).getD i False
andNotl : andN (notList (h₁ :: h₂ :: hs))
⊢ False
Tactic:
match i with
| 0 => have ⟨nh₁p, _⟩ := andNotl
       exact absurd p nh₁p
| i' + 1 =>
  have IH := cnfOrNeg (h₂::hs) i'
  have orNTail := orImplies₂ (orComm IH) p
  have ⟨_, notOrNTail⟩ := deMorganSmall orNl
  exact absurd orNTail notOrNTail
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfOrNeg
Proof state before:
l : List Prop
i : Nat
h₁ h₂ : Prop
hs : List Prop
orNl : ¬orN (h₁ :: h₂ :: hs)
andNotl : andN (notList (h₁ :: h₂ :: hs))
p : (h₁ :: h₂ :: hs).getD 0 False
⊢ False
Tactic:
have ⟨nh₁p, _⟩ := andNotl
Proof state after:
l : List Prop
i : Nat
h₁ h₂ : Prop
hs : List Prop
orNl : ¬orN (h₁ :: h₂ :: hs)
andNotl : andN (notList (h₁ :: h₂ :: hs))
p : (h₁ :: h₂ :: hs).getD 0 False
nh₁p : ¬h₁
right✝ : andN ((¬h₂) :: map Not hs)
⊢ False
Theorem: Smt.Reconstruct.Prop.cnfOrNeg
Proof state before:
l : List Prop
i : Nat
h₁ h₂ : Prop
hs : List Prop
orNl : ¬orN (h₁ :: h₂ :: hs)
andNotl : andN (notList (h₁ :: h₂ :: hs))
p : (h₁ :: h₂ :: hs).getD 0 False
nh₁p : ¬h₁
right✝ : andN ((¬h₂) :: map Not hs)
⊢ False
Tactic:
exact absurd p nh₁p
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfOrNeg
Proof state before:
l : List Prop
i : Nat
h₁ h₂ : Prop
hs : List Prop
orNl : ¬orN (h₁ :: h₂ :: hs)
andNotl : andN (notList (h₁ :: h₂ :: hs))
i' : Nat
p : (h₁ :: h₂ :: hs).getD (i' + 1) False
⊢ False
Tactic:
have IH := cnfOrNeg (h₂::hs) i'
Proof state after:
l : List Prop
i : Nat
h₁ h₂ : Prop
hs : List Prop
orNl : ¬orN (h₁ :: h₂ :: hs)
andNotl : andN (notList (h₁ :: h₂ :: hs))
i' : Nat
p : (h₁ :: h₂ :: hs).getD (i' + 1) False
IH : orN (h₂ :: hs) ∨ ¬(h₂ :: hs).getD i' False
⊢ False
Theorem: Smt.Reconstruct.Prop.cnfOrNeg
Proof state before:
l : List Prop
i : Nat
h₁ h₂ : Prop
hs : List Prop
orNl : ¬orN (h₁ :: h₂ :: hs)
andNotl : andN (notList (h₁ :: h₂ :: hs))
i' : Nat
p : (h₁ :: h₂ :: hs).getD (i' + 1) False
IH : orN (h₂ :: hs) ∨ ¬(h₂ :: hs).getD i' False
⊢ False
Tactic:
have orNTail := orImplies₂ (orComm IH) p
Proof state after:
l : List Prop
i : Nat
h₁ h₂ : Prop
hs : List Prop
orNl : ¬orN (h₁ :: h₂ :: hs)
andNotl : andN (notList (h₁ :: h₂ :: hs))
i' : Nat
p : (h₁ :: h₂ :: hs).getD (i' + 1) False
IH : orN (h₂ :: hs) ∨ ¬(h₂ :: hs).getD i' False
orNTail : orN (h₂ :: hs)
⊢ False
Theorem: Smt.Reconstruct.Prop.cnfOrNeg
Proof state before:
l : List Prop
i : Nat
h₁ h₂ : Prop
hs : List Prop
orNl : ¬orN (h₁ :: h₂ :: hs)
andNotl : andN (notList (h₁ :: h₂ :: hs))
i' : Nat
p : (h₁ :: h₂ :: hs).getD (i' + 1) False
IH : orN (h₂ :: hs) ∨ ¬(h₂ :: hs).getD i' False
orNTail : orN (h₂ :: hs)
⊢ False
Tactic:
have ⟨_, notOrNTail⟩ := deMorganSmall orNl
Proof state after:
l : List Prop
i : Nat
h₁ h₂ : Prop
hs : List Prop
orNl : ¬orN (h₁ :: h₂ :: hs)
andNotl : andN (notList (h₁ :: h₂ :: hs))
i' : Nat
p : (h₁ :: h₂ :: hs).getD (i' + 1) False
IH : orN (h₂ :: hs) ∨ ¬(h₂ :: hs).getD i' False
orNTail : orN (h₂ :: hs)
left✝ : ¬h₁
notOrNTail : ¬orN (h₂ :: hs)
⊢ False
Theorem: Smt.Reconstruct.Prop.cnfOrNeg
Proof state before:
l : List Prop
i : Nat
h₁ h₂ : Prop
hs : List Prop
orNl : ¬orN (h₁ :: h₂ :: hs)
andNotl : andN (notList (h₁ :: h₂ :: hs))
i' : Nat
p : (h₁ :: h₂ :: hs).getD (i' + 1) False
IH : orN (h₂ :: hs) ∨ ¬(h₂ :: hs).getD i' False
orNTail : orN (h₂ :: hs)
left✝ : ¬h₁
notOrNTail : ¬orN (h₂ :: hs)
⊢ False
Tactic:
exact absurd orNTail notOrNTail
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfOrPos
Proof state before:
l : List Prop
⊢ orN ((¬orN l) :: l)
Tactic:
cases l with
| nil => exact not_false
| cons l ls =>
  simp only [orN]
  apply cnfOrPos'
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfOrPos
Proof state before:
case nil

⊢ orN [¬orN []]
Tactic:
exact not_false
Proof state after:
no goals