1
$\begingroup$

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?

$\endgroup$

3 Answers 3

2
$\begingroup$

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.
$\endgroup$
1
  • 1
    $\begingroup$ Induction on p worked! Thank you! $\endgroup$ Dec 27, 2022 at 15:05
1
$\begingroup$

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

$\endgroup$
1
  • $\begingroup$ This worked, thank you! $\endgroup$ Dec 27, 2022 at 15:05
1
$\begingroup$

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. 
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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