證明在小於且小於或等於上NAT

Question

假設下面的定義（前兩個是從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. 

我想證明如下：

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. 

的我能夠得到的最遠是假設blt_nat_flip，假設blt_nat_flip0。我花了很多時間，我幾乎在那裏，但總體來看，它似乎比它應該更復雜。任何人對如何證明這兩個引理有更好的想法？

這裏是我的嘗試至今：

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. 

Answer 1

COQ似乎有麻煩你感應的情況下，最後上做H一個inversion，但如果你unfold blt_nat之前，它似乎像預期的那樣。