CODEWITHSUNDEEP
proofcoq
huynhjl
huynhjl

Reputation: 41646

Proof on less than and less or equal on nat

Assuming the following definitions (the first two are taken from http://www.cis.upenn.edu/~bcpierce/sf/Basics.html):

Fixpoint beq_nat (n m : nat) : bool :=
  match n with
  | O => match m with
         | O => true
         | S m' => false
         end
  | S n' => match m with
            | O => false
            | S m' => beq_nat n' m'
            end
  end.

Fixpoint ble_nat (n m : nat) : bool :=
  match n with
  | O => true
  | S n' =>
      match m with
      | O => false
      | S m' => ble_nat n' m'
      end
  end.

Definition blt_nat (n m : nat) : bool :=
  if andb (ble_nat n m) (negb (beq_nat n m)) then true else false.

I would like to prove the following:

Lemma blt_nat_flip0 : forall (x y : nat),
  blt_nat x y = false -> ble_nat y x = true.

Lemma blt_nat_flip : forall (x y : nat),
  blt_nat x y = false -> beq_nat x y = false -> blt_nat y x = true.

The furthest I was able to get to is to prove blt_nat_flip assuming blt_nat_flip0. I spent a lot of time and I am almost there but overall it seems more complex than it should be. Anybody has a better idea on how to prove the two lemmas?

Here is my attempt so far:

Lemma beq_nat_symmetric : forall (x y : nat),
  beq_nat x y = beq_nat y x.
Proof.
  intros x. induction x.
    intros y. simpl. destruct y.
      reflexivity. reflexivity.
    intros y. simpl. destruct y.
      reflexivity.
      simpl. apply IHx.
  Qed. 

Lemma and_negb_false : forall (b1 b2 : bool),
  b2 = false -> andb b1 (negb b2) = b1.
Proof. 
  intros. rewrite -> H. unfold negb. destruct b1.
    simpl. reflexivity.
    simpl. reflexivity.
  Qed.

Lemma blt_nat_flip0 : forall (x y : nat),
  blt_nat x y = false -> ble_nat y x = true.
Proof.
  intros x.
  induction x.
    intros. destruct y.
      simpl. reflexivity.
      simpl. inversion H.
    intros. destruct y. simpl. reflexivity.
    simpl. rewrite -> IHx. reflexivity. 
    (* I am giving up for now at this point ... *)
  Admitted.

Lemma blt_nat_flip : forall (x y : nat),
  blt_nat x y = false -> beq_nat x y = false ->
    blt_nat y x = true.
Proof.
  intros. 
  unfold blt_nat.
  rewrite -> beq_nat_symmetric. rewrite -> H0.
  rewrite -> and_negb_false.
  replace (ble_nat y x) with true.
  reflexivity. 
  rewrite -> blt_nat_flip0. reflexivity. apply H. reflexivity.
  Qed.

Upvotes: 0

Views: 2695

Answers (1)

Virgile
Virgile

Reputation: 10158

coq seems to have trouble doing an inversion on H in the last case of your induction, but if you unfold blt_nat before, it seems to work as intended.

Upvotes: 2

Related Questions