A rigorous proof of ∀ m ∈ ℕ, 0 < m → 1 < 2 * m

Question

There's a class of problems I struggle to prove by induction/recursion (I'm working in CIC). The best way I can describe this class of problems is "finite cases below m, inductive case above m".

An "easy" example problem of this kind is ∀ m ∈ ℕ, 0 < m → 1 < 2 * m

I can think of two approaches.

1. Assume 0 < m, and recurse on m with 1 < 2 * m as the induction motive. This works really well for the inductive case, but I struggle to prove the base case.
2. Don't assume anything (except m ∈ ℕ), and recurse on 0 < m → 1 < 2 * m. This works really well for the base case, but I struggle to prove the inductive case.

Obviously this class of problems includes much "harder" problems, such as ∀ m : nat, 4 < m → 10 < 2 * m. I suspect that such problem would require slightly more sophisticated machinery to prove succinctly, i.e. development of lists and using decidability of 10 < 2 * m for all m ∈ [0, 4].

To make it clear, although I'm working in CIC, I'm not using anything too fancy/ CIC-specific, so a rigorous proof in some other foundation (say PA) could also be helpful, i.e. could help me finish the proof in CIC.

An attempt at the second approach is given below (I'm using the notation of the "lean" proof assisstant, but I've heavily annotated my proofs to show what's going on).

-- A lemma, which shows that given a natural number a, a ≮ a 
lemma same_nlt : ∀ (a : nat), ∀ (P : a < a), false :=
    -- assume a
    assume a : nat,
    -- assume a < a
    assume P : a < a,
    -- take a = a from reflexivity of equality
    have H : a = a, from eq.refl a,
    -- Using a standard library lemma a < b → a ≠ b, substitue b for a
    -- prove negation by applying a = a to a ≠ a
    ne_of_lt P H

-- The second approach
theorem one_lt_twice2 : ∀ (m : nat), 0 < m → 1 < 2 * m  :=
    -- start with a natural number m
    assume m : nat,
    -- induction on m, with the induction motive being, for any natural k', 0 < k' → 2 * k'
    @nat.rec_on (λ k' : nat, 0 < k' → 1 < 2 * k') m (
        -- for the base case assume 0 < 0, use a lemma to derive a proof of negation, apply the principle of explosion.
        assume P : 0 < 0, false.elim (same_nlt 0 P))
        -- for the inductive case assume a proof of the motive for k, i.e. 0 < k → 1 < 2 * k
        (assume (k : nat) (InductiveHypothesis : 0 < k → 1 < 2 * k),
        -- it must be shown that 0 < k + 1 → 1 < 2 * (k + 1)
        show 0 < k + 1 → 1 < 2 * (k + 1), from
        -- assume 0 < k + 1
        assume (Q : 0 < k + 1),
            -- We have to show 2 * 1 < (k + 1).
            -- This could be easily done if we had access to a proof R of 1 < 2 * (k + 1).
            -- But in order to get Q, we have to unpack InductiveHypothesis by providing a proof of 0 < k.
            -- There's really no way to prove `0 < k` at this stage.
            -- In other words, the inductive step doesn't "know" we're above 0.
            have H1 : 0 < k, from sorry,
            -- we have to forfeit the proof attempt.
            sorry
        )

As the comments show, this question/ questions is not very clear. I'd like to know, from most important to least important:

1. What is a general way of formally proving in Calculus of Constructions (CIC), claims of the form ∀ m ∈ ℕ, k < m → P m, where k is some fixed natural number and P is some property of natural numbers? Examples of this problem include 0 < m → 1 < 2 * m and 4 < m → 10 < 2 * m. As pointed out, this roughly translated to "starting the induction at k + 1, as opposed to 0"
2. What is a general way of formally proving these statements in Peano Arithmetics, or any other foundational system?
3. How can I formally prove 0 < m → 1 < 2 * m in CIC or PA?

Answer 1

If you want to prove a statement of the form $\forall x (k < x \rightarrow P(x))$ by induction, then the second method is really the only method you can use:

Since induction proves a statement of the form $\forall x \ \varphi(x)$, your $\varphi(x)$ will have to be all of $k < x \rightarrow P(x)$ ... your first method really cannot be used, since you are not trying to prove $\forall x \ P(x)$ (or: as applied tyo your specific example: you are not trying to prove $\forall x \ 1 < x + x$ ... since that is just not true!)

So, this means that the base case is:

$k < 0 \rightarrow P(0)$

... which, as you point out, is easy to prove, since $k < 0$ will be false, and hence $k < 0 \rightarrow P(0)$ will be true.

For the step, you take some arbitrary $x$, and assume (inductive hypothesis) $k < x \rightarrow P(x)$, and you now want to show $k < s(x) \rightarrow P(s(x))$ (the expression $s(x)$ is what PA typically uses instead of $x + 1$)

Now, as again you say, this will be a bit tricky, since once you assume $k < s(x)$ to set up the conditional proof, it of course does not follow that $k < x$, since possibly $x = k$, and so it seems you can't use the inductive hypothesis.

However, the solution is easy: If $k < s(x)$, then it follows (this is easily proven in PA) that $k = x \lor k < x$. So, do a proof by cases:

If $k = x$, then show the specific case that $P(s(k))$, from which $P(s(x))$ immediately follows

If $k < x$, then you can use the inductive hypothesis, so get $(P(x)$, and from that, presumably, you can now infer $P(s(x))$.

Hence, you get $P(s(x))$ in both cases, and that completes the conditional proof to get $k < s(x) \rightarrow P(s(x))$

Below is a formal proof (I assumed some elementary truths as premises, but again, these are all easily provable in PA ... note how line 5 is the one specific case $P(s(k))$):

Answer 2

Base : we have it, for $0$ as well as $1$.

Induction step

Assume the induction hypoyheses: $0 < k \to 1 < 2k$ and we have to show that:

$0 < (k+1) \to 1 < 2(k+1)$.

Assume that $k+1 > 0$.

Now two cases:

(i) $k >0$. Then we can apply the induction hypotheses to get:

$2(k+1)=2k+2 > 1+2 > 1$.

(ii) $k=0$. Then $2(k+1)=2 >1$.

In both cases we have: $2(k+1) >1$.

---

The details for a formal proof in $\mathsf {PA}$ are a little bit cumbersome, because in it $<$ is defined:

$m < n \text { iff } \exists k \ (n=m+(k+1))$.

We need a proof by cases based on: $(n = 0) \lor (n > 0)$.

This in turn can be derived from the tautology: $(n=0) \lor \lnot (n=0)$ using:

$\lnot (n=0) \to (n > 0)$

that in turn can be proved by induction.

Answer 3

This is really meant to be a comment on Mauro's answer.

I've taken his idea and encoded it in CIC + EM using lean. Unfortunately, it proved rather lengthy, and there's still a little bit missing (the lemma zero_le_zero is not finished).

Perhaps more worryingly (or maybe not), it uses Excluded Middle (EM), which isn't part of CIC by default, and results in a non-constructive proof.

I still hope I can come up with a much cleaner solution, by addressing the more generic case. If anybody wants, it is possible to copy this code and paste it here to see that it's correct.

open classical
lemma nat.lte_zero (n : nat) : 0 ≤ n :=
    @nat.rec_on (λ k', 0 ≤ k') n (le_refl 0) (λ k (p : 0 ≤ k),
        have q : 0 ≤ 1, from nat.le_add_left 0 1,
        show (0 ≤ k + 1), from le_add_of_le_of_nonneg p q
    )

lemma lt_eq {a b c : nat} (h1 : b = c) (h2 : a < b) : (a < c) :=
    eq.subst h1 h2

lemma le_add_right (a b c : nat) (h1: a < b) : (a < b + c) :=
    have H1: c + b = b + c, from nat.add_comm c b,
    lt_eq H1 (lt_add_of_nonneg_of_lt (nat.lte_zero c) h1)

lemma subst2 (a b : nat) (H : a = b) (P1 : 1 < 2 * (a + 1)) : 1 < 2 * (b + 1) := eq.subst H P1

lemma zero_le_zero (k : nat) (H : k ≤ 0) : (k = 0) := sorry

lemma same_lt {a : nat} (P : a < a) : false :=
    have H : a = a, from eq.refl a,
    ne_of_lt P H

lemma one_lt_twice (m : nat) : 0 < m → 1 < 2 * m  :=
    @nat.rec_on (assume k' : nat, 0 < k' → 1 < 2 * k') m (
        assume (P : 0 < 0), (false.elim (same_lt P)))
        (assume k : nat, assume (IH : 0 < k → 1 < 2 * k),
        show (0 < k + 1 → 1 < 2 * (k + 1)), from
        assume (P : 0 < k + 1),
            show 1 < 2 * (k + 1), from
            (or.elim (em (0 < k))
                (assume H2 : 0 < k,
                    have H4 : 1 < 2 * k, from IH H2,
                        have H8 : 1 < 2 * k + 2, from le_add_right 1 (2 * k) 2 H4,
                        have H7 : 2 * k + 2 = 2 * (k + 1), by simp [mul_add],
                        show 1 < 2 * (k + 1), from eq.subst H7 H8
                    )
                (assume (H3 : 0 < k → false),
                    have H6 : k > 0 → false, from H3,
                    have H4 : k ≤ 0, from le_of_not_gt H6,
                    have H5 : k = 0, from zero_le_zero k H4,
                    have Q : (1 : nat) < 2 * (0 + 1), from of_as_true trivial,
                    show 1 < 2 * (k + 1), from (subst2 0 k (eq.symm H5)) Q
                    )
            )
        )