Commit 2022-03-25 02:56 9ee02c6c

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

/-- 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.