How do I approach the final inductive step in plus_leb_compat_l from Software Foundations?

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' and m, as 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 a to 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?

3 Answers

Induction on p, as Pierre Jouvelot suggests, makes this proof much easier (the challenge is recognising it but it will come with experience).

Theorem plus_leb_compat_l : forall n m p : nat,
n <=? m = true -> (p + n) <=? (p + m) = true.
Proof.
intros ? ? ?.
revert m;
revert n.
induction p as [|p IHp];
simpl.
+
intros ? ? Ha;
exact Ha.
+
intros ? ? Ha;
eapply IHp;
exact Ha.
Qed.

• Induction on p worked! Thank you! Commented Dec 27, 2022 at 15:05

You could try to do the induction on p instead of n.

• This worked, thank you! Commented Dec 27, 2022 at 15:05

Indeed, there is no need to use explicit rewriting. The reductions of leb (S n) (S m)to leb n m and S n + m to S (n+m) suggest a simple proof by induction on p.

Lemma L:
forall n m p : nat, (n <=? m) = true -> (p + n <=? p + m) = true.
Proof.
induction p; simpl.
- now intros ?.
- assumption.
Qed.