## Stream: general

### Topic: Induction on a set

#### Alice Laroche (Nov 29 2021 at 12:06):

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 (Nov 29 2021 at 12:09):

Do you have a proof on paper already?

#### Alice Laroche (Nov 29 2021 at 12:21):

No, it was assumed in the lecture

#### Anne Baanen (Nov 29 2021 at 12:22):

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 (Nov 29 2021 at 12:24):

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 (Nov 29 2021 at 12:25):

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 (Nov 29 2021 at 12:27):

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 (Nov 29 2021 at 12:32):

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.

Proof:

#### Alice Laroche (Nov 29 2021 at 14:04):

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

#### Eric Wieser (Nov 29 2021 at 23:27):

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

#### Eric Wieser (Nov 29 2021 at 23:31):

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

Last updated: Aug 03 2023 at 10:10 UTC