internlm/Lean-Github huggingface dataset:
Theorem: Smt.Reconstruct.Prop.cnfOrPos
Proof state before:
case cons
l : Prop
ls : List Prop
⊢ orN ((¬orN (l :: ls)) :: l :: ls)
Tactic:
simp only [orN]
Proof state after:
case cons
l : Prop
ls : List Prop
⊢ ¬orN (l :: ls) ∨ orN (l :: ls)
Theorem: Smt.Reconstruct.Prop.cnfOrPos
Proof state before:
case cons
l : Prop
ls : List Prop
⊢ ¬orN (l :: ls) ∨ orN (l :: ls)
Tactic:
apply cnfOrPos'
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfImpliesPos
Proof state before:
⊢ ∀ {p q : Prop}, ¬(p → q) ∨ ¬p ∨ q
Tactic:
intros p q
Proof state after:
p q : Prop
⊢ ¬(p → q) ∨ ¬p ∨ q
Theorem: Smt.Reconstruct.Prop.cnfImpliesPos
Proof state before:
p q : Prop
⊢ ¬(p → q) ∨ ¬p ∨ q
Tactic:
match Classical.em p, Classical.em q with
| _,         Or.inl hq  => exact Or.inr (Or.inr hq)
| Or.inl hp, Or.inr hnq => apply Or.inl
                           intro f
                           exact absurd (f hp) hnq
| Or.inr hnp, _         => exact Or.inr (Or.inl hnp)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfImpliesPos
Proof state before:
p q : Prop
x✝ : p ∨ ¬p
hq : q
⊢ ¬(p → q) ∨ ¬p ∨ q
Tactic:
exact Or.inr (Or.inr hq)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfImpliesPos
Proof state before:
p q : Prop
hp : p
hnq : ¬q
⊢ ¬(p → q) ∨ ¬p ∨ q
Tactic:
apply Or.inl
Proof state after:
case h
p q : Prop
hp : p
hnq : ¬q
⊢ ¬(p → q)
Theorem: Smt.Reconstruct.Prop.cnfImpliesPos
Proof state before:
case h
p q : Prop
hp : p
hnq : ¬q
⊢ ¬(p → q)
Tactic:
intro f
Proof state after:
case h
p q : Prop
hp : p
hnq : ¬q
f : p → q
⊢ False
Theorem: Smt.Reconstruct.Prop.cnfImpliesPos
Proof state before:
case h
p q : Prop
hp : p
hnq : ¬q
f : p → q
⊢ False
Tactic:
exact absurd (f hp) hnq
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfImpliesPos
Proof state before:
p q : Prop
hnp : ¬p
x✝ : q ∨ ¬q
⊢ ¬(p → q) ∨ ¬p ∨ q
Tactic:
exact Or.inr (Or.inl hnp)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfImpliesNeg1
Proof state before:
⊢ ∀ {p q : Prop}, (p → q) ∨ p
Tactic:
intros p q
Proof state after:
p q : Prop
⊢ (p → q) ∨ p
Theorem: Smt.Reconstruct.Prop.cnfImpliesNeg1
Proof state before:
p q : Prop
⊢ (p → q) ∨ p
Tactic:
apply orComm
Proof state after:
case a
p q : Prop
⊢ p ∨ (p → q)
Theorem: Smt.Reconstruct.Prop.cnfImpliesNeg1
Proof state before:
case a
p q : Prop
⊢ p ∨ (p → q)
Tactic:
apply orImplies
Proof state after:
case a.a
p q : Prop
⊢ ¬p → p → q
Theorem: Smt.Reconstruct.Prop.cnfImpliesNeg1
Proof state before:
case a.a
p q : Prop
⊢ ¬p → p → q
Tactic:
exact flip absurd
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfImpliesNeg2
Proof state before:
⊢ ∀ {p q : Prop}, (p → q) ∨ ¬q
Tactic:
intros p q
Proof state after:
p q : Prop
⊢ (p → q) ∨ ¬q
Theorem: Smt.Reconstruct.Prop.cnfImpliesNeg2
Proof state before:
p q : Prop
⊢ (p → q) ∨ ¬q
Tactic:
apply orComm
Proof state after:
case a
p q : Prop
⊢ ¬q ∨ (p → q)
Theorem: Smt.Reconstruct.Prop.cnfImpliesNeg2
Proof state before:
case a
p q : Prop
⊢ ¬q ∨ (p → q)
Tactic:
apply orImplies
Proof state after:
case a.a
p q : Prop
⊢ ¬¬q → p → q
Theorem: Smt.Reconstruct.Prop.cnfImpliesNeg2
Proof state before:
case a.a
p q : Prop
⊢ ¬¬q → p → q
Tactic:
intros hnnq _
Proof state after:
case a.a
p q : Prop
hnnq : ¬¬q
a✝ : p
⊢ q
Theorem: Smt.Reconstruct.Prop.cnfImpliesNeg2
Proof state before:
case a.a
p q : Prop
hnnq : ¬¬q
a✝ : p
⊢ q
Tactic:
exact notNotElim hnnq
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfEquivPos1
Proof state before:
⊢ ∀ {p q : Prop}, p ≠ q ∨ ¬p ∨ q
Tactic:
intros _ _
Proof state after:
p✝ q✝ : Prop
⊢ p✝ ≠ q✝ ∨ ¬p✝ ∨ q✝
Theorem: Smt.Reconstruct.Prop.cnfEquivPos1
Proof state before:
p✝ q✝ : Prop
⊢ p✝ ≠ q✝ ∨ ¬p✝ ∨ q✝
Tactic:
apply orImplies
Proof state after:
case a
p✝ q✝ : Prop
⊢ ¬p✝ ≠ q✝ → ¬p✝ ∨ q✝
Theorem: Smt.Reconstruct.Prop.cnfEquivPos1
Proof state before:
case a
p✝ q✝ : Prop
⊢ ¬p✝ ≠ q✝ → ¬p✝ ∨ q✝
Tactic:
exact equivElim1 ∘ notNotElim
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfEquivPos2
Proof state before:
⊢ ∀ {p q : Prop}, p ≠ q ∨ p ∨ ¬q
Tactic:
intros _ _
Proof state after:
p✝ q✝ : Prop
⊢ p✝ ≠ q✝ ∨ p✝ ∨ ¬q✝
Theorem: Smt.Reconstruct.Prop.cnfEquivPos2
Proof state before:
p✝ q✝ : Prop
⊢ p✝ ≠ q✝ ∨ p✝ ∨ ¬q✝
Tactic:
apply orImplies
Proof state after:
case a
p✝ q✝ : Prop
⊢ ¬p✝ ≠ q✝ → p✝ ∨ ¬q✝
Theorem: Smt.Reconstruct.Prop.cnfEquivPos2
Proof state before:
case a
p✝ q✝ : Prop
⊢ ¬p✝ ≠ q✝ → p✝ ∨ ¬q✝
Tactic:
exact equivElim2 ∘ notNotElim
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfEquivNeg1
Proof state before:
⊢ ∀ {p q : Prop}, p = q ∨ p ∨ q
Tactic:
intros _ _
Proof state after:
p✝ q✝ : Prop
⊢ p✝ = q✝ ∨ p✝ ∨ q✝
Theorem: Smt.Reconstruct.Prop.cnfEquivNeg1
Proof state before:
p✝ q✝ : Prop
⊢ p✝ = q✝ ∨ p✝ ∨ q✝
Tactic:
apply orImplies
Proof state after:
case a
p✝ q✝ : Prop
⊢ ¬p✝ = q✝ → p✝ ∨ q✝
Theorem: Smt.Reconstruct.Prop.cnfEquivNeg1
Proof state before:
case a
p✝ q✝ : Prop
⊢ ¬p✝ = q✝ → p✝ ∨ q✝
Tactic:
exact notEquivElim1
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.cnfEquivNeg2
Proof state before:
⊢ ∀ {p q : Prop}, p = q ∨ ¬p ∨ ¬q
Tactic:
intros _ _
Proof state after:
p✝ q✝ : Prop
⊢ p✝ = q✝ ∨ ¬p✝ ∨ ¬q✝
Theorem: Smt.Reconstruct.Prop.cnfEquivNeg2
Proof state before:
p✝ q✝ : Prop
⊢ p✝ = q✝ ∨ ¬p✝ ∨ ¬q✝
Tactic:
apply orImplies
Proof state after:
case a
p✝ q✝ : Prop
⊢ ¬p✝ = q✝ → ¬p✝ ∨ ¬q✝
Theorem: Smt.Reconstruct.Prop.cnfEquivNeg2
Proof state before:
case a
p✝ q✝ : Prop
⊢ ¬p✝ = q✝ → ¬p✝ ∨ ¬q✝
Tactic:
exact notEquivElim2
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.iteIntro
Proof state before:
α : Type u
c : Prop
t e : α
⊢ if c then (if c then t else e) = t else (if c then t else e) = e
Tactic:
match Classical.em c with
| Or.inl hc  => rw [if_pos hc, if_pos hc]
| Or.inr hnc => rw [if_neg hnc, if_neg hnc]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.iteIntro
Proof state before:
α : Type u
c : Prop
t e : α
hc : c
⊢ if c then (if c then t else e) = t else (if c then t else e) = e
Tactic:
rw [if_pos hc, if_pos hc]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.iteIntro
Proof state before:
α : Type u
c : Prop
t e : α
hnc : ¬c
⊢ if c then (if c then t else e) = t else (if c then t else e) = e
Tactic:
rw [if_neg hnc, if_neg hnc]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.congrIte
Proof state before:
c₁ c₂ : Prop
α : Sort u_1
inst✝¹ : Decidable c₁
inst✝ : Decidable c₂
t₁ t₂ e₁ e₂ : α
⊢ c₁ = c₂ → t₁ = t₂ → e₁ = e₂ → (if c₁ then t₁ else e₁) = if c₂ then t₂ else e₂
Tactic:
intros h₁ h₂ h₃
Proof state after:
c₁ c₂ : Prop
α : Sort u_1
inst✝¹ : Decidable c₁
inst✝ : Decidable c₂
t₁ t₂ e₁ e₂ : α
h₁ : c₁ = c₂
h₂ : t₁ = t₂
h₃ : e₁ = e₂
⊢ (if c₁ then t₁ else e₁) = if c₂ then t₂ else e₂
Theorem: Smt.Reconstruct.Prop.congrIte
Proof state before:
c₁ c₂ : Prop
α : Sort u_1
inst✝¹ : Decidable c₁
inst✝ : Decidable c₂
t₁ t₂ e₁ e₂ : α
h₁ : c₁ = c₂
h₂ : t₁ = t₂
h₃ : e₁ = e₂
⊢ (if c₁ then t₁ else e₁) = if c₂ then t₂ else e₂
Tactic:
simp only [h₁, h₂, h₃]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.congrHAdd
Proof state before:
α β γ : Type
inst✝ : HAdd α β γ
⊢ ∀ {a₁ a₂ : α} {b₁ b₂ : β}, a₁ = a₂ → b₁ = b₂ → a₁ + b₁ = a₂ + b₂
Tactic:
intros a₁ a₂ b₁ b₂ h₁ h₂
Proof state after:
α β γ : Type
inst✝ : HAdd α β γ
a₁ a₂ : α
b₁ b₂ : β
h₁ : a₁ = a₂
h₂ : b₁ = b₂
⊢ a₁ + b₁ = a₂ + b₂
Theorem: Smt.Reconstruct.Prop.congrHAdd
Proof state before:
α β γ : Type
inst✝ : HAdd α β γ
a₁ a₂ : α
b₁ b₂ : β
h₁ : a₁ = a₂
h₂ : b₁ = b₂
⊢ a₁ + b₁ = a₂ + b₂
Tactic:
rw [h₁, h₂]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.eqResolve
Proof state before:
P Q : Prop
⊢ P → P = Q → Q
Tactic:
intros h₁ h₂
Proof state after:
P Q : Prop
h₁ : P
h₂ : P = Q
⊢ Q
Theorem: Smt.Reconstruct.Prop.eqResolve
Proof state before:
P Q : Prop
h₁ : P
h₂ : P = Q
⊢ Q
Tactic:
rewrite [← h₂]
Proof state after:
P Q : Prop
h₁ : P
h₂ : P = Q
⊢ P
Theorem: Smt.Reconstruct.Prop.eqResolve
Proof state before:
P Q : Prop
h₁ : P
h₂ : P = Q
⊢ P
Tactic:
exact h₁
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.notAnd
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.notAnd
Proof state before:
l : List Prop
h : ¬andN l
⊢ orN (notList l)
Tactic:
match l with
| []         => exact False.elim (h True.intro)
| [_]        => exact h
| p₁::p₂::ps => simp [orN, notList, map]
                match deMorganSmall₃ h with
                | Or.inl hnp₁ => exact Or.inl hnp₁
                | Or.inr hnAndTail =>
                  have IH := notAnd (p₂::ps) hnAndTail
                  exact Or.inr IH
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.notAnd
Proof state before:
l : List Prop
h : ¬andN []
⊢ orN (notList [])
Tactic:
exact False.elim (h True.intro)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.notAnd
Proof state before:
l : List Prop
head✝ : Prop
h : ¬andN [head✝]
⊢ orN (notList [head✝])
Tactic:
exact h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.notAnd
Proof state before:
l : List Prop
p₁ p₂ : Prop
ps : List Prop
h : ¬andN (p₁ :: p₂ :: ps)
⊢ orN (notList (p₁ :: p₂ :: ps))
Tactic:
simp [orN, notList, map]
Proof state after:
l : List Prop
p₁ p₂ : Prop
ps : List Prop
h : ¬andN (p₁ :: p₂ :: ps)
⊢ ¬p₁ ∨ orN ((¬p₂) :: map Not ps)
Theorem: Smt.Reconstruct.Prop.notAnd
Proof state before:
l : List Prop
p₁ p₂ : Prop
ps : List Prop
h : ¬andN (p₁ :: p₂ :: ps)
⊢ ¬p₁ ∨ orN ((¬p₂) :: map Not ps)
Tactic:
match deMorganSmall₃ h with
| Or.inl hnp₁ => exact Or.inl hnp₁
| Or.inr hnAndTail =>
  have IH := notAnd (p₂::ps) hnAndTail
  exact Or.inr IH
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.notAnd
Proof state before:
l : List Prop
p₁ p₂ : Prop
ps : List Prop
h : ¬andN (p₁ :: p₂ :: ps)
hnp₁ : ¬p₁
⊢ ¬p₁ ∨ orN ((¬p₂) :: map Not ps)
Tactic:
exact Or.inl hnp₁
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.notAnd
Proof state before:
l : List Prop
p₁ p₂ : Prop
ps : List Prop
h : ¬andN (p₁ :: p₂ :: ps)
hnAndTail : ¬andN (p₂ :: ps)
⊢ ¬p₁ ∨ orN ((¬p₂) :: map Not ps)
Tactic:
have IH := notAnd (p₂::ps) hnAndTail
Proof state after:
l : List Prop
p₁ p₂ : Prop
ps : List Prop
h : ¬andN (p₁ :: p₂ :: ps)
hnAndTail : ¬andN (p₂ :: ps)
IH : orN (notList (p₂ :: ps))
⊢ ¬p₁ ∨ orN ((¬p₂) :: map Not ps)
Theorem: Smt.Reconstruct.Prop.notAnd
Proof state before:
l : List Prop
p₁ p₂ : Prop
ps : List Prop
h : ¬andN (p₁ :: p₂ :: ps)
hnAndTail : ¬andN (p₂ :: ps)
IH : orN (notList (p₂ :: ps))
⊢ ¬p₁ ∨ orN ((¬p₂) :: map Not ps)
Tactic:
exact Or.inr IH
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.trueIntro
Proof state before:
⊢ ∀ {A : Prop}, A → A = True
Tactic:
intros A h
Proof state after:
A : Prop
h : A
⊢ A = True
Theorem: Smt.Reconstruct.Prop.trueIntro
Proof state before:
A : Prop
h : A
⊢ A = True
Tactic:
exact propext (Iff.intro (λ _ => True.intro) (λ _ => h))
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.trueImplies
Proof state before:
p : Prop
⊢ (True → p) → p
Tactic:
intro htp
Proof state after:
p : Prop
htp : True → p
⊢ p
Theorem: Smt.Reconstruct.Prop.trueImplies
Proof state before:
p : Prop
htp : True → p
⊢ p
Tactic:
exact htp trivial
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.trueElim
Proof state before:
⊢ ∀ {A : Prop}, A = True → A
Tactic:
intros A h
Proof state after:
A : Prop
h : A = True
⊢ A
Theorem: Smt.Reconstruct.Prop.trueElim
Proof state before:
A : Prop
h : A = True
⊢ A
Tactic:
rewrite [h]
Proof state after:
A : Prop
h : A = True
⊢ True
Theorem: Smt.Reconstruct.Prop.trueElim
Proof state before:
A : Prop
h : A = True
⊢ True
Tactic:
trivial
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_cons
Proof state before:
t : Prop
l : List Prop
⊢ orN (t :: l) = (t ∨ orN l)
Tactic:
cases l with
| nil => simp [orN]
| cons t' l => simp [orN]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_cons
Proof state before:
case nil
t : Prop
⊢ orN [t] = (t ∨ orN [])
Tactic:
simp [orN]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_cons
Proof state before:
case cons
t t' : Prop
l : List Prop
⊢ orN (t :: t' :: l) = (t ∨ orN (t' :: l))
Tactic:
simp [orN]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_eraseIdx
Proof state before:
j : Nat
qs : List Prop
hj : j < qs.length
⊢ (orN (qs.eraseIdx j) ∨ qs[j]) = orN qs
Tactic:
revert j
Proof state after:
qs : List Prop
⊢ ∀ {j : Nat} (hj : j < qs.length), (orN (qs.eraseIdx j) ∨ qs[j]) = orN qs
Theorem: Smt.Reconstruct.Prop.orN_eraseIdx
Proof state before:
qs : List Prop
⊢ ∀ {j : Nat} (hj : j < qs.length), (orN (qs.eraseIdx j) ∨ qs[j]) = orN qs
Tactic:
induction qs with
| nil =>
  intro j hj
  simp at hj; exfalso
  exact not_succ_le_zero j hj
| cons t l ih =>
  intro j hj
  cases j with
  | zero =>
    simp only [eraseIdx_cons_zero, cons_getElem_zero, orN_cons, eraseIdx_cons_succ, cons_getElem_succ]
    rw [or_comm]
  | succ j =>
    simp only [eraseIdx_cons_succ, cons_getElem_succ, orN_cons, eraseIdx, or_assoc]
    congr
    rw [@ih j (by rw [length_cons, succ_lt_succ_iff] at hj; exact hj)]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_eraseIdx
Proof state before:
case nil

⊢ ∀ {j : Nat} (hj : j < [].length), (orN ([].eraseIdx j) ∨ [][j]) = orN []
Tactic:
intro j hj
Proof state after:
case nil
j : Nat
hj : j < [].length
⊢ (orN ([].eraseIdx j) ∨ [][j]) = orN []
Theorem: Smt.Reconstruct.Prop.orN_eraseIdx
Proof state before:
case nil
j : Nat
hj : j < [].length
⊢ (orN ([].eraseIdx j) ∨ [][j]) = orN []
Tactic:
simp at hj
Proof state after:
case nil
j : Nat
hj : j < 0
⊢ (orN ([].eraseIdx j) ∨ [][j]) = orN []
Theorem: Smt.Reconstruct.Prop.orN_eraseIdx
Proof state before:
case nil
j : Nat
hj : j < 0
⊢ (orN ([].eraseIdx j) ∨ [][j]) = orN []
Tactic:
exfalso
Proof state after:
case nil
j : Nat
hj : j < 0
⊢ False
Theorem: Smt.Reconstruct.Prop.orN_eraseIdx
Proof state before:
case nil
j : Nat
hj : j < 0
⊢ False
Tactic:
exact not_succ_le_zero j hj
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_eraseIdx
Proof state before:
case cons
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
⊢ ∀ {j : Nat} (hj : j < (t :: l).length), (orN ((t :: l).eraseIdx j) ∨ (t :: l)[j]) = orN (t :: l)
Tactic:
intro j hj
Proof state after:
case cons
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j < (t :: l).length
⊢ (orN ((t :: l).eraseIdx j) ∨ (t :: l)[j]) = orN (t :: l)
Theorem: Smt.Reconstruct.Prop.orN_eraseIdx
Proof state before:
case cons
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j < (t :: l).length
⊢ (orN ((t :: l).eraseIdx j) ∨ (t :: l)[j]) = orN (t :: l)
Tactic:
cases j with
| zero =>
  simp only [eraseIdx_cons_zero, cons_getElem_zero, orN_cons, eraseIdx_cons_succ, cons_getElem_succ]
  rw [or_comm]
| succ j =>
  simp only [eraseIdx_cons_succ, cons_getElem_succ, orN_cons, eraseIdx, or_assoc]
  congr
  rw [@ih j (by rw [length_cons, succ_lt_succ_iff] at hj; exact hj)]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_eraseIdx
Proof state before:
case cons.zero
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
hj : 0 < (t :: l).length
⊢ (orN ((t :: l).eraseIdx 0) ∨ (t :: l)[0]) = orN (t :: l)
Tactic:
simp only [eraseIdx_cons_zero, cons_getElem_zero, orN_cons, eraseIdx_cons_succ, cons_getElem_succ]
Proof state after:
case cons.zero
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
hj : 0 < (t :: l).length
⊢ (orN l ∨ t) = (t ∨ orN l)
Theorem: Smt.Reconstruct.Prop.orN_eraseIdx
Proof state before:
case cons.zero
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
hj : 0 < (t :: l).length
⊢ (orN l ∨ t) = (t ∨ orN l)
Tactic:
rw [or_comm]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_eraseIdx
Proof state before:
case cons.succ
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j + 1 < (t :: l).length
⊢ (orN ((t :: l).eraseIdx (j + 1)) ∨ (t :: l)[j + 1]) = orN (t :: l)
Tactic:
simp only [eraseIdx_cons_succ, cons_getElem_succ, orN_cons, eraseIdx, or_assoc]
Proof state after:
case cons.succ
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j + 1 < (t :: l).length
⊢ (t ∨ orN (l.eraseIdx j) ∨ l[j]) = (t ∨ orN l)
Theorem: Smt.Reconstruct.Prop.orN_eraseIdx
Proof state before:
case cons.succ
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j + 1 < (t :: l).length
⊢ (t ∨ orN (l.eraseIdx j) ∨ l[j]) = (t ∨ orN l)
Tactic:
congr
Proof state after:
case cons.succ.e_b
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j + 1 < (t :: l).length
⊢ (orN (l.eraseIdx j) ∨ l[j]) = orN l
Theorem: Smt.Reconstruct.Prop.orN_eraseIdx
Proof state before:
case cons.succ.e_b
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j + 1 < (t :: l).length
⊢ (orN (l.eraseIdx j) ∨ l[j]) = orN l
Tactic:
rw [@ih j (by rw [length_cons, succ_lt_succ_iff] at hj; exact hj)]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_eraseIdx
Proof state before:
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j + 1 < (t :: l).length
⊢ j < l.length
Tactic:
rw [length_cons, succ_lt_succ_iff] at hj
Proof state after:
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j < l.length
⊢ j < l.length
Theorem: Smt.Reconstruct.Prop.orN_eraseIdx
Proof state before:
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j < l.length
⊢ j < l.length
Tactic:
exact hj
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_subList
Proof state before:
ps qs : List Prop
i j : Nat
hps : orN ps
hpq : ps = subList' qs i j
⊢ orN qs
Tactic:
revert i j ps
Proof state after:
qs : List Prop
⊢ ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = subList' qs i j → orN qs
Theorem: Smt.Reconstruct.Prop.orN_subList
Proof state before:
qs : List Prop
⊢ ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = subList' qs i j → orN qs
Tactic:
induction qs with
| nil =>
  intro ps i j hp hps
  simp [subList', *] at *; assumption
| cons t l ih =>
  simp only [subList'] at *
  intro ps i j hp hps
  rw [orN_cons]
  cases j with
  | zero =>
    simp [*, orN] at *
  | succ j =>
    simp only [take_cons_succ] at hps
    cases i with
    | zero =>
      simp only [hps, orN_cons, drop_zero] at hp
      exact congOrLeft (fun hp => @ih (drop 0 (take j l)) 0 j (by simp [hp]) rfl) hp
    | succ i =>
      apply Or.inr
      apply @ih ps i j hp
      simp [hps]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_subList
Proof state before:
case nil

⊢ ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = subList' [] i j → orN []
Tactic:
intro ps i j hp hps
Proof state after:
case nil
ps : List Prop
i j : Nat
hp : orN ps
hps : ps = subList' [] i j
⊢ orN []
Theorem: Smt.Reconstruct.Prop.orN_subList
Proof state before:
case nil
ps : List Prop
i j : Nat
hp : orN ps
hps : ps = subList' [] i j
⊢ orN []
Tactic:
simp [subList', *] at *
Proof state after:
case nil
ps : List Prop
i j : Nat
hp : orN []
hps : ps = []
⊢ orN []
Theorem: Smt.Reconstruct.Prop.orN_subList
Proof state before:
case nil
ps : List Prop
i j : Nat
hp : orN []
hps : ps = []
⊢ orN []
Tactic:
assumption
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_subList
Proof state before:
case cons
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = subList' l i j → orN l
⊢ ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = subList' (t :: l) i j → orN (t :: l)
Tactic:
simp only [subList'] at *
Proof state after:
case cons
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
⊢ ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j (t :: l)) → orN (t :: l)
Theorem: Smt.Reconstruct.Prop.orN_subList
Proof state before:
case cons
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
⊢ ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j (t :: l)) → orN (t :: l)
Tactic:
intro ps i j hp hps
Proof state after:
case cons
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
i j : Nat
hp : orN ps
hps : ps = drop i (take j (t :: l))
⊢ orN (t :: l)
Theorem: Smt.Reconstruct.Prop.orN_subList
Proof state before:
case cons
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
i j : Nat
hp : orN ps
hps : ps = drop i (take j (t :: l))
⊢ orN (t :: l)
Tactic:
rw [orN_cons]
Proof state after:
case cons
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
i j : Nat
hp : orN ps
hps : ps = drop i (take j (t :: l))
⊢ t ∨ orN l
Theorem: Smt.Reconstruct.Prop.orN_subList
Proof state before:
case cons
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
i j : Nat
hp : orN ps
hps : ps = drop i (take j (t :: l))
⊢ t ∨ orN l
Tactic:
cases j with
| zero =>
  simp [*, orN] at *
| succ j =>
  simp only [take_cons_succ] at hps
  cases i with
  | zero =>
    simp only [hps, orN_cons, drop_zero] at hp
    exact congOrLeft (fun hp => @ih (drop 0 (take j l)) 0 j (by simp [hp]) rfl) hp
  | succ i =>
    apply Or.inr
    apply @ih ps i j hp
    simp [hps]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_subList
Proof state before:
case cons.zero
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
i : Nat
hp : orN ps
hps : ps = drop i (take 0 (t :: l))
⊢ t ∨ orN l
Tactic:
simp [*, orN] at *
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_subList
Proof state before:
case cons.succ
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
i : Nat
hp : orN ps
j : Nat
hps : ps = drop i (take (j + 1) (t :: l))
⊢ t ∨ orN l
Tactic:
simp only [take_cons_succ] at hps
Proof state after:
case cons.succ
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
i : Nat
hp : orN ps
j : Nat
hps : ps = drop i (t :: take j l)
⊢ t ∨ orN l
Theorem: Smt.Reconstruct.Prop.orN_subList
Proof state before:
case cons.succ
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
i : Nat
hp : orN ps
j : Nat
hps : ps = drop i (t :: take j l)
⊢ t ∨ orN l
Tactic:
cases i with
| zero =>
  simp only [hps, orN_cons, drop_zero] at hp
  exact congOrLeft (fun hp => @ih (drop 0 (take j l)) 0 j (by simp [hp]) rfl) hp
| succ i =>
  apply Or.inr
  apply @ih ps i j hp
  simp [hps]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_subList
Proof state before:
case cons.succ.zero
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
hp : orN ps
j : Nat
hps : ps = drop 0 (t :: take j l)
⊢ t ∨ orN l
Tactic:
simp only [hps, orN_cons, drop_zero] at hp
Proof state after:
case cons.succ.zero
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
j : Nat
hps : ps = drop 0 (t :: take j l)
hp : t ∨ orN (take j l)
⊢ t ∨ orN l
Theorem: Smt.Reconstruct.Prop.orN_subList
Proof state before:
case cons.succ.zero
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
j : Nat
hps : ps = drop 0 (t :: take j l)
hp : t ∨ orN (take j l)
⊢ t ∨ orN l
Tactic:
exact congOrLeft (fun hp => @ih (drop 0 (take j l)) 0 j (by simp [hp]) rfl) hp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orN_subList
Proof state before:
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
j : Nat
hps : ps = drop 0 (t :: take j l)
hp✝ : t ∨ orN (take j l)
hp : orN (take j l)
⊢ orN (drop 0 (take j l))
Tactic:
simp [hp]
Proof state after:
no goals