# Lecture - Functional Programming, MT22, VII

> Source: https://ollybritton.com/notes/uni/prelims/mt22/functional-programming/lectures/7/ · Updated: 2022-11-08 · Tags: uni, lecture

- [Course - Functional Programming MT22](https://ollybritton.com/notes/uni/prelims/mt22/functional-programming/)

### Flashcards
What is the “take lemma” about $\text{xs}$ and $\text{ys}$?::
$$
\forall n \in \mathbb{N} \text{ (take n xs} = \text{take n ys)} \implies \text{xs} = \text{ys}
$$

Why is the take lemma useful?::
Because it lets you prove stuff about functions that return lists using induction on the natural numbers.

What is a partial list?::
A list with a tail that is either $\bot$ or a smaller partial list.

What’s the induction scheme for proving a property $P(\text{xs})$  is true for all finite lists?::
- Prove $P([])$
- Prove $P(\text{xs}) \implies P(\text{x}:\text{xs})$

What’s the induction scheme for proving a property $P(\text{xs})$ is true for all partial lists?::
- Prove $P(\bot)$
- Prove $P([])$
- Prove $P(\text{xs}) \implies P(\text{x}:\text{xs})$

Given that $P$ is chain-complete (i.e. because it’s an equation between haskell expressions) then what is the induction scheme for proving a property $P(\text{xs})$ about all infinite lists?::
- Prove $P(\bot)$
- Prove $P([])$
- Prove $P(\text{xs}) \implies P(\text{x}:\text{xs})$

What’s a good heuristic for deciding what variable to induct on when proving something about a program?::
Look at what the definition recurses on.

---
Olly Britton — https://ollybritton.com. Machine-readable index: https://ollybritton.com/llms.txt