Theorem: Misc.Array.range_idx (LeanSAT/Util/Misc.lean)

State before:
n x : Nat
h : x < n
⊢ x < (Array.range n).size
Tactic:
rw [Array.range_size]
State after:
n x : Nat
h : x < n
⊢ x < n

State before:
n x : Nat
h : x < n
⊢ x < n
Tactic:
exact h
State after:
no goals

State before:
n x : Nat
h : x < n
⊢ (Array.range n)[x] = x
Tactic:
induction n
State after:
case zero
x : Nat
h : x < 0
⊢ (Array.range 0)[x] = x

case succ
x n✝ : Nat
a✝ : ∀ (h : x < n✝), (Array.range n✝)[x] = x
h : x < n✝ + 1
⊢ (Array.range (n✝ + 1))[x] = x

State before:
case zero
x : Nat
h : x < 0
⊢ (Array.range 0)[x] = x

case succ
x n✝ : Nat
a✝ : ∀ (h : x < n✝), (Array.range n✝)[x] = x
h : x < n✝ + 1
⊢ (Array.range (n✝ + 1))[x] = x
Tactic:
. contradiction
State after:
case succ
x n✝ : Nat
a✝ : ∀ (h : x < n✝), (Array.range n✝)[x] = x
h : x < n✝ + 1
⊢ (Array.range (n✝ + 1))[x] = x

State before:
case succ
x n✝ : Nat
a✝ : ∀ (h : x < n✝), (Array.range n✝)[x] = x
h : x < n✝ + 1
⊢ (Array.range (n✝ + 1))[x] = x
Tactic:
. next n ih =>
  rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ h with x_lt_n | x_eq_n
  . specialize ih x_lt_n
    simp only [Array.range, Nat.fold, flip, Array.get_push]
    simp only [Array.range, flip] at ih
    split
    . exact ih
    . next x_ge_n =>
      exfalso
      have h_range_size : (Array.range n).size = n := Array.range_size
      simp only [Array.mkEmpty_eq, Array.range, flip] at h_range_size
      simp only [Array.mkEmpty_eq, h_range_size] at x_ge_n
      exact x_ge_n x_lt_n
  . simp only [Array.range, Nat.fold, flip, Array.get_push]
    split
    . next x_lt_n =>
      exfalso
      have h_range_size : (Array.range n).size = n := Array.range_size
      simp only [Array.range, Array.mkEmpty_eq] at h_range_size
      simp only [x_eq_n, Array.mkEmpty_eq, h_range_size, Nat.lt_irrefl] at x_lt_n
    . rw [x_eq_n]
State after:
no goals

State before:
case zero
x : Nat
h : x < 0
⊢ (Array.range 0)[x] = x
Tactic:
contradiction
State after:
no goals

State before:
case succ
x n✝ : Nat
a✝ : ∀ (h : x < n✝), (Array.range n✝)[x] = x
h : x < n✝ + 1
⊢ (Array.range (n✝ + 1))[x] = x
Tactic:
next n ih =>
rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ h with x_lt_n | x_eq_n
. specialize ih x_lt_n
  simp only [Array.range, Nat.fold, flip, Array.get_push]
  simp only [Array.range, flip] at ih
  split
  . exact ih
  . next x_ge_n =>
    exfalso
    have h_range_size : (Array.range n).size = n := Array.range_size
    simp only [Array.mkEmpty_eq, Array.range, flip] at h_range_size
    simp only [Array.mkEmpty_eq, h_range_size] at x_ge_n
    exact x_ge_n x_lt_n
. simp only [Array.range, Nat.fold, flip, Array.get_push]
  split
  . next x_lt_n =>
    exfalso
    have h_range_size : (Array.range n).size = n := Array.range_size
    simp only [Array.range, Array.mkEmpty_eq] at h_range_size
    simp only [x_eq_n, Array.mkEmpty_eq, h_range_size, Nat.lt_irrefl] at x_lt_n
  . rw [x_eq_n]
State after:
no goals

State before:
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
⊢ (Array.range (n + 1))[x] = x
Tactic:
rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ h with x_lt_n | x_eq_n
State after:
case inl
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_lt_n : x < n
⊢ (Array.range (n + 1))[x] = x

case inr
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
⊢ (Array.range (n + 1))[x] = x

State before:
case inl
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_lt_n : x < n
⊢ (Array.range (n + 1))[x] = x

case inr
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
⊢ (Array.range (n + 1))[x] = x
Tactic:
. specialize ih x_lt_n
  simp only [Array.range, Nat.fold, flip, Array.get_push]
  simp only [Array.range, flip] at ih
  split
  . exact ih
  . next x_ge_n =>
    exfalso
    have h_range_size : (Array.range n).size = n := Array.range_size
    simp only [Array.mkEmpty_eq, Array.range, flip] at h_range_size
    simp only [Array.mkEmpty_eq, h_range_size] at x_ge_n
    exact x_ge_n x_lt_n
State after:
case inr
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
⊢ (Array.range (n + 1))[x] = x

State before:
case inr
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
⊢ (Array.range (n + 1))[x] = x
Tactic:
. simp only [Array.range, Nat.fold, flip, Array.get_push]
  split
  . next x_lt_n =>
    exfalso
    have h_range_size : (Array.range n).size = n := Array.range_size
    simp only [Array.range, Array.mkEmpty_eq] at h_range_size
    simp only [x_eq_n, Array.mkEmpty_eq, h_range_size, Nat.lt_irrefl] at x_lt_n
  . rw [x_eq_n]
State after:
no goals

State before:
case inl
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_lt_n : x < n
⊢ (Array.range (n + 1))[x] = x
Tactic:
specialize ih x_lt_n
State after:
case inl
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Array.range n)[x] = x
⊢ (Array.range (n + 1))[x] = x

State before:
case inl
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Array.range n)[x] = x
⊢ (Array.range (n + 1))[x] = x
Tactic:
simp only [Array.range, Nat.fold, flip, Array.get_push]
State after:
case inl
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Array.range n)[x] = x
⊢ (if h : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size then
      (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x]
    else n) =
    x

State before:
case inl
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Array.range n)[x] = x
⊢ (if h : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size then
      (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x]
    else n) =
    x
Tactic:
simp only [Array.range, flip] at ih
State after:
case inl
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
⊢ (if h : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size then
      (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x]
    else n) =
    x

State before:
case inl
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
⊢ (if h : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size then
      (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x]
    else n) =
    x
Tactic:
split
State after:
case inl.isTrue
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h✝ : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x] = x

case inl.isFalse
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x

State before:
case inl.isTrue
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h✝ : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x] = x

case inl.isFalse
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x
Tactic:
. exact ih
State after:
case inl.isFalse
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x

State before:
case inl.isFalse
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x
Tactic:
. next x_ge_n =>
  exfalso
  have h_range_size : (Array.range n).size = n := Array.range_size
  simp only [Array.mkEmpty_eq, Array.range, flip] at h_range_size
  simp only [Array.mkEmpty_eq, h_range_size] at x_ge_n
  exact x_ge_n x_lt_n
State after:
no goals

State before:
case inl.isTrue
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h✝ : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x] = x
Tactic:
exact ih
State after:
no goals

State before:
case inl.isFalse
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x
Tactic:
next x_ge_n =>
exfalso
have h_range_size : (Array.range n).size = n := Array.range_size
simp only [Array.mkEmpty_eq, Array.range, flip] at h_range_size
simp only [Array.mkEmpty_eq, h_range_size] at x_ge_n
exact x_ge_n x_lt_n
State after:
no goals

State before:
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
x_ge_n : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x
Tactic:
exfalso
State after:
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
x_ge_n : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ False

State before:
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
x_ge_n : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ False
Tactic:
have h_range_size : (Array.range n).size = n := Array.range_size
State after:
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
x_ge_n : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
h_range_size : (Array.range n).size = n
⊢ False

State before:
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
x_ge_n : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
h_range_size : (Array.range n).size = n
⊢ False
Tactic:
simp only [Array.mkEmpty_eq, Array.range, flip] at h_range_size
State after:
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
x_ge_n : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
h_range_size : (Nat.fold (flip Array.push) n #[]).size = n
⊢ False

State before:
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
x_ge_n : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
h_range_size : (Nat.fold (flip Array.push) n #[]).size = n
⊢ False
Tactic:
simp only [Array.mkEmpty_eq, h_range_size] at x_ge_n
State after:
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h_range_size : (Nat.fold (flip Array.push) n #[]).size = n
x_ge_n : ¬x < n
⊢ False

State before:
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h_range_size : (Nat.fold (flip Array.push) n #[]).size = n
x_ge_n : ¬x < n
⊢ False
Tactic:
exact x_ge_n x_lt_n
State after:
no goals

State before:
case inr
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
⊢ (Array.range (n + 1))[x] = x
Tactic:
simp only [Array.range, Nat.fold, flip, Array.get_push]
State after:
case inr
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
⊢ (if h : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size then
      (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x]
    else n) =
    x

State before:
case inr
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
⊢ (if h : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size then
      (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x]
    else n) =
    x
Tactic:
split
State after:
case inr.isTrue
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
h✝ : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x] = x

case inr.isFalse
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x

State before:
case inr.isTrue
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
h✝ : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x] = x

case inr.isFalse
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x
Tactic:
. next x_lt_n =>
  exfalso
  have h_range_size : (Array.range n).size = n := Array.range_size
  simp only [Array.range, Array.mkEmpty_eq] at h_range_size
  simp only [x_eq_n, Array.mkEmpty_eq, h_range_size, Nat.lt_irrefl] at x_lt_n
State after:
case inr.isFalse
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x

State before:
case inr.isFalse
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x
Tactic:
. rw [x_eq_n]
State after:
no goals

State before:
case inr.isTrue
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
h✝ : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x] = x
Tactic:
next x_lt_n =>
exfalso
have h_range_size : (Array.range n).size = n := Array.range_size
simp only [Array.range, Array.mkEmpty_eq] at h_range_size
simp only [x_eq_n, Array.mkEmpty_eq, h_range_size, Nat.lt_irrefl] at x_lt_n
State after:
no goals

State before:
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
x_lt_n : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x] = x
Tactic:
exfalso
State after:
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
x_lt_n : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ False

State before:
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
x_lt_n : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ False
Tactic:
have h_range_size : (Array.range n).size = n := Array.range_size
State after:
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
x_lt_n : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
h_range_size : (Array.range n).size = n
⊢ False

State before:
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
x_lt_n : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
h_range_size : (Array.range n).size = n
⊢ False
Tactic:
simp only [Array.range, Array.mkEmpty_eq] at h_range_size
State after:
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
x_lt_n : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
h_range_size : (Nat.fold (flip Array.push) n #[]).size = n
⊢ False

State before:
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
x_lt_n : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
h_range_size : (Nat.fold (flip Array.push) n #[]).size = n
⊢ False
Tactic:
simp only [x_eq_n, Array.mkEmpty_eq, h_range_size, Nat.lt_irrefl] at x_lt_n
State after:
no goals

State before:
case inr.isFalse
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x
Tactic:
rw [x_eq_n]
State after:
no goals