✔ How to prove a <= b -> a <= S b? · Coq users

Stream: Coq users

Topic: ✔ How to prove a <= b -> a <= S b?

Daniel Hilst Selli (Dec 28 2021 at 15:43):

Hi everybody, I posted the question on SO but ppl is voting for close as offtopic, so I'm comming directly here

I was trying to prove this lemma, which seems reasonable to be but I couldn't figure out how to do it

Lemma leb_0_r : forall x, x <=? 0 = true -> x = 0.
  intros. induction x. reflexivity. discriminate H.
Qed.

Lemma leb_S : forall a b, a <=? b = true -> a <=? S b = true.
  intros a b Hab. induction b. apply leb_0_r in Hab. now rewrite Hab.

But here I got stuck on the induction hypothesis

1 subgoal

a, b : nat
Hab : (a <=? S b) = true
IHb : (a <=? b) = true -> (a <=? S b) = true

========================= (1 / 1)

(a <=? S (S b)) = true

I tried induction on a too

Lemma leb_S : forall a b, a <=? b = true -> a <=? S b = true.
  intros a b Hab. induction a. reflexivity. simpl. destruct b.
  discriminate Hab. simpl in Hab.


1 subgoal

a, b : nat
Hab : (a <=? b) = true
IHa : (a <=? S b) = true -> (a <=? S (S b)) = true

========================= (1 / 1)

(a <=? S b) = true

The problem is that I always get to S a <= b or a <= S b and I can't simplify that.

Li-yao (Dec 28 2021 at 15:53):

Try to generalize the induction hypothesis (generalize dependent before induction).

Pierre Castéran (Dec 28 2021 at 16:54):

You may try an induction on a, before pushing b in the context.

Lemma leb_S : forall a b, a <=? b = true -> a <=? S b = true.
   induction a.
   - cbn; reflexivity.
   - destruct b.
   + discriminate.
   +  cbn; intros; apply IHa; assumption.
Qed.

Daniel Hilst Selli (Dec 28 2021 at 23:31):

Thank you Pierre!

Notification Bot (Dec 28 2021 at 23:31):

Daniel Hilst Selli has marked this topic as resolved.

Last updated: Oct 01 2023 at 18:01 UTC