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.
- 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.
- 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:
- 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 * mand
4 < m → 10 < 2 * m. As pointed out, this roughly translated to "starting the induction at k + 1, as opposed to 0"
- What is a general way of formally proving these statements in Peano Arithmetics, or any other foundational system?
- How can I formally prove
0 < m → 1 < 2 * min CIC or PA?