Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive (LeanSAT/LRAT/Formula/RupAddSound.lean)

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
⊢ reduce_postcondition_induction_motive c_arr assignment (↑idx + 1) (reduce_fold_fn assignment res c_arr[idx])
Tactic:
simp only [reduce_postcondition_induction_motive, Fin.getElem_fin, forall_exists_index, and_imp, Prod.forall]
State after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
⊢ (reduce_fold_fn assignment res c_arr[↑idx] = reducedToEmpty →
      ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)) ∧
    ∀ (a : PosFin n) (b : Bool),
      reduce_fold_fn assignment res c_arr[↑idx] = reducedToUnit (a, b) →
        ∀ (p : PosFin n → Bool), p ⊨ assignment → ∀ (x : Fin c_arr.size), ↑x < ↑idx + 1 → p ⊨ c_arr[↑x] → p ⊨ (a, b)

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
⊢ (reduce_fold_fn assignment res c_arr[↑idx] = reducedToEmpty →
      ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)) ∧
    ∀ (a : PosFin n) (b : Bool),
      reduce_fold_fn assignment res c_arr[↑idx] = reducedToUnit (a, b) →
        ∀ (p : PosFin n → Bool), p ⊨ assignment → ∀ (x : Fin c_arr.size), ↑x < ↑idx + 1 → p ⊨ c_arr[↑x] → p ⊨ (a, b)
Tactic:
constructor
State after:
case left
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
⊢ reduce_fold_fn assignment res c_arr[↑idx] = reducedToEmpty →
    ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case right
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
⊢ ∀ (a : PosFin n) (b : Bool),
    reduce_fold_fn assignment res c_arr[↑idx] = reducedToUnit (a, b) →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → ∀ (x : Fin c_arr.size), ↑x < ↑idx + 1 → p ⊨ c_arr[↑x] → p ⊨ (a, b)

State before:
case left
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
⊢ reduce_fold_fn assignment res c_arr[↑idx] = reducedToEmpty →
    ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
intro h p
State after:
case left
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
h : reduce_fold_fn assignment res c_arr[↑idx] = reducedToEmpty
p : PosFin n → Bool
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
case left
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
h : reduce_fold_fn assignment res c_arr[↑idx] = reducedToEmpty
p : PosFin n → Bool
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
rw [reduce_fold_fn] at h
State after:
case left
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
h :
  (match res with
    | encounteredBoth => encounteredBoth
    | reducedToEmpty =>
      match assignment[c_arr[↑idx].fst.val]! with
      | pos => if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
      | neg => if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
      | both => encounteredBoth
      | unassigned => reducedToUnit c_arr[↑idx]
    | reducedToUnit l' =>
      match assignment[c_arr[↑idx].fst.val]! with
      | pos => if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l'
      | neg => if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l'
      | both => encounteredBoth
      | unassigned => reducedToNonunit
    | reducedToNonunit => reducedToNonunit) =
    reducedToEmpty
p : PosFin n → Bool
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
case left
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
h :
  (match res with
    | encounteredBoth => encounteredBoth
    | reducedToEmpty =>
      match assignment[c_arr[↑idx].fst.val]! with
      | pos => if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
      | neg => if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
      | both => encounteredBoth
      | unassigned => reducedToUnit c_arr[↑idx]
    | reducedToUnit l' =>
      match assignment[c_arr[↑idx].fst.val]! with
      | pos => if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l'
      | neg => if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l'
      | both => encounteredBoth
      | unassigned => reducedToNonunit
    | reducedToNonunit => reducedToNonunit) =
    reducedToEmpty
p : PosFin n → Bool
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
split at h
State after:
case left.h_1
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) encounteredBoth
h : encounteredBoth = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case left.h_2
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | neg => if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | both => encounteredBoth
    | unassigned => reducedToUnit c_arr[↑idx]) =
    reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case left.h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l'✝)
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l'✝
    | neg => if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l'✝
    | both => encounteredBoth
    | unassigned => reducedToNonunit) =
    reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case left.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToNonunit
h : reducedToNonunit = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
case left.h_1
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) encounteredBoth
h : encounteredBoth = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case left.h_2
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | neg => if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | both => encounteredBoth
    | unassigned => reducedToUnit c_arr[↑idx]) =
    reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case left.h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l'✝)
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l'✝
    | neg => if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l'✝
    | both => encounteredBoth
    | unassigned => reducedToNonunit) =
    reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case left.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToNonunit
h : reducedToNonunit = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
. simp only at h
State after:
case left.h_2
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | neg => if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | both => encounteredBoth
    | unassigned => reducedToUnit c_arr[↑idx]) =
    reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case left.h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l'✝)
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l'✝
    | neg => if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l'✝
    | both => encounteredBoth
    | unassigned => reducedToNonunit) =
    reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case left.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToNonunit
h : reducedToNonunit = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
case left.h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l'✝)
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l'✝
    | neg => if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l'✝
    | both => encounteredBoth
    | unassigned => reducedToNonunit) =
    reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case left.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToNonunit
h : reducedToNonunit = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
. next l =>
  split at h
  . split at h <;> contradiction
  . split at h <;> contradiction
  . simp only at h
  . simp only at h
State after:
case left.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToNonunit
h : reducedToNonunit = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
case left.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToNonunit
h : reducedToNonunit = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
. simp only at h
State after:
no goals

State before:
case left.h_1
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) encounteredBoth
h : encounteredBoth = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
simp only at h
State after:
no goals

State before:
case left.h_2
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | neg => if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | both => encounteredBoth
    | unassigned => reducedToUnit c_arr[↑idx]) =
    reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
split at h
State after:
case left.h_2.h_1
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = pos
h : (if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty) = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case left.h_2.h_2
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = neg
h : (if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty) = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case left.h_2.h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = both
h : encounteredBoth = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case left.h_2.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToUnit c_arr[↑idx] = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
case left.h_2.h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = both
h : encounteredBoth = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case left.h_2.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToUnit c_arr[↑idx] = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
. simp only at h
State after:
case left.h_2.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToUnit c_arr[↑idx] = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
case left.h_2.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToUnit c_arr[↑idx] = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
. simp only at h
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : (if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty) = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
split at h
State after:
case isTrue
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h✝ : c_arr[↑idx].snd = true
h : False
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h✝ : ¬c_arr[↑idx].snd = true
h : reducedToEmpty = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
case isTrue
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h✝ : c_arr[↑idx].snd = true
h : False
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h✝ : ¬c_arr[↑idx].snd = true
h : reducedToEmpty = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
. exact False.elim h
State after:
case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h✝ : ¬c_arr[↑idx].snd = true
h : reducedToEmpty = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
case isTrue
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h✝ : c_arr[↑idx].snd = true
h : False
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
exact False.elim h
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : ¬c_arr[↑idx].snd = true
h : reducedToEmpty = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
simp only [Bool.not_eq_true] at c_arr_idx_eq_false
State after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
rcases ih.1 rfl p with ih1 | ih1
State after:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
. exact Or.inr ih1
State after:
no goals

State before:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
by_cases p ⊨ assignment
State after:
case pos
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
h✝ : p ⊨ assignment
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case neg
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
h✝ : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
case neg
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
h✝ : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
. next h =>
  exact Or.inr h
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
apply Or.inl
State after:
case h
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
⊢ ∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])

State before:
case h
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
⊢ ∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])
Tactic:
intro i i_lt_idx_add_one p_entails_c_arr_i
State after:
case h
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
⊢ False

State before:
case h
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
⊢ False
Tactic:
rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ i_lt_idx_add_one with i_lt_idx | i_eq_idx
State after:
case h.inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
i_lt_idx : ↑i < ↑idx
⊢ False

case h.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
i_eq_idx : ↑i = ↑idx
⊢ False

State before:
case h.inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
i_lt_idx : ↑i < ↑idx
⊢ False

case h.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
i_eq_idx : ↑i = ↑idx
⊢ False
Tactic:
. exact ih1 i i_lt_idx p_entails_c_arr_i
State after:
case h.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
i_eq_idx : ↑i = ↑idx
⊢ False

State before:
case h.inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
i_lt_idx : ↑i < ↑idx
⊢ False
Tactic:
exact ih1 i i_lt_idx p_entails_c_arr_i
State after:
no goals

State before:
case h.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
i_eq_idx : ↑i = ↑idx
p_entails_c_arr_i : p c_arr[↑idx].fst = false
p_entails_assignment : ∀ (i : PosFin n), hasAssignment (decide (p i = false)) assignment[i.val]! = false
⊢ False
Tactic:
specialize p_entails_assignment c_arr[idx.1].1
State after:
case h.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
i_eq_idx : ↑i = ↑idx
p_entails_c_arr_i : p c_arr[↑idx].fst = false
p_entails_assignment : hasAssignment (decide (p c_arr[↑idx].fst = false)) assignment[c_arr[↑idx].fst.val]! = false
⊢ False

State before:
case h.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
i_eq_idx : ↑i = ↑idx
p_entails_c_arr_i : p c_arr[↑idx].fst = false
p_entails_assignment : hasAssignment (decide (p c_arr[↑idx].fst = false)) assignment[c_arr[↑idx].fst.val]! = false
⊢ False
Tactic:
simp (config := { decide := true }) only [p_entails_c_arr_i, decide_True, heq] at p_entails_assignment
State after:
no goals

State before:
case neg
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
h✝ : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
next h =>
exact Or.inr h
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h✝ : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
h : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
exact Or.inr h
State after:
no goals

State before:
case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = false
ih1 : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
exact Or.inr ih1
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : (if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty) = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
split at h
State after:
case isTrue
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : (!c_arr[↑idx].snd) = true
h : False
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : ¬(!c_arr[↑idx].snd) = true
h : reducedToEmpty = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
case isTrue
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : (!c_arr[↑idx].snd) = true
h : False
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : ¬(!c_arr[↑idx].snd) = true
h : reducedToEmpty = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
. exact False.elim h
State after:
case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : ¬(!c_arr[↑idx].snd) = true
h : reducedToEmpty = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
case isTrue
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : (!c_arr[↑idx].snd) = true
h : False
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
exact False.elim h
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_false : ¬(!c_arr[↑idx].snd) = true
h : reducedToEmpty = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
simp only [Bool.not_eq_true', Bool.not_eq_false] at c_arr_idx_eq_false
State after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
rcases ih.1 rfl p with ih1 | ih1
State after:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
. exact Or.inr ih1
State after:
no goals

State before:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
by_cases p ⊨ assignment
State after:
case pos
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
h✝ : p ⊨ assignment
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case neg
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
h✝ : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
case neg
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
h✝ : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
. next h =>
  exact Or.inr h
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
apply Or.inl
State after:
case h
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
⊢ ∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])

State before:
case h
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
⊢ ∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])
Tactic:
intro i i_lt_idx_add_one p_entails_c_arr_i
State after:
case h
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
⊢ False

State before:
case h
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
⊢ False
Tactic:
rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ i_lt_idx_add_one with i_lt_idx | i_eq_idx
State after:
case h.inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
i_lt_idx : ↑i < ↑idx
⊢ False

case h.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
i_eq_idx : ↑i = ↑idx
⊢ False

State before:
case h.inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
i_lt_idx : ↑i < ↑idx
⊢ False

case h.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
i_eq_idx : ↑i = ↑idx
⊢ False
Tactic:
. exact ih1 i i_lt_idx p_entails_c_arr_i
State after:
case h.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
i_eq_idx : ↑i = ↑idx
⊢ False

State before:
case h.inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
p_entails_assignment : p ⊨ assignment
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
p_entails_c_arr_i : p ⊨ c_arr[↑i]
i_lt_idx : ↑i < ↑idx
⊢ False
Tactic:
exact ih1 i i_lt_idx p_entails_c_arr_i
State after:
no goals

State before:
case h.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
i_eq_idx : ↑i = ↑idx
p_entails_c_arr_i : p c_arr[↑idx].fst = true
p_entails_assignment : ∀ (i : PosFin n), hasAssignment (decide (p i = false)) assignment[i.val]! = false
⊢ False
Tactic:
specialize p_entails_assignment c_arr[idx.1].1
State after:
case h.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
i_eq_idx : ↑i = ↑idx
p_entails_c_arr_i : p c_arr[↑idx].fst = true
p_entails_assignment : hasAssignment (decide (p c_arr[↑idx].fst = false)) assignment[c_arr[↑idx].fst.val]! = false
⊢ False

State before:
case h.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
i : Fin c_arr.size
i_lt_idx_add_one : ↑i < ↑idx + 1
i_eq_idx : ↑i = ↑idx
p_entails_c_arr_i : p c_arr[↑idx].fst = true
p_entails_assignment : hasAssignment (decide (p c_arr[↑idx].fst = false)) assignment[c_arr[↑idx].fst.val]! = false
⊢ False
Tactic:
simp (config := { decide := true }) only [p_entails_c_arr_i, decide_True, heq] at p_entails_assignment
State after:
no goals

State before:
case neg
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
h✝ : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
next h =>
exact Or.inr h
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
h : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
exact Or.inr h
State after:
no goals

State before:
case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToEmpty = reducedToEmpty
c_arr_idx_eq_false : c_arr[↑idx].snd = true
ih1 : ¬(p ⊨ assignment)
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
exact Or.inr ih1
State after:
no goals

State before:
case left.h_2.h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = both
h : encounteredBoth = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
simp only at h
State after:
no goals

State before:
case left.h_2.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToUnit c_arr[↑idx] = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
simp only at h
State after:
no goals

State before:
case left.h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l'✝)
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l'✝
    | neg => if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l'✝
    | both => encounteredBoth
    | unassigned => reducedToNonunit) =
    reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
next l =>
split at h
. split at h <;> contradiction
. split at h <;> contradiction
. simp only at h
. simp only at h
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l
    | neg => if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l
    | both => encounteredBoth
    | unassigned => reducedToNonunit) =
    reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
split at h
State after:
case h_1
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = pos
h : (if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l) = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case h_2
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = neg
h : (if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l) = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = both
h : encounteredBoth = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToNonunit = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
case h_1
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = pos
h : (if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l) = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case h_2
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = neg
h : (if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l) = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = both
h : encounteredBoth = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToNonunit = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
. split at h <;> contradiction
State after:
case h_2
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = neg
h : (if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l) = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = both
h : encounteredBoth = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToNonunit = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
case h_2
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = neg
h : (if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l) = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = both
h : encounteredBoth = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToNonunit = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
. split at h <;> contradiction
State after:
case h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = both
h : encounteredBoth = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToNonunit = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
case h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = both
h : encounteredBoth = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToNonunit = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
. simp only at h
State after:
case h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToNonunit = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

State before:
case h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToNonunit = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
. simp only at h
State after:
no goals

State before:
case h_1
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = pos
h : (if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l) = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
split at h <;> contradiction
State after:
no goals

State before:
case h_2
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = neg
h : (if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l) = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
split at h <;> contradiction
State after:
no goals

State before:
case h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = both
h : encounteredBoth = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
simp only at h
State after:
no goals

State before:
case h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToNonunit = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
simp only at h
State after:
no goals

State before:
case left.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
p : PosFin n → Bool
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToNonunit
h : reducedToNonunit = reducedToEmpty
⊢ (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)
Tactic:
simp only at h
State after:
no goals

State before:
case right
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
⊢ ∀ (a : PosFin n) (b : Bool),
    reduce_fold_fn assignment res c_arr[↑idx] = reducedToUnit (a, b) →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → ∀ (x : Fin c_arr.size), ↑x < ↑idx + 1 → p ⊨ c_arr[↑x] → p ⊨ (a, b)
Tactic:
intro i b h p hp j j_lt_idx_add_one p_entails_c_arr_j
State after:
case right
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
i : PosFin n
b : Bool
h : reduce_fold_fn assignment res c_arr[↑idx] = reducedToUnit (i, b)
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
⊢ p ⊨ (i, b)

State before:
case right
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
i : PosFin n
b : Bool
h : reduce_fold_fn assignment res c_arr[↑idx] = reducedToUnit (i, b)
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
⊢ p ⊨ (i, b)
Tactic:
rw [reduce_fold_fn] at h
State after:
case right
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
i : PosFin n
b : Bool
h :
  (match res with
    | encounteredBoth => encounteredBoth
    | reducedToEmpty =>
      match assignment[c_arr[↑idx].fst.val]! with
      | pos => if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
      | neg => if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
      | both => encounteredBoth
      | unassigned => reducedToUnit c_arr[↑idx]
    | reducedToUnit l' =>
      match assignment[c_arr[↑idx].fst.val]! with
      | pos => if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l'
      | neg => if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l'
      | both => encounteredBoth
      | unassigned => reducedToNonunit
    | reducedToNonunit => reducedToNonunit) =
    reducedToUnit (i, b)
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
⊢ p ⊨ (i, b)

State before:
case right
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
i : PosFin n
b : Bool
h :
  (match res with
    | encounteredBoth => encounteredBoth
    | reducedToEmpty =>
      match assignment[c_arr[↑idx].fst.val]! with
      | pos => if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
      | neg => if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
      | both => encounteredBoth
      | unassigned => reducedToUnit c_arr[↑idx]
    | reducedToUnit l' =>
      match assignment[c_arr[↑idx].fst.val]! with
      | pos => if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l'
      | neg => if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l'
      | both => encounteredBoth
      | unassigned => reducedToNonunit
    | reducedToNonunit => reducedToNonunit) =
    reducedToUnit (i, b)
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
⊢ p ⊨ (i, b)
Tactic:
split at h
State after:
case right.h_1
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) encounteredBoth
h : encounteredBoth = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case right.h_2
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | neg => if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | both => encounteredBoth
    | unassigned => reducedToUnit c_arr[↑idx]) =
    reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case right.h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l'✝)
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l'✝
    | neg => if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l'✝
    | both => encounteredBoth
    | unassigned => reducedToNonunit) =
    reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case right.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToNonunit
h : reducedToNonunit = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

State before:
case right.h_1
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) encounteredBoth
h : encounteredBoth = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case right.h_2
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | neg => if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | both => encounteredBoth
    | unassigned => reducedToUnit c_arr[↑idx]) =
    reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case right.h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l'✝)
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l'✝
    | neg => if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l'✝
    | both => encounteredBoth
    | unassigned => reducedToNonunit) =
    reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case right.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToNonunit
h : reducedToNonunit = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
. simp only at h
State after:
case right.h_2
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | neg => if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | both => encounteredBoth
    | unassigned => reducedToUnit c_arr[↑idx]) =
    reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case right.h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l'✝)
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l'✝
    | neg => if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l'✝
    | both => encounteredBoth
    | unassigned => reducedToNonunit) =
    reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case right.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToNonunit
h : reducedToNonunit = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

State before:
case right.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToNonunit
h : reducedToNonunit = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
. simp only at h
State after:
no goals

State before:
case right.h_1
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) encounteredBoth
h : encounteredBoth = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
simp only at h
State after:
no goals

State before:
case right.h_2
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | neg => if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | both => encounteredBoth
    | unassigned => reducedToUnit c_arr[↑idx]) =
    reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
split at h
State after:
case right.h_2.h_1
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = pos
h : (if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty) = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case right.h_2.h_2
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = neg
h : (if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty) = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case right.h_2.h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = both
h : encounteredBoth = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case right.h_2.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToUnit c_arr[↑idx] = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

State before:
case right.h_2.h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = both
h : encounteredBoth = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case right.h_2.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToUnit c_arr[↑idx] = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
. simp only at h
State after:
case right.h_2.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToUnit c_arr[↑idx] = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

State before:
case right.h_2.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToUnit c_arr[↑idx] = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
. simp only [reducedToUnit.injEq] at h
  rw [← h]
  rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ j_lt_idx_add_one with j_lt_idx | j_eq_idx
  . exfalso
    rcases ih.1 rfl p with ih1 | ih1
    . exact ih1 j j_lt_idx p_entails_c_arr_j
    . exact ih1 hp
  . simp only [j_eq_idx] at p_entails_c_arr_j
    exact p_entails_c_arr_j
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : (if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty) = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
split at h
State after:
case isTrue
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h✝ : c_arr[↑idx].snd = true
h : reducedToUnit c_arr[↑idx] = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h✝ : ¬c_arr[↑idx].snd = true
h : False
⊢ p ⊨ (i, b)

State before:
case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h✝ : ¬c_arr[↑idx].snd = true
h : False
⊢ p ⊨ (i, b)
Tactic:
. exact False.elim h
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : reducedToUnit c_arr[↑idx] = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
simp only [reducedToUnit.injEq] at h
State after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : c_arr[↑idx] = (i, b)
⊢ p ⊨ (i, b)

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : c_arr[↑idx] = (i, b)
⊢ p ⊨ (i, b)
Tactic:
simp only [h] at c_arr_idx_eq_true
State after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
⊢ p ⊨ (i, b)

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : ∀ (i : PosFin n), hasAssignment (decide (p i = false)) assignment[i.val]! = false
⊢ p ⊨ (i, b)
Tactic:
specialize hp c_arr[idx.val].1
State after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) assignment[c_arr[↑idx].fst.val]! = false
⊢ p ⊨ (i, b)

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) assignment[c_arr[↑idx].fst.val]! = false
⊢ p ⊨ (i, b)
Tactic:
rw [heq] at hp
State after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) pos = false
⊢ p ⊨ (i, b)

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) pos = false
⊢ p ⊨ (i, b)
Tactic:
by_cases p c_arr[idx.val].1
State after:
case pos
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) pos = false
h✝ : p c_arr[↑idx].fst = true
⊢ p ⊨ (i, b)

case neg
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) pos = false
h✝ : ¬p c_arr[↑idx].fst = true
⊢ p ⊨ (i, b)

State before:
case neg
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) pos = false
h✝ : ¬p c_arr[↑idx].fst = true
⊢ p ⊨ (i, b)
Tactic:
. next p_c_arr_idx_eq_false =>
  simp only [h, Bool.not_eq_true] at p_c_arr_idx_eq_false
  simp (config := { decide := true }) only [h, p_c_arr_idx_eq_false] at hp
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) pos = false
p_c_arr_idx_eq_true : p c_arr[↑idx].fst = true
⊢ p ⊨ (i, b)
Tactic:
simp only [h] at p_c_arr_idx_eq_true
State after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) pos = false
p_c_arr_idx_eq_true : p i = true
⊢ p ⊨ (i, b)

State before:
case neg
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) pos = false
h✝ : ¬p c_arr[↑idx].fst = true
⊢ p ⊨ (i, b)
Tactic:
next p_c_arr_idx_eq_false =>
simp only [h, Bool.not_eq_true] at p_c_arr_idx_eq_false
simp (config := { decide := true }) only [h, p_c_arr_idx_eq_false] at hp
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) pos = false
p_c_arr_idx_eq_false : ¬p c_arr[↑idx].fst = true
⊢ p ⊨ (i, b)
Tactic:
simp only [h, Bool.not_eq_true] at p_c_arr_idx_eq_false
State after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) pos = false
p_c_arr_idx_eq_false : p i = false
⊢ p ⊨ (i, b)

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) pos = false
p_c_arr_idx_eq_false : p i = false
⊢ p ⊨ (i, b)
Tactic:
simp (config := { decide := true }) only [h, p_c_arr_idx_eq_false] at hp
State after:
no goals

State before:
case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h✝ : ¬c_arr[↑idx].snd = true
h : False
⊢ p ⊨ (i, b)
Tactic:
exact False.elim h
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : (if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty) = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
split at h
State after:
case isTrue
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : (!c_arr[↑idx].snd) = true
h : reducedToUnit c_arr[↑idx] = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : ¬(!c_arr[↑idx].snd) = true
h : False
⊢ p ⊨ (i, b)

State before:
case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : ¬(!c_arr[↑idx].snd) = true
h : False
⊢ p ⊨ (i, b)
Tactic:
. exact False.elim h
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : (!c_arr[↑idx].snd) = true
h : reducedToUnit c_arr[↑idx] = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
simp only [reducedToUnit.injEq] at h
State after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : (!c_arr[↑idx].snd) = true
h : c_arr[↑idx] = (i, b)
⊢ p ⊨ (i, b)

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : (!c_arr[↑idx].snd) = true
h : c_arr[↑idx] = (i, b)
⊢ p ⊨ (i, b)
Tactic:
simp only [h, Bool.not_eq_true'] at c_arr_idx_eq_true
State after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = false
⊢ p ⊨ (i, b)

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = false
hp : ∀ (i : PosFin n), hasAssignment (decide (p i = false)) assignment[i.val]! = false
⊢ p ⊨ (i, b)
Tactic:
specialize hp c_arr[idx.val].1
State after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) assignment[c_arr[↑idx].fst.val]! = false
⊢ p ⊨ (i, b)

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) assignment[c_arr[↑idx].fst.val]! = false
⊢ p ⊨ (i, b)
Tactic:
rw [heq] at hp
State after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) neg = false
⊢ p ⊨ (i, b)

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) neg = false
⊢ p ⊨ (i, b)
Tactic:
by_cases p c_arr[idx.val].1
State after:
case pos
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) neg = false
h✝ : p c_arr[↑idx].fst = true
⊢ p ⊨ (i, b)

case neg
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) neg = false
h✝ : ¬p c_arr[↑idx].fst = true
⊢ p ⊨ (i, b)

State before:
case pos
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) neg = false
h✝ : p c_arr[↑idx].fst = true
⊢ p ⊨ (i, b)

case neg
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) neg = false
h✝ : ¬p c_arr[↑idx].fst = true
⊢ p ⊨ (i, b)
Tactic:
. next p_c_arr_idx_eq_true =>
  simp only [h, Bool.not_eq_true] at p_c_arr_idx_eq_true
  simp (config := { decide := true }) only [h, p_c_arr_idx_eq_true] at hp
State after:
case neg
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) neg = false
h✝ : ¬p c_arr[↑idx].fst = true
⊢ p ⊨ (i, b)

State before:
case pos
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) neg = false
h✝ : p c_arr[↑idx].fst = true
⊢ p ⊨ (i, b)
Tactic:
next p_c_arr_idx_eq_true =>
simp only [h, Bool.not_eq_true] at p_c_arr_idx_eq_true
simp (config := { decide := true }) only [h, p_c_arr_idx_eq_true] at hp
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) neg = false
p_c_arr_idx_eq_true : p c_arr[↑idx].fst = true
⊢ p ⊨ (i, b)
Tactic:
simp only [h, Bool.not_eq_true] at p_c_arr_idx_eq_true
State after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) neg = false
p_c_arr_idx_eq_true : p i = true
⊢ p ⊨ (i, b)

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) neg = false
p_c_arr_idx_eq_true : p i = true
⊢ p ⊨ (i, b)
Tactic:
simp (config := { decide := true }) only [h, p_c_arr_idx_eq_true] at hp
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) neg = false
p_c_arr_idx_eq_false : ¬p c_arr[↑idx].fst = true
⊢ p ⊨ (i, b)
Tactic:
simp only [h] at p_c_arr_idx_eq_false
State after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : c_arr[↑idx] = (i, b)
c_arr_idx_eq_true : b = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) neg = false
p_c_arr_idx_eq_false : ¬p i = true
⊢ p ⊨ (i, b)

State before:
case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : ¬(!c_arr[↑idx].snd) = true
h : False
⊢ p ⊨ (i, b)
Tactic:
exact False.elim h
State after:
no goals

State before:
case right.h_2.h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = both
h : encounteredBoth = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
simp only at h
State after:
no goals

State before:
case right.h_2.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToUnit c_arr[↑idx] = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
simp only [reducedToUnit.injEq] at h
State after:
case right.h_2.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
⊢ p ⊨ (i, b)

State before:
case right.h_2.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
⊢ p ⊨ (i, b)
Tactic:
rw [← h]
State after:
case right.h_2.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
⊢ p ⊨ c_arr[↑idx]

State before:
case right.h_2.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
⊢ p ⊨ c_arr[↑idx]
Tactic:
rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ j_lt_idx_add_one with j_lt_idx | j_eq_idx
State after:
case right.h_2.h_4.inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ c_arr[↑idx]

case right.h_2.h_4.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ c_arr[↑idx]

State before:
case right.h_2.h_4.inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ c_arr[↑idx]

case right.h_2.h_4.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ c_arr[↑idx]
Tactic:
. exfalso
  rcases ih.1 rfl p with ih1 | ih1
  . exact ih1 j j_lt_idx p_entails_c_arr_j
  . exact ih1 hp
State after:
case right.h_2.h_4.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ c_arr[↑idx]

State before:
case right.h_2.h_4.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ c_arr[↑idx]
Tactic:
. simp only [j_eq_idx] at p_entails_c_arr_j
  exact p_entails_c_arr_j
State after:
no goals

State before:
case right.h_2.h_4.inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ c_arr[↑idx]
Tactic:
exfalso
State after:
case right.h_2.h_4.inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ False

State before:
case right.h_2.h_4.inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ False
Tactic:
rcases ih.1 rfl p with ih1 | ih1
State after:
case right.h_2.h_4.inl.inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
⊢ False

case right.h_2.h_4.inl.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
ih1 : ¬(p ⊨ assignment)
⊢ False

State before:
case right.h_2.h_4.inl.inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
⊢ False

case right.h_2.h_4.inl.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
ih1 : ¬(p ⊨ assignment)
⊢ False
Tactic:
. exact ih1 j j_lt_idx p_entails_c_arr_j
State after:
case right.h_2.h_4.inl.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
ih1 : ¬(p ⊨ assignment)
⊢ False

State before:
case right.h_2.h_4.inl.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
ih1 : ¬(p ⊨ assignment)
⊢ False
Tactic:
. exact ih1 hp
State after:
no goals

State before:
case right.h_2.h_4.inl.inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
ih1 : ∀ (i : Fin c_arr.size), ↑i < ↑idx → ¬(p ⊨ c_arr[i])
⊢ False
Tactic:
exact ih1 j j_lt_idx p_entails_c_arr_j
State after:
no goals

State before:
case right.h_2.h_4.inl.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_lt_idx : ↑j < ↑idx
ih1 : ¬(p ⊨ assignment)
⊢ False
Tactic:
exact ih1 hp
State after:
no goals

State before:
case right.h_2.h_4.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ c_arr[↑idx]
Tactic:
simp only [j_eq_idx] at p_entails_c_arr_j
State after:
case right.h_2.h_4.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_eq_idx : ↑j = ↑idx
p_entails_c_arr_j : p ⊨ c_arr[↑idx]
⊢ p ⊨ c_arr[↑idx]

State before:
case right.h_2.h_4.inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : c_arr[↑idx] = (i, b)
j_eq_idx : ↑j = ↑idx
p_entails_c_arr_j : p ⊨ c_arr[↑idx]
⊢ p ⊨ c_arr[↑idx]
Tactic:
exact p_entails_c_arr_j
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l
    | neg => if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l
    | both => encounteredBoth
    | unassigned => reducedToNonunit) =
    reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
split at h
State after:
case h_1
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = pos
h : (if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l) = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case h_2
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = neg
h : (if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l) = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = both
h : encounteredBoth = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToNonunit = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

State before:
case h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = both
h : encounteredBoth = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToNonunit = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
. simp only at h
State after:
case h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToNonunit = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

State before:
case h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToNonunit = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
. simp only at h
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : (if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l) = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
split at h
State after:
case isTrue
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h✝ : c_arr[↑idx].snd = true
h : False
⊢ p ⊨ (i, b)

case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h✝ : ¬c_arr[↑idx].snd = true
h : reducedToUnit l = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

State before:
case isTrue
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h✝ : c_arr[↑idx].snd = true
h : False
⊢ p ⊨ (i, b)

case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h✝ : ¬c_arr[↑idx].snd = true
h : reducedToUnit l = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
. exact False.elim h
State after:
case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h✝ : ¬c_arr[↑idx].snd = true
h : reducedToUnit l = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

State before:
case isTrue
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h✝ : c_arr[↑idx].snd = true
h : False
⊢ p ⊨ (i, b)
Tactic:
exact False.elim h
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : ¬c_arr[↑idx].snd = true
h : reducedToUnit l = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
simp only [Bool.not_eq_true] at c_arr_idx_eq_false
State after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToUnit l = reducedToUnit (i, b)
c_arr_idx_eq_false : c_arr[↑idx].snd = false
⊢ p ⊨ (i, b)

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
h : reducedToUnit l = reducedToUnit (i, b)
c_arr_idx_eq_false : c_arr[↑idx].snd = false
⊢ p ⊨ (i, b)
Tactic:
simp only [reducedToUnit.injEq] at h
State after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
⊢ p ⊨ (i, b)

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
⊢ p ⊨ (i, b)
Tactic:
rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ j_lt_idx_add_one with j_lt_idx | j_eq_idx
State after:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ (i, b)

case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ (i, b)

State before:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ (i, b)

case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ (i, b)
Tactic:
. rw [← h]
  have ih2_precondition : ∃ i : Fin c_arr.size, i.val < idx.val ∧ (p ⊨ c_arr[i]) :=
    (Exists.intro j ∘ And.intro j_lt_idx) p_entails_c_arr_j
  exact ih.2 l rfl p hp ih2_precondition
State after:
case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ (i, b)

State before:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ (i, b)
Tactic:
rw [← h]
State after:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ l

State before:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ l
Tactic:
have ih2_precondition : ∃ i : Fin c_arr.size, i.val < idx.val ∧ (p ⊨ c_arr[i]) :=
  (Exists.intro j ∘ And.intro j_lt_idx) p_entails_c_arr_j
State after:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
ih2_precondition : ∃ i, ↑i < ↑idx ∧ (p ⊨ c_arr[i])
⊢ p ⊨ l

State before:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
ih2_precondition : ∃ i, ↑i < ↑idx ∧ (p ⊨ c_arr[i])
⊢ p ⊨ l
Tactic:
exact ih.2 l rfl p hp ih2_precondition
State after:
no goals

State before:
case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
p_entails_c_arr_j : p c_arr[↑idx].fst = false
hp : ∀ (i : PosFin n), hasAssignment (decide (p i = false)) assignment[i.val]! = false
⊢ p ⊨ (i, b)
Tactic:
specialize hp c_arr[idx.1].1
State after:
case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
p_entails_c_arr_j : p c_arr[↑idx].fst = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) assignment[c_arr[↑idx].fst.val]! = false
⊢ p ⊨ (i, b)

State before:
case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = pos
c_arr_idx_eq_false : c_arr[↑idx].snd = false
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
p_entails_c_arr_j : p c_arr[↑idx].fst = false
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) assignment[c_arr[↑idx].fst.val]! = false
⊢ p ⊨ (i, b)
Tactic:
simp (config := { decide := true }) only [p_entails_c_arr_j, decide_True, heq] at hp
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : (if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l) = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
split at h
State after:
case isTrue
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : (!c_arr[↑idx].snd) = true
h : False
⊢ p ⊨ (i, b)

case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : ¬(!c_arr[↑idx].snd) = true
h : reducedToUnit l = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

State before:
case isTrue
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : (!c_arr[↑idx].snd) = true
h : False
⊢ p ⊨ (i, b)

case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : ¬(!c_arr[↑idx].snd) = true
h : reducedToUnit l = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
. exact False.elim h
State after:
case isFalse
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : ¬(!c_arr[↑idx].snd) = true
h : reducedToUnit l = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

State before:
case isTrue
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h✝ : (!c_arr[↑idx].snd) = true
h : False
⊢ p ⊨ (i, b)
Tactic:
exact False.elim h
State after:
no goals

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : ¬(!c_arr[↑idx].snd) = true
h : reducedToUnit l = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
simp only [Bool.not_eq_true', Bool.not_eq_false] at c_arr_idx_eq_true
State after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToUnit l = reducedToUnit (i, b)
c_arr_idx_eq_true : c_arr[↑idx].snd = true
⊢ p ⊨ (i, b)

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
h : reducedToUnit l = reducedToUnit (i, b)
c_arr_idx_eq_true : c_arr[↑idx].snd = true
⊢ p ⊨ (i, b)
Tactic:
simp only [reducedToUnit.injEq] at h
State after:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
⊢ p ⊨ (i, b)

State before:
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
⊢ p ⊨ (i, b)
Tactic:
rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ j_lt_idx_add_one with j_lt_idx | j_eq_idx
State after:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ (i, b)

case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ (i, b)

State before:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ (i, b)

case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ (i, b)
Tactic:
. rw [← h]
  have ih2_precondition : ∃ i : Fin c_arr.size, i.val < idx.val ∧ (p ⊨ c_arr[i]) :=
    (Exists.intro j ∘ And.intro j_lt_idx) p_entails_c_arr_j
  exact ih.2 l rfl p hp ih2_precondition
State after:
case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
⊢ p ⊨ (i, b)

State before:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ (i, b)
Tactic:
rw [← h]
State after:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ l

State before:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
⊢ p ⊨ l
Tactic:
have ih2_precondition : ∃ i : Fin c_arr.size, i.val < idx.val ∧ (p ⊨ c_arr[i]) :=
  (Exists.intro j ∘ And.intro j_lt_idx) p_entails_c_arr_j
State after:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
ih2_precondition : ∃ i, ↑i < ↑idx ∧ (p ⊨ c_arr[i])
⊢ p ⊨ l

State before:
case inl
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_lt_idx : ↑j < ↑idx
ih2_precondition : ∃ i, ↑i < ↑idx ∧ (p ⊨ c_arr[i])
⊢ p ⊨ l
Tactic:
exact ih.2 l rfl p hp ih2_precondition
State after:
no goals

State before:
case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
p_entails_c_arr_j : p c_arr[↑idx].fst = true
hp : ∀ (i : PosFin n), hasAssignment (decide (p i = false)) assignment[i.val]! = false
⊢ p ⊨ (i, b)
Tactic:
specialize hp c_arr[idx.1].1
State after:
case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
p_entails_c_arr_j : p c_arr[↑idx].fst = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) assignment[c_arr[↑idx].fst.val]! = false
⊢ p ⊨ (i, b)

State before:
case inr
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq : assignment[c_arr[↑idx].fst.val]! = neg
c_arr_idx_eq_true : c_arr[↑idx].snd = true
h : l = (i, b)
j_eq_idx : ↑j = ↑idx
p_entails_c_arr_j : p c_arr[↑idx].fst = true
hp : hasAssignment (decide (p c_arr[↑idx].fst = false)) assignment[c_arr[↑idx].fst.val]! = false
⊢ p ⊨ (i, b)
Tactic:
simp (config := { decide := true }) only [p_entails_c_arr_j, decide_True, heq] at hp
State after:
no goals

State before:
case h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = both
h : encounteredBoth = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
simp only at h
State after:
no goals

State before:
case h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l)
x✝ : Assignment
heq✝ : assignment[c_arr[↑idx].fst.val]! = unassigned
h : reducedToNonunit = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
simp only at h
State after:
no goals

State before:
case right.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToNonunit
h : reducedToNonunit = reducedToUnit (i, b)
⊢ p ⊨ (i, b)
Tactic:
simp only at h
State after:
no goals