[Merged by Bors] - feat(computability/tm_to_partrec): partrec functions are TM-computable

src/computability/turing_machine.lean

@@ -582,8 +582,7 @@ theorem tape.map_mk₁ {Γ Γ'} [inhabited Γ] [inhabited Γ'] (f : pointed_map
 state returned before a `none` result. If the state transition function always returns `some`,
 then the computation diverges, returning `roption.none`. -/
 def eval {σ} (f : σ → option σ) : σ → roption σ :=
-pfun.fix (λ s, roption.some $
-  match f s with none := sum.inl s | some s' := sum.inr s' end)
+pfun.fix (λ s, roption.some $ (f s).elim (sum.inl s) sum.inr)
 
 /-- The reflexive transitive closure of a state transition function. `reaches f a b` means
 there is a finite sequence of steps `f a = some a₁`, `f a₁ = some a₂`, ... such that `aₙ = b`.
@@ -654,10 +653,21 @@ theorem reaches₀.tail' {σ} {f : σ → option σ} {a b c : σ}
   (h : reaches₀ f a b) (h₂ : c ∈ f b) : reaches₁ f a c :=
 h _ (trans_gen.single h₂)
 
+/-- (co-)Induction principle for `eval`. If a property `C` holds of any point `a` evaluating to `b`
+which is either terminal (meaning `a = b`) or where the next point also satisfies `C`, then it
+holds of any point where `eval f a` evaluates to `b`. This formalizes the notion that if
+`eval f a` evaluates to `b` then it reaches terminal state `b` in finitely many steps. -/
+@[elab_as_eliminator] def eval_induction {σ}
+  {f : σ → option σ} {b : σ} {C : σ → Sort*} {a : σ} (h : b ∈ eval f a)
+  (H : ∀ a, b ∈ eval f a →
+    (∀ a', b ∈ eval f a' → f a = some a' → C a') → C a) : C a :=
+pfun.fix_induction h (λ a' ha' h', H _ ha' $ λ b' hb' e, h' _ hb' $
+  roption.mem_some_iff.2 $ by rw e; refl)
+
 theorem mem_eval {σ} {f : σ → option σ} {a b} :
   b ∈ eval f a ↔ reaches f a b ∧ f b = none :=
 ⟨λ h, begin
-  refine pfun.fix_induction h (λ a h IH, _),
+  refine eval_induction h (λ a h IH, _),
   cases e : f a with a',
   { rw roption.mem_unique h (pfun.mem_fix_iff.2 $ or.inl $
       roption.mem_some_iff.2 $ by rw e; refl),
@@ -1810,7 +1820,7 @@ instance cfg.inhabited [inhabited σ] : inhabited cfg := ⟨⟨default _, defaul
 
 parameters {Γ Λ σ K}
 /-- The step function for the TM2 model. -/
-def step_aux : stmt → σ → (∀ k, list (Γ k)) → cfg
+@[simp] def step_aux : stmt → σ → (∀ k, list (Γ k)) → cfg
 | (push k f q)     v S := step_aux q v (update S k (f v :: S k))
 | (peek k f q)     v S := step_aux q (f v (S k).head') S
 | (pop k f q)      v S := step_aux q (f v (S k).head') (update S k (S k).tail)
@@ -1821,7 +1831,7 @@ def step_aux : stmt → σ → (∀ k, list (Γ k)) → cfg
 | halt             v S := ⟨none, v, S⟩
 
 /-- The step function for the TM2 model. -/
-def step (M : Λ → stmt) : cfg → option cfg
+@[simp] def step (M : Λ → stmt) : cfg → option cfg
 | ⟨none,   v, S⟩ := none
 | ⟨some l, v, S⟩ := some (step_aux (M l) v S)
 

src/data/list/basic.lean

@@ -2674,6 +2674,10 @@ theorem take_prefix (n) (l : list α) : take n l <+: l := ⟨_, take_append_drop
 
 theorem drop_suffix (n) (l : list α) : drop n l <:+ l := ⟨_, take_append_drop _ _⟩
 
+theorem tail_suffix (l : list α) : tail l <:+ l := by rw ← drop_one; apply drop_suffix
+
+theorem tail_subset (l : list α) : tail l ⊆ l := (sublist_of_suffix (tail_suffix l)).subset
+
 theorem prefix_iff_eq_append {l₁ l₂ : list α} : l₁ <+: l₂ ↔ l₁ ++ drop (length l₁) l₂ = l₂ :=
 ⟨by rintros ⟨r, rfl⟩; rw drop_left, λ e, ⟨_, e⟩⟩
 

src/data/option/defs.lean

@@ -12,7 +12,7 @@ variables {α : Type*} {β : Type*}
 attribute [inline] option.is_some option.is_none
 
 /-- An elimination principle for `option`. It is a nondependent version of `option.rec_on`. -/
-protected def elim : option α → β → (α → β) → β
+@[simp] protected def elim : option α → β → (α → β) → β
 | (some x) y f := f x
 | none     y f := y
 

src/data/pfun.lean

@@ -264,6 +264,7 @@ by rw [show f = id, from funext H]; exact id_map o
 @[simp] theorem bind_some_right (x : roption α) : x.bind some = x :=
 by rw [bind_some_eq_map]; simp [map_id']
 
+@[simp] theorem pure_eq_some (a : α) : pure a = some a := rfl
 @[simp] theorem ret_eq_some (a : α) : return a = some a := rfl
 
 @[simp] theorem map_eq_map {α β} (f : α → β) (o : roption α) :

src/data/vector2.lean

@@ -25,6 +25,15 @@ instance [inhabited α] : inhabited (vector α n) :=
 theorem to_list_injective : function.injective (@to_list α n) :=
 subtype.val_injective
 
+@[simp] theorem cons_val (a : α) : ∀ (v : vector α n), (a :: v).val = a :: v.val
+| ⟨_, _⟩ := rfl
+
+@[simp] theorem cons_head (a : α) : ∀ (v : vector α n), (a :: v).head = a
+| ⟨_, _⟩ := rfl
+
+@[simp] theorem cons_tail (a : α) : ∀ (v : vector α n), (a :: v).tail = v
+| ⟨_, _⟩ := rfl
+
 @[simp] theorem to_list_of_fn : ∀ {n} (f : fin n → α), to_list (of_fn f) = list.of_fn f
 | 0     f := rfl
 | (n+1) f := by rw [of_fn, list.of_fn_succ, to_list_cons, to_list_of_fn]
@@ -60,6 +69,9 @@ end
   nth (tail v) i = nth v i.succ
 | ⟨a::l, e⟩ ⟨i, h⟩ := by simp [nth_eq_nth_le]; refl
 
+@[simp] theorem tail_val : ∀ (v : vector α n.succ), v.tail.val = v.val.tail
+| ⟨a::l, e⟩ := rfl
+
 @[simp] theorem tail_of_fn {n : ℕ} (f : fin n.succ → α) :
   tail (of_fn f) = of_fn (λ i, f i.succ) :=
 (of_fn_nth _).symm.trans $ by congr; funext i; simp

src/logic/function/basic.lean

@@ -274,6 +274,19 @@ begin
   { simp [h] }
 end
 
+theorem update_comm {α} [decidable_eq α] {β : α → Sort*}
+  {a b : α} (h : a ≠ b) (v : β a) (w : β b) (f : Πa, β a) :
+  update (update f a v) b w = update (update f b w) a v :=
+begin
+  funext c, simp [update],
+  by_cases h₁ : c = b; by_cases h₂ : c = a; try {simp [h₁, h₂]},
+  cases h (h₂.symm.trans h₁),
+end
+
+@[simp] theorem update_idem {α} [decidable_eq α] {β : α → Sort*}
+  {a : α} (v w : β a) (f : Πa, β a) : update (update f a v) a w = update f a w :=
+by {funext b, by_cases b = a; simp [update, h]}
+
 end update
 
 lemma uncurry_def {α β γ} (f : α → β → γ) : uncurry f = (λp, f p.1 p.2) :=

src/logic/relation.lean

@@ -117,6 +117,7 @@ end
 lemma cases_tail : refl_trans_gen r a b → b = a ∨ (∃c, refl_trans_gen r a c ∧ r c b) :=
 (cases_tail_iff r a b).1
 
+@[elab_as_eliminator]
 lemma head_induction_on
   {P : ∀(a:α), refl_trans_gen r a b → Prop}
   {a : α} (h : refl_trans_gen r a b)
@@ -133,6 +134,7 @@ begin
   }
 end
 
+@[elab_as_eliminator]
 lemma trans_induction_on
   {P : ∀{a b : α}, refl_trans_gen r a b → Prop}
   {a b : α} (h : refl_trans_gen r a b)
@@ -254,7 +256,8 @@ end
 
 lemma refl_trans_gen_lift {p : β → β → Prop} {a b : α} (f : α → β)
   (h : ∀a b, r a b → p (f a) (f b)) (hab : refl_trans_gen r a b) : refl_trans_gen p (f a) (f b) :=
-hab.trans_induction_on (assume a, refl) (assume a b, refl_trans_gen.single ∘ h _ _) (assume a b c _ _, trans)
+refl_trans_gen.trans_induction_on hab (assume a, refl)
+  (assume a b, refl_trans_gen.single ∘ h _ _) (assume a b c _ _, trans)
 
 lemma refl_trans_gen_mono {p : α → α → Prop} :
   (∀a b, r a b → p a b) → refl_trans_gen r a b → refl_trans_gen p a b :=
@@ -279,7 +282,8 @@ lemma refl_trans_gen_idem :
 refl_trans_gen_eq_self reflexive_refl_trans_gen transitive_refl_trans_gen
 
 lemma refl_trans_gen_lift' {p : β → β → Prop} {a b : α} (f : α → β)
-  (h : ∀a b, r a b → refl_trans_gen p (f a) (f b)) (hab : refl_trans_gen r a b) : refl_trans_gen p (f a) (f b) :=
+  (h : ∀a b, r a b → refl_trans_gen p (f a) (f b))
+  (hab : refl_trans_gen r a b) : refl_trans_gen p (f a) (f b) :=
 by simpa [refl_trans_gen_idem] using refl_trans_gen_lift f h hab
 
 lemma refl_trans_gen_closed {p : α → α → Prop} :

src/topology/list.lean

@@ -149,9 +149,6 @@ open list
 instance (n : ℕ) [topological_space α] : topological_space (vector α n) :=
 by unfold vector; apply_instance
 
-lemma cons_val {n : ℕ} {a : α} : ∀{v : vector α n}, (a :: v).val = a :: v.val
-| ⟨l, hl⟩ := rfl
-
 lemma tendsto_cons [topological_space α] {n : ℕ} {a : α} {l : vector α n}:
   tendsto (λp:α×vector α n, vector.cons p.1 p.2) ((𝓝 a).prod (𝓝 l)) (𝓝 (a :: l)) :=
 by