## Stream: general

### Topic: Induction on a constructed number

#### Alice Laroche (Aug 26 2021 at 14:15):

I want to prove P x, I have a function f .which associate every x to a number.
I can prove that if f x = 0 then P x
and if f x = n then P x then if f x = n + 1 then P x
How can i make induction on f x in lean ?

#### Eric Wieser (Aug 26 2021 at 14:21):

Does induction f x work?

#### Kevin Buzzard (Aug 26 2021 at 14:22):

Why don't you formalise the statement of what you want to prove in Lean and post it here as a #mwe? Then people will be able to suggest various solutions. but right now it's to a certain extent guesswork because we don't know exactly what you are doing.

#### Alice Laroche (Aug 26 2021 at 15:37):

I think an MWE would be something like this

example (T : Type) (f : T → T → ℕ) (p : T → T → Prop)
(h₁ : ∀x, ∃y, f x y = 0 → p x y)
(h₂ : ∀n, (∀x, ∃y, f x y = n → p x y) → (∀x, ∃y, f x y = n + 1 → p x y))
: ∀x, ∃y, p x y :=
begin

end


#### Kyle Miller (Aug 26 2021 at 16:06):

I'm not sure that conclusion is true as-is, but this is something you can prove using those hypotheses:

example (T : Type) (f : T → T → ℕ) (p : T → T → Prop)
(h₁ : ∀x, ∃y, f x y = 0 → p x y)
(h₂ : ∀n, (∀x, ∃y, f x y = n → p x y) → (∀x, ∃y, f x y = n + 1 → p x y))
: ∀n, ∀x, ∃y, f x y = n → p x y :=
begin
intro n,
induction n,
{ exact h₁, },
{ apply h₂,
exact n_ih },
end


#### Filippo A. E. Nuccio (Aug 26 2021 at 16:17):

This is not working for me; did you import something? No, it works, sorry!

#### Floris van Doorn (Aug 26 2021 at 16:25):

@Alice Laroche your MWE is false:

import tactic.basic
example : ¬ ∀ (T : Type) (f : T → T → ℕ) (p : T → T → Prop)
(h₁ : ∀x, ∃y, f x y = 0 → p x y)
(h₂ : ∀n, (∀x, ∃y, f x y = n → p x y) → (∀x, ∃y, f x y = n + 1 → p x y)),
∀x, ∃y, p x y :=
begin
simp_rw [not_forall],
refine ⟨bool, λ x y, if y then 0 else 1, λ x y, false, λ x, _, λ n h x, _, _⟩,
{ use ff },
{ use tt },
{ use tt, simp }
end


#### Alice Laroche (Aug 26 2021 at 16:54):

Oh...Any idea on how i could correct it ? IF you understand what i wanted to do.

#### Kevin Buzzard (Aug 26 2021 at 17:12):

I think it's much easier for you to figure out what you mean than for someone else to :-) If it's any help, then here's an explanation of Floris' counterexample: T is bool={tt,ff}, f(x,y)=1 if y is false and 0 if it's true, and p x y is always false. It's not hard to check that h1 and h2 are satisfied (use ff for y in h1 and use tt in h2), but the conclusion is false.

#### Kyle Miller (Aug 26 2021 at 17:17):

@Alice Laroche I take it my correction wasn't what you were looking for?

#### Kyle Miller (Aug 26 2021 at 17:23):

It seems that implications inside existentials are usually a mistake, since they're rather weak. Strengthening the hypotheses with ands, you can get this:

example (T : Type) (f : T → T → ℕ) (p : T → T → Prop)
(h₁ : ∀x, ∃y, f x y = 0 ∧ p x y)
(h₂ : ∀n, (∀x, ∃y, f x y = n ∧ p x y) → (∀x, ∃y, f x y = n + 1 ∧ p x y))
: ∀n, ∀x, ∃y, f x y = n ∧ p x y :=
begin
intro n,
induction n,
{ exact h₁, },
{ apply h₂,
exact n_ih },
end


#### Chris Hughes (Aug 26 2021 at 22:50):

induction h : f x is the usual way to do this.

Last updated: Aug 03 2023 at 10:10 UTC