1
$\begingroup$

If we have the natural numbers defined as:

enter image description here

Plus the following:

$pred \space \_\_<\_\_ \space: Nat \times Nat$

$\forall i,j:Nat$

  • $0<suc(j)$

  • $\neg(i<0)$

  • $suc(i) < suc(j) \Longleftrightarrow i<j$

How to prove $0<i => 0 < i + j$ by induction?

For the base case the premise fails when $i=0$, and thus the implication holds.

For the induction step, we assume $i = suc(i')$ for some $i':Nat$ such that $\forall j:Nat, \space 0<i' => 0 < i' + j $ (IH)

We assume $0 < i$ (H), so, we have $0 < i => 0 < suc(i')$

But I can't move from there, as I need to find a way to use the inductive hypothesis (IH) to complete the proof, but I don't know how. Can you help please?

$\endgroup$

1 Answer 1

1
$\begingroup$

There is no need for an induction here.

  • if $j = 0$ then $0<i \Rightarrow i + j = i + 0 = i>0$;
  • otherwise, $j = suc(j')$ and $0 < i \Rightarrow i+j = i+suc(j') = suc(i + j') > 0$.
$\endgroup$

This site is temporarily in read-only mode and not accepting new answers.

Not the answer you're looking for? Browse other questions tagged .