How can I proove forall a b, a <=? b = true -> a <=? S b = true in Coq

user_652528 0
Viewed 90

Is it possible to prove this forall (a b : nat), a <=? b = true -> a <=? S b = true. in Coq?

I tried this so far

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.

After posting here I realized that conclusion of IHa is equal to the goal of second try and vice versa :thinking:

coq
2 Answers

I am nor sure if you are learning Coq and this is an exercise or if you are using Coq. In the latter case the answer is: I would have thought the lia tactic can do this, but it requires a bit of massaging:

Require Import PeanoNat.
Require Import Lia.

Lemma leb_0_r : forall x, x <=? 0 = true -> x = 0.
Proof.
  intros.
  Fail lia.
  Search (_ <=? _ = true).
  apply Nat.leb_le in H.
  lia.
Qed.

In the former case, I would need to know what you are allowed to use. E.g. this works:

Require Import PeanoNat.

Lemma leb_0_r : forall x, x <=? 0 = true -> x = 0.
Proof.
  intros.
  apply Nat.leb_le in H.
  inversion H.
  reflexivity.
Qed.
user_143149440

You could try not to use induction, but transitivity of the <= relation instead.

user_134163650
Related