lean4 induction with multiple base cases

Stream: new members

[Augustin d'Oultremont]

Hi !

For context, for my master's thesis I'm working on a proof of concept for a translation system that would translate natural language proofs to lean4, hence I try to get the structure of my lean4 proofs as close to what I need to parse from natural language. I'm posting in #new members, but this question might be better suited for #lean4 ?

Problem

The part where I am currently stuck is trying to add support for induction, I try to implement it based on a proof for $2^k > k^2 - 1$. The idea is the following :

• base cases for $0$, $1$, $2$ and $3$,
• prove $2^{k+1} > (k+1)^2 - 1$ based on
  • $2^{k} > k^2 - 1$
  • $k \geq 3$

Questions :

• Is it possible to make the induction tactic work with multiple base cases ? (and how)
• For the generalisation, induction gives access to the first hypothesis I need ($2^{k} > k^2 - 1$), but how can I access the second ($k \geq 3$) ?
• Is there a similar tactic to ring that could work for inequalities ? (e.g. proving $k ^ 2 \geq 3k$ using the hypothesis that $k \geq 3$)

Current progress :

The closest I could get in terms of clean and readable structure is using match, but this does not give access to the hypotheses I need.

theorem two_exp_n (n : Nat) : 2^n > n^2 - 1 := by
  match n with
  | 0 => simp
  | 1 => simp
  | 2 => simp
  | k => admit -- needs access to the 2 hypotheses

My best bet to have access to the hypotheses is using multiple inductions chained, or maybe using an induction in the last case of the match ? None of these seem really straight forward (and I did not manage to make these work... I read custom induction on hypothesis, there seems to be a way to create a custom inductions, but I would ideally want it to be generalised to any number of base cases and had a hard time understanding the thread...

Thanks for your help ! I hope my question is clear, but do not hesitate to ask me to specify anything !

[Chris Bailey]

@Augustin d'Oultremont

If I understood your question, here's one way to do the custom induction deal. The match h : x with pattern is how you preserve stuff in later arms.

theorem threeBase
  {motive : Nat → Prop}
  (minor0 : motive 0)
  (minor1 : motive 1)
  (minor2 : motive 2)
  (minor3 : ∀ n, n >= 3 → motive n)
  (m : Nat) : motive m :=
  match h : m with
  | 0 => minor0
  | 1 => minor1
  | 2 => minor2
  | x+3 =>
    have hGe : (x+3) >= 3 := by simp_arith
    minor3 (x+3) hGe

theorem two_exp_n (n : Nat) : 2^n > n^2 - 1 := by
  induction n using threeBase with
  | minor0 => simp
  | minor1 => simp
  | minor2 => simp
  | minor3 x =>
    trace_state
    sorry

[Chris Bailey]

But in this case you can just use a match and forego the custom induction I think.

[Augustin d'Oultremont]

Thanks for your answer !

Using your code, I don't seem to have access to the first hypothesis I need (to prove P x in minor 3, I need P (x-1) and x ≥ 3), I am looking into the custom induction to see how I can do that ;)

Also, is it possible to make a "modular" version of the induction n using threeBase that would not require knowing in advance how many cases we'll use ? There's probably no way to do that, but we never know...

[Chris Bailey]

My bad, you should be able to use structural recursion for the other hypothesis.

theorem threeBase
  {motive : Nat → Prop}
  (minor0 : motive 0)
  (minor1 : motive 1)
  (minor2 : motive 2)
  (minor3 : ∀ n, n >= 3 → motive (n - 1) → motive n)
  (m : Nat) : motive m :=
  match h : m with
  | 0 => minor0
  | 1 => minor1
  | 2 => minor2
  | x+3 =>
    have hGe : (x+3) >= 3 := by simp_arith
    have ih := threeBase minor0 minor1 minor2 minor3 ((x+3) - 1)
    minor3 _ hGe ih

But I think the answer to your second question is to use match/the equation compiler:

theorem two_exp_n (n : Nat) : 2^n > n^2 - 1 := by
  match n with
  | 0 => simp
  | 1 => simp
  | 2 => simp
  | x+3 =>
    have hGe : (x+3) >= 3 := by simp_arith
    have ih := two_exp_n ((x+3) - 1)
    sorry

[Augustin d'Oultremont]

I think the 2nd way to do it is the one I was looking for ! Thanks a lot ! I still have a few problems with some operations :

Here, should ring work ? it does not, but I guess that it is due to it not being fully implemented yet ?
(using mathlib4's latest chore bumb)

example (n : Nat) : 2^(n+1) = 2 * 2^n := by
  admit

gives me

ring failed, ring expressions not equal:
(1) * (2 ^ (n + 1))^1 + 0
  !=
(2) * (2 ^ n)^1 + 0

And for this one, is there a tactic that would be able to derive this ? (ring, simp, rw seem to only work with equalities)

example (m n : Nat) (h₁ : m > n): 2 * m > 2 * n := by
  admit

[Chris Bailey]

Ring solves it in lean3, mathlib4 is still just experiments I think. The second one can be solved with linarith, which doesn't exist in lean4 yet.