From 9ee02c6c2208fd7795005aa394107c0374906cca Mon Sep 17 00:00:00 2001 From: prakol16 Date: Fri, 25 Mar 2022 02:56:04 +0000 Subject: [PATCH] feat(data/pfun): Remove unneeded assumption from pfun.fix_induction (#12920) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 2 +- src/computability/tm_to_partrec.lean | 17 ++++++---------- src/computability/turing_machine.lean | 8 ++++---- src/data/pfun.lean | 28 ++++++++++++++++++--------- 4 files changed, 30 insertions(+), 25 deletions(-) diff --git a/src/computability/partrec.lean b/src/computability/partrec.lean index 4ce2cf46d9215..f8124d3ee4546 100644 --- a/src/computability/partrec.lean +++ b/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 }, diff --git a/src/computability/tm_to_partrec.lean b/src/computability/tm_to_partrec.lean index 01057905a87c1..aaf1d55083009 100644 --- a/src/computability/tm_to_partrec.lean +++ b/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 := diff --git a/src/computability/turing_machine.lean b/src/computability/turing_machine.lean index 1500d95d69931..90a3cb3444c17 100644 --- a/src/computability/turing_machine.lean +++ b/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, _), diff --git a/src/data/pfun.lean b/src/data/pfun.lean index 61a0960e3b51a..01b830c0d31c4 100644 --- a/src/data/pfun.lean +++ b/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 : α →. β)