Induction on a constructed number

Stream: general

[Alice Laroche]

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]

Does induction f x work?

[Kevin Buzzard]

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]

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]

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]

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

[Floris van Doorn]

@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]

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

[Kevin Buzzard]

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]

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

[Kyle Miller]

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]

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