internlm/Lean-Github huggingface dataset:
Theorem: Array.zipWithAux_cons_cons_succ
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
⊢ (if h : n + 1 < size (cons a x) then
      let a_1 := (cons a x)[n + 1];
      if h : n + 1 < size (cons b y) then
        let b_1 := (cons b y)[n + 1];
        zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f a_1 b_1))
      else z
    else z) =
    if h : n < size x then
      let a := x[n];
      if h : n < size y then
        let b := y[n];
        zipWithAux f x y (n + 1) (push z (f a b))
      else z
    else z
Tactic:
refine dite_congr (propext ⟨Nat.lt_of_succ_lt_succ,Nat.succ_lt_succ⟩) ?_ (λ _ => rfl)
Proof state after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
⊢ ∀ (h : n < size x),
    (let a_1 := (cons a x)[n + 1];
      if h : n + 1 < size (cons b y) then
        let b_1 := (cons b y)[n + 1];
        zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f a_1 b_1))
      else z) =
      let a := x[n];
      if h : n < size y then
        let b := y[n];
        zipWithAux f x y (n + 1) (push z (f a b))
      else z
Theorem: Array.zipWithAux_cons_cons_succ
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
⊢ ∀ (h : n < size x),
    (let a_1 := (cons a x)[n + 1];
      if h : n + 1 < size (cons b y) then
        let b_1 := (cons b y)[n + 1];
        zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f a_1 b_1))
      else z) =
      let a := x[n];
      if h : n < size y then
        let b := y[n];
        zipWithAux f x y (n + 1) (push z (f a b))
      else z
Tactic:
intros
Proof state after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
h✝ : n < size x
⊢ (let a_1 := (cons a x)[n + 1];
    if h : n + 1 < size (cons b y) then
      let b_1 := (cons b y)[n + 1];
      zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f a_1 b_1))
    else z) =
    let a := x[n];
    if h : n < size y then
      let b := y[n];
      zipWithAux f x y (n + 1) (push z (f a b))
    else z
Theorem: Array.zipWithAux_cons_cons_succ
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
h✝ : n < size x
⊢ (let a_1 := (cons a x)[n + 1];
    if h : n + 1 < size (cons b y) then
      let b_1 := (cons b y)[n + 1];
      zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f a_1 b_1))
    else z) =
    let a := x[n];
    if h : n < size y then
      let b := y[n];
      zipWithAux f x y (n + 1) (push z (f a b))
    else z
Tactic:
refine dite_congr (propext ⟨Nat.lt_of_succ_lt_succ,Nat.succ_lt_succ⟩) ?_ (λ _ => rfl)
Proof state after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
h✝ : n < size x
⊢ ∀ (h : n < size y),
    (let b_1 := (cons b y)[n + 1];
      zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f (cons a x)[n + 1] b_1))) =
      let b := y[n];
      zipWithAux f x y (n + 1) (push z (f x[n] b))
Theorem: Array.zipWithAux_cons_cons_succ
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
h✝ : n < size x
⊢ ∀ (h : n < size y),
    (let b_1 := (cons b y)[n + 1];
      zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f (cons a x)[n + 1] b_1))) =
      let b := y[n];
      zipWithAux f x y (n + 1) (push z (f x[n] b))
Tactic:
intros
Proof state after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
h✝¹ : n < size x
h✝ : n < size y
⊢ (let b_1 := (cons b y)[n + 1];
    zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f (cons a x)[n + 1] b_1))) =
    let b := y[n];
    zipWithAux f x y (n + 1) (push z (f x[n] b))
Theorem: Array.zipWithAux_cons_cons_succ
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
h✝¹ : n < size x
h✝ : n < size y
⊢ (let b_1 := (cons b y)[n + 1];
    zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f (cons a x)[n + 1] b_1))) =
    let b := y[n];
    zipWithAux f x y (n + 1) (push z (f x[n] b))
Tactic:
dsimp
Proof state after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
h✝¹ : n < size x
h✝ : n < size y
⊢ zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f x[n] y[n])) =
    zipWithAux f x y (n + 1) (push z (f x[n] y[n]))
Theorem: Array.zipWithAux_cons_cons_succ
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
n : Nat
z : Array γ
h✝¹ : n < size x
h✝ : n < size y
⊢ zipWithAux f (cons a x) (cons b y) (n + 1 + 1) (push z (f x[n] y[n])) =
    zipWithAux f x y (n + 1) (push z (f x[n] y[n]))
Tactic:
exact zipWithAux_cons_cons_succ f a x b y (n+1) _
Proof state after:
no goals
Theorem: Array.zipWithAux_cons_cons_zero
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
z : Array γ
⊢ zipWithAux f (cons a x) (cons b y) 0 z = zipWithAux f x y 0 (push z (f a b))
Tactic:
conv =>
  lhs
  unfold zipWithAux; dsimp
  rw [dif_pos x.size.zero_lt_succ, dif_pos y.size.zero_lt_succ]
  rw [zipWithAux_cons_cons_succ]
Proof state after:
no goals
Theorem: Array.zipWithAux_data_eq_zipWithTR_go
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
y : Array β
z : Array γ
⊢ (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
Tactic:
induction x using cons_induction generalizing y z with
| empty =>
  rw [zipWithAux_nil_first]; exact z.toList_eq.symm
| cons a x IH =>
  cases y using cons_cases_on with
  | empty =>
    rw [zipWithAux_nil_second]; exact z.toList_eq.symm
  | cons b y =>
    rw [zipWithAux_cons_cons_zero]; exact IH _ _
Proof state after:
no goals
Theorem: Array.zipWithAux_data_eq_zipWithTR_go
Proof state before:
case empty
α : Type u
β : Type v
γ : Type w
f : α → β → γ
y : Array β
z : Array γ
⊢ (zipWithAux f #[] y 0 z).data = List.zipWithTR.go f #[].data y.data z
Tactic:
rw [zipWithAux_nil_first]
Proof state after:
case empty
α : Type u
β : Type v
γ : Type w
f : α → β → γ
y : Array β
z : Array γ
⊢ z.data = List.zipWithTR.go f #[].data y.data z
Theorem: Array.zipWithAux_data_eq_zipWithTR_go
Proof state before:
case empty
α : Type u
β : Type v
γ : Type w
f : α → β → γ
y : Array β
z : Array γ
⊢ z.data = List.zipWithTR.go f #[].data y.data z
Tactic:
exact z.toList_eq.symm
Proof state after:
no goals
Theorem: Array.zipWithAux_data_eq_zipWithTR_go
Proof state before:
case cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
IH : ∀ (y : Array β) (z : Array γ), (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
y : Array β
z : Array γ
⊢ (zipWithAux f (cons a x) y 0 z).data = List.zipWithTR.go f (cons a x).data y.data z
Tactic:
cases y using cons_cases_on with
| empty =>
  rw [zipWithAux_nil_second]; exact z.toList_eq.symm
| cons b y =>
  rw [zipWithAux_cons_cons_zero]; exact IH _ _
Proof state after:
no goals
Theorem: Array.zipWithAux_data_eq_zipWithTR_go
Proof state before:
case cons.empty
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
IH : ∀ (y : Array β) (z : Array γ), (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
z : Array γ
⊢ (zipWithAux f (cons a x) #[] 0 z).data = List.zipWithTR.go f (cons a x).data #[].data z
Tactic:
rw [zipWithAux_nil_second]
Proof state after:
case cons.empty
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
IH : ∀ (y : Array β) (z : Array γ), (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
z : Array γ
⊢ z.data = List.zipWithTR.go f (cons a x).data #[].data z
Theorem: Array.zipWithAux_data_eq_zipWithTR_go
Proof state before:
case cons.empty
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
IH : ∀ (y : Array β) (z : Array γ), (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
z : Array γ
⊢ z.data = List.zipWithTR.go f (cons a x).data #[].data z
Tactic:
exact z.toList_eq.symm
Proof state after:
no goals
Theorem: Array.zipWithAux_data_eq_zipWithTR_go
Proof state before:
case cons.cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
IH : ∀ (y : Array β) (z : Array γ), (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
z : Array γ
b : β
y : Array β
⊢ (zipWithAux f (cons a x) (cons b y) 0 z).data = List.zipWithTR.go f (cons a x).data (cons b y).data z
Tactic:
rw [zipWithAux_cons_cons_zero]
Proof state after:
case cons.cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
IH : ∀ (y : Array β) (z : Array γ), (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
z : Array γ
b : β
y : Array β
⊢ (zipWithAux f x y 0 (push z (f a b))).data = List.zipWithTR.go f (cons a x).data (cons b y).data z
Theorem: Array.zipWithAux_data_eq_zipWithTR_go
Proof state before:
case cons.cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
IH : ∀ (y : Array β) (z : Array γ), (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
z : Array γ
b : β
y : Array β
⊢ (zipWithAux f x y 0 (push z (f a b))).data = List.zipWithTR.go f (cons a x).data (cons b y).data z
Tactic:
exact IH _ _
Proof state after:
no goals
Theorem: Array.zipWith_data_eq_zipWith_data
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
y : Array β
⊢ (zipWith x y f).data = List.zipWith f x.data y.data
Tactic:
show (zipWithAux f x y 0 #[]).data = List.zipWith f x.data y.data
Proof state after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
y : Array β
⊢ (zipWithAux f x y 0 #[]).data = List.zipWith f x.data y.data
Theorem: Array.zipWith_data_eq_zipWith_data
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
y : Array β
⊢ (zipWithAux f x y 0 #[]).data = List.zipWith f x.data y.data
Tactic:
rw [zipWithAux_data_eq_zipWithTR_go, List.zipWith_eq_zipWithTR]
Proof state after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
y : Array β
⊢ List.zipWithTR.go f x.data y.data #[] = List.zipWithTR f x.data y.data
Theorem: Array.zipWith_data_eq_zipWith_data
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
y : Array β
⊢ List.zipWithTR.go f x.data y.data #[] = List.zipWithTR f x.data y.data
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.size_zipWith
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
y : Array β
⊢ size (zipWith x y f) = min (size x) (size y)
Tactic:
simp only [size, zipWith_data_eq_zipWith_data]
Proof state after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
y : Array β
⊢ List.length (List.zipWith f x.data y.data) = min (List.length x.data) (List.length y.data)
Theorem: Array.size_zipWith
Proof state before:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
y : Array β
⊢ List.length (List.zipWith f x.data y.data) = min (List.length x.data) (List.length y.data)
Tactic:
exact List.length_zipWith' f x.data y.data
Proof state after:
no goals
Theorem: Array.size_modifyM
Proof state before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
⊢ SatisfiesM (fun y => size y = size x) (modifyM x n f)
Tactic:
unfold modifyM
Proof state after:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
⊢ SatisfiesM (fun y => size y = size x)
    (if h : n < size x then
      let idx := { val := n, isLt := h };
      let v := get x idx;
      do
      let v ← f v
      pure (set x idx v)
    else pure x)
Theorem: Array.size_modifyM
Proof state before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
⊢ SatisfiesM (fun y => size y = size x)
    (if h : n < size x then
      let idx := { val := n, isLt := h };
      let v := get x idx;
      do
      let v ← f v
      pure (set x idx v)
    else pure x)
Tactic:
if h : n < x.size
then
  rw [dif_pos h]; dsimp
  exists (f x[n] >>= λ v => pure ⟨x.set ⟨n,h⟩ v, x.size_set ⟨n,h⟩ v⟩)
  rw [map_eq_pure_bind, bind_assoc]
  apply bind_congr; intro a
  exact pure_bind ..
else rw [dif_neg h]; exact ⟨pure ⟨x,rfl⟩, map_pure Subtype.val _⟩
Proof state after:
no goals
Theorem: Array.size_modifyM
Proof state before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ SatisfiesM (fun y => size y = size x)
    (if h : n < size x then
      let idx := { val := n, isLt := h };
      let v := get x idx;
      do
      let v ← f v
      pure (set x idx v)
    else pure x)
Tactic:
rw [dif_pos h]
Proof state after:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ SatisfiesM (fun y => size y = size x)
    (let idx := { val := n, isLt := h };
    let v := get x idx;
    do
    let v ← f v
    pure (set x idx v))
Theorem: Array.size_modifyM
Proof state before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ SatisfiesM (fun y => size y = size x)
    (let idx := { val := n, isLt := h };
    let v := get x idx;
    do
    let v ← f v
    pure (set x idx v))
Tactic:
dsimp
Proof state after:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ SatisfiesM (fun y => size y = size x) do
    let v ← f x[n]
    pure (set x { val := n, isLt := h } v)
Theorem: Array.size_modifyM
Proof state before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ SatisfiesM (fun y => size y = size x) do
    let v ← f x[n]
    pure (set x { val := n, isLt := h } v)
Tactic:
exists (f x[n] >>= λ v => pure ⟨x.set ⟨n,h⟩ v, x.size_set ⟨n,h⟩ v⟩)
Proof state after:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ (Subtype.val <$> do
      let v ← f x[n]
      pure
          { val := set x { val := n, isLt := h } v,
            property := (_ : size (set x { val := n, isLt := h } v) = size x) }) =
    do
    let v ← f x[n]
    pure (set x { val := n, isLt := h } v)
Theorem: Array.size_modifyM
Proof state before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ (Subtype.val <$> do
      let v ← f x[n]
      pure
          { val := set x { val := n, isLt := h } v,
            property := (_ : size (set x { val := n, isLt := h } v) = size x) }) =
    do
    let v ← f x[n]
    pure (set x { val := n, isLt := h } v)
Tactic:
rw [map_eq_pure_bind, bind_assoc]
Proof state after:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ (do
      let x_1 ← f x[n]
      let a ←
        pure
            { val := set x { val := n, isLt := h } x_1,
              property := (_ : size (set x { val := n, isLt := h } x_1) = size x) }
      pure a.val) =
    do
    let v ← f x[n]
    pure (set x { val := n, isLt := h } v)
Theorem: Array.size_modifyM
Proof state before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ (do
      let x_1 ← f x[n]
      let a ←
        pure
            { val := set x { val := n, isLt := h } x_1,
              property := (_ : size (set x { val := n, isLt := h } x_1) = size x) }
      pure a.val) =
    do
    let v ← f x[n]
    pure (set x { val := n, isLt := h } v)
Tactic:
apply bind_congr
Proof state after:
case h
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ ∀ (a : α),
    (do
        let a ←
          pure
              { val := set x { val := n, isLt := h } a,
                property := (_ : size (set x { val := n, isLt := h } a) = size x) }
        pure a.val) =
      pure (set x { val := n, isLt := h } a)
Theorem: Array.size_modifyM
Proof state before:
case h
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
⊢ ∀ (a : α),
    (do
        let a ←
          pure
              { val := set x { val := n, isLt := h } a,
                property := (_ : size (set x { val := n, isLt := h } a) = size x) }
        pure a.val) =
      pure (set x { val := n, isLt := h } a)
Tactic:
intro a
Proof state after:
case h
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
a : α
⊢ (do
      let a ←
        pure
            { val := set x { val := n, isLt := h } a,
              property := (_ : size (set x { val := n, isLt := h } a) = size x) }
      pure a.val) =
    pure (set x { val := n, isLt := h } a)
Theorem: Array.size_modifyM
Proof state before:
case h
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : n < size x
a : α
⊢ (do
      let a ←
        pure
            { val := set x { val := n, isLt := h } a,
              property := (_ : size (set x { val := n, isLt := h } a) = size x) }
      pure a.val) =
    pure (set x { val := n, isLt := h } a)
Tactic:
exact pure_bind ..
Proof state after:
no goals
Theorem: Array.size_modifyM
Proof state before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : ¬n < size x
⊢ SatisfiesM (fun y => size y = size x)
    (if h : n < size x then
      let idx := { val := n, isLt := h };
      let v := get x idx;
      do
      let v ← f v
      pure (set x idx v)
    else pure x)
Tactic:
rw [dif_neg h]
Proof state after:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : ¬n < size x
⊢ SatisfiesM (fun y => size y = size x) (pure x)
Theorem: Array.size_modifyM
Proof state before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : ¬n < size x
⊢ SatisfiesM (fun y => size y = size x) (pure x)
Tactic:
exact ⟨pure ⟨x,rfl⟩, map_pure Subtype.val _⟩
Proof state after:
no goals
Theorem: Array.size_modify
Proof state before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
⊢ ∀ (x : Array α) (n : Nat) (f : α → α), size (modify x n f) = size x
Tactic:
intro x n f
Proof state after:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → α
⊢ size (modify x n f) = size x
Theorem: Array.size_modify
Proof state before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → α
⊢ size (modify x n f) = size x
Tactic:
cases size_modifyM (m:=Id) x n f with | intro w hw =>
dsimp at hw
conv at hw => rhs; change modify x n f
rw [←hw]
exact w.property
Proof state after:
no goals
Theorem: Array.size_modify
Proof state before:
case intro
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → α
w : Id { a // (fun y => size y = size x) a }
hw : Subtype.val <$> w = modifyM x n f
⊢ size (modify x n f) = size x
Tactic:
dsimp at hw
Proof state after:
case intro
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → α
w : Id { a // (fun y => size y = size x) a }
hw : w.val = modifyM x n f
⊢ size (modify x n f) = size x
Theorem: Array.size_modify
Proof state before:
case intro
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → α
w : Id { a // (fun y => size y = size x) a }
hw : w.val = modifyM x n f
⊢ size (modify x n f) = size x
Tactic:
conv at hw => rhs; change modify x n f
Proof state after:
case intro
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → α
w : Id { a // (fun y => size y = size x) a }
hw : w.val = modify x n f
⊢ size (modify x n f) = size x
Theorem: Array.size_modify
Proof state before:
case intro
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → α
w : Id { a // (fun y => size y = size x) a }
hw : w.val = modify x n f
⊢ size (modify x n f) = size x
Tactic:
rw [←hw]
Proof state after:
case intro
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → α
w : Id { a // (fun y => size y = size x) a }
hw : w.val = modify x n f
⊢ size w.val = size x
Theorem: Array.size_modify
Proof state before:
case intro
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → α
w : Id { a // (fun y => size y = size x) a }
hw : w.val = modify x n f
⊢ size w.val = size x
Tactic:
exact w.property
Proof state after:
no goals
Theorem: Array.modify_eq_set_get
Proof state before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
i : Nat
f : α → α
hi : i < size x
⊢ modify x i f = set x { val := i, isLt := hi } (f x[i])
Tactic:
dsimp [modify, modifyM, Id.run]
Proof state after:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
i : Nat
f : α → α
hi : i < size x
⊢ (if h : i < size x then set x { val := i, isLt := h } (f x[i]) else x) = set x { val := i, isLt := hi } (f x[i])
Theorem: Array.modify_eq_set_get
Proof state before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
i : Nat
f : α → α
hi : i < size x
⊢ (if h : i < size x then set x { val := i, isLt := h } (f x[i]) else x) = set x { val := i, isLt := hi } (f x[i])
Tactic:
simp only [dif_pos hi]
Proof state after:
no goals
Theorem: Array.getElem_modify_eq
Proof state before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
i : Nat
f : α → α
hi : i < size x
⊢ (modify x i f)[i] = f x[i]
Tactic:
dsimp [modify, modifyM, Id.run]
Proof state after:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
i : Nat
f : α → α
hi : i < size x
⊢ (if h : i < size x then set x { val := i, isLt := h } (f x[i]) else x)[i] = f x[i]
Theorem: Array.getElem_modify_eq
Proof state before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
i : Nat
f : α → α
hi : i < size x
⊢ (if h : i < size x then set x { val := i, isLt := h } (f x[i]) else x)[i] = f x[i]
Tactic:
simp only [dif_pos hi]
Proof state after:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
i : Nat
f : α → α
hi : i < size x
⊢ (set x { val := i, isLt := hi } (f x[i]))[i] = f x[i]
Theorem: Array.getElem_modify_eq
Proof state before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
i : Nat
f : α → α
hi : i < size x
⊢ (set x { val := i, isLt := hi } (f x[i]))[i] = f x[i]
Tactic:
rw [Array.get_set_eq]
Proof state after:
no goals
Theorem: Array.ofFn_go_zero
Proof state before:
α : Type u
f : Fin 0 → α
i : Nat
acc : Array α
⊢ ofFn.go f i acc = acc
Tactic:
unfold ofFn.go
Proof state after:
α : Type u
f : Fin 0 → α
i : Nat
acc : Array α
⊢ (if h : i < 0 then ofFn.go f (i + 1) (push acc (f { val := i, isLt := h })) else acc) = acc
Theorem: Array.ofFn_go_zero
Proof state before:
α : Type u
f : Fin 0 → α
i : Nat
acc : Array α
⊢ (if h : i < 0 then ofFn.go f (i + 1) (push acc (f { val := i, isLt := h })) else acc) = acc
Tactic:
exact dif_neg i.not_lt_zero
Proof state after:
no goals