I'm provided with this theorem from the Software Foundations textbook:
Theorem plus_leb_compat_l : forall n m p : nat, n <=? m = true -> (p + n) <=? (p + m) = true.
Pretty simple proof up until the second step in the nested inductive step. This is my work so far:
Theorem plus_leb_compat_l : forall n m p : nat, n <=? m = true -> (p + n) <=? (p + m) = true. Proof. intros n m p H. induction n as [| n' IHn' ]. - (* n = 0 *) simpl. rewrite -> add_0_r_firsttry. rewrite -> n_le_sum_n_m. reflexivity. - (* n = S n' *) induction p as [| p' IHp' ]. -- (* p = 0 *) rewrite -> add_comm, add_0_r_firsttry, add_comm, add_0_r_firsttry. rewrite -> H. reflexivity. -- (* p = S n' *) simpl.
I end up with the hypothesis
(p' + S n' <=? p' + m) = true, which I don't think can be proven true for arbitrary
n' is any arbitrary nonnegative, and
m is any natural number. I think I could perform an inductive proof on
m, but I'm unsure that would be fruitful.
The textbook provides the hint "If a hypothesis has the form
H: P -> a = b, then
rewrite H will rewrite
b in the goal, and add
P as a new subgoal. Use that in the inductive step of this exercise." This doesn't seem too helpful, is there anything clear that I'm missing?