0

次の定義を前提としています (最初の 2 つは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です。私は多くの時間を費やし、ほとんどそこにいますが、全体的には必要以上に複雑に見えます. 2つの補題を証明する方法について、より良いアイデアを持っている人はいますか?

これまでの私の試みは次のとおりです。

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

coq は、誘導の最後のケースでinversiononを実行するのに問題があるようですが、前の場合は、意図したとおりに機能するようです。Hunfold blt_nat

于 2012-11-06T10:32:58.593 に答える