0

假设以下定义（前两个取自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.
4

1 回答 1

1

inversioncoq在H你归纳的最后一种情况下似乎有麻烦，但如果你unfold blt_nat以前，它似乎按预期工作。

于 2012-11-06T10:32:58.593 回答