24

すでに coq でいくつかの定理を証明しており、後で別の定理の証明の仮説として導入したいとします。これを行う簡潔な方法はありますか？

これは通常、ケースバイケースの証明のようなことをしたいときに必要になります。そして、これを行う1つの方法は、定理のステートメントを使用して、すぐにそれを証明することであることを発見しましたが、これは少しassert面倒に思えます. たとえば、私は次のようなことを書く傾向があります。

Require Import Arith.EqNat.

Definition Decide P := P \/ ~P.

Theorem decide_eq_nat: forall x y: nat, Decide (x = y).
Proof.
  intros x y. remember (beq_nat x y) as b eqn:E. destruct b.
    left. apply beq_nat_eq. assumption.
    right. apply beq_nat_false. symmetry. assumption. Qed.

Theorem silly: forall x y: nat, x = y \/ x <> y.
Proof.
  intros x y.
  assert (Decide (x = y)) as [E|N] by apply decide_eq_nat.
    left. assumption.
    right. assumption. Qed.

しかし、すべてを入力するよりも簡単な方法はありassert [statement] by apply [theorem]ますか?

4

1 に答える 1

23

を使用できますpose proof theorem_name as X.。ここXで、紹介したい名前です。

すぐに破壊する場合は、次のこともできます。destruct (decide_eq_nat x y).

于 2013-02-15T23:45:37.333 に答える