Fix induction

Stream: general

[Bolton Bailey]

Looking at the recursion principle for the fixpoint operator docs#fix_induction, we have

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

It seems like an easier to understand and more useful principle would be

lemma inheriting_from_chains
  (f : α →. β ⊕ α) (b : β) {C : α → Sort*} {a : α} (h : b ∈ f.fix a)
  (hbase : (∀ a_final : α, sum.inl b ∈ f a_final -> C a_final))
  (hind : (∀ a_0 a_1 : α, sum.inr a_1 ∈ f a_0 -> C a_1 -> C a_0)) : C a

But I'm finding it hard to prove the latter from the former. Is there a particular reason why the latter isn't provided?

[Yaël Dillies]

This is a very @Mario Carneiro question.

[Bolton Bailey]

Yeah, I guess I'm thrown for a loop by this forall within an implication within a forall in a hypothesis. I have a hard time even getting it straight in my head what the first lemma is saying.

[Bolton Bailey]

Note that I've edited it to remove the reuse of the variable a.

[Yaël Dillies]

I remember writing the docstring for that recursor. Although I didn't end up saying much, I think I understood it at some point.

[Yaël Dillies]

Okay so the problem I see with your recursor is that it requires too strong of an hypothesis. It asks for stuff about branches that never fix.

[Bolton Bailey]

Ok, can you give me an example of something you can prove with the first one but not the second?

[Yaël Dillies]

No, the opposite.

[Yaël Dillies]

Or are you telling you managed to prove inheriting_from_chains from fix_induction? I think that's impossible.

[Bolton Bailey]

I haven't managed to prove the second one, but I think it's true and I want it

[Bolton Bailey]

At first I thought I would be able to prove it from induction_fix by just using a bunch of apply statements, but somehow I can't

[Yaël Dillies]

Argh sorry I am the one who is confused. inheriting_from_chains is certainly true, but you can't prove fix_induction from it.

[Bolton Bailey]

Ok, I believe you but I don't see why

[Eric Rodriguez]

I think Bolton wants to go the other way round, Yael

[Yaël Dillies]

Yeah, and I think this is possible.

[Bolton Bailey]

Right, I would like to prove inheriting _from_chains using fix_induction

[Bolton Bailey]

Hmm, maybe I need to use mem_fix_iff?

[Bolton Bailey]

lemma inheriting_predicates
  (f : α →. β ⊕ α) (b : β) {C : α → Sort*} {a : α} (h : b ∈ f.fix a)
  (hbase : (∀ a_final : α, sum.inl b ∈ f a_final -> C a_final))
  (hind : (∀ a_0 a_1 : α, sum.inr a_1 ∈ f a_0 -> C a_1 -> C a_0)) : C a :=
begin
  apply fix_induction h,
  intros a' hba' H,
  clear H,
  rw mem_fix_iff at hba',
  cases hba',-- induction tactic failed, recursor 'or.dcases_on' can only eliminate into Prop

end

[Reid Barton]

You have lemma ... : C a but C : α → Sort*--is that what you wanted?

[Bolton Bailey]

Well, I don't really care about proving it for Sorts, let me switch to Prop

[Yaël Dillies]

Probably C : α → Prop, because it won't be able to construct data anymore anyway.

[Bolton Bailey]

This is as far as I get Got it.

lemma inheriting_predicates
  (f : α →. β ⊕ α) (b : β) {C : α → Prop} {a : α} (h : b ∈ f.fix a)
  (hbase : (∀ a_final : α, sum.inl b ∈ f a_final -> C a_final))
  (hind : (∀ a_0 a_1 : α, sum.inr a_1 ∈ f a_0 -> C a_1 -> C a_0)) : C a :=
begin
  apply fix_induction h,
  intros a' hba' H,
  -- clear H,
  rw mem_fix_iff at hba',
  cases hba',
  { apply hbase, exact hba', },
  { rcases hba',
    apply hind a' hba'_w,
    exact hba'_h.left,
    apply H,
    exact hba'_h.right,
    exact hba'_h.left, },
end

[Bolton Bailey]

(I'm dumb, you actually do need H)

[Bolton Bailey]

Now for my own edification: Why is it impossible to prove fix_induction from inheriting_from_chains?

[Bolton Bailey]

Or is it only that inheriting uses Prop?

[Mario Carneiro]

I think they are equivalent

[Mario Carneiro]

Proving the reverse direction is annoying because you don't have the b ∈ f.fix a' assumption in the hypotheses

[Mario Carneiro]

import data.pfun

namespace pfun
variables {α β : Type*}

@[elab_as_eliminator]
def inheriting_from_chains
  (f : α →. β ⊕ α) (b : β) {C : α → Sort*} {a : α} (h : b ∈ f.fix a)
  (hbase : (∀ a_final : α, sum.inl b ∈ f a_final -> C a_final))
  (hind : (∀ a_0 a_1 : α, sum.inr a_1 ∈ f a_0 -> C a_1 -> C a_0)) : C a :=
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 _ _ e (ih _ this e) },
end

@[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 :=
begin
  have := h, revert this,
  refine inheriting_from_chains _ _ h (λ a' h _, _) (λ a' a'' h ih h', _),
  { refine H _ (mem_fix_iff.2 (or.inl h)) (λ a₂ _ h₂, _),
    cases part.mem_unique h h₂ },
  { refine H _ h' (λ a₂ h₂ e, _),
    cases part.mem_unique h e,
    apply ih,
    obtain h'' | ⟨a, h'', e'⟩ := mem_fix_iff.1 h'; cases part.mem_unique h h'', exact e' },
end

end pfun

[Mario Carneiro]

There should probably be a simpler to use version of mem_fix_iff in the case where you know f has a next element

[Mario Carneiro]

Here's a version that adds the fix assumption in inheriting_from_chains:

import data.pfun

namespace pfun
variables {α β : Type*}

@[elab_as_eliminator]
def inheriting_from_chains
  (f : α →. β ⊕ α) (b : β) {C : α → Sort*} {a : α} (h : b ∈ f.fix a)
  (hbase : (∀ a_final : α, sum.inl b ∈ f a_final → C a_final))
  (hind : (∀ a_0 a_1 : α, b ∈ f.fix a_1 → sum.inr a_1 ∈ f a_0 → C a_1 → C a_0)) : C a :=
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) },
end

@[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 :=
begin
  refine inheriting_from_chains _ _ h (λ a' h, _) (λ a' a'' h' h ih, _),
  { refine H _ (mem_fix_iff.2 (or.inl h)) (λ a₂ _ h₂, _),
    cases part.mem_unique h h₂ },
  { refine H _ (mem_fix_iff.2 (or.inr ⟨_, h, h'⟩)) (λ a₂ h₂ e, _),
    cases part.mem_unique h e,
    exact ih },
end

end pfun