Induction on a set

Stream: general

[Alice Laroche]

Hello,
I have absolutly no idea on how i can prove this, can i have some help ?

theorem prop_on_inductive_set
(T : Type)
(B X : set T)
(f : T -> T)
(P : T -> Prop)
(h₁ : X = B ∪ f '' X)
(h₂ : ∀x ∈ B, P x)
(h₃ : ∀x, P x -> P (f x))
: ∀x ∈ X, P x :=
begin
sorry,
end

[Anne Baanen]

Do you have a proof on paper already?

[Alice Laroche]

No, it was assumed in the lecture

[Anne Baanen]

Ah, I see. Because the hypotheses are probably not saying what you want to say: if B = ∅ and f = id then the hypotheses hold for all T, B, P, x, in particular P = λ x, false.

[Anne Baanen]

In particular, h₁ should be something like "X contains the elements of B with f applied a finite number of times to them". (And then you'd be able to apply induction to the number of times you apply f.)

[Anne Baanen]

The counterexample:

import data.set

theorem prop_on_inductive_set
  (h : Π (T : Type) (B X : set T) (f : T -> T) (P : T -> Prop) (h₁ : X = B ∪ f '' X) (h₂ : ∀x ∈ B, P x) (h₃ : ∀x, P x -> P (f x)), ∀x ∈ X, P x) :
  false :=
begin
  refine h ℕ ∅ ⊤ id (λ _, false) _ _ _ 0 (set.mem_univ 0),
  { simp },
  { rintro x ⟨⟩ },
  { intros x h, exact h }
end

[Anne Baanen]

So this is probably what you want to prove instead:

import data.set

theorem prop_on_inductive_set
  (T : Type) (B X : set T) (f : T -> T) (P : T -> Prop)
  (h₁ : ∀ x ∈ X, ∃ (b ∈ B) (n : ℕ), (f^[n]) b = x)
  (h₂ : ∀x ∈ B, P x)
  (h₃ : ∀x, P x -> P (f x)) :
   ∀x ∈ X, P x :=
begin
  sorry
end

[Alice Laroche]

Oooh, yes , this is what i want to prove indeed, I wanted to prove the thing as it was write in our lecture, without thinking of the formal definition of the notation. Thank you.

[Patrick Johnson]

Proof:

lemma iter_succ {T : Type} {f : T → T} {x : T} {n : ℕ} :
(f^[n]) (f x) = f ((f^[n]) x) := begin
  induction n with n hn generalizing x,
  { refl },
  { unfold iterate, rw hn },
end

theorem prop_on_inductive_set
  (T : Type) (B X : set T) (f : T → T) (P : T → Prop)
  (h₁ : ∀ x ∈ X, ∃ (b ∈ B) (n : ℕ), (f^[n]) b = x)
  (h₂ : ∀x ∈ B, P x)
  (h₃ : ∀x, P x → P (f x)) :
  ∀x ∈ X, P x :=
begin
  rintro x h₄,
  obtain ⟨b, h₅, n, h₆⟩ := h₁ _ h₄,
  clear h₄, subst h₆,
  induction n with n h₆; unfold iterate,
  { apply h₂ b h₅ },
  { rw iter_succ, apply h₃ _ h₆ },
end

[Alice Laroche]

Whoaa, this is way better than mine, thank you too.

[Eric Wieser]

Isn't that iter_succ just the equation lemma for docs#nat.iterate? nevermind

[Eric Wieser]

It's actually docs#function.commute.iterate_left, as (function.commute.refl f).iterate_left n