2
$\begingroup$

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?
$\endgroup$
  • $\begingroup$ The base case is simply $m=0$; in this case: $0 < 0$ is false, and thus $0 < 0 \to 1 < 2 \times 0$ is true. $\endgroup$ – Mauro ALLEGRANZA Aug 2 '17 at 11:42
  • $\begingroup$ What is your induction motive? If it is 0 < m → 1 < 2 * m then that's exactly how the presented proof attempt proceeds, but the difficulty lies in the inductive step. If it's 1 < 2 * m, then you're out of luck, because 1 < 2 * 0 is false. $\endgroup$ – Adam Kurkiewicz Aug 2 '17 at 11:54
  • $\begingroup$ @MauroALLEGRANZA why did you remove the foundations tag? The question is asking about a proof in CIC, which is a type theory, or a proof in any other foundational system, which can be easily translated to CIC. $\endgroup$ – Adam Kurkiewicz Aug 2 '17 at 11:58
  • $\begingroup$ Base case: $0 < 0 \to 1 < 2 \times 0$. $False \to False$ is $True$. $\endgroup$ – Mauro ALLEGRANZA Aug 2 '17 at 11:58
  • $\begingroup$ Induction hypo: $0 < m \to 1 < 2 \times m$. Assume it to prove: $(0 < (m+1)) \to (1 < 2 \times (m+1))$ $\endgroup$ – Mauro ALLEGRANZA Aug 2 '17 at 11:59
1
$\begingroup$

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))$):

enter image description here

$\endgroup$
  • $\begingroup$ Wow, a really nice answer! What's this proof assistant that you're using? $\endgroup$ – Adam Kurkiewicz Aug 2 '17 at 16:18
  • $\begingroup$ @AdamKurkiewicz Thanks! (I like doing formal proofs ... :) ) It's called 'Fitch'. It comes with the book 'Language, Proof, and Logic' $\endgroup$ – Bram28 Aug 2 '17 at 16:21
  • $\begingroup$ Does the logic of Fitch assume Excluded Middle (EM)? The reason I'm asking is because I was working off of @MauroALLEGRANZA 's answer and one of the steps he suggested (I think it's step 13 in your case, but I'm not sure) uses EM. And I can get his proof to work in lean, but only by assuming EM (CIC comes without EM by default). $\endgroup$ – Adam Kurkiewicz Aug 2 '17 at 16:30
  • $\begingroup$ @AdamKurkiewicz No, Fitch does not have EM either ... though it does have a 'Tautological Consequence' 'rule' (an internal automated theorem proving mechanism, really) that can verify that the use of EM is logically valid. $\endgroup$ – Bram28 Aug 2 '17 at 16:38
  • $\begingroup$ also, do you think that this approach will scale to the more general case of arbitrary threshold k, i.e. the most general version of the question (i.e. question 1). $\endgroup$ – Adam Kurkiewicz Aug 2 '17 at 16:39
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks for this hint. I've translated this reasoning into a formal proof in CIC (with one minor gap). $\endgroup$ – Adam Kurkiewicz Aug 2 '17 at 17:05
  • 1
    $\begingroup$ @AdamKurkiewicz - in order to avoid EM, you can prove by induction: $n < m \lor n=m \lor n > m$. With this we have $\lnot (n < 0) \to (n=0 \lor n >0)$. But we have from axiom: $\lnot (n <0)$ and thus by MP we get $n=0 \lor n >0$ which in turn is: $\lnot (n=0) \to n >0$. $\endgroup$ – Mauro ALLEGRANZA Aug 2 '17 at 17:14
0
$\begingroup$

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
                    )
            )
        )
$\endgroup$
  • $\begingroup$ Comment: $0 \le 0$ is an abbrebiation of $0=0 \lor 0 < 0$ taht follows by $\lor$-intro from the equality axiom $0=0$. $\endgroup$ – Mauro ALLEGRANZA Aug 2 '17 at 17:07
  • $\begingroup$ $0 < k$ is a decidable proposition, so you can eliminate the use of excluded middle by simply constructively proving that it is decidable, that is $\forall k:\mathbb{N}.(0 < k)\lor\neg(0 < k)$ which you can do by induction on $k$. $\endgroup$ – Derek Elkins Aug 2 '17 at 22:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.