[Merged by Bors] - feat(Data/Fin/Tuple): Define Fin.take and initial theorems

[quangvdao]

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).

---

[github-actions]

PR summary f508575c15

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Data.Fin.Tuple.Take	336

---

Declarations diff

+ get_take_eq_take_get_comp_cast
+ get_take_ofFn_eq_take_comp_cast
+ ofFn_take_eq_take_ofFn
+ ofFn_take_get
+ take
+ take_addCases_left
+ take_addCases_right
+ take_append_left
+ take_append_right
+ take_apply
+ take_eq_init
+ take_eq_self
+ take_init
+ take_one
+ take_repeat
+ take_succ_eq_snoc
+ take_take
+ take_update_of_ge
+ take_update_of_lt
+ take_zero

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[YaelDillies]

What's your use case for Fin.take?

[quangvdao]

What's your use case for Fin.take?

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).

[YaelDillies]

Seems reasonable, but let me ask among the reviewers which repository it should live in.

[quangvdao]

@kim-em I have added four theorems that intertwines Fin.take and List.take with List.get and List.ofFn. Two of the theorems have to be stated in terms of heterogeneous equality, since the types are only propeq:

/-- `Fin.take` intertwines with `List.take` via `List.get`. -/
theorem list_take_get_heq {α : Type*} {m : ℕ} (l : List α) (h : m ≤ l.length) :
    HEq (l.take m).get (take m h l.get) :=
  (Fin.heq_fun_iff (List.length_take_of_le h)).mpr (by simp)

/-- Alternative version of `list_take_get_heq` with `v : Fin n → α` instead of `l : List α`. -/
theorem list_ofFn_take_get_heq {α : Type*} {m : ℕ} (v : Fin n → α) (h : m ≤ n) :
    HEq ((List.ofFn v).take m).get (take m h v) :=
  (Fin.heq_fun_iff (by simp [h])).mpr (by simp)

Would appreciate your feedback on theorem statement & naming. Maybe I should get rid of heq in the name?

[YaelDillies]

Thanks for your patience! The end is in sight.

[YaelDillies]

I'm appy with this. What about you, @kim-em ?

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style