Commit 2024-10-31 00:24 4b5f1a09

feat(Data/Fin/Tuple): Define Fin.take and initial theorems (#17196) This PR defines Fin.take, which takes the first m elements of an n-tuple (from the left). It requires that m ≤ n, and returns an m-tuple. This is an analogue of List.take. It also provides initial theorems for Fin.take. If all goes well, I plan to add more theorems over time, and also define rtake to be taking from the right, similar to List.rtake. Context: I'm working on a formalization of interactive proof systems. As part of that process, I need to define the type of message sent in each round, as something like:

def MessageType (numRounds : ℕ) := Fin numRounds → Type
def message (numRounds : ℕ) : ∀ i, (MessageType numRounds) i

Then I will also need to talk about composition and restriction of interactive protocols. Composition amounts to Fin.addCases, but restriction is my new Fin.take, and also Fin.rtake in the future (taking from the right).