Options and list heads for fun_prop at degree one

fun_prop assembles ComputableInDegree … 1 1 certificates from rules for each operation. This module adds the rules for options and list heads that it lacked, so that a definition using them needs no restatement in terms of tests and defaults:

• Option.elim, which is also the form option_match_to_elim gives a match on an option;
• List.head?;
• Option.some, Option.getD, List.headD, List.tail and List.isEmpty, registered as fun_prop rules.

Option.elim and List.head? are stated for linear time and space and linear output growth, which is what composition at degree one needs.

Main results

• Turing.MultiTapeTM.ComputableInDegree.optionElim_one: eliminating an option.
• Turing.MultiTapeTM.ComputableInDegree.head?_one: the head of a framed list.

theorem Turing.MultiTapeTM.ComputableInDegree.optionElim_one {α β γ : Type} [Inhabited β] {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {value : α → Option β} {fallback : α → γ} {body : α → β → γ} (hv : ComputableInDegree value encA (encOption encB) 1 1) (hn : ComputableInDegree fallback encA encC 1 1) (hb : ComputableInDegree (fun (p : α × β) => body p.1 p.2) (encPair encA encB) encC 1 1) : ComputableInDegree (fun (a : α) => (value a).elim (fallback a) (body a)) encA encC 1 1

Eliminating an option in linear time and space: the handler of some receives the input and the value.

theorem Turing.MultiTapeTM.ComputableInDegree.head?_one {β : Type} [Inhabited β] {enc : β ↪ List Bool} : ComputableInDegree (fun (l : List β) => l.head?) (encList enc) (encOption enc) 1 1

The head of a framed list, as an option, in linear time and space.