Theorem: Smt.Reconstruct.Prop.cnfOrNeg (Smt/Reconstruct/Prop/Lemmas.lean)

State before:
⊢ ∀ (l : List Prop) (i : Nat), orN l ∨ ¬l.getD i False
Tactic:
intros l i
State after:
l : List Prop
i : Nat
⊢ orN l ∨ ¬l.getD i False

State before:
l : List Prop
i : Nat
⊢ orN l ∨ ¬l.getD i False
Tactic:
apply orImplies
State after:
case a
l : List Prop
i : Nat
⊢ ¬orN l → ¬l.getD i False

State before:
case a
l : List Prop
i : Nat
⊢ ¬orN l → ¬l.getD i False
Tactic:
intros orNl p
State after:
case a
l : List Prop
i : Nat
orNl : ¬orN l
p : l.getD i False
⊢ False

State before:
case a
l : List Prop
i : Nat
orNl : ¬orN l
p : l.getD i False
⊢ False
Tactic:
have andNotl := @deMorgan₃ l orNl
State after:
case a
l : List Prop
i : Nat
orNl : ¬orN l
p : l.getD i False
andNotl : andN (notList l)
⊢ False

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
State after:
no goals

State before:
l : List Prop
i : Nat
orNl : ¬orN []
p : [].getD i False
andNotl : andN (notList [])
⊢ False
Tactic:
exact False.elim p
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals

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'
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

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
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

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
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

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
State after:
no goals