feat(data/pfun): Remove unneeded assumption from pfun.fix_induction (#…

…12920)

Removed a hypothesis from `pfun.fix_induction`. Note that it was two "layers" deep, so this is actually a strengthening. The original can be recovered by

```lean
/-- A recursion principle for `pfun.fix`. -/
@[elab_as_eliminator] def fix_induction_original
  {f : α →. β ⊕ α} {b : β} {C : α → Sort*} {a : α} (h : b ∈ f.fix a)
  (H : ∀ a', b ∈ f.fix a' →
    (∀ a'', /- this hypothesis was removed -/ b ∈ f.fix a'' → sum.inr a'' ∈ f a' → C a'') → C a') : C a :=
by { apply fix_induction h, intros, apply H; tauto, }
```

Note that `eval_induction` copies this syntax, so the same argument was removed there as well.

This allows for some simplifications of other parts of the code. Unfortunately, it was hard to figure out what was going on in the very dense parts of `tm_to_partrec.lean` and `partrec.lean`. I mostly just mechanically removed the hypotheses that were unnecessarily being supplied, and then checked if that caused some variable to be unused and removed that etc. But I cannot tell if this allows for greater simplifications.

I also extracted two lemmas `fix_fwd` and `fix_stop` that I thought would be useful on their own.

src/computability/partrec.lean

@@ -696,7 +696,7 @@ begin
     { refine ⟨k.succ, _, λ m mk km, ⟨a₂, _⟩⟩,
       { simp [F], exact or.inr ⟨_, hk, h₂⟩ },
       { rwa le_antisymm (nat.le_of_lt_succ mk) km } },
-    { rcases IH _ fa₃ am₃ k.succ _ with ⟨n, hn₁, hn₂⟩,
+    { rcases IH _ am₃ k.succ _ with ⟨n, hn₁, hn₂⟩,
       { refine ⟨n, hn₁, λ m mn km, _⟩,
         cases km.lt_or_eq_dec with km km,
         { exact hn₂ _ mn km },

src/computability/tm_to_partrec.lean

@@ -272,9 +272,7 @@ begin
       { simp only [list.head, exists_false, or_false, part.mem_some_iff,
           list.tail_cons, false_and] at this,
         subst this, exact ⟨_, ⟨h, hm⟩, rfl⟩ },
-      { simp only [list.head, exists_eq_left, part.mem_some_iff,
-          list.tail_cons, false_or] at this,
-        refine IH _ this (by simp * at *) _ rfl (λ m h', _),
+      { refine IH (n.succ :: v.val) (by simp * at *) _ rfl (λ m h', _),
         obtain h|rfl := nat.lt_succ_iff_lt_or_eq.1 h', exacts [hm _ h, h] } },
     { rintro ⟨n, ⟨hn, hm⟩, rfl⟩, refine ⟨n.succ :: v.1, _, rfl⟩,
       have : (n.succ :: v.1 : list ℕ) ∈ pfun.fix
@@ -535,32 +533,29 @@ begin
         have e₁ := step_normal_then f cont.halt (cont.fix f k) v'.tail,
         rw [e₀, cont.then, cfg.then] at e₁,
         obtain ⟨v₁, hv₁, v₂, hv₂, h₃⟩ :=
-          IH (step_ret (k₀.then (cont.fix f k)) v₀) _ _ v'.tail _ step_ret_then _,
+          IH (step_ret (k₀.then (cont.fix f k)) v₀) _ v'.tail _ step_ret_then _,
         { refine ⟨_, pfun.mem_fix_iff.2 _, h₃⟩,
           simp only [part.eq_some_iff.2 hv₁, part.map_some, part.mem_some_iff],
           split_ifs at hv₂ ⊢; [exact or.inl (part.mem_some_iff.1 hv₂),
             exact or.inr ⟨_, rfl, hv₂⟩] },
-        { rwa [← @reaches_eval _ _ (cfg.ret (k₀.then (cont.fix f k)) v₀), ← e₁],
-          exact refl_trans_gen.single rfl },
         { rw [step_ret, if_neg he, e₁], refl },
         { apply refl_trans_gen.single, rw e₀, exact rfl } } },
-    { rw reaches_eval at h, swap, exact refl_trans_gen.single rfl,
-      exact IH _ h rfl _ _ step_ret_then (refl_trans_gen.tail hr rfl) } },
+    { exact IH _ rfl _ _ step_ret_then (refl_trans_gen.tail hr rfl) } },
   { rintro ⟨v', he, hr⟩,
     rw reaches_eval at hr, swap, exact refl_trans_gen.single rfl,
     refine pfun.fix_induction he (λ v (he : v' ∈ f.fix.eval v) IH, _),
     rw [fok, part.bind_eq_bind, part.mem_bind_iff],
-    obtain he | ⟨v'', he₁', he₂'⟩ := pfun.mem_fix_iff.1 he,
+    obtain he | ⟨v'', he₁', _⟩ := pfun.mem_fix_iff.1 he,
     { obtain ⟨v', he₁, he₂⟩ := (part.mem_map_iff _).1 he, split_ifs at he₂; cases he₂,
       refine ⟨_, he₁, _⟩,
       rw reaches_eval, swap, exact refl_trans_gen.single rfl,
       rwa [step_ret, if_pos h] },
     { obtain ⟨v₁, he₁, he₂⟩ := (part.mem_map_iff _).1 he₁', split_ifs at he₂; cases he₂,
-      clear he₂ he₁', change _ ∈ f.fix.eval _ at he₂',
+      clear he₂ he₁',
       refine ⟨_, he₁, _⟩,
       rw reaches_eval, swap, exact refl_trans_gen.single rfl,
       rwa [step_ret, if_neg h],
-      exact IH v₁.tail he₂' ((part.mem_map_iff _).2 ⟨_, he₁, if_neg h⟩) } }
+      exact IH v₁.tail ((part.mem_map_iff _).2 ⟨_, he₁, if_neg h⟩) } }
 end
 
 theorem code_is_ok (c) : code.ok c :=

src/computability/turing_machine.lean

@@ -663,8 +663,8 @@ holds of any point where `eval f a` evaluates to `b`. This formalizes the notion
 @[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' $
+    (∀ a', f a = some a' → C a') → C a) : C a :=
+pfun.fix_induction h (λ a' ha' h', H _ ha' $ λ b' e, h' _ $
   part.mem_some_iff.2 $ by rw e; refl)
 
 theorem mem_eval {σ} {f : σ → option σ} {a b} :
@@ -675,9 +675,9 @@ theorem mem_eval {σ} {f : σ → option σ} {a b} :
   { rw part.mem_unique h (pfun.mem_fix_iff.2 $ or.inl $
       part.mem_some_iff.2 $ by rw e; refl),
     exact ⟨refl_trans_gen.refl, e⟩ },
-  { rcases pfun.mem_fix_iff.1 h with h | ⟨_, h, h'⟩;
+  { rcases pfun.mem_fix_iff.1 h with h | ⟨_, h, _⟩;
       rw e at h; cases part.mem_some_iff.1 h,
-    cases IH a' h' (by rwa e) with h₁ h₂,
+    cases IH a' (by rwa e) with h₁ h₂,
     exact ⟨refl_trans_gen.head e h₁, h₂⟩ }
 end, λ ⟨h₁, h₂⟩, begin
   refine refl_trans_gen.head_induction_on h₁ _ (λ a a' h _ IH, _),

src/data/pfun.lean

@@ -233,17 +233,31 @@ theorem mem_fix_iff {f : α →. β ⊕ α} {a : α} {b : β} :
       rw well_founded.fix_F_eq, simp [h₁, h₂, h₄] } }
 end⟩
 
+/-- If advancing one step from `a` leads to `b : β`, then `f.fix a = b` -/
+theorem fix_stop {f : α →. β ⊕ α} (a : α) {b : β} (hb : sum.inl b ∈ f a) : b ∈ f.fix a :=
+by { rw [pfun.mem_fix_iff], exact or.inl hb, }
+
+/-- If advancing one step from `a` on `f` leads to `a' : α`, then `f.fix a = f.fix a'` -/
+theorem fix_fwd {f : α →. β ⊕ α} (a a' : α) (ha' : sum.inr a' ∈ f a) :
+  f.fix a = f.fix a' :=
+begin
+  ext b, split,
+  { intro h, obtain h' | ⟨a, h', e'⟩ := mem_fix_iff.1 h; cases part.mem_unique ha' h', exact e', },
+  { intro h, rw pfun.mem_fix_iff, right, use a', exact ⟨ha', h⟩, }
+end
+
 /-- A recursion principle for `pfun.fix`. -/
 @[elab_as_eliminator] def fix_induction
   {f : α →. β ⊕ α} {b : β} {C : α → Sort*} {a : α} (h : b ∈ f.fix a)
   (H : ∀ a', b ∈ f.fix a' →
-    (∀ a'', b ∈ f.fix a'' → sum.inr a'' ∈ f a' → C a'') → C a') : C a :=
+    (∀ a'', sum.inr a'' ∈ f a' → C a'') → C a') : C a :=
 begin
   replace h := part.mem_assert_iff.1 h,
   have := h.snd, revert this,
   induction h.fst with a ha IH, intro h₂,
-  refine H a (part.mem_assert_iff.2 ⟨⟨_, ha⟩, h₂⟩)
-    (λ a'' ha'' fa'', _),
+  have fb : b ∈ f.fix a := (part.mem_assert_iff.2 ⟨⟨_, ha⟩, h₂⟩),
+  refine H a fb (λ a'' fa'', _),
+  have ha'' : b ∈ f.fix a'' := by rwa fix_fwd _ _ fa'' at fb,
   have := (part.mem_assert_iff.1 ha'').snd,
   exact IH _ fa'' ⟨ha _ fa'', this⟩ this,
 end
@@ -260,12 +274,8 @@ def fix_induction'
 begin
   refine fix_induction h (λ a' h ih, _),
   cases e : (f a').get (dom_of_mem_fix h) with b' a''; replace e : _ ∈ f a' := ⟨_, e⟩,
-  { have : b' = b,
-    { obtain h'' | ⟨a, h'', _⟩ := mem_fix_iff.1 h; cases part.mem_unique e h'', refl },
-    subst this, exact hbase _ e },
-  { have : b ∈ f.fix a'',
-    { obtain h'' | ⟨a, h'', e'⟩ := mem_fix_iff.1 h; cases part.mem_unique e h'', exact e' },
-    refine hind _ _ this e (ih _ this e) },
+  { apply hbase, convert e, exact part.mem_unique h (fix_stop _ e), },
+  { refine hind _ _ _ e (ih _ e), rwa fix_fwd _ _ e at h, },
 end
 
 variables (f : α →. β)