Mathlib.Computability.TuringMachine._auxLemma.5
theorem Mathlib.Computability.TuringMachine._auxLemma.5 : ∀ {a b c : Prop}, (a ∧ b → c) = (a → b → c)
This theorem states that for any three propositions `a`, `b`, and `c`, the statement "`a` and `b` imply `c`" is equivalent to the statement "`a` implies that `b` implies `c`". In other words, if `a` and `b` are both true, then `c` is true; this is the same as saying that if `a` is true, then if `b` is also true, `c` must be true. This illustrates one of the ways in which logical implications can be chained together.
More concisely: The theorem asserts that `(a → b) → (a → c) ≡ a → (b → c)` in propositional logic.
|
Turing.PointedMap.map_pt
theorem Turing.PointedMap.map_pt :
∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ'),
f.f default = default
This theorem, `Turing.PointedMap.map_pt`, states that for all types 'Γ' and 'Γ'', assuming both types are inhabited (i.e., they contain at least one element), any pointed map 'f' from 'Γ' to 'Γ'' maps the default value of 'Γ' to the default value of 'Γ''. In other words, the pointed map preserves the default values between the two types.
More concisely: For any inhabited types 'Γ' and 'Γ'' and a pointed map f from 'Γ' to 'Γ'' between them, the default value of 'Γ' maps to the default value of 'Γ'' under f.
|
Mathlib.Computability.TuringMachine._auxLemma.15
theorem Mathlib.Computability.TuringMachine._auxLemma.15 :
∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [inst : DecidableEq β] {b : β},
(b ∈ s.biUnion t) = ∃ a ∈ s, b ∈ t a
The theorem `_auxLemma.15` from the `Mathlib.Computability.TuringMachine` module states that for any types `α` and `β`, a finite set `s` of type `α`, a function `t` which maps elements of `α` to finite sets of `β`, and a decidable equality on `β`, then for any element `b` of `β`, `b` is in the bi-union of `s` and `t` if and only if there exists an element `a` in `s` such that `b` is in `t(a)`. Here, `biUnion s t` represents the union of the sets `t a` for all `a` in `s`.
More concisely: For any types α and β, finite set s of α, function t: α → β with values in finite sets, and decidable equality on β, an element b is in the bi-union of s and t if and only if there exists an a in s such that b is in t(a).
|
Turing.ListBlank.tail_map
theorem Turing.ListBlank.tail_map :
∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ')
(l : Turing.ListBlank Γ), (Turing.ListBlank.map f l).tail = Turing.ListBlank.map f l.tail
The theorem `Turing.ListBlank.tail_map` states that for any types `Γ` and `Γ'` such that `Γ` and `Γ'` are inhabited, and for any pointed map `f` from `Γ` to `Γ'` and any list blank `l` of type `Γ`, the tail of the map of `f` on `l` is the same as the map of `f` on the tail of `l`. In other words, mapping a function over a list blank and then taking the tail is the same as taking the tail first and then mapping the function. This is a kind of commutativity property between the tail operation and the map operation on list blanks in the context of Turing machines.
More concisely: For any type `Γ`, any inhabited types `Γ'`, any pointed map `f` from `Γ` to `Γ'`, and any list blank `l` of type `Γ`, the map of `f` on the tail of `l` is equal to the tail of the map of `f` on `l`.
|
Mathlib.Computability.TuringMachine._auxLemma.6
theorem Mathlib.Computability.TuringMachine._auxLemma.6 :
∀ {α : Sort u_1} {p : α → Prop} {b : Prop}, ((∃ x, p x) → b) = ∀ (x : α), p x → b
This theorem states that for any type `α` and any predicates `p` on `α` and `b`, the proposition that if there exists an `x` of type `α` such that `p x` is true then `b` is true, is equivalent to the proposition that for all `x` of type `α`, if `p x` is true then `b` is true. In LaTeX form it says: $(\exists x \, p(x)) \rightarrow b \equiv \forall x \, (p(x) \rightarrow b)$.
More concisely: The theorem asserts that existence and universality quantifier logic equivalence holds for predicates `p` on type `α` and proposition `b`, i.e., `(∃x:α. p x) → b ↔ ∀x:α. p x → b`.
|
Turing.ListBlank.map_cons
theorem Turing.ListBlank.map_cons :
∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ')
(l : Turing.ListBlank Γ) (a : Γ),
Turing.ListBlank.map f (Turing.ListBlank.cons a l) = Turing.ListBlank.cons (f.f a) (Turing.ListBlank.map f l)
The theorem `Turing.ListBlank.map_cons` states that for any given types `Γ` and `Γ'` that are inhabited, any pointed map `f` from `Γ` to `Γ'`, any list blank `l` of type `Γ`, and any element `a` of type `Γ`, the operation of mapping `f` over the list blank that is obtained by consing `a` onto `l` is equivalent to consing the result of applying `f` to `a` onto the list blank that is obtained by mapping `f` over `l`. In other words, it states that the map function provided for `ListBlank`s commutes with the cons operation.
More concisely: For any types `Γ` and `Γ'`, pointed maps `f : Γ → Γ'`, list blanks `l : ListBlank Γ`, and elements `a : Γ`, the application of `f` to the cons operation `a :: l` is equivalent to `f a :: f <$> l`.
|
Mathlib.Computability.TuringMachine._auxLemma.8
theorem Mathlib.Computability.TuringMachine._auxLemma.8 :
∀ {α : Sort u_1} {p : α → Prop} {a' : α}, (∀ (a : α), a' = a → p a) = p a'
This theorem, from the Turing Machine section of the Mathlib library in Lean, states that for any type 'α' and any predicate 'p' on this type, and for any element 'a' of type 'α', the proposition that 'p' is true for all elements 'a' that are equal to 'a', is equivalent to the proposition that 'p' is true for 'a'. In simpler terms, it means that if a predicate is true for all elements equal to a given element, then it is true for that given element.
More concisely: For any type 'α' and predicate 'p' on 'α', the equality 'a = x' implies 'p(a) <-> ∀(y : α), a = y -> p(y)' (where '<->' denotes logical equivalence).
|
Turing.ListBlank.tail_cons
theorem Turing.ListBlank.tail_cons :
∀ {Γ : Type u_1} [inst : Inhabited Γ] (a : Γ) (l : Turing.ListBlank Γ), (Turing.ListBlank.cons a l).tail = l := by
sorry
The theorem `Turing.ListBlank.tail_cons` states that for any type `Γ` that has an instance of the `Inhabited` type class, any element `a` of type `Γ`, and any Turing `ListBlank` `l` of type `Γ`, the tail of the `ListBlank` resulting from consing `a` onto `l` is equal to `l`. In other words, if you prepend an element `a` to a Turing `ListBlank` `l` and then take the tail of the resulting `ListBlank`, the result is the original `ListBlank` `l`. This theorem formalizes a fundamental property of the `cons` function in traditional list theory in the context of Turing `ListBlank`.
More concisely: For any type `Γ` with an `Inhabited` instance, and any `a : Γ` and `l : ListBlank Γ`, the tail of the list obtained by consing `a` to `l` is equal to `l`.
|
Turing.BlankExtends.refl
theorem Turing.BlankExtends.refl : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (l : List Γ), Turing.BlankExtends l l := by
sorry
The theorem `Turing.BlankExtends.refl` states that, for any type `Γ` that has an inhabited instance and any list `l` of type `List Γ`, the `Turing.BlankExtends` partial order holds between `l` and itself. In other words, any list `l` can be viewed as being obtained by adding zero blanks to the end of itself.
More concisely: For any type `Γ` with an inhabited instance and any list `l` of type `List Γ`, `l` is related to itself under the `Turing.BlankExtends` partial order.
|
Turing.BlankExtends.above_of_le
theorem Turing.BlankExtends.above_of_le :
∀ {Γ : Type u_1} [inst : Inhabited Γ] {l l₁ l₂ : List Γ},
Turing.BlankExtends l₁ l → Turing.BlankExtends l₂ l → l₁.length ≤ l₂.length → Turing.BlankExtends l₁ l₂
The theorem `Turing.BlankExtends.above_of_le` asserts that for any type `Γ` that is inhabited, and for any lists `l`, `l₁`, and `l₂` of type `Γ`, if `l` can be obtained by adding blanks to the end of `l₁` (denoted by `Turing.BlankExtends l₁ l`) and to the end of `l₂` (denoted by `Turing.BlankExtends l₂ l`), and if the length of `l₁` is less than or equal to the length of `l₂` (`List.length l₁ ≤ List.length l₂`), then `l₂` can be obtained by adding blanks to the end of `l₁` (denoted by `Turing.BlankExtends l₁ l₂`). This theorem is relevant in the context of Turing machines, where "adding blanks to the end of a list" can be interpreted as extending the tape of the machine to the right.
More concisely: If `Γ` is inhabited and `l₁`, `l₂` are lists of type `Γ` such that `l` is obtained by extending `l₁` and `l₂` with blanks, and the length of `l₁` is less than or equal to that of `l₂`, then `l₂` can be obtained by extending `l₁` with blanks.
|
Turing.ListBlank.cons_head_tail
theorem Turing.ListBlank.cons_head_tail :
∀ {Γ : Type u_1} [inst : Inhabited Γ] (l : Turing.ListBlank Γ), Turing.ListBlank.cons l.head l.tail = l
The theorem `Turing.ListBlank.cons_head_tail` asserts that for any type `Γ` that is inhabited and for any 'ListBlank' of type `Γ`, the 'cons' function and the 'head'/'tail' functions are mutually inverse. This simply means that if you take the head of a `ListBlank` and cons it onto the tail of the `ListBlank`, you get back the original `ListBlank`. This is in contrast to the case of `List`, where this property only holds for nonempty lists.
More concisely: For any type `Γ` and any `ListBlank` of length `n+1` over `Γ`, the `cons` function applied to the `head` of `ListBlank` and the `tail` of `ListBlank` is equal to the original `ListBlank`.
|
Turing.ListBlank.head_cons
theorem Turing.ListBlank.head_cons :
∀ {Γ : Type u_1} [inst : Inhabited Γ] (a : Γ) (l : Turing.ListBlank Γ), (Turing.ListBlank.cons a l).head = a := by
sorry
This theorem states that for any type `Γ` that is inhabited (i.e., it is not an empty type), and any element `a` of type `Γ` and any `ListBlank` of `Γ` named `l`, the head of the `ListBlank` obtained by consing `a` onto `l` is `a`. It essentially posits the basic property of a "cons" operation in a list-like structure, asserting that when an element is added to the beginning of a list, it becomes the new head of the list.
More concisely: For any type `Γ` and element `a` in `Γ`, the head of the list obtained by consing `a` to a list `l` of type `ListBlank Γ` is `a`.
|
Turing.ListBlank.nth_map
theorem Turing.ListBlank.nth_map :
∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ')
(l : Turing.ListBlank Γ) (n : ℕ), (Turing.ListBlank.map f l).nth n = f.f (l.nth n)
The theorem `Turing.ListBlank.nth_map` states that for any types `Γ` and `Γ'` (assumed to be inhabited), a pointed map `f` from `Γ` to `Γ'`, a `ListBlank` `l` of type `Γ`, and a natural number `n`, the `n`-th element of the `ListBlank` obtained by mapping `f` over `l` is the same as the result of applying `f` to the `n`-th element of `l`. In other words, it establishes the property that the `map` and `nth` operations on `ListBlank`s commute with each other under the application of a pointed map.
More concisely: For any pointed map `f` and `ListBlank` `l`, the `n`-th element of the list obtained by mapping `f` over `l` is equal to applying `f` to the `n`-th element of `l`.
|
Turing.ListBlank.nth_succ
theorem Turing.ListBlank.nth_succ :
∀ {Γ : Type u_1} [inst : Inhabited Γ] (l : Turing.ListBlank Γ) (n : ℕ), l.nth (n + 1) = l.tail.nth n
This theorem states that for any type `Γ`, given that `Γ` is inhabited, and for any `l` of type `ListBlank Γ` and any natural number `n`, the `n+1`-th element of `l` is the same as the `n`-th element of the tail of `l`. In other words, removing the first element from a `ListBlank` and then retrieving the `n`-th element is equivalent to retrieving the `n+1`-th element from the original `ListBlank`. This is analogous to the behavior of lists in many programming languages where retrieving an element from the tail of the list effectively decreases the index by one.
More concisely: For any inhabited type `Γ` and `ListBlank Γ` `l` with `n` greater than zero, the `n+1`-th element of `l` equals the `n`-th element of `l.tail`.
|
Turing.ListBlank.head_map
theorem Turing.ListBlank.head_map :
∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ')
(l : Turing.ListBlank Γ), (Turing.ListBlank.map f l).head = f.f l.head
The theorem `Turing.ListBlank.head_map` states that for any `ListBlank` `l` of type `Γ` and any pointed map `f` from `Γ` to `Γ'`, the result of applying `f` to the head of `l` is the same as the head of the result of mapping `f` over `l`. That is, when we have an infinitely extendable list (a `ListBlank`) and a function that can be applied to each element of the list, applying this function to the first element of the list is the same as first applying the function to all elements of the list and then taking the first element. This aligns with the expected behaviour of the `map` operation in functional programming.
More concisely: For any `ListBlank` `l` of type `Γ` and any pointed map `f` from `Γ` to `Γ'`, the head of `map f l` equals `f (head l)`.
|
Turing.ListBlank.nth_zero
theorem Turing.ListBlank.nth_zero : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (l : Turing.ListBlank Γ), l.nth 0 = l.head
The theorem `Turing.ListBlank.nth_zero` states that for any type `Γ` that has an instance of `Inhabited` and any `ListBlank` of this type `l`, the element at the zeroth index of `l` (obtained using `Turing.ListBlank.nth`) is the same as the head of `l` (obtained using `Turing.ListBlank.head`). This is akin to stating that for an infinitely extended list, the first element is the same as the head of the list.
More concisely: For any type `Γ` with an `Inhabited` instance and any `ListBlank Γ l`, the zeroth element of `l` equals the head of `l`.
|
Turing.ListBlank.exists_cons
theorem Turing.ListBlank.exists_cons :
∀ {Γ : Type u_1} [inst : Inhabited Γ] (l : Turing.ListBlank Γ), ∃ a l', l = Turing.ListBlank.cons a l'
This theorem states that for every instance of a `ListBlank` type, denoted by `l`, in a given type `Γ`, there exists an element `a` and another `ListBlank` `l'` such that `l` is obtained by appending `a` onto `l'` using the `cons` operation. This behavior is unlike the case of the `List` type, where it only holds for non-empty lists. In other words, `ListBlank` can always be decomposed into a head and a tail, due to its interpretation as an infinite list with trailing blanks.
More concisely: For every `ListBlank` `l` in type `Γ`, there exist an element `a` and a `ListBlank` `l'` such that `l = cons a l'`.
|
Turing.mem_eval
theorem Turing.mem_eval :
∀ {σ : Type u_1} {f : σ → Option σ} {a b : σ}, b ∈ Turing.eval f a ↔ Turing.Reaches f a b ∧ f b = none
This theorem states that for any type `σ` and a state transition function `f : σ → Option σ`, and for any elements `a` and `b` of type `σ`, `b` is in the "completion" of the evaluation of `f` starting from `a` if and only if there is a finite sequence of steps starting from `a` and ending at `b` (possibly with no steps, i.e., `a` equals `b`) such that each step is a valid transition under `f`, and at the end state `b`, the function `f` does not produce a new state (i.e., `f b = none`). This theorem is essentially characterizing the completion of state transitions as sequences of steps that eventually reach a state from which there is no next state under the transition function.
More concisely: A state `b` is in the completion of the evaluation of the state transition function `f` starting from state `a` if and only if there exists a finite sequence of valid transitions from `a` to `b` such that `f` does not produce a new state at `b`.
|
Turing.TM2to1.addBottom.proof_1
theorem Turing.TM2to1.addBottom.proof_1 : ∀ {K : Type u_1} {Γ : K → Type u_2}, (false, default) = (false, default) := by
sorry
This theorem states that for any Type `K` and any function `Γ` that maps from `K` to some other Type, the pair `(false, default)` is equal to itself. The theorem is applicable in the context of Turing machines, specifically in the conversion from a 2-stack to a 1-stack Turing machine (`TM2to1`). Here, `false` represents a boolean value and `default` refers to a default value of an unspecified type.
More concisely: The theorem asserts that the pair `(false, default)` is equal to itself, for any type `K` and function `Γ`.
|
Turing.BlankExtends.below_of_le
theorem Turing.BlankExtends.below_of_le :
∀ {Γ : Type u_1} [inst : Inhabited Γ] {l l₁ l₂ : List Γ},
Turing.BlankExtends l l₁ → Turing.BlankExtends l l₂ → l₁.length ≤ l₂.length → Turing.BlankExtends l₁ l₂
This theorem is saying that for any type `Γ`, given three lists `l`, `l₁`, and `l₂` of type `Γ`, if the partial order `Turing.BlankExtends` holds between `l` and `l₁` and also between `l` and `l₂`, and the length of `l₁` is less than or equal to the length of `l₂`, then `Turing.BlankExtends` also holds between `l₁` and `l₂`.
In other words, if `l₁` and `l₂` are extensions of the same list `l` where they extend `l` by adding blanks at the end and the length of `l₁` is less than or equal to the length of `l₂`, then `l₂` can be viewed as an extension of `l₁` by adding blanks at the end.
More concisely: If `l`, `l₁`, and `l₂` are lists of the same type `Γ` such that `Turing.BlankExtends l l₁` and `Turing.BlankExtends l l₂`, and the length of `l₁` is less than or equal to the length of `l₂`, then `Turing.BlankExtends l₁ l₂`.
|
Mathlib.Computability.TuringMachine._auxLemma.14
theorem Mathlib.Computability.TuringMachine._auxLemma.14 :
∀ {α : Type u_1} {s : Finset α} {o : Option α}, (o ∈ Finset.insertNone s) = ∀ a ∈ o, a ∈ s
This theorem states that for any type `α`, any finite set `s` of type `α`, and any optional value `o` of type `α`, `o` is an element of the finite set obtained by inserting 'None' into `s` (via the `Finset.insertNone` function) if and only if for all elements `a` in `o`, `a` is also an element of `s`. In other words, this theorem characterizes the membership of an optional value in the finite set formed by lifting `s` to 'Option α' and adding 'None' as an additional element.
More concisely: For any type `α`, any finite set `s` of `α`, and optional value `o` of `α`, `o` is an element of the finite set `{None} ⊎ s` if and only if every component of `o` (if it is some value) is in `s`.
|
Mathlib.Computability.TuringMachine._auxLemma.16
theorem Mathlib.Computability.TuringMachine._auxLemma.16 :
∀ {α : Type u_1} {a : α} {b : Option α}, (a ∈ b) = (b = some a)
This theorem, named `Mathlib.Computability.TuringMachine._auxLemma.16` in the Lean theorem prover, states that for any type `α` and any elements `a` of type `α` and `b` of type `Option α`, `a` is in `b` if and only if `b` is equal to `some a`. In other words, an element `a` is contained in an option `b` if and only if that option is not `none`, but specifically the option of `a`.
More concisely: For any type `α` and `a : α`, ` Option.equal (some a) (some x) ≃ (x = a) ` (where `Option` is the Lean option type).
|