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

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

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

State before:
case a
l : List Prop
i : Nat
⊢ ¬¬andN l → l.getD i True
Tactic:
intro h
State after:
case a
l : List Prop
i : Nat
h : ¬¬andN l
⊢ l.getD i True

State before:
case a
l : List Prop
i : Nat
h : ¬¬andN l
⊢ l.getD i True
Tactic:
have h' := notNotElim h
State after:
case a
l : List Prop
i : Nat
h : ¬¬andN l
h' : andN l
⊢ l.getD i True

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

State before:
l : List Prop
i : Nat
h : ¬¬andN []
h' : andN []
⊢ [].getD i True
Tactic:
exact True.intro
State after:
no goals

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

State before:
l : List Prop
i : Nat
p : Prop
h : ¬¬andN [p]
h' : andN [p]
⊢ [p].getD 0 True
Tactic:
exact h'
State after:
no goals

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

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

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

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

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