fix tests

doc/examples/interp.lean

@@ -12,17 +12,17 @@ Remark: this example is based on an example found in the Idris manual.
 Vectors
 --------
 
-A `Vector` is a list of size `n` whose elements belong to a type `α`.
+A `Vec` is a list of size `n` whose elements belong to a type `α`.
 -/
 
-inductive Vector (α : Type u) : Nat → Type u
-  | nil : Vector α 0
-  | cons : α → Vector α n → Vector α (n+1)
+inductive Vec (α : Type u) : Nat → Type u
+  | nil : Vec α 0
+  | cons : α → Vec α n → Vec α (n+1)
 
 /-!
-We can overload the `List.cons` notation `::` and use it to create `Vector`s.
+We can overload the `List.cons` notation `::` and use it to create `Vec`s.
 -/
-infix:67 " :: " => Vector.cons
+infix:67 " :: " => Vec.cons
 
 /-!
 Now, we define the types of our simple functional language.
@@ -50,11 +50,11 @@ the builtin instance for `Add Int` as the solution.
 /-!
 Expressions are indexed by the types of the local variables, and the type of the expression itself.
 -/
-inductive HasType : Fin n → Vector Ty n → Ty → Type where
+inductive HasType : Fin n → Vec Ty n → Ty → Type where
   | stop : HasType 0 (ty :: ctx) ty
   | pop  : HasType k ctx ty → HasType k.succ (u :: ctx) ty
 
-inductive Expr : Vector Ty n → Ty → Type where
+inductive Expr : Vec Ty n → Ty → Type where
   | var   : HasType i ctx ty → Expr ctx ty
   | val   : Int → Expr ctx Ty.int
   | lam   : Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)
@@ -102,8 +102,8 @@ indexed over the types in scope. Since an environment is just another form of li
 to the vector of local variable types, we overload again the notation `::` so that we can use the usual list syntax.
 Given a proof that a variable is defined in the context, we can then produce a value from the environment.
 -/
-inductive Env : Vector Ty n → Type where
-  | nil  : Env Vector.nil
+inductive Env : Vec Ty n → Type where
+  | nil  : Env Vec.nil
   | cons : Ty.interp a → Env ctx → Env (a :: ctx)
 
 infix:67 " :: " => Env.cons

src/Init/Data.lean

@@ -43,3 +43,4 @@ import Init.Data.Zero
 import Init.Data.NeZero
 import Init.Data.Function
 import Init.Data.RArray
+import Init.Data.Vector

src/Init/Data/Array/Lemmas.lean

@@ -1717,6 +1717,14 @@ theorem eraseIdx_eq_eraseIdxIfInBounds {a : Array α} {i : Nat} (h : i < a.size)
   cases bs
   simp
 
+@[simp] theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) :
+    (as.zipWith bs f).size = min as.size bs.size := by
+  rw [size_eq_length_toList, toList_zipWith, List.length_zipWith]
+
+@[simp] theorem size_zip (as : Array α) (bs : Array β) :
+    (as.zip bs).size = min as.size bs.size :=
+  as.size_zipWith bs Prod.mk
+
 /-! ### findSomeM?, findM?, findSome?, find? -/
 
 @[simp] theorem findSomeM?_toList [Monad m] [LawfulMonad m] (p : α → m (Option β)) (as : Array α) :

src/Init/Data/Vector.lean

@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Vector.Basic

src/Init/Data/Vector/Basic.lean

@@ -0,0 +1,258 @@
+/-
+Copyright (c) 2024 Shreyas Srinivas. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Shreyas Srinivas, François G. Dorais, Kim Morrison
+-/
+
+prelude
+import Init.Data.Array.Lemmas
+
+/-!
+# Vectors
+
+`Vector α n` is a thin wrapper around `Array α` for arrays of fixed size `n`.
+-/
+
+/-- `Vector α n` is an `Array α` with size `n`. -/
+structure Vector (α : Type u) (n : Nat) extends Array α where
+  /-- Array size. -/
+  size_toArray : toArray.size = n
+deriving Repr, DecidableEq
+
+attribute [simp] Vector.size_toArray
+
+namespace Vector
+
+/-- Syntax for `Vector α n` -/
+syntax "#v[" withoutPosition(sepBy(term, ", ")) "]" : term
+
+open Lean in
+macro_rules
+  | `(#v[ $elems,* ]) => `(Vector.mk (n := $(quote elems.getElems.size)) #[$elems,*] rfl)
+
+/-- Custom eliminator for `Vector α n` through `Array α` -/
+@[elab_as_elim]
+def elimAsArray {motive : Vector α n → Sort u}
+    (mk : ∀ (a : Array α) (ha : a.size = n), motive ⟨a, ha⟩) :
+    (v : Vector α n) → motive v
+  | ⟨a, ha⟩ => mk a ha
+
+/-- Custom eliminator for `Vector α n` through `List α` -/
+@[elab_as_elim]
+def elimAsList {motive : Vector α n → Sort u}
+    (mk : ∀ (a : List α) (ha : a.length = n), motive ⟨⟨a⟩, ha⟩) :
+    (v : Vector α n) → motive v
+  | ⟨⟨a⟩, ha⟩ => mk a ha
+
+/-- The empty vector. -/
+@[inline] def empty : Vector α 0 := ⟨.empty, rfl⟩
+
+/-- Make an empty vector with pre-allocated capacity. -/
+@[inline] def mkEmpty (capacity : Nat) : Vector α 0 := ⟨.mkEmpty capacity, rfl⟩
+
+/-- Makes a vector of size `n` with all cells containing `v`. -/
+@[inline] def mkVector (n) (v : α) : Vector α n := ⟨mkArray n v, by simp⟩
+
+/-- Returns a vector of size `1` with element `v`. -/
+@[inline] def singleton (v : α) : Vector α 1 := ⟨#[v], rfl⟩
+
+instance [Inhabited α] : Inhabited (Vector α n) where
+  default := mkVector n default
+
+/-- Get an element of a vector using a `Fin` index. -/
+@[inline] def get (v : Vector α n) (i : Fin n) : α :=
+  v.toArray[(i.cast v.size_toArray.symm).1]
+
+/-- Get an element of a vector using a `USize` index and a proof that the index is within bounds. -/
+@[inline] def uget (v : Vector α n) (i : USize) (h : i.toNat < n) : α :=
+  v.toArray.uget i (v.size_toArray.symm ▸ h)
+
+instance : GetElem (Vector α n) Nat α fun _ i => i < n where
+  getElem x i h := get x ⟨i, h⟩
+
+/--
+Get an element of a vector using a `Nat` index. Returns the given default value if the index is out
+of bounds.
+-/
+@[inline] def getD (v : Vector α n) (i : Nat) (default : α) : α := v.toArray.getD i default
+
+/-- The last element of a vector. Panics if the vector is empty. -/
+@[inline] def back! [Inhabited α] (v : Vector α n) : α := v.toArray.back!
+
+/-- The last element of a vector, or `none` if the array is empty. -/
+@[inline] def back? (v : Vector α n) : Option α := v.toArray.back?
+
+/-- The last element of a non-empty vector. -/
+@[inline] def back [NeZero n] (v : Vector α n) : α :=
+  -- TODO: change to just `v[n]`
+  have : Inhabited α := ⟨v[0]'(Nat.pos_of_neZero n)⟩
+  v.back!
+
+/-- The first element of a non-empty vector.  -/
+@[inline] def head [NeZero n] (v : Vector α n) := v[0]'(Nat.pos_of_neZero n)
+
+/-- Push an element `x` to the end of a vector. -/
+@[inline] def push (x : α) (v : Vector α n)  : Vector α (n + 1) :=
+  ⟨v.toArray.push x, by simp⟩
+
+/-- Remove the last element of a vector. -/
+@[inline] def pop (v : Vector α n) : Vector α (n - 1) :=
+  ⟨Array.pop v.toArray, by simp⟩
+
+/--
+Set an element in a vector using a `Nat` index, with a tactic provided proof that the index is in
+bounds.
+
+This will perform the update destructively provided that the vector has a reference count of 1.
+-/
+@[inline] def set (v : Vector α n) (i : Nat) (x : α) (h : i < n := by get_elem_tactic): Vector α n :=
+  ⟨v.toArray.set i x (by simp [*]), by simp⟩
+
+/--
+Set an element in a vector using a `Nat` index. Returns the vector unchanged if the index is out of
+bounds.
+
+This will perform the update destructively provided that the vector has a reference count of 1.
+-/
+@[inline] def setIfInBounds (v : Vector α n) (i : Nat) (x : α) : Vector α n :=
+  ⟨v.toArray.setIfInBounds i x, by simp⟩
+
+/--
+Set an element in a vector using a `Nat` index. Panics if the index is out of bounds.
+
+This will perform the update destructively provided that the vector has a reference count of 1.
+-/
+@[inline] def set! (v : Vector α n) (i : Nat) (x : α) : Vector α n :=
+  ⟨v.toArray.set! i x, by simp⟩
+
+/-- Append two vectors. -/
+@[inline] def append (v : Vector α n) (w : Vector α m) : Vector α (n + m) :=
+  ⟨v.toArray ++ w.toArray, by simp⟩
+
+instance : HAppend (Vector α n) (Vector α m) (Vector α (n + m)) where
+  hAppend := append
+
+/-- Creates a vector from another with a provably equal length. -/
+@[inline] protected def cast (h : n = m) (v : Vector α n) : Vector α m :=
+  ⟨v.toArray, by simp [*]⟩
+
+/--
+Extracts the slice of a vector from indices `start` to `stop` (exclusive). If `start ≥ stop`, the
+result is empty. If `stop` is greater than the size of the vector, the size is used instead.
+-/
+@[inline] def extract (v : Vector α n) (start stop : Nat) : Vector α (min stop n - start) :=
+  ⟨v.toArray.extract start stop, by simp⟩
+
+/-- Maps elements of a vector using the function `f`. -/
+@[inline] def map (f : α → β) (v : Vector α n) : Vector β n :=
+  ⟨v.toArray.map f, by simp⟩
+
+/-- Maps corresponding elements of two vectors of equal size using the function `f`. -/
+@[inline] def zipWith (a : Vector α n) (b : Vector β n) (f : α → β → φ) : Vector φ n :=
+  ⟨Array.zipWith a.toArray b.toArray f, by simp⟩
+
+/-- The vector of length `n` whose `i`-th element is `f i`. -/
+@[inline] def ofFn (f : Fin n → α) : Vector α n :=
+  ⟨Array.ofFn f, by simp⟩
+
+/--
+Swap two elements of a vector using `Fin` indices.
+
+This will perform the update destructively provided that the vector has a reference count of 1.
+-/
+@[inline] def swap (v : Vector α n) (i j : Nat)
+    (hi : i < n := by get_elem_tactic) (hj : j < n := by get_elem_tactic) : Vector α n :=
+  ⟨v.toArray.swap i j (by simpa using hi) (by simpa using hj), by simp⟩
+
+/--
+Swap two elements of a vector using `Nat` indices. Panics if either index is out of bounds.
+
+This will perform the update destructively provided that the vector has a reference count of 1.
+-/
+@[inline] def swapIfInBounds (v : Vector α n) (i j : Nat) : Vector α n :=
+  ⟨v.toArray.swapIfInBounds i j, by simp⟩
+
+/--
+Swaps an element of a vector with a given value using a `Fin` index. The original value is returned
+along with the updated vector.
+
+This will perform the update destructively provided that the vector has a reference count of 1.
+-/
+@[inline] def swapAt (v : Vector α n) (i : Nat) (x : α) (hi : i < n := by get_elem_tactic) :
+    α × Vector α n :=
+  let a := v.toArray.swapAt i x (by simpa using hi)
+  ⟨a.fst, a.snd, by simp [a]⟩
+
+/--
+Swaps an element of a vector with a given value using a `Nat` index. Panics if the index is out of
+bounds. The original value is returned along with the updated vector.
+
+This will perform the update destructively provided that the vector has a reference count of 1.
+-/
+@[inline] def swapAt! (v : Vector α n) (i : Nat) (x : α) : α × Vector α n :=
+  let a := v.toArray.swapAt! i x
+  ⟨a.fst, a.snd, by simp [a]⟩
+
+/-- The vector `#v[0,1,2,...,n-1]`. -/
+@[inline] def range (n : Nat) : Vector Nat n := ⟨Array.range n, by simp⟩
+
+/--
+Extract the first `m` elements of a vector. If `m` is greater than or equal to the size of the
+vector then the vector is returned unchanged.
+-/
+@[inline] def take (v : Vector α n) (m : Nat) : Vector α (min m n) :=
+  ⟨v.toArray.take m, by simp⟩
+
+/--
+Deletes the first `m` elements of a vector. If `m` is greater than or equal to the size of the
+vector then the empty vector is returned.
+-/
+@[inline] def drop (v : Vector α n) (m : Nat) : Vector α (n - m) :=
+  ⟨v.toArray.extract m v.size, by simp⟩
+
+/--
+Compares two vectors of the same size using a given boolean relation `r`. `isEqv v w r` returns
+`true` if and only if `r v[i] w[i]` is true for all indices `i`.
+-/
+@[inline] def isEqv (v w : Vector α n) (r : α → α → Bool) : Bool :=
+  Array.isEqvAux v.toArray w.toArray (by simp) r 0 (by simp)
+
+instance [BEq α] : BEq (Vector α n) where
+  beq a b := isEqv a b (· == ·)
+
+/-- Reverse the elements of a vector. -/
+@[inline] def reverse (v : Vector α n) : Vector α n :=
+  ⟨v.toArray.reverse, by simp⟩
+
+/-- Delete an element of a vector using a `Nat` index and a tactic provided proof. -/
+@[inline] def eraseIdx (v : Vector α n) (i : Nat) (h : i < n := by get_elem_tactic) :
+    Vector α (n-1) :=
+  ⟨v.toArray.eraseIdx i (v.size_toArray.symm ▸ h), by simp [Array.size_eraseIdx]⟩
+
+/-- Delete an element of a vector using a `Nat` index. Panics if the index is out of bounds. -/
+@[inline] def eraseIdx! (v : Vector α n) (i : Nat) : Vector α (n-1) :=
+  if _ : i < n then
+    v.eraseIdx i
+  else
+    have : Inhabited (Vector α (n-1)) := ⟨v.pop⟩
+    panic! "index out of bounds"
+
+/-- Delete the first element of a vector. Returns the empty vector if the input vector is empty. -/
+@[inline] def tail (v : Vector α n) : Vector α (n-1) :=
+  if _ : 0 < n then
+    v.eraseIdx 0
+  else
+    v.cast (by omega)
+
+/--
+Finds the first index of a given value in a vector using `==` for comparison. Returns `none` if the
+no element of the index matches the given value.
+-/
+@[inline] def indexOf? [BEq α] (v : Vector α n) (x : α) : Option (Fin n) :=
+  match v.toArray.indexOf? x with
+  | some res => some (res.cast v.size_toArray)
+  | none => none
+
+/-- Returns `true` when `v` is a prefix of the vector `w`. -/
+@[inline] def isPrefixOf [BEq α] (v : Vector α m) (w : Vector α n) : Bool :=
+  v.toArray.isPrefixOf w.toArray

tests/lean/1081.lean

@@ -10,28 +10,28 @@ example : f 0 0 = 0 := rfl
 
 example : f 0 (y+1) = y+1 := rfl
 
-inductive Vector (α : Type u) : Nat → Type u where
-  | nil  : Vector α 0
-  | cons : α → Vector α n → Vector α (n+1)
+inductive Vector' (α : Type u) : Nat → Type u where
+  | nil  : Vector' α 0
+  | cons : α → Vector' α n → Vector' α (n+1)
 
-namespace Vector
-  def insert (a: α): Fin (n+1) → Vector α n → Vector α (n+1)
+namespace Vector'
+  def insert (a: α): Fin (n+1) → Vector' α n → Vector' α (n+1)
   | ⟨0  , _⟩,        xs => cons a   xs
   | ⟨i+1, h⟩, cons x xs => cons x $ xs.insert a ⟨i, Nat.lt_of_succ_lt_succ h⟩
 
-  theorem insert_at_0_eq_cons1 (a: α) (v: Vector α n):  v.insert a ⟨0, Nat.zero_lt_succ n⟩ = cons a v :=
+  theorem insert_at_0_eq_cons1 (a: α) (v: Vector' α n):  v.insert a ⟨0, Nat.zero_lt_succ n⟩ = cons a v :=
     rfl -- Error, it does not hold by reflexivity because the recursion is on v
 
   example (a : α) :  nil.insert a ⟨0, by simp_arith⟩ = cons a nil :=
     rfl
 
-  example (a : α) (b : α) (bs : Vector α n) :  (cons b bs).insert a ⟨0, by simp_arith⟩ = cons a (cons b bs) :=
+  example (a : α) (b : α) (bs : Vector' α n) :  (cons b bs).insert a ⟨0, by simp_arith⟩ = cons a (cons b bs) :=
     rfl
 
-  theorem insert_at_0_eq_cons2 (a: α) (v: Vector α n):  v.insert a ⟨0, Nat.zero_lt_succ n⟩ = cons a v := by
+  theorem insert_at_0_eq_cons2 (a: α) (v: Vector' α n):  v.insert a ⟨0, Nat.zero_lt_succ n⟩ = cons a v := by
     rw [insert]
 
-  theorem insert_at_0_eq_cons3 (a: α) (v: Vector α n):  v.insert a ⟨0, Nat.zero_lt_succ n⟩ = cons a v := by
+  theorem insert_at_0_eq_cons3 (a: α) (v: Vector' α n):  v.insert a ⟨0, Nat.zero_lt_succ n⟩ = cons a v := by
     simp only [insert]
 
-end Vector
+end Vector'

tests/lean/doNotation1.lean

@@ -11,14 +11,14 @@ def f3 (xs : List (Nat × Nat)) : List (Nat × Nat) := Id.run <| do
 for p in xs do
   p := (p.2, p.1) -- works. `forInMap` requires a variable
 
-inductive Vector (α : Type) : Nat → Type
-| nil  : Vector α 0
-| cons : α → {n : Nat} → Vector α n → Vector α (n+1)
-def f4 (b : Bool) (n : Nat) (v : Vector Nat n) : Vector Nat (n+1) := Id.run <| do
+inductive Vector' (α : Type) : Nat → Type
+| nil  : Vector' α 0
+| cons : α → {n : Nat} → Vector' α n → Vector' α (n+1)
+def f4 (b : Bool) (n : Nat) (v : Vector' Nat n) : Vector' Nat (n+1) := Id.run <| do
 let mut v := v
 if b then
-  v := Vector.cons 1 v
-Vector.cons 1 v
+  v := Vector'.cons 1 v
+Vector'.cons 1 v
 def f5 (y : Nat) (xs : List Nat) : List Bool := Id.run <| do
 let mut y := y
 for x in xs do

tests/lean/doNotation1.lean.expected.out

@@ -1,10 +1,10 @@
 doNotation1.lean:4:0-4:6: error: `y` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intend to mutate but define `y`, consider using `let y` instead
 doNotation1.lean:8:2-8:18: error: `y` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intend to mutate but define `y`, consider using `let y` instead
 doNotation1.lean:12:2-12:17: error: `p` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intend to mutate but define `p`, consider using `let p` instead
-doNotation1.lean:20:7-20:22: error: invalid reassignment, value has type
-  Vector Nat (n + 1) : Type
+doNotation1.lean:20:7-20:23: error: invalid reassignment, value has type
+  Vector' Nat (n + 1) : Type
 but is expected to have type
-  Vector Nat n : Type
+  Vector' Nat n : Type
 doNotation1.lean:25:7-25:11: error: invalid reassignment, value has type
   Bool : Type
 but is expected to have type

tests/lean/interactive/autoBoundIssue.lean

@@ -1,15 +1,15 @@
-inductive Vector (α : Type u) : Nat → Type u
-  | nil : Vector α 0
-  | cons : α → Vector α n → Vector α (n+1)
+inductive Vector' (α : Type u) : Nat → Type u
+  | nil : Vector' α 0
+  | cons : α → Vector' α n → Vector' α (n+1)
 
-infix:67 " :: " => Vector.cons
+infix:67 " :: " => Vector'.cons
 
 inductive Ty where
   | int
   | bool
   | fn (a r : Ty)
 
-inductive HasType : Fin n → Vector Ty n → Ty → Type where
+inductive HasType : Fin n → Vector' Ty n → Ty → Type where
   | stop : HasType 0 (ty :: ctx) ty
   | pop  : HasType k ctx ty → HasType k.succ (u :: ctx) ty
                    --^ $/lean/plainTermGoal

tests/lean/interactive/autoBoundIssue.lean.expected.out

@@ -3,34 +3,34 @@
 {"range":
  {"start": {"line": 13, "character": 21}, "end": {"line": 13, "character": 24}},
  "goal":
- "k : Fin ?m\nctx : Vector Ty ?m\nty u : Ty\n⊢ Vector Ty ?m"}
+ "k : Fin ?m\nctx : Vector' Ty ?m\nty u : Ty\n⊢ Vector' Ty ?m"}
 {"textDocument": {"uri": "file:///autoBoundIssue.lean"},
  "position": {"line": 16, "character": 26}}
 {"range":
  {"start": {"line": 16, "character": 26}, "end": {"line": 16, "character": 29}},
  "goal":
- "k : Fin ?m\nctx : Vector Ty ?m\nty : Ty\n⊢ Vector Ty ?m"}
+ "k : Fin ?m\nctx : Vector' Ty ?m\nty : Ty\n⊢ Vector' Ty ?m"}
 {"textDocument": {"uri": "file:///autoBoundIssue.lean"},
  "position": {"line": 19, "character": 20}}
 {"range":
  {"start": {"line": 19, "character": 20}, "end": {"line": 19, "character": 23}},
  "goal":
- "k : Fin ?m\nctx : Vector Ty ?m\nty : Ty\n⊢ Vector Ty ?m"}
+ "k : Fin ?m\nctx : Vector' Ty ?m\nty : Ty\n⊢ Vector' Ty ?m"}
 {"textDocument": {"uri": "file:///autoBoundIssue.lean"},
  "position": {"line": 24, "character": 18}}
 {"range":
  {"start": {"line": 24, "character": 18}, "end": {"line": 24, "character": 21}},
  "goal":
- "k : Fin ?m\nctx : Vector Ty ?m\nty : Ty\n⊢ Vector Ty ?m"}
+ "k : Fin ?m\nctx : Vector' Ty ?m\nty : Ty\n⊢ Vector' Ty ?m"}
 {"textDocument": {"uri": "file:///autoBoundIssue.lean"},
  "position": {"line": 26, "character": 18}}
 {"range":
  {"start": {"line": 26, "character": 18}, "end": {"line": 26, "character": 21}},
  "goal":
- "aux : {x : Nat} → {k : Fin x} → {ctx : Vector Ty x} → {ty : Ty} → HasType k ctx ty\nk : Fin ?m\nctx : Vector Ty ?m\nty : Ty\n⊢ Vector Ty ?m"}
+ "aux : {x : Nat} → {k : Fin x} → {ctx : Vector' Ty x} → {ty : Ty} → HasType k ctx ty\nk : Fin ?m\nctx : Vector' Ty ?m\nty : Ty\n⊢ Vector' Ty ?m"}
 {"textDocument": {"uri": "file:///autoBoundIssue.lean"},
  "position": {"line": 29, "character": 24}}
 {"range":
  {"start": {"line": 29, "character": 24}, "end": {"line": 29, "character": 27}},
  "goal":
- "k : Fin ?m\nctx : Vector Ty ?m\nty : Ty\n⊢ Vector Ty ?m"}
+ "k : Fin ?m\nctx : Vector' Ty ?m\nty : Ty\n⊢ Vector' Ty ?m"}

tests/lean/match4.lean

@@ -41,15 +41,15 @@ match x with
 
 #eval f6 (5, 20)
 
-def Vector (α : Type) (n : Nat) := { a : Array α // a.size = n }
+def Vector' (α : Type) (n : Nat) := { a : Array α // a.size = n }
 
-def mkVec {α : Type} (n : Nat) (a : α) : Vector α n :=
+def mkVec {α : Type} (n : Nat) (a : α) : Vector' α n :=
 ⟨mkArray n a, Array.size_mkArray ..⟩
 
 structure S :=
 (n : Nat)
-(y : Vector Nat n)
-(z : Vector Nat n)
+(y : Vector' Nat n)
+(z : Vector' Nat n)
 (h : y = z)
 (m : { v : Nat // v = y.val.size })
 

tests/lean/matchLeftovers.lean

@@ -15,13 +15,13 @@ example (x : Nat) : Nat :=
   match g x with
   | (a, b) => by done
 
-inductive Vector (α : Type u) : Nat → Type u where
-  | nil  : Vector α 0
-  | cons : α → Vector α n → Vector α (n+1)
+inductive Vector' (α : Type u) : Nat → Type u where
+  | nil  : Vector' α 0
+  | cons : α → Vector' α n → Vector' α (n+1)
 
-namespace Vector
-  def insert (a: α): Fin (n+1) → Vector α n → Vector α (n+1)
+namespace Vector'
+  def insert (a: α): Fin (n+1) → Vector' α n → Vector' α (n+1)
     | ⟨0  , _⟩,        xs => cons a xs
     | ⟨i+1, h⟩, cons x xs => by done
 
-end Vector
+end Vector'

tests/lean/matchLeftovers.lean.expected.out

@@ -16,5 +16,5 @@ a : α
 i n✝ : Nat
 h : i + 1 < n✝ + 1 + 1
 x : α
-xs : Vector α n✝
-⊢ Vector α (n✝ + 1 + 1)
+xs : Vector' α n✝
+⊢ Vector' α (n✝ + 1 + 1)

tests/lean/run/1024.lean

@@ -1,17 +1,17 @@
-inductive Vector (α : Type u): Nat → Type u where
-| nil : Vector α 0
-| cons (head : α) (tail : Vector α n) : Vector α (n+1)
+inductive Vector' (α : Type u): Nat → Type u where
+| nil : Vector' α 0
+| cons (head : α) (tail : Vector' α n) : Vector' α (n+1)
 
-namespace Vector
-  def nth : ∀{n}, Vector α n → Fin n → α
+namespace Vector'
+  def nth : ∀{n}, Vector' α n → Fin n → α
   | n+1, cons x xs, ⟨  0, _⟩ => x
   | n+1, cons x xs, ⟨k+1, h⟩ => xs.nth ⟨k, sorry⟩
 
-  def snoc : ∀{n : Nat} (xs : Vector α n) (x : α), Vector α (n+1)
+  def snoc : ∀{n : Nat} (xs : Vector' α n) (x : α), Vector' α (n+1)
   | _, nil,    x' => cons x' nil
   | _, cons x xs, x' => cons x (snoc xs x')
 
-  theorem nth_snoc_eq (k: Fin (n+1))(v : Vector α n)
+  theorem nth_snoc_eq (k: Fin (n+1))(v : Vector' α n)
     (h: k.val = n):
     (v.snoc x).nth k = x := by
     cases k; rename_i k hk
@@ -19,11 +19,11 @@ namespace Vector
     · simp only [nth]
     · simp! [*]
 
-  theorem nth_snoc_eq_works (k: Fin (n+1))(v : Vector α n)
+  theorem nth_snoc_eq_works (k: Fin (n+1))(v : Vector' α n)
     (h: k.val = n):
     (v.snoc x).nth k = x := by
     cases k; rename_i k hk
     induction v generalizing k <;> subst h
     · simp only [nth]
     · simp[*,nth]
-end Vector
+end Vector'

tests/lean/run/1025.lean

@@ -1,24 +1,24 @@
-inductive Vector (α : Type u): Nat → Type u where
-| nil : Vector α 0
-| cons (head : α) (tail : Vector α n) : Vector α (n+1)
+inductive Vector' (α : Type u): Nat → Type u where
+| nil : Vector' α 0
+| cons (head : α) (tail : Vector' α n) : Vector' α (n+1)
 
 class Order (α : Type u) extends LE α, LT α, Max α where
   ltDecidable : DecidableRel (@LT.lt α _)
   max_def x y : max x y = if x < y then x else y
 
-namespace Vector
-  def mem (a : α) : Vector α n → Prop
+namespace Vector'
+  def mem (a : α) : Vector' α n → Prop
   | nil => False
   | cons b l => a = b ∨ mem a l
 
-  def foldr (f : α → β → β) (init : β) : Vector α n → β
+  def foldr (f : α → β → β) (init : β) : Vector' α n → β
   | nil     => init
   | cons a l => f a (foldr f init l)
 
-  theorem foldr_max [Order β] {v: Vector α n} (f : α → β) (init : β)
+  theorem foldr_max [Order β] {v: Vector' α n} (f : α → β) (init : β)
     (h: v.mem y):
     f y ≤ v.foldr (λ x acc => max (f x) acc) init := by
     induction v <;> simp only[foldr,Order.max_def]
     · admit
     · split <;> admit
-end Vector
+end Vector'

tests/lean/run/2901.lean

@@ -1,7 +1,7 @@
-def Vector (α : Type u) (n : Nat) :=
+def Vector' (α : Type u) (n : Nat) :=
   { l : List α // l.length = n }
 
-inductive HVect : (n : Nat) -> (Vector (Type v) n) -> Type (v+1)  where
+inductive HVect : (n : Nat) -> (Vector' (Type v) n) -> Type (v+1)  where
    | Nil  : HVect 0 ⟨ [], simp ⟩
    | Cons : (t : Type v) -> (x : t) -> HVect n ⟨ts, p⟩ -> HVect (n+1) ⟨t::ts, by simp [p]⟩
 

tests/lean/run/ac_rfl.lean

@@ -14,14 +14,14 @@ example (x y : Nat) : (x + y = 42) = (y + x = 42) := by ac_rfl
 
 example (x y : Nat) (P : Prop) : (x + y = 42 → P) = (y + x = 42 → P) := by ac_rfl
 
-inductive Vector (α : Type u) : Nat → Type u where
-  | nil  : Vector α 0
-  | cons : α → Vector α n → Vector α (n+1)
+inductive Vector' (α : Type u) : Nat → Type u where
+  | nil  : Vector' α 0
+  | cons : α → Vector' α n → Vector' α (n+1)
 
-def f (n : Nat) (xs : Vector α n) := xs
+def f (n : Nat) (xs : Vector' α n) := xs
 
 -- Repro: Dependent types trigger incorrect proofs
-theorem ex₂ (n m : Nat) (xs : Vector α (n+m)) (ys : Vector α (m+n)) : (f (n+m) xs, f (m+n) ys, n+m) = (f (n+m) xs, f (m+n) ys, m+n) := by
+theorem ex₂ (n m : Nat) (xs : Vector' α (n+m)) (ys : Vector' α (m+n)) : (f (n+m) xs, f (m+n) ys, n+m) = (f (n+m) xs, f (m+n) ys, m+n) := by
   ac_rfl
 
 -- Repro: Binders also trigger invalid proofs

tests/lean/run/binderNotation.lean

@@ -5,15 +5,15 @@
 
 theorem ex1 : (∃ x y : Nat, x > y) = (∃ (x : Nat) (y : Nat), x > y) := rfl
 
-abbrev Vector α n := { a : Array α // a.size = n }
+abbrev Vector' α n := { a : Array α // a.size = n }
 
-#check Σ α n, Vector α n
-#check Σ (α : Type) (n : Nat), Vector α n
-#check (α : Type) × (n : Nat) × Vector α n
+#check Σ α n, Vector' α n
+#check Σ (α : Type) (n : Nat), Vector' α n
+#check (α : Type) × (n : Nat) × Vector' α n
 
-#check Σ' α n, Vector α n
-#check Σ' (α : Type) (n : Nat), Vector α n
-#check (α : Type) ×' (n : Nat) ×' Vector α n
+#check Σ' α n, Vector' α n
+#check Σ' (α : Type) (n : Nat), Vector' α n
+#check (α : Type) ×' (n : Nat) ×' Vector' α n
 
-#check @Vector
-#check fun (α : Type) => Sigma fun (n : Nat) => Vector α n
+#check @Vector'
+#check fun (α : Type) => Sigma fun (n : Nat) => Vector' α n

tests/lean/run/eqTheoremForVec.lean

@@ -1,7 +1,7 @@
-inductive Vector (α : Type u): Nat → Type u where
-| nil : Vector α 0
-| cons (head : α) (tail : Vector α n) : Vector α (n+1)
+inductive Vector' (α : Type u): Nat → Type u where
+| nil : Vector' α 0
+| cons (head : α) (tail : Vector' α n) : Vector' α (n+1)
 
-def Vector.nth : ∀{n}, Vector α n → Fin n → α
-| n+1, Vector.cons x xs, ⟨  0, _⟩ => x
-| n+1, Vector.cons x xs, ⟨k+1, h⟩ => xs.nth ⟨k, Nat.lt_of_add_lt_add_right h⟩
+def Vector'.nth : ∀{n}, Vector' α n → Fin n → α
+| n+1, Vector'.cons x xs, ⟨  0, _⟩ => x
+| n+1, Vector'.cons x xs, ⟨k+1, h⟩ => xs.nth ⟨k, Nat.lt_of_add_lt_add_right h⟩

tests/lean/run/injectionsIssue.lean

@@ -1,10 +1,10 @@
-inductive Vector (α : Type u): Nat → Type u where
-| nil : Vector α 0
-| cons (head : α) (tail : Vector α n) : Vector α (n+1)
+inductive Vector' (α : Type u): Nat → Type u where
+| nil : Vector' α 0
+| cons (head : α) (tail : Vector' α n) : Vector' α (n+1)
 
-namespace Vector
+namespace Vector'
 
-def nth : Vector α n → Fin n → α
+def nth : Vector' α n → Fin n → α
   | cons x xs, ⟨0, _⟩ => x
   | cons x xs, ⟨k+1, h⟩ => xs.nth ⟨k, Nat.le_of_succ_le_succ h⟩
 

tests/lean/run/instanceIssues.lean

@@ -1,9 +1,9 @@
-inductive Vector (α : Type u) : Nat → Type u
-  | nil  : Vector α 0
-  | cons : α → Vector α n → Vector α (n + 1)
+inductive Vector' (α : Type u) : Nat → Type u
+  | nil  : Vector' α 0
+  | cons : α → Vector' α n → Vector' α (n + 1)
 
-def test [Monad m] (xs : Vector α a) : m Unit :=
+def test [Monad m] (xs : Vector' α a) : m Unit :=
   match xs with
-  | Vector.nil => return ()
-  | Vector.cons _ xs => test xs
+  | Vector'.nil => return ()
+  | Vector'.cons _ xs => test xs
 termination_by sizeOf xs

tests/lean/run/interp.lean

@@ -1,8 +1,8 @@
-inductive Vector (α : Type u) : Nat → Type u
-  | nil : Vector α 0
-  | cons : α → Vector α n → Vector α (n+1)
+inductive Vector' (α : Type u) : Nat → Type u
+  | nil : Vector' α 0
+  | cons : α → Vector' α n → Vector' α (n+1)
 
-infix:67 " :: " => Vector.cons
+infix:67 " :: " => Vector'.cons
 
 inductive Ty where
   | int
@@ -14,13 +14,13 @@ abbrev Ty.interp : Ty → Type
   | bool   => Bool
   | fn a r => a.interp → r.interp
 
-inductive HasType : Fin n → Vector Ty n → Ty → Type where
+inductive HasType : Fin n → Vector' Ty n → Ty → Type where
   | stop : HasType 0 (ty :: ctx) ty
   | pop  : HasType k ctx ty → HasType k.succ (u :: ctx) ty
 
 open HasType (stop pop)
 
-inductive Expr : Vector Ty n → Ty → Type where
+inductive Expr : Vector' Ty n → Ty → Type where
   | var   : HasType i ctx ty → Expr ctx ty
   | val   : Int → Expr ctx Ty.int
   | lam   : Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)
@@ -29,8 +29,8 @@ inductive Expr : Vector Ty n → Ty → Type where
   | ife   : Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx a
   | delay : (Unit → Expr ctx a) → Expr ctx a
 
-inductive Env : Vector Ty n → Type where
-  | nil  : Env Vector.nil
+inductive Env : Vector' Ty n → Type where
+  | nil  : Env Vector'.nil
   | cons : Ty.interp a → Env ctx → Env (a :: ctx)
 
 infix:67 " :: " => Env.cons

tests/lean/run/interp2.lean

@@ -1,8 +1,8 @@
-inductive Vector (α : Type u) : Nat → Type u
-  | nil : Vector α 0
-  | cons : α → Vector α n → Vector α (n+1)
+inductive Vector' (α : Type u) : Nat → Type u
+  | nil : Vector' α 0
+  | cons : α → Vector' α n → Vector' α (n+1)
 
-infix:67 " :: " => Vector.cons
+infix:67 " :: " => Vector'.cons
 
 inductive Ty where
   | int
@@ -14,11 +14,11 @@ abbrev Ty.interp : Ty → Type
   | bool   => Bool
   | fn a r => a.interp → r.interp
 
-inductive HasType : Fin n → Vector Ty n → Ty → Type where
+inductive HasType : Fin n → Vector' Ty n → Ty → Type where
   | stop : HasType 0 (ty :: ctx) ty
   | pop  : HasType k ctx ty → HasType k.succ (u :: ctx) ty
 
-inductive Expr : Vector Ty n → Ty → Type where
+inductive Expr : Vector' Ty n → Ty → Type where
   | var   : HasType i ctx ty → Expr ctx ty
   | val   : Int → Expr ctx Ty.int
   | lam   : Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)
@@ -27,8 +27,8 @@ inductive Expr : Vector Ty n → Ty → Type where
   | ife   : Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx a
   | delay : (Unit → Expr ctx a) → Expr ctx a
 
-inductive Env : Vector Ty n → Type where
-  | nil  : Env Vector.nil
+inductive Env : Vector' Ty n → Type where
+  | nil  : Env Vector'.nil
   | cons : Ty.interp a → Env ctx → Env (a :: ctx)
 
 infix:67 " :: " => Env.cons

tests/lean/run/overloadsAndDelayedCoercions.lean

@@ -1,19 +1,19 @@
 universe u
 
-inductive Vector (α : Type u) : Nat → Type u
-  | nil : Vector α 0
-  | cons : {n : Nat} → α → Vector α n → Vector α (n+1)
+inductive Vector' (α : Type u) : Nat → Type u
+  | nil : Vector' α 0
+  | cons : {n : Nat} → α → Vector' α n → Vector' α (n+1)
 
-infix:67 " :: " => Vector.cons
+infix:67 " :: " => Vector'.cons
 
 inductive Ty where
   | int
   | bool
   | fn (a r : Ty)
 
-inductive HasType' : {n : Nat} → Vector Ty n → Type where
+inductive HasType' : {n : Nat} → Vector' Ty n → Type where
   | stop {ty : Ty} : HasType' (ty :: ctx)
 
-inductive HasType : Fin n → Vector Ty n → Ty → Type where
+inductive HasType : Fin n → Vector' Ty n → Ty → Type where
   | stop : HasType 0 (ty :: ctx) ty
   | pop  : HasType k ctx ty → HasType k.succ (u :: ctx) ty

tests/lean/run/smartUnfoldingBug.lean

@@ -76,15 +76,15 @@ def delete{α : Type}{n: Nat}(k : Nat) (kw : k < (n + 1)) (seq : FinSeq (n + 1)
 
 end FinSeq
 
-inductive Vector (α : Type) : Nat → Type where
-  | nil : Vector α zero
-  | cons{n: Nat}(head: α) (tail: Vector  α n) : Vector α  (n + 1)
+inductive Vector' (α : Type) : Nat → Type where
+  | nil : Vector' α zero
+  | cons{n: Nat}(head: α) (tail: Vector'  α n) : Vector' α  (n + 1)
 
-infixr:66 "+:" => Vector.cons
+infixr:66 "+:" => Vector'.cons
 
-open Vector
+open Vector'
 
-def Vector.coords {α : Type}{n : Nat}(v: Vector α n) : FinSeq n α :=
+def Vector'.coords {α : Type}{n : Nat}(v: Vector' α n) : FinSeq n α :=
   fun j jw =>
   match n, v, j, jw with
   | .(zero), nil, k, lt => nomatch lt
@@ -92,8 +92,8 @@ def Vector.coords {α : Type}{n : Nat}(v: Vector α n) : FinSeq n α :=
   | m + 1, cons head tail, j + 1, w =>  tail.coords j (Nat.le_of_succ_le_succ w)
 
 def seqVecAux {α: Type}{n m l: Nat}: (s : n + m = l) →
-    (seq1 : FinSeq n α) → (accum : Vector α m) →
-       Vector α l:=
+    (seq1 : FinSeq n α) → (accum : Vector' α m) →
+       Vector' α l:=
     match n with
     | zero => fun s => fun _ => fun seq2 =>
       by
@@ -101,7 +101,7 @@ def seqVecAux {α: Type}{n m l: Nat}: (s : n + m = l) →
           rw [← s]
           apply Nat.zero_add
           done
-        have sf : Vector α l = Vector α m := by
+        have sf : Vector' α l = Vector' α m := by
           rw [ss]
         exact Eq.mpr sf seq2
         done
@@ -114,24 +114,24 @@ def seqVecAux {α: Type}{n m l: Nat}: (s : n + m = l) →
           done
       seqVecAux ss (seq1.init) ((seq1.last) +: seq2)
 
-def FinSeq.vec {α : Type}{n: Nat} : FinSeq n α  →  Vector α n :=
-    fun seq => seqVecAux (Nat.add_zero n) seq Vector.nil
+def FinSeq.vec {α : Type}{n: Nat} : FinSeq n α  →  Vector' α n :=
+    fun seq => seqVecAux (Nat.add_zero n) seq Vector'.nil
 
-def Clause(n : Nat) : Type := Vector (Option Bool) n
+def Clause(n : Nat) : Type := Vector' (Option Bool) n
 
-def Valuation(n: Nat) : Type := Vector Bool n
+def Valuation(n: Nat) : Type := Vector' Bool n
 
-inductive SatAnswer{dom n: Nat}(clauses : Vector (Clause n) dom) where
+inductive SatAnswer{dom n: Nat}(clauses : Vector' (Clause n) dom) where
   | unsat : SatAnswer clauses
   | sat :  SatAnswer clauses
 
 structure SimpleRestrictionClauses{dom n: Nat}
-    (clauses: Vector (Clause (n + 1)) dom) where
+    (clauses: Vector' (Clause (n + 1)) dom) where
   codom : Nat
-  restClauses : Vector  (Clause n) codom
+  restClauses : Vector'  (Clause n) codom
 
 def prependRes{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1)
-    (clauses: Vector (Clause (n + 1)) dom):
+    (clauses: Vector' (Clause (n + 1)) dom):
         (rd : SimpleRestrictionClauses clauses) →
            (head : Clause (n + 1)) →
         SimpleRestrictionClauses (head +: clauses) :=
@@ -142,15 +142,15 @@ def prependRes{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1)
             ⟨rd.codom + 1, (FinSeq.vec (FinSeq.delete focus focusLt head.coords)) +: rd.restClauses⟩
 
 def restClauses{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1)
-        (clauses: Vector (Clause (n + 1)) dom) :
+        (clauses: Vector' (Clause (n + 1)) dom) :
          SimpleRestrictionClauses clauses :=
             match dom, clauses with
-            | 0, _ =>  ⟨0, Vector.nil⟩
-            | m + 1, Vector.cons head clauses =>
+            | 0, _ =>  ⟨0, Vector'.nil⟩
+            | m + 1, Vector'.cons head clauses =>
                 prependRes branch focus focusLt clauses
                             (restClauses branch focus focusLt clauses) head
 
-def answerSAT{n dom : Nat}: (clauses : Vector (Clause n) dom) →  SatAnswer clauses :=
+def answerSAT{n dom : Nat}: (clauses : Vector' (Clause n) dom) →  SatAnswer clauses :=
       match n with
       | zero =>
            match dom with
@@ -193,11 +193,11 @@ syntax (name:= nrmlform)"whnf!" term : term
 
 
 def cls1 : Clause 2 := -- ¬P
-  (some false) +: (none) +: Vector.nil
+  (some false) +: (none) +: Vector'.nil
 
-def cls2 : Clause 2 := (some true) +: none +: Vector.nil  -- P
+def cls2 : Clause 2 := (some true) +: none +: Vector'.nil  -- P
 
-def egStatement := cls1 +: cls2 +: Vector.nil
+def egStatement := cls1 +: cls2 +: Vector'.nil
 
 def egAnswer : SatAnswer egStatement := answerSAT egStatement
 

tests/lean/tabulate.lean

@@ -1,13 +1,13 @@
-inductive Vector (α : Type u) : Nat → Type u
-  | nil : Vector α 0
-  | cons : α → Vector α n → Vector α (n+1)
+inductive Vector' (α : Type u) : Nat → Type u
+  | nil : Vector' α 0
+  | cons : α → Vector' α n → Vector' α (n+1)
   deriving Repr
 
-infix:67 " :: " => Vector.cons
+infix:67 " :: " => Vector'.cons
 
-def tabulate (f : Fin n → α) : Vector α n :=
+def tabulate (f : Fin n → α) : Vector' α n :=
   match n with
-  | 0   => Vector.nil
+  | 0   => Vector'.nil
   | n+1 => f 0 :: tabulate (f ∘ Fin.succ)
 
 #eval tabulate fun i : Fin 5 => i

tests/lean/tabulate.lean.expected.out

@@ -1 +1 @@
-Vector.cons 0 (Vector.cons 1 (Vector.cons 2 (Vector.cons 3 (Vector.cons 4 (Vector.nil)))))
+Vector'.cons 0 (Vector'.cons 1 (Vector'.cons 2 (Vector'.cons 3 (Vector'.cons 4 (Vector'.nil)))))