1

コンテキスト内にネストされた実存ステートメントH : exists ( a : A ) ( b : B ) ( c : C ) ... ( z : Z ), P a b c ... zがあるとします。H新しい仮説をインスタンス化して取得する最良の方法は何H' : P a b c ... zですか? これを繰り返すinversionと時間がかかり、 のような不要な中間ステップがすべて残りますH0 : exists ( b : B ) ( c : C ) ... ( z : Z ), P a b c ... z。

私の以前の質問は、これと非常によく似ています。たぶん、これを使用するpose proofかgeneralize、これを機能させる方法もあります。

4

1 に答える 1

1

あなたがやりたいことは「インスタンス化」とは呼ばれません。普遍的に定量化された仮説をインスタンス化し、存在論的に定量化された結論をインスタンス化することはできますが、その逆はできません。正式名称は「はじめに」だと思います。仮説に存在量化を導入し、結論に全称量化を導入できます。代わりに「排除」しているように見える場合、それは、何かを証明するときに、逐次微積分の導出の最下部から開始し、最上位に戻るように作業するためです。

とにかく、戦術を使用してfirstorderください。また、目標を単純化するだけの場合は、コマンドを使用Set Firstorder Depth 0してプルーフ サーチをオフにします。

ただし、目標に高次の要素がある場合は、おそらくエラー メッセージが表示されます。その場合、 のようなものを使用できますsimplify。

Ltac simplify := repeat
  match goal with
  | h1 : False |- _ => destruct h1
  | |- True => constructor
  | h1 : True |- _ => clear h1
  | |- ~ _ => intro
  | h1 : ~ ?p1, h2 : ?p1 |- _ => destruct (h1 h2)
  | h1 : _ \/ _ |- _ => destruct h1
  | |- _ /\ _ => constructor
  | h1 : _ /\ _ |- _ => destruct h1
  | h1 : exists _, _ |- _ => destruct h1
  | |- forall _, _ => intro
  | _ : ?x1 = ?x2 |- _ => subst x2 || subst x1
  end.
于 2014-09-10T12:56:02.133 に答える