1

次のような前提があるとします。

H2: ~ a b c <> a b c

そして、私はそれを次のように変更したい:

a b c = a b c

どこ

a はターム -> ターム -> ターム

b と c は両方とも項

どうすればいいですか？ありがとう！

4

2 に答える 2

3

と の定義を展開する~と<>、仮説は次のタイプになります。

H2: (a b c = a b c -> False) -> False

したがって、達成したいことは、論理学者が通常「二重否定除去」と呼ぶものです。これは直観的に証明できる定理ではないためClassical、Coq のモジュールで定義されています (詳細については、 http: //coq.inria.fr/distrib/V8.4/stdlib/Coq.Logic.Classical_Prop.htmlを参照してください)。

Classical.NNPP : forall (p : Prop), ~ ~ p -> p

あなたの実際の問題は よりも複雑だと思いますa b c = a b cが、言及するために、その特定の仮説を得ることを本当に気にしているなら、H2 を見なくても安全に証明できます:

assert (abc_refl : a b c = a b c) by reflexivity.

実際の例がすぐに再帰的ではなく、等式が実際に偽である場合、目標を H2 がばかげていることを示すことに変えたいと思うかもしれません。elim H2.H2 ( 、基本的に型のカットを行う) を削除することでこれを行うことができFalse、最終的には次のコンテキストになります。

H2 : ~ a b c <> a b c
EQ : a b c = a b c
=====================
False

これがすべて役立つかどうかはわかりませんが、問題を単純化しすぎている可能性があるため、実際の問題が何であるかについてこれ以上の洞察を提供することはできません.

于 2013-03-03T17:35:36.730 に答える
1

Ptival の回答に追加するちょっとした考え - 目的の目標が によって自明に解決されなかった場合でも、たとえば次の小さな補題を適用することによって、 にreflexivity決定可能な平等があれば、前進することができます。Term

Section S.
  Parameter T : Type.
  Parameter T_eq_dec : forall (x y : T), {x = y} + {x <> y}.

  Lemma not_ne : forall (x y : T), ~ (x <> y) -> x = y.
  Proof.
    intros.
    destruct (T_eq_dec x y); auto.
    unfold not in *.
    assert False.
    apply (H n).
    contradiction.
  Qed.
End S.
于 2013-03-03T21:08:50.560 に答える