[GOAL]
α : Type u_1
n : ℕ
xs : Vector α n
x : α
⊢ reverse (x ::ᵥ xs) = snoc (reverse xs) x
[PROOFSTEP]
cases xs
[GOAL]
case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ reverse (x ::ᵥ { val := val✝, property := property✝ }) = snoc (reverse { val := val✝, property := property✝ }) x
[PROOFSTEP]
simp only [reverse, cons, toList_mk, List.reverse_cons, snoc]
[GOAL]
case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ { val := List.reverse val✝ ++ [x],
      property := (_ : (fun l => List.length l = Nat.succ n) (List.reverse val✝ ++ [x])) } =
    append { val := List.reverse val✝, property := (_ : (fun l => List.length l = n) (List.reverse val✝)) }
      { val := [x], property := (_ : Nat.succ (List.length []) = Nat.succ 0) }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
n : ℕ
xs : Vector α n
x : α
⊢ reverse (snoc xs x) = x ::ᵥ reverse xs
[PROOFSTEP]
cases xs
[GOAL]
case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ reverse (snoc { val := val✝, property := property✝ } x) = x ::ᵥ reverse { val := val✝, property := property✝ }
[PROOFSTEP]
simp only [reverse, snoc, cons, toList_mk]
[GOAL]
case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ {
      val :=
        List.reverse
          (toList
            (append { val := val✝, property := property✝ }
              { val := [x], property := (_ : Nat.succ (List.length []) = Nat.succ 0) })),
      property :=
        (_ :
          (fun l => List.length l = n + 1)
            (List.reverse
              (toList
                (append { val := val✝, property := property✝ }
                  { val := [x], property := (_ : Nat.succ (List.length []) = Nat.succ 0) })))) } =
    { val := x :: List.reverse val✝, property := (_ : Nat.succ (List.length (List.reverse val✝)) = Nat.succ n) }
[PROOFSTEP]
congr
[GOAL]
case mk.e_val
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ List.reverse
      (toList
        (append { val := val✝, property := property✝ }
          { val := [x], property := (_ : Nat.succ (List.length []) = Nat.succ 0) })) =
    x :: List.reverse val✝
[PROOFSTEP]
simp [toList, (· ++ ·), Vector.append, Append.append]
[GOAL]
case mk.e_val
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ [] ++ [x] ++ List.reverse val✝ = x :: List.reverse val✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
n : ℕ
xs : Vector α n
val : α
⊢ replicate (n + 1) val = snoc (replicate n val) val
[PROOFSTEP]
clear xs
[GOAL]
α : Type u_1
n : ℕ
val : α
⊢ replicate (n + 1) val = snoc (replicate n val) val
[PROOFSTEP]
induction n
[GOAL]
case zero
α : Type u_1
n : ℕ
val : α
⊢ replicate (Nat.zero + 1) val = snoc (replicate Nat.zero val) val
case succ
α : Type u_1
n : ℕ
val : α
n✝ : ℕ
n_ih✝ : replicate (n✝ + 1) val = snoc (replicate n✝ val) val
⊢ replicate (Nat.succ n✝ + 1) val = snoc (replicate (Nat.succ n✝) val) val
[PROOFSTEP]
case zero => rfl
[GOAL]
α : Type u_1
n : ℕ
val : α
⊢ replicate (Nat.zero + 1) val = snoc (replicate Nat.zero val) val
[PROOFSTEP]
case zero => rfl
[GOAL]
α : Type u_1
n : ℕ
val : α
⊢ replicate (Nat.zero + 1) val = snoc (replicate Nat.zero val) val
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
n : ℕ
val : α
n✝ : ℕ
n_ih✝ : replicate (n✝ + 1) val = snoc (replicate n✝ val) val
⊢ replicate (Nat.succ n✝ + 1) val = snoc (replicate (Nat.succ n✝) val) val
[PROOFSTEP]
case succ n ih =>
  rw [replicate_succ]
  conv => {rhs; rw [replicate_succ]}
  rw [snoc_cons, ih]
[GOAL]
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = snoc (replicate n val) val
⊢ replicate (Nat.succ n + 1) val = snoc (replicate (Nat.succ n) val) val
[PROOFSTEP]
case succ n ih =>
  rw [replicate_succ]
  conv => {rhs; rw [replicate_succ]}
  rw [snoc_cons, ih]
[GOAL]
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = snoc (replicate n val) val
⊢ replicate (Nat.succ n + 1) val = snoc (replicate (Nat.succ n) val) val
[PROOFSTEP]
rw [replicate_succ]
[GOAL]
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = snoc (replicate n val) val
⊢ val ::ᵥ replicate (n + 1) val = snoc (replicate (Nat.succ n) val) val
[PROOFSTEP]
conv => {rhs; rw [replicate_succ]}
[GOAL]
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = snoc (replicate n val) val
| val ::ᵥ replicate (n + 1) val = snoc (replicate (Nat.succ n) val) val
[PROOFSTEP]
{rhs; rw [replicate_succ]}
[GOAL]
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = snoc (replicate n val) val
| val ::ᵥ replicate (n + 1) val = snoc (replicate (Nat.succ n) val) val
[PROOFSTEP]
{rhs; rw [replicate_succ]}
[GOAL]
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = snoc (replicate n val) val
| val ::ᵥ replicate (n + 1) val = snoc (replicate (Nat.succ n) val) val
[PROOFSTEP]
rhs
[GOAL]
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = snoc (replicate n val) val
| snoc (replicate (Nat.succ n) val) val
[PROOFSTEP]
rw [replicate_succ]
[GOAL]
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = snoc (replicate n val) val
⊢ val ::ᵥ replicate (n + 1) val = snoc (val ::ᵥ replicate n val) val
[PROOFSTEP]
rw [snoc_cons, ih]
[GOAL]
α : Type ?u.2475
C : {n : ℕ} → Vector α n → Sort u_1
n : ℕ
v : Vector α n
nil : C Vector.nil
snoc : {n : ℕ} → (xs : Vector α n) → (x : α) → C xs → C (Vector.snoc xs x)
⊢ (fun {n} v => C (reverse v)) (reverse v) = C v
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.2475
C : {n : ℕ} → Vector α n → Sort u_1
n✝ : ℕ
v : Vector α n✝
nil : C Vector.nil
snoc : {n : ℕ} → (xs : Vector α n) → (x : α) → C xs → C (Vector.snoc xs x)
n : ℕ
x : α
xs : Vector α n
r : C (reverse xs)
⊢ C (Vector.snoc (reverse xs) x) = (fun {n} v => C (reverse v)) (x ::ᵥ xs)
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.2985
β : Type ?u.2988
C : {n : ℕ} → Vector α n → Vector β n → Sort u_1
n : ℕ
v : Vector α n
w : Vector β n
nil : C Vector.nil Vector.nil
snoc :
  {n : ℕ} →
    (xs : Vector α n) → (ys : Vector β n) → (x : α) → (y : β) → C xs ys → C (Vector.snoc xs x) (Vector.snoc ys y)
⊢ (fun {n} v w => C (reverse v) (reverse w)) (reverse v) (reverse w) = C v w
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.2985
β : Type ?u.2988
C : {n : ℕ} → Vector α n → Vector β n → Sort u_1
n✝ : ℕ
v : Vector α n✝
w : Vector β n✝
nil : C Vector.nil Vector.nil
snoc :
  {n : ℕ} →
    (xs : Vector α n) → (ys : Vector β n) → (x : α) → (y : β) → C xs ys → C (Vector.snoc xs x) (Vector.snoc ys y)
n : ℕ
x : α
y : β
xs : Vector α n
ys : Vector β n
r : C (reverse xs) (reverse ys)
⊢ C (Vector.snoc (reverse xs) x) (Vector.snoc (reverse ys) y) =
    (fun {n} v w => C (reverse v) (reverse w)) (x ::ᵥ xs) (y ::ᵥ ys)
[PROOFSTEP]
simp
[GOAL]
α : Type u_2
n : ℕ
xs : Vector α n
α✝ : Type u_1
f : α → α✝
x : α
⊢ map f (snoc xs x) = snoc (map f xs) (f x)
[PROOFSTEP]
induction xs using Vector.inductionOn
[GOAL]
case h_nil
α : Type u_2
n : ℕ
xs : Vector α n
α✝ : Type u_1
f : α → α✝
x : α
⊢ map f (snoc nil x) = snoc (map f nil) (f x)
[PROOFSTEP]
simp_all
[GOAL]
case h_cons
α : Type u_2
n : ℕ
xs : Vector α n
α✝ : Type u_1
f : α → α✝
x : α
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
a✝ : map f (snoc w✝ x) = snoc (map f w✝) (f x)
⊢ map f (snoc (x✝ ::ᵥ w✝) x) = snoc (map f (x✝ ::ᵥ w✝)) (f x)
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_2
n : ℕ
xs : Vector α n
α✝ : Type
β✝ : Type u_1
f : α → α✝ → α✝ × β✝
x : α
s : α✝
⊢ mapAccumr f (snoc xs x) s =
    let q := f x s;
    let r := mapAccumr f xs q.fst;
    (r.fst, snoc r.snd q.snd)
[PROOFSTEP]
induction xs using Vector.inductionOn
[GOAL]
case h_nil
α : Type u_2
n : ℕ
xs : Vector α n
α✝ : Type
β✝ : Type u_1
f : α → α✝ → α✝ × β✝
x : α
s : α✝
⊢ mapAccumr f (snoc nil x) s =
    let q := f x s;
    let r := mapAccumr f nil q.fst;
    (r.fst, snoc r.snd q.snd)
[PROOFSTEP]
rfl
[GOAL]
case h_cons
α : Type u_2
n : ℕ
xs : Vector α n
α✝ : Type
β✝ : Type u_1
f : α → α✝ → α✝ × β✝
x : α
s : α✝
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
a✝ :
  mapAccumr f (snoc w✝ x) s =
    let q := f x s;
    let r := mapAccumr f w✝ q.fst;
    (r.fst, snoc r.snd q.snd)
⊢ mapAccumr f (snoc (x✝ ::ᵥ w✝) x) s =
    let q := f x s;
    let r := mapAccumr f (x✝ ::ᵥ w✝) q.fst;
    (r.fst, snoc r.snd q.snd)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_2
n : ℕ
β : Type u_3
xs : Vector α n
ys : Vector β n
α✝ : Type u_1
f : α → β → α✝
x : α
y : β
⊢ map₂ f (snoc xs x) (snoc ys y) = snoc (map₂ f xs ys) (f x y)
[PROOFSTEP]
induction xs, ys using Vector.inductionOn₂
[GOAL]
case nil
α : Type u_2
n : ℕ
β : Type u_3
xs : Vector α n
ys : Vector β n
α✝ : Type u_1
f : α → β → α✝
x : α
y : β
⊢ map₂ f (snoc nil x) (snoc nil y) = snoc (map₂ f nil nil) (f x y)
[PROOFSTEP]
simp_all
[GOAL]
case cons
α : Type u_2
n : ℕ
β : Type u_3
xs : Vector α n
ys : Vector β n
α✝ : Type u_1
f : α → β → α✝
x : α
y : β
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : map₂ f (snoc x✝ x) (snoc y✝ y) = snoc (map₂ f x✝ y✝) (f x y)
⊢ map₂ f (snoc (a✝¹ ::ᵥ x✝) x) (snoc (b✝ ::ᵥ y✝) y) = snoc (map₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝)) (f x y)
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ φ : Type
c : σ
f : α → β → σ → σ × φ
x : α
y : β
⊢ mapAccumr₂ f (snoc xs x) (snoc ys y) c =
    let q := f x y c;
    let r := mapAccumr₂ f xs ys q.fst;
    (r.fst, snoc r.snd q.snd)
[PROOFSTEP]
induction xs, ys using Vector.inductionOn₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ φ : Type
c : σ
f : α → β → σ → σ × φ
x : α
y : β
⊢ mapAccumr₂ f (snoc nil x) (snoc nil y) c =
    let q := f x y c;
    let r := mapAccumr₂ f nil nil q.fst;
    (r.fst, snoc r.snd q.snd)
[PROOFSTEP]
simp_all
[GOAL]
case cons
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ φ : Type
c : σ
f : α → β → σ → σ × φ
x : α
y : β
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ :
  mapAccumr₂ f (snoc x✝ x) (snoc y✝ y) c =
    let q := f x y c;
    let r := mapAccumr₂ f x✝ y✝ q.fst;
    (r.fst, snoc r.snd q.snd)
⊢ mapAccumr₂ f (snoc (a✝¹ ::ᵥ x✝) x) (snoc (b✝ ::ᵥ y✝) y) c =
    let q := f x y c;
    let r := mapAccumr₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) q.fst;
    (r.fst, snoc r.snd q.snd)
[PROOFSTEP]
simp_all
