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: Dec 20 2023 at 11:08 UTC