Theorem: List.List.getF_implies_mem (MLIR/Util/List.lean)

State before:
⊢ ∀ {α : Type} (xs : List α) (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
Tactic:
intros α xs
State after:
α : Type
xs : List α
⊢ ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs

State before:
α : Type
xs : List α
⊢ ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
Tactic:
induction xs
State after:
case nil
α : Type
⊢ ∀ (i : ℕ) (INBOUND : i < length []), Mem (getF [] i INBOUND) []

case cons
α : Type
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (i : ℕ) (INBOUND : i < length tail✝), Mem (getF tail✝ i INBOUND) tail✝
⊢ ∀ (i : ℕ) (INBOUND : i < length (head✝ :: tail✝)), Mem (getF (head✝ :: tail✝) i INBOUND) (head✝ :: tail✝)

State before:
α : Type
⊢ ∀ (i : ℕ) (INBOUND : i < length []), Mem (getF [] i INBOUND) []
Tactic:
case nil => {
  intros i INBOUND; simp at INBOUND;
}
State after:
no goals

State before:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
⊢ ∀ (i : ℕ) (INBOUND : i < length (x' :: xs)), Mem (getF (x' :: xs) i INBOUND) (x' :: xs)
Tactic:
case cons x' xs IH => {
  intros i INBOUND;
  cases i;
  case zero => {
     simp [List.getF];
     constructor;
  }
  case succ i' => {
   simp [List.getF];
   constructor;
   apply IH;
 }
}
State after:
no goals

State before:
α : Type
⊢ ∀ (i : ℕ) (INBOUND : i < length []), Mem (getF [] i INBOUND) []
Tactic:
intros i INBOUND
State after:
α : Type
i : ℕ
INBOUND : i < length []
⊢ Mem (getF [] i INBOUND) []

State before:
α : Type
i : ℕ
INBOUND : i < length []
⊢ Mem (getF [] i INBOUND) []
Tactic:
simp at INBOUND
State after:
no goals

State before:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
⊢ ∀ (i : ℕ) (INBOUND : i < length (x' :: xs)), Mem (getF (x' :: xs) i INBOUND) (x' :: xs)
Tactic:
intros i INBOUND
State after:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
i : ℕ
INBOUND : i < length (x' :: xs)
⊢ Mem (getF (x' :: xs) i INBOUND) (x' :: xs)

State before:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
i : ℕ
INBOUND : i < length (x' :: xs)
⊢ Mem (getF (x' :: xs) i INBOUND) (x' :: xs)
Tactic:
cases i
State after:
case zero
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
INBOUND : Nat.zero < length (x' :: xs)
⊢ Mem (getF (x' :: xs) Nat.zero INBOUND) (x' :: xs)

case succ
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
n✝ : ℕ
INBOUND : Nat.succ n✝ < length (x' :: xs)
⊢ Mem (getF (x' :: xs) (Nat.succ n✝) INBOUND) (x' :: xs)

State before:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
INBOUND : Nat.zero < length (x' :: xs)
⊢ Mem (getF (x' :: xs) Nat.zero INBOUND) (x' :: xs)
Tactic:
case zero => {
   simp [List.getF];
   constructor;
}
State after:
no goals

State before:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
i' : ℕ
INBOUND : Nat.succ i' < length (x' :: xs)
⊢ Mem (getF (x' :: xs) (Nat.succ i') INBOUND) (x' :: xs)
Tactic:
case succ i' => {
 simp [List.getF];
 constructor;
 apply IH;
}
State after:
no goals

State before:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
INBOUND : Nat.zero < length (x' :: xs)
⊢ Mem (getF (x' :: xs) Nat.zero INBOUND) (x' :: xs)
Tactic:
simp [List.getF]
State after:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
INBOUND : Nat.zero < length (x' :: xs)
⊢ Mem x' (x' :: xs)

State before:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
INBOUND : Nat.zero < length (x' :: xs)
⊢ Mem x' (x' :: xs)
Tactic:
constructor
State after:
no goals

State before:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
i' : ℕ
INBOUND : Nat.succ i' < length (x' :: xs)
⊢ Mem (getF (x' :: xs) (Nat.succ i') INBOUND) (x' :: xs)
Tactic:
simp [List.getF]
State after:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
i' : ℕ
INBOUND : Nat.succ i' < length (x' :: xs)
⊢ Mem (getF xs i' (_ : i' < length xs)) (x' :: xs)

State before:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
i' : ℕ
INBOUND : Nat.succ i' < length (x' :: xs)
⊢ Mem (getF xs i' (_ : i' < length xs)) (x' :: xs)
Tactic:
constructor
State after:
case a
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
i' : ℕ
INBOUND : Nat.succ i' < length (x' :: xs)
⊢ Mem (getF xs i' (_ : i' < length xs)) xs

State before:
case a
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
i' : ℕ
INBOUND : Nat.succ i' < length (x' :: xs)
⊢ Mem (getF xs i' (_ : i' < length xs)) xs
Tactic:
apply IH
State after:
no goals