Generic Slice Type Classes

This file defines type classes for slicing operations on collections, inspired by Python's slice notation. The notation provides three operations:

• v⟦:m⟧ takes the first m elements (via SliceLT)
• v⟦m:⟧ drops the first m elements (via SliceGE)
• v⟦m₁:m₂⟧ takes elements from index m₁ to m₂ - 1 (via Slice)

Each notation also supports manual proof syntax with 'h:

• v⟦:m⟧'h for explicit proof in SliceLT
• v⟦m:⟧'h for explicit proof in SliceGE
• v⟦m₁:m₂⟧'h for explicit proof in Slice

The design follows the pattern of GetElem from the standard library, with:

• outParam annotations for better type inference
• Validity predicates that can be automatically proven by tactics like omega
• Dependent types where the result collection type can depend on all parameters

Type Classes

• SliceLT: For "take first n elements" operations
• SliceGE: For "drop first n elements" operations
• Slice: For "range slice" operations

The type classes are generic and can be implemented for any collection type. This file provides instances for:

• Fin tuples: Available in Starlib.Data.Fin.Tuple.Notation (with proof obligations)
• Array: With True validity (no proof obligations needed)
• List: With True validity (no proof obligations needed)

Sliceable type classes

class SliceLT (coll : Type u) (stop : Type v) (valid : outParam (coll → stop → Prop)) (subcoll : outParam ((xs : coll) → (stop : stop) → valid xs stop → Type w)) : Type (max (max u v) w)

Type class for "take first n elements" operations: v⟦:m⟧

We allow for the final subcollection type subcoll to depend on all prior parameters: the collection type coll, the stop index type stop, the validity predicate valid.

• sliceLT (xs : coll) (stop : stop) (h : valid xs stop) : subcoll xs stop h

class SliceGE (coll : Type u) (start : Type v) (valid : outParam (coll → start → Prop)) (subcoll : outParam ((xs : coll) → (start : start) → valid xs start → Type w)) : Type (max (max u v) w)

Type class for "drop first n elements" operations: v⟦m:⟧

We allow for the final subcollection type subcoll to depend on all prior parameters: the collection type coll, the start index type start, the validity predicate valid.

• sliceGE (xs : coll) (start : start) (h : valid xs start) : subcoll xs start h

class Slice (coll : Type u) (start : Type v) (stop : Type v') (valid : outParam (coll → start → stop → Prop)) (subcoll : outParam ((xs : coll) → (start : start) → (stop : stop) → valid xs start stop → Type w)) : Type (max (max (max u v) v') w)

Type class for "slice range" operations: v⟦m₁:m₂⟧

We allow for the final subcollection type subcoll to depend on all prior parameters: the collection type coll, the start index type start, the stop index type stop, the validity predicate valid.

• slice (xs : coll) (start : start) (stop : stop) (h : valid xs start stop) : subcoll xs start stop h

Slice notation

Note: currently we use get_elem_tactic to automatically prove the validity of the indices. We should switch to a more tailored tactic in the future.

def sliceLTNotation : Lean.TrailingParserDescr

Notation v⟦:stop⟧ for taking the first stop elements (indexed from 0 to stop - 1) of a collection, assuming the validity for stop can be automatically proven

def sliceLTNotationWithProof : Lean.TrailingParserDescr

Notation v⟦:stop⟧'h for taking the first stop elements (indexed from 0 to stop - 1) with explicit proof

def sliceGENotation : Lean.TrailingParserDescr

Notation v⟦start:⟧ for dropping the first start elements of a collection, assuming the validity for start can be automatically proven

def sliceGENotationWithProof : Lean.TrailingParserDescr

Notation v⟦start:⟧'h for dropping the first start elements with explicit proof

def sliceNotation : Lean.TrailingParserDescr

Notation v⟦start:stop⟧ for taking elements from index start to stop - 1 (e.g., v⟦1:3⟧ = v[1] ++ v[2]), with range proofs automatically synthesized

def sliceNotationWithProof : Lean.TrailingParserDescr

Notation v⟦start:stop⟧'h for taking elements from index start to stop - 1 (e.g., v⟦1:3⟧ = ![v 1, v 2]), with explicit proof

Unexpander for slice notation

We provide unexpanders to display slice operations in their slice notation form in goal states and error messages, providing a better user experience.

def sliceLTUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander for SliceLT.sliceLT to display as v⟦:stop⟧

def sliceGEUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander for SliceGE.sliceGE to display as v⟦start:⟧

def sliceUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander for Slice.slice to display as v⟦start:stop⟧

Instances for Array

Arrays support slice notation with no proof obligations since Array operations handle boundary cases gracefully (e.g., taking more elements than exist returns the whole array).

@[implicit_reducible]

instance instSliceLTArrayNatTrue {α : Type u} : SliceLT (Array α) Nat (fun (x : Array α) (x_1 : Nat) => True) fun (x : Array α) (x_1 : Nat) (x_2 : True) => Array α

@[implicit_reducible]

instance instSliceGEArrayNatTrue {α : Type u} : SliceGE (Array α) Nat (fun (x : Array α) (x_1 : Nat) => True) fun (x : Array α) (x_1 : Nat) (x_2 : True) => Array α

@[implicit_reducible]

instance instSliceArrayNatTrue {α : Type u} : Slice (Array α) Nat Nat (fun (x : Array α) (x_1 x_2 : Nat) => True) fun (x : Array α) (x_1 x_2 : Nat) (x_3 : True) => Array α

Instances for List

Lists support slice notation with no proof obligations since List operations handle boundary cases gracefully (e.g., taking more elements than exist returns the whole list).

@[implicit_reducible]

instance instSliceLTListNatTrue {α : Type u} : SliceLT (List α) Nat (fun (x : List α) (x_1 : Nat) => True) fun (x : List α) (x_1 : Nat) (x_2 : True) => List α

@[implicit_reducible]

instance instSliceGEListNatTrue {α : Type u} : SliceGE (List α) Nat (fun (x : List α) (x_1 : Nat) => True) fun (x : List α) (x_1 : Nat) (x_2 : True) => List α

@[implicit_reducible]

instance instSliceListNatTrue {α : Type u} : Slice (List α) Nat Nat (fun (x : List α) (x_1 x_2 : Nat) => True) fun (x : List α) (x_1 x_2 : Nat) (x_3 : True) => List α

Examples